Non-contractive logics, Paradoxes, and Multiplicative Quantifiers

TL;DR

The paper investigates non-contractive logics to avoid semantic and logical paradoxes, contrasting additive and multiplicative quantifiers within affine logic. It introduces contraction-free systems based on naive comprehension (UTS) and analyzes their consistency, undecidability, and modal extensions, while also exploring how vacuous quantification can simulate exponentials and recover classical logic through a faithful embedding into affine logic with modalities $!$ and $?$ and vacuous quantifiers. It identifies fundamental issues with Zardini’s multiplicative-quantifier approach and provides a syntactic cut-elimination framework for infinitary sequents in the multiplicative-quantifier setting (without disquotational truth). These results advance the proof-theoretic understanding of infinitary, non-contractive logics and offer a pathway for studying paradoxes through syntactic methods rather than semantic arguments.

Abstract

The paper investigates from a proof-theoretic perspective various non-contractive logical systems circumventing logical and semantic paradoxes. Until recently, such systems only displayed additive quantifiers (Grišin, Cantini). Systems with multiplicative quantifers have also been proposed in the 2010s (Zardini), but they turned out to be inconsistent with the naive rules for truth or comprehension. We start by presenting a first-order system for disquotational truth with additive quantifiers and we compare it with Grišin set theory. We then analyze the reasons behind the inconsistency phenomenon affecting multiplicative quantifers: after interpreting the exponentials in affine logic as vacuous quantifiers, we show how such a logic can be simulated within a truth-free fragment of a system with multiplicative quantifiers. Finally, we prove that the logic of these multiplicative quantifiers (but without disquotational truth) is consistent, by showing that an infinitary version of the cut rule can be eliminated. This paves the way to a syntactic approach to the proof theory of infinitary logic with infinite sequents.