NON-CONTRACTIVE LOGICS, PARADOXES, AND MULTIPLICATIVE QUANTIFIERS

Abstract

The paper investigates from a proof-theoretic perspective various non-contractive logical systems, which circumvent logical and semantic paradoxes. Until recently, such systems only displayed additive quantifiers (Grišin and Cantini). Systems with multiplicative quantifiers were 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 compare it with Grišin set theory. We then analyze the reasons behind the inconsistency phenomenon affecting multiplicative quantifiers. 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 establish that the logic for these multiplicative quantifiers (but without disquotational truth) is consistent, by proving 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.

1 Introduction

Since [6] it is well-known that the contraction rule plays an essential role in the derivation of logical and semantic paradoxes such as the Liar, Russell’s and Curry’s. In the last few decades, there has been a renewed interest in non-contractive logical systems, as Fitch called them, that block these paradoxes by dropping contraction from their sequent calculus formulation. Grišin [8] established the consistency of unrestricted abstraction based on what is nowadays called affine logic, i.e., linear logic equipped with the weaking rule. Petersen [13] further elaborates on Grišin’s proposal by giving a proof-theoretic analysis of a system with unrestricted abstraction and some additional axioms. Moreover, Cantini embeds combinatory logic in Grišin set theory, thereby establishing its undecidability [2]. It is well-known—and it will be recalled below—that Grišin’s set theory gives rise to a consistent theory of disquotational truth.

Nevertheless, it also clear that the solution thus provided cannot be the whole story since it only features additive quantifiers, which are in effect classical quantifiers in disguise. Indeed, as stressed in [11, 12], the difference between the additive universal quantifier and the multiplicative one may be roughly understood as the one between any and every. Given the splitting phenomenon of the connectives into additive and multiplicative ones determined by the absence of contraction, the additive quantifiers generalize additive connectives, but there is no logical device corresponding to the generalization of multiplicative ones [1, 9, 11]. One spontaneous way of conceiving of multiplicative quantifiers is to identify the universal and the existential quantifiers with infinitary multiplicative conjunctions and disjunctions, respectively,

Following this intuition, Zardini [19] presented a theory of disquotational truth based on a purely multiplicative fragment of affine logic featuring infinitary quantifiers. However, this theory has received enough attention to make it clear that: (i) it cannot be extended with suitable primitive recursive functions [3]; (ii) the attempted proof of consistency of the system via cut-elimination contains a gap [4]; and (iii) the system is outright inconsistent given some plausible principles for vacuous quantification [5].

In this paper we aim to contribute to the understanding of the non-contractive landscape by addressing a set of interconnected issues. Specifically:

• • We simplify the cut-elimination proof for Grišin’s set theory presented in [2], while also fixing a problem in Cantini’s strategy. Furthermore, we show that the seemingly weaker theory of disquotational truth based on affine logic supports Cantini’s derivation of Löb’s principle given a $\mathtt {K4}$ modality.

• • We show that the rules for vacuous quantification, which are responsible for the inconsistency of Zardini’s system, can actually be employed to recover classical logic in the context of affine logic. We prove that there exists an exact translation of (predicate, infinitary) classical logic into affine logic with vacuous quantification.

• • In the field of linear logic, the dismissed contraction and weakening can be recovered and controlled using exponentials: ! and ?, which essentially behave as $\mathtt {S4}$ modalities. We provide a new perspective on exponentials by interpreting them as vacuous quantifiers. In particular, we show how to simulate affine linear logic within a proper fragment of the system of multiplicative quantifiers by giving a sound and faithful translation. This approach involves implementing Girard’s old (but so far unexplored) idea to interpret exponentials as infinitary operations [7].

• • We directly show that Zardini’s cut-elimination algorithm is based on a proof-manipulation that does not preserve provability.

• • Finally, we show that an infinitary version of the cut rule can be eliminated from the purely logical system featuring infinitary quantifiers.

The last point also answers to a question recently posed by [14]. However, the proof-theoretic interest of this result extends beyond a non-contractive approach to paradoxes. The proof theory of well-founded infinitely branching derivations has been extensively studied and has found significant application in the context of ordinal analysis [15] and structural proof theory [17]. Well-founded infinitary derivations involving sequents with infinitely many formulas have received less attention. The investigations concerning these kinds of calculi have been conducted using semantical methods (see [16]).

A semantic argument can be employed to show the cut-free completeness of a calculus for infinitary classical logic with infinite sequents. However, since the logic of multiplicative quantifiers does not enjoy a semantic presentation, this indirect strategy here is not available. We present a syntactic proof of cut-elimination for the system involving sequents with infinitely many formulas for the logic of multiplicative quantifiers.

The paper is structured as follows: Section 2 discusses a contraction-free and cut-free system for disquotational truth in relation to Grišin set theory. Section 3 shows how the exponentials ! and ? can be demodalized by conceptualizing them in terms of vacuous quantifiers within (a truth-free fragment of) Zardini’s system. Section 4 is divided into two parts, a pars destruens that investigates the reasons for the inconsistency of Zardini’s system and a pars construens that presents the cut-elimination procedure for multiplicative quantifiers. Finally, Section 5 concludes by outlining open problems generated by the results of the paper.

2 Contraction and the paradoxes

Non-contractive approaches to the logical and semantic paradoxes are known to be formally successful. Without contraction, it’s possible to extend a standard cut-elimination procedure for first-order affine logic without exponentials (henceforth, affine logic $\mathtt {AL}$ ) to its extension with naïve rules for truth, (class-)membership, predication.

Definition 1 (Affine Logic $\mathtt {AL}$ )

$\Gamma ,\Delta ,\Theta ,\Lambda ,...$ range over finite multisets of formulae of a countable, first-order Tait language $\mathcal {L}$ .

where $y!$ expresses the fact that the variable y does not occur in the conclusion.

We follow the linear logic tradition and use $\oplus $ and for, respectively, additive disjunction and conjunction, and and $\otimes $ for, respectively, multiplicative disjunction and conjunction. Furthermore, we use $\exists $ and $\forall $ for the additive quantifiers. Lastly, we use $\overline {A}$ for the negation of the formula A. Following the Tait convention for negation (see also [15]), however, we take A to be defined as follows:

• • If A is the atomic formula P, then $\overline {A}=\overline {P}$ .

• • If A is the atomic formula $\overline {P} $ , then $\overline {A}= P$ .

• • If A is the formula $B\oplus C$ , then .

• • If A is the formula , then $\overline {A}=\overline {B}\oplus \overline {C}$ .

• • If A is the formula , then $\overline {A}=\overline {B}\otimes \overline {C}$ .

• • If A is the formula $B\otimes C$ , then .

• • If A is the formula $\forall x B$ , then $\overline {A}=\exists x\overline {B}$ .

• • If A is the formula $\exists x B$ , then $\overline {A}=\forall x \overline {B}$ .

Linear logic without exponentials is obtained from affine logic by restricting the initial sequents to those of the form initial sequents of the form $\vdash P,\overline {P}$ . We use a double line to denote a multiple, but finite, application of the rules of the calculi.

Let $\mathcal {L}^+$ be a language featuring:

• • for $n,m\in \mathbb {N}$ , n-ary predicates $\mathrm {S}^{n,m}$ and their negated dual $\overline {\mathrm {S}^{n,m}}$ ;

• • the logical symbols of $\mathtt {AL}$ ;

• • the $\lambda $ term forming operator $\lambda \cdot .\cdot $ ;

• • Variables $v_1,v_2,\ldots $ (we employ $x,y,z$ for metavariables).

In the predicate $\mathrm {S}^{n,m}$ the superscript n denotes the arity, whereas m indicates the number of free variables. For formulae $A\in \mathcal {L}^+$ , $\lambda x A$ is a term whose free variables are the free variables of A minus x. We abbreviate

$$\begin{align*}\lambda x_1\ldots x_n\,A:= \lambda x_1.(\ldots \lambda x_n \, A \ldots). \end{align*}$$

Notice that we allow for “self-referential” names to be built in the system. For instance, we allow for the existence of terms l such that

$$\begin{align*}l:= \ulcorner\overline{\mathrm{S}^{1,0}}(l)\urcorner. \end{align*}$$

The term l, as we shall see shortly, plays the role of a name for a Liar sentence. Similar terms are available for other paradoxical sentences such as Russell’s and Curry’s.

Definition 2 (Semantic extensions of $\mathtt {AL}$ )

1. (i) The system $\mathtt {UTS}^{n,m}$ is obtained by formulating $\mathtt {AL}$ in $\mathcal {L}^+$ and by adding the rules

   

   for all formulae A with exactly m free variables.

2. (ii) $\mathtt {UTS}$ comprises rules for $\mathrm {S}^{n,m}$ for all $n,m\in \mathbb {N}$ .

Remark 3. The template provided by the theories $\mathtt {UTS}^{n,m}$ enables us to define several systems that are relevant for the analysis of the paradoxes in a non-contractive setting. As we shall see shortly, the systems $\mathtt {UTS}^{1,m}$ , for each $m\in \mathbb {N}$ , correspond to Grišin set theory. ¹ A non-contractive theory of disquotational truth corresponds to $\mathtt {UTS}^{1,0}$ .

Derivations in $\mathtt {AL}$ and extensions thereof are finite trees that are locally correct with respect to the rules just given. Cantini [2] provides a cut-elimination strategy for the system $\mathtt {UTS}^{1,m}$ . The strategy relies on a triple induction on, respectively, the number of naïve comprehension rules, the depth of the cut-formula, i.e., the number of logical symbols occurring in it, and the level of the cut. The strategy, as it stands, cannot deal satisfactorily with some of the cases, for instance, the one in which the last inference in one of the branches before a cut is an additive conjunction and in which the cut formula is not principal in the last inference. ² We circumvent the problem by showing that an induction on a single parameter suffices. In order to do this, we provide a slightly nonstandard measure of length of the derivation. ³

Definition 4. Given a proof $\pi $ , its height $h(\pi )$ is given by the following recursion:

• • $h(\pi )=1$ for $\pi $ an instance of (in);

• • $h(\pi )=\mathrm {max}(h(\pi _0),h(\pi _1))+1$ , with $\pi $ ending with an application of to $\pi _0$ and $\pi _1$ ;

• • $h(\pi )=h(\pi _0)+h(\pi _1)$ , with $\pi $ ending with an application of $(\otimes )$ to $\pi _0$ and $\pi _1$ ;

• • $h(\pi )=h(\pi _0)+1$ in all other cases.

Proposition 5. Cut is admissible in $\mathtt {UTS}$ . Therefore, $\mathtt {UTS}$ is consistent.

Proof. The proof rests on the following reduction lemma:

1. (r) if $\pi _0$ and $\pi _1$ are cut-free proofs of $\Gamma ,A$ and $\Delta ,\overline {A}$ , respectively, then there is a cut-free proof $\pi $ of $\Gamma ,\Delta $ with $h(\pi )\leq h(\pi _0)+h(\pi _1)$ .

(r) is proved by an induction on $h(\pi _0)+h(\pi _1)$ . We consider two cases for illustration. If the “cut formulae” are principal in the last inference, and they are obtained by (for notational simplicity) $\mathrm {S}^{n,n}$ and $\overline {\mathrm {S}^{n,n}}$ , respectively, then we have

We can then simply apply the induction hypothesis to $\pi _{00}$ and $\pi _{10}$ . If the last rules applied are $(\otimes )$ and , respectively, we have

Then the desired $\pi $ is obtained by applying the induction hypothesis to, e.g., $\pi _{00}$ and $\pi _{10}$ , and then to the resulting derivation and $\pi _{01}$ . ⁴

Cantini shows that the addition of a $\mathtt {K4}$ modality to Grišin set theory—that is, a rule corresponding to the modal principle $4$ —and a necessitation rule is strong enough to derive Löb’s principle $\Box (\Box A \rightarrow A) \rightarrow \Box A$ . We strengthen Cantini’s observation and show that the schema $\mathtt {UTS}^{1,0}$ suffices for the task. In what follows, it will be convenient to refer to the canonical name $\ulcorner A\urcorner $ of a sentence A of $\mathcal {L}$ , and to the corresponding truth-ascription $\mathrm {Tr}\ulcorner A\urcorner $ . We let, for A a sentence,

$$ \begin{align*} & \ulcorner A\urcorner:= \lambda v_0\,A, && \mathrm{Tr}\ulcorner A\urcorner:\leftrightarrow \mathrm{S}^{1,0}(\ulcorner A\urcorner,v_0). \end{align*} $$

Definition 6. The system $\mathtt {UTS}^{1,0}+\mathtt {K4}$ is obtained by extending $\mathtt {UTS}^{1,0}$ with the rules:

Lemma 7. $ \mathtt {UTS}^{1,0}+\mathtt {K4}$ derives the schema $\Box (\Box A\rightarrow A)\rightarrow \Box A$ .

Proof. Let $C:\leftrightarrow (\Box \mathrm {Tr}\ulcorner C\urcorner \to A)$ , for arbitrary A. We show that if $\Diamond \overline {A} ,A$ is derivable, then so is A. We proceed as follows:

Since $\vdash \Diamond (\Box (\Diamond \overline {A}\lor A)\land \Diamond \overline {A}), \Diamond (\Box P\land \overline {P})\lor \Box P $ is easily seen to be derivable, we immediately get the desired conclusion as reported also in [2, theorem 2.8].

By translating the box modality as for a designated atom P, we immediately obtain the conservativity of $ \mathtt {UTS}^{1,0}+\mathtt {K4}$ over $\mathtt {UTS}^{1,0}$ which in turn immediately yields the consistency of the former system.

We would like to conclude this section by observing that the calculus $\mathtt {UTS}^{1,0}+\mathtt {K4}$ provably does not admit cut-elimination. To witness this it is enough to consider the sequent $\vdash \Diamond (\Box P\otimes \overline {P}), \Box P$ . The latter is indeed provable via cut as shown by the above derivation, but does not admit a cut-free proof by inspection of the rules.

Open problem 8. Can we obtain a cut-free system equivalent to $\mathtt {UTS}^{1,0}+\mathtt {K4}$ ? A natural approach would be to substitute the modal rule with:

The systems considered so far feature only additive quantifiers, which can be viewed as straightforward generalizations of the additive conjunction and disjunction. However, this straightforward solution to the logical paradoxes may not be completely satisfactory: the system lacks quantifiers that generalize multiplicative connectives. Several logicians and philosophers encouraged such a strengthening of the basic non-contractive theory [1, 9, 11]. The challenge was taken up by Zardini in [19].

3 Multiplicative quantifiers and inconsistency

Zardini [19] attempts to establish a cut elimination theorem for the multiplicative fragment of affine logic extended with a combination of multiplicative quantifiers and naïve truth ( $\mathtt {IKT}_{\omega }$ ) (see Figure 1). We opted for a Tait style presentation of the original calculus by Zardini. Indeed, the two calculi are easily seen to be equivalent in terms of provability. By $\biguplus _{i\in I}\Gamma _i$ we denote the infinitary multiset union of the $\Gamma _i$ . Terms $t_1,t_2,t_3,...$ constitute an exhaustive enumeration of the terms of the language.

Figure 1 $\mathtt {IKT}_{\omega }$ .

Zardini motivates the theory by emphasizing that additive connectives are not compatible with the solutions to the semantic paradoxes he defends; as a consequence, multiplicative quantifiers become the natural extension of multiplicative conjunction and disjunction. The proposal consists in equating multiplicative universal and existential quantifiers with an infinitary multiplicative conjunction and disjunction, respectively. This move is not without consequences from the point of view of the structural analysis of the system. In particular, the choice of such a reading of quantifiers has the immediate consequence of working with sequents with infinite multisets of formulas.

It is worth noting a nonstandard feature of the multiset notion employed by Zardini, which is specifically required by his formulation of the $(\forall )$ rule. ⁵ While standard multisets (even infinite ones) allow only for finite multiplicities of formulas, Zardini’s multisets permit $\omega $ -many repetitions of formulae. However, one of the problems with Zardini’s notion is that it does not allow for tracking copies of different infinite multiplicities (which may be made up of infinite repetitions of the same formula), thereby reintroducing a form of contraction into the system. Many of the results that follow are based on the consequences of this choice. Formally, multisets are not, as usual, functions $\Gamma :\mathcal {L}\to \omega $ , but rather functions $\Gamma :\mathcal {L}\to \omega +1$ . We write $\Gamma (A)>0$ to denote the fact that A occurs in $\Gamma $ (possibly infinitely many times).

Several problems have been found with Zardini’s proposal, but his work contains insightful ideas that prompted interest in the study of infinitary systems with multiplicative quantifiers and their interaction with paradox-breeding notions. Da Ré and Rosenblatt showed that extending Zardini’s system with basic arithmetical axioms leads to inconsistency [3], while Fjellstad identified a gap in the cut-elimination proof [4]. In Section 4.1, we directly show that Zardini’s cut-elimination algorithm is based on a proof-manipulation that does not preserve provability. In a recent paper, Fjellstad also showed that the system $\mathtt {IKT}_{\omega }$ is outright inconsistent, if the rules for the multiplicative quantifiers are used to deal with vacuous quantification in a natural way [5]. In this section we show how, even without a truth predicate or similar semantic resources, the implicit rules for vacuous quantification in $\mathtt {IKT}_{\omega }$ are problematic. In particular, we prove that vacuous quantification simulates the role played by exponentials in linear logic. Therefore, vacuous quantification in the setting of Zardini’s system allows one to faithfully interpret classical logic as a fragment.

Since the system $\mathtt {IKT}_{\omega }$ and its fragment obtained from removing the truth predicate are systems in which derivations are infinitely branching well-founded trees, we need to suitably modify the notion of height in order to carry out inductive arguments. To deal with infinitary derivations we assign ordinals to measure the heights of the derivations. The assignment is the standard one as can be found in [15], the key point is that for every rule $\rho $ ,

the height of the premise $\Gamma _i$ is strictly less than the height of the conclusion $\Gamma $ for every i. More generally, the height of a derivation $\pi $ is inductively defined as follows: with $h_i$ the heights of the direct sub-derivations of $\pi $ , $i\in I$ , the height of $\pi $ is the supremum of $\{h_i+1\;|\; i\in I\}$ .

3.1 Vacuous quantifiers and classical logic

We recall that a rule is said to be (height-preserving) invertible if the derivability of the conclusion entails the derivability of each of its premises (and the height is less or equal). We start by showing that the rule for the existential quantifier is height-preserving invertible.

Lemma 9. The rule $\exists $ is height-preserving invertible.

Proof. By induction on the height of the derivation. If the sequent $\vdash \Gamma ,\exists x A$ is an initial sequent, then so is $\vdash \Gamma , A(t_0/x), A(t_1/x),...$ since $\exists x A$ is not an atomic formula and initial sequents are all on the form $\vdash \Gamma , P, \overline {P}$ for atomic P’s. If the formula $\exists x A$ is principal, the premise gives the desired conclusion. If the last rule applied is any other rule, we apply the induction hypothesis to each of the premise(s) and then the rule again. For example, if the last rule applied is $\forall $ , we have

We construct the following derivation:

where $IH$ denotes the application of the inductive hypothesis.

We also observe that the weakening rule (Weak) is height-preserving admissible in the system $\mathtt {IZ}_{\omega }$ . This fact will shortly be employed in the proof of Proposition 13.

Lemma 10. The weakening rule

is height-preserving admissible for every multiset $\Delta $ .

Proof. Straightforward by induction on the height of the derivation.

Definition 11. The translation from classical logic in a language containing signed propositional atoms, conjunctions and disjunctions (in what follows we assume that the quantifiers are vacuous) is inductively defined as follows:

• • $(P)^{*}=P$ ;

• • $(\overline {P})^{*}= \overline {P}$ ;

• • ;

• • $(A\land B)^{*}= \exists x A^{*}\otimes \exists y B^{*}$ .

The translation extends to multisets: if $\Gamma $ is a finite multiset of formulae in the classical language, we let $\Gamma ^*=\exists x \Gamma ^{*}$ , where $\exists x \Gamma ^*$ stands for the multiset obtained by prefixing every formula in $\Gamma $ with a vacuous quantifier. We write $A^\infty $ to denote the multiset of formula containing infinitely many copies of A. The definition naturally extends to multisets of formulas.

Definition 12 ( $\mathtt {ALV}$ )

$\mathtt {ALV}$ extends $\mathtt {AL}$ with the following rules for vacuous quantification:

Proposition 13. Classical propositional logic is a subsystem of affine propositional logic extended with infinitary rules for vacuous quantification ( $\mathtt {ALV}$ ).

The proof of the proposition rests on the following lemma, which ensures the admissibility of an infinitary form of contraction for vacuously existentially quantified formulas.

Lemma 14. The following rule is admissible in $\mathtt {ALV}$ :

Proof. We argue by induction on the height of the derivation. If $\vdash \Gamma ,\exists x A^\infty $ is an initial sequent, so is $\vdash \Gamma ,\exists x A$ , because only literals can be principal in initial sequents. If one of the existential quantifiers is principal, we have

By applying the invertibility of the rule for the existential quantifier we get a derivation of $\vdash \Gamma ,A^\infty $ , because the countable union of a countable multiset of formulas is a countable multiset. The desired conclusion follows by an application of the rule $\exists $ .

Figure 2 $\mathtt {CPL}$ .

If the last rule is a unary rule and $\exists x A$ is not principal, we apply the induction hypothesis to the premise and then the rule again. If the last rule applied is $\otimes $ , we have

In this case we construct the following derivation:

Proof of Proposition

We first prove that, for $\vdash \Gamma $ a finite sequent in the classical logical language,

(1) $$ \begin{align} \mathtt{CPL}\text{ derives }\vdash\Gamma\text{ only if }\mathtt{ALV}\text{ derives }\vdash\exists x \Gamma^*, \end{align} $$

where $\mathtt {CPL}$ is a Tait-style formulation of classical logic (cf. Figure 2). (1) is obtained by induction on the length n of the proof of $\vdash \Gamma $ in $\mathtt {CPL}$ , where length can be taken to be the number of nodes in the maximal path of the derivation tree. If $n=1$ , we have the following derivation of $\vdash \exists x P,\exists x \overline {P}$ in $\mathtt {ALV}$ : ⁶

For $n> 1$ , we consider the two different cases of ( $\land $ ) and ( $\vee $ ). In the former case, we reason as follows:

In the latter, we consider the following proof in $\mathtt {ALV}$ :

We observe that Lemma 14 can be proved also if the premise $\vdash \Gamma , \exists x A^{n}$ for every $n\geq 1$ .

Lemma 15. If is derivable in $\mathtt {ALV}$ , then $\mathtt {CPL}$ derives .

Proof. The proof is by induction on the height of the derivation in $\mathtt {ALV}$ . If is an initial sequent, then is an initial sequent in $\mathtt {CPL}$ . If is the conclusion of a logical rule we distinguish cases according to the last rule applied. If the last rule applied is $\otimes $ we have

We proceed as follows:

where $(C)$ denotes an application of height-preserving admissibility of the rule of contraction in the calculus for classical logic. If the last rule applied is , we have

We construct the following derivation:

We can now prove the faithfulness of the embedding.

Theorem 16. $\vdash \Gamma $ is derivable in $\mathtt {CPL}$ if and only if $\vdash \exists x \Gamma ^{*}$ is derivable in $\mathtt {ALV}$ .

Proof. From left to right we exploit the soundness of the translation. From right to left we apply invertibility of the rule for the existential quantifier and we get a derivation of $\vdash \Gamma ^{*\infty }$ . We then apply the faithfulness lemma which yields the desired conclusion.

3.2 Extension to first-order and infinitary logic

We now extend to first-order logic the soundness of the embedding. To do so, we need to introduce clauses which translate the universal and the existential quantifiers. We propose the following:

• • $(\exists x A)^{*}=\exists x \exists y A^{*}$ , y does not occur in A.

• • $(\forall x A)^{*}=\forall x \exists y A^{*}$ , y does not occur in A.

We recall the rules for the universal and existential quantifiers in classical logic in Figure 3. The rule ( $\exists $ ) is formulated in a Kleene-style version in order to eliminate the need for an explicit contraction rule [18].

Figure 3 Classical rules for quantifiers.

Proposition 17. The embedding extends to first-order classical logic.

Proof. We only need to check the case of the existential quantifier and the universal one. If the last rule applied is $\exists $ , we have

By induction on the height of the derivation we get

In the case of the rule $\forall $ , we proceed as follows:

The embedding can be further extended to encompass infinitary classical logic, that is the extension of classical logic with the rule:

with $\Gamma $ a finite multiset. The claim follows immediately from the next lemma.

Lemma 18. The rule ( $\forall ^\infty $ -cl) is admissible in $\mathtt {ALV}$ via the translation ${}^*$ of its formulas.

Proof. We proceed as follows:

In the case of infinitary classical logic, we can show that the embedding is indeed faithful, in the sense that if the translation of a sequent is provable in $\mathtt {ALV}$ , then the sequent is provable in infinitary classical logic.

Theorem 19. For any sequent $\vdash \Gamma $ , if $\vdash \Gamma ^{*\infty }$ is provable in $\mathtt {ALV}$ , then $\vdash \Gamma $ is provable in infinitary classical logic.

Proof. The proof is by induction on the height of the derivation in $\mathtt {ALV}$ distinguishing cases according to the last rule applied.

Suppose that the last rule applied is $\forall $ with principal formula $\forall x \exists y A^{*}$ , then we have:

we safely assume that the premises contain infinitely many copies of each of the formulas. We construct the following derivation:

3.3 Vacuous quantification and exponentials

In this section we show that affine logic with exponentials can be embedded via a faithful translation in $\mathtt {ALV}$ . ⁷

First we recall the rules which govern the exponentials in affine logic

We call $\mathtt {ALE}$ the resulting system—Affine Logic with Exponentials.

Consider the translation:

• • $(P)^\circ =P$ ,

• • $(\overline {P})^\circ = \overline {P}$ ,

• • ,

• • $(A\otimes B)^\circ = A^\circ \otimes B^\circ $ ,

• • $(? A)^\circ =\exists x A^\circ $ ,

• • $(!A)^\circ =\forall x A^\circ $ ,

where the quantifiers are vacuous.

Proposition 20. $\vdash \Gamma $ is provable in $\mathtt {ALE}$ if and only if $\vdash \Gamma ^\circ $ is provable in $\mathtt {ALV}$ .

The proof of Proposition 20 follows immediately from the next lemmata.

Lemma 21. The following rule is admissible in $\mathtt {ALV}$ for every finite multiset $\Gamma $ :

Proof. The admissibility is proved with the following steps:

Lemma 22. If $\mathtt {ALE}$ proves $\vdash \Gamma $ , then $\mathtt {ALV}$ proves $\vdash \Gamma ^\circ $ .

Proof. We argue by induction on the height of the derivation of $\vdash \Gamma $ in $\mathtt {ALE}$ . The only cases to check are the ones involving exponentials. If the last rule applied is $?$ C or $!$ we exploit Lemmas 14 and 21. If the last rule applied is $?$ we use height-preserving admissibility of weakening and the rule $\exists $ .

Lemma 23. Let $\Gamma $ be a finite multiset of formulas of $\mathtt {ALE}$ and $A_1,...,A_n$ be formulas of $\mathtt {ALE}$ :

$$ \begin{align*} \text{If }\mathtt{ALV}\text{ derives }\vdash\Gamma^\circ, A^{\circ\infty}_1,...,A^{\circ\infty}_n,\text{ then }\vdash\Gamma, ?A_1,...,?A_n\text{ is derivable in }\mathtt{ALE}. \end{align*} $$

Proof. We argue by induction on the height of the derivation of $\vdash \Gamma ^\circ , A^{\circ \infty }_1,...,A^{\circ \infty }_n$ in $\mathtt {ALV}$ distinguishing cases according to the last rule applied.

Since we are working in a setting with admissible weakening, we can safely assume that in applications of the rule $\otimes $ and $\forall $ for every infinitely many occurrences of $A^{\circ \infty }_i$ are present in each premise. If the last rule applied is $\forall $ and the principal formula is in $\Gamma ^{\circ }$ , we have

Since by assumption $\Gamma ^{\circ '}$ is finite, there must be an $i<\omega $ such that $\Gamma _i=\emptyset $ . We consider that premise $\vdash B^{\circ } ,A^{\circ \infty }_1,...,A^{\circ \infty }_n$ and we construct the following derivation:

If $\forall x B$ is a formula among $A^{\circ \infty }_1,...,A^{\circ \infty }_n$ we proceed analogously with an extra application of the rule $?$ .

If the last rule applied is $\exists $ and the principal formula is among the formulas in $A^{\circ \infty }_1,...,A^{\circ \infty }_n$ , we have

We construct the following derivation:

The application of the inductive hypothesis suffices.

The remaining cases are easily provable by applications of the inductive hypothesis followed by applications of the rules of the calculus $\mathtt {ALE}$ .

Lemma 23 gives a formal representation of the intuitive claim about the infinitary nature of exponentials. Indeed, the context-restriction imposed on the rule for the operator $!$ is simulated by the fact that the infinitary multiplicative rule for $\forall $ yields a premise in which the context not under the scope of $?$ is absent.

Remark 24. We observe that due to the transitivity of faithful translations we obtain an alternative proof of the embedding of classical logic into $\mathtt {ALV}$ as follows:

$$ \begin{align*} \mathtt{CL}\text{ proves }\vdash\Gamma \Leftrightarrow \mathtt{ALE}\text{ proves }\vdash\Gamma^{\bullet}\Leftrightarrow\mathtt{ALV}\text{ proves }\vdash (\Gamma^{\bullet})^{\circ}, \end{align*} $$

where $\bullet $ is the translation of affine logic into classical logic.

3.4 Exponential Liar

From the previous results linking vacuous quantification and the exponentials, and the inconsistency Zardini’s system established by [5], we can restore the propositional structure of the derivation of the Liar paradox in full linear and affine logics extended with rules for full disquotation. By our assumptions on $\lambda $ -terms, we can assume that there is a term $l:=\ulcorner ?\overline {\mathrm {Tr}}(l)\urcorner $ . We abbreviate with L the sentence $?\overline {\mathrm {Tr}}(l)$ . We are also assuming that $\overline {L}$ abbreviates $!\mathrm {Tr} (l)$ . Therefore, the rules

are obviously admissible—in fact, the conclusions are just notational variants of the premisses.

Proposition 25. Full, propositional linear and affine logics are inconsistent with the rules

for A a sentence possibly containing exponentials.

Proof.

Remark 26. The content of Proposition 25 shows that—in general—full linear logic with exponentials is enough to simulate the liar paradox when paired with rules for naïve truth. We would like to point out that in our setting the faithful embedding of the exponentials in $\mathtt {ALV}$ requires the presence of the structural rule of weakening.

4 Cut-elimination for multiplicative quantifiers

4.1 Zardini’s cut-elimination: another visit

The results in the previous sections tell us that Zardini’s cut-elimination argument for the theory of naïve truth based on his multiplicative quantifiers cannot work. This leaves open the question whether Zardini’s procedure could work in the absence of the rules for the truth predicate. However, the answer is still negative. Fjellstad indeed found a gap in Zardini’s reduction for the quantifiers by isolating an example of a sequent which is obviously cut-free derivable, but such that the cut involved in its proof cannot be eliminated following Zardini’s instructions [4]. Although pointing to a serious gap in Zardini’s reduction, Fiellstad’s example involves a case that can nonetheless be dealt with by supplementing Zardini’s original reduction strategy with extra conditions. ⁸ By contrast, we directly show that Zardini’s cut-elimination algorithm is based on a proof-manipulation that does not preserve provability.

The problem involves the elimination of cuts in which the cut formula is principal in both the premises of the cut and is a universal or existential formula. Consider the cut which needs to be eliminated.

The solution proposed by Zardini is to reduce the size of the multiset of cut formulas $\overline {A}(t_{1}/x),\overline {A}(t_{2}/x),...$ introduced by the application of $\exists $ . In particular, one should trace up the multiset in the derivation until it becomes finite in a branch. By the design of the system a countably infinite (sub)multiset of $\overline {A}(t_{1}/x),\overline {A}(t_{2}/x),...$ can only be introduced by the rule $\forall $ or by a weakened initial sequent, we detail the first case.

Notice that the principal formula in $\forall $ is not displayed. According to Zardini, we should pick the premise $ \vdash \overline {A}(t_{i}/x),\Delta ^{\prime }_{i}$ and construct the following derivation.

The cut is then replaced by i many cuts and the desired conclusion follows from the application of the weakening rule. Now, the gap in Zardini argument is exactly in the passage displayed above. In fact, while the sequent $ \vdash \overline {A}(t_{i}/x),\Delta ^{\prime }_{i} $ is indeed provable, the same cannot be said of the sequent $ \vdash \overline {A}(t_{1}/x),\overline {A}(t_{2}/x),...,\overline {A}(t_{i}/x), \Delta ' $ . In other words, Zardini’s reduction is based on the idea that the derivation $\pi $ could be performed even if one focused on a single premiss only, instead of infinitely many. For instance, according to the reduction, one could start with the derivation

According to the reduction, one could then transform the derivation into

The sequent $\vdash \overline {P}(t_{i}/x), \forall x P $ , however, is clearly not (cut-free) provable.

4.2 Eliminating cuts

Zardini’s reduction is flawed even if one considers the system without the truth predicate. However, as we shall now demonstrate, cut is eliminable in Zardini’s infinitary logic (without truth), i.e., the system $\mathtt {IK}_{\omega }$ .

Our strategy is based on a double induction, on the length of the derivation and on a modified notion of the degree of formulas which is extended so as to measure the complexity of (possibly infinite) multisets of formulas: for this reason, the proof cannot be lifted to the system with a fully disquotational truth predicate since, as it is well-known, truth collapses the depth of sentences.

We shall eliminate cuts of the form:

Intuitively, the (CUT) rule allows one to cut infinitely many formulas simultaneously. Hence we have one premise $\vdash \Gamma ,\Phi $ , where $\Phi $ is the multiset of formulas to cut and (possibly) infinitely many premises $\vdash \Delta _\varphi ,\overline {\varphi }$ , one for every formula $\varphi $ with $\Phi (\varphi )>0$ . Finally, the multiset $\Delta $ in the conclusion denotes the infinitary multiset union of all the multisets $\Delta _\varphi $ .

The depth of a formula $dp(\varphi )$ is the number of logical symbols (including quantifiers) occurring in it. We shall reason by double induction, with main induction hypothesis on the degree of the multiset of cut formulas, i.e., $dg(\Phi )=sup_{\Phi (\varphi )>0} (dp(\varphi ))+1$ (the degree of a multiset will be—in general—an ordinal), and secondary induction hypothesis on the Hessenberg ordinal sum of the height of the derivations (which is commutative, associative, left and right cancellative and strictly monotone in both arguments). The key point of the reduction is the fact that infinite multisets of the form $[A(t_{i}/x)\,|\, i\in I]$ have a finite degree, because all the formulas occurring inside them have the same depth.

We first prove an auxiliary lemma which enables us to remove cuts on atomic formulas.

Lemma 27. For any multiset $\Gamma ,\Delta $ and any literal P, the rule

is admissible.

Proof. The proof is by induction on the height of $\vdash \Gamma , P$ . If $\Gamma , P$ is an initial sequent, the proof follows by admissibility of weakening. If $\vdash \Gamma , P$ is not an initial sequent, then it is the conclusion of a rule and P cannot be the principal formula. In this case, we permute the cut upward and we eliminate it by induction on the height of the derivation.

Theorem 28. The cut rule is admissible in $\mathtt {IK}_{\omega }$ .

Proof. By double (transfinite) induction with main induction hypothesis on the degree of the multiset of cut formulas and secondary induction hypothesis on the height of the left premise of the cut, i.e., $\Gamma ,\Phi $ .

If $\vdash \Gamma ,\Phi $ is an initial sequent, we distinguish cases. If no formula is active in $\Phi $ , then $\vdash \Gamma ,\Delta $ is an initial sequent too. If one formula is active in $\Phi $ , then the proof follows by weakening. If both the atomic formulas are active in $\Phi $ , i.e., if $\Phi \equiv \Phi ',P,\overline {P}$ , then we have two premises $\vdash \Delta _{P}, P$ and $\vdash \Delta _{\overline {P}}, \overline {P}$ and the desired conclusion follows by an application of the admissible rule Cutat.

If no formula in $\Phi $ is principal, the cut is permuted upwards (possibly replaced by infinitely many cuts) and removed by secondary induction hypothesis.

If a formula is principal in $\Phi $ , we distinguish cases according to its shape. We focus on the cases of the quantifiers, as they are the relevant ones. If a formula of the shape $\forall x A$ is principal, we have

The other premises of the cut will be $\Delta ,\exists x \overline {A}$ and $\Theta _{\varphi },\overline {\varphi }$ for every $\varphi $ in $\Phi $ . First, for every $ i<\omega $ , we perform the following reduction:

where $\Theta _i$ is the multiset union of all the multisets $\Theta _{\varphi }$ with $\Phi _i(\varphi )>0$ . The cut is removed by secondary induction hypothesis on the height of the left premise of the cut. We then apply height-preserving invertibility of the rule $\exists $ to $\vdash \Delta ,\exists x \overline {A}$ to get . Finally we proceed with the following cut:

This cut is removed by primary induction hypothesis on the degree of the multiset of cut formulas which is strictly decreased.

If the principal formula is an existential one, we have

In this case we look at the premise of the cut of the shape $\vdash \Delta ,\forall x\overline {A}$ and we distinguish two subcases. Either $\forall x\overline {A}$ is principal in an inference rule in the derivation or not. In the latter case, then $\Delta $ is already derivable and we obtain the desired conclusion via weakening. In the former case we go upwards to the point in which $\forall x\overline {A}$ is principal (by the design of the rules $\forall x\overline {A}$ will be only in one branch). We have

We perform the following reduction:

The topmost cut is removed by secondary induction hypothesis on the height of the left premise of the cut, whereas the lowermost is removed by induction on the degree of the multiset of cut formulas which has—again—strictly decreased.

We have introduced an approach to cut-elimination for multiplicative quantifiers. It seems hard to generalize it so as to encompass a theory of truth. Indeed, we use a double induction on two measures, one of which is a kind of measure of complexity of formulas. It is well known that rules for naïve truth collapse the depth of sentences: any attempt to reduce a cut on $\mathrm {Tr}\ulcorner A\urcorner $ to a cut on A need to deal with the fact that the depth of A is arbitrary larger than the minimal depth of $\mathrm {Tr}\ulcorner A\urcorner $ . However, this is coherent with what we know about the interaction of truth and Zardini’s rules, given that the original system by Zardini is inconsistent. We believe that—as pointed out also in [14]—the explicit presence of a double inductive parameter in the cut-elimination procedure brings to the fore the hidden presence of contraction.

5 Concluding remarks and future work

We conducted an investigation into contraction-free systems and their potential use in solving paradoxes in the context of truth theories. Furthermore, we proposed a novel way of understanding exponentials, which offers an alternative interpretation of an inherently modal concept. Our study ultimately led us to develop a new cut-elimination procedure for infinitary sequents, allowing for a proof-theoretical analysis of multiplicative quantifiers.

Moving forward, several open problems warrant further investigation. For example, finding a suitable truth predicate to incorporate into the base theory while maintaining consistency is an intriguing challenge, given that systems based on multiplicative quantifiers are not entirely contraction-free. Moreover, Grišin set theory is inconsistent modulo the addition of extensionality. A natural question arises as to whether there exists a natural corresponding property in the case of truth theories based on contraction-free systems with additive (or classical, one may say) quantifiers.

Furthermore, it is important to determine whether the cut-elimination theorem can be generalized to the case of infinitary logic with infinite sequents, with particular attention to the strength of the resulting system.

Finally, in order to avoid the implicit contraction found in the notion of infinite multiset in Zardini’s naive non-contractive system, it would be beneficial to investigate multiplicative, infinitary rules developed using a notion of multiset that can account for copies of different infinite multiplicities.