Linear Logic Using Negative Connectives

Whether or not an inference rule is invertible is an important property to note. Although Gentzen seemingly did not consider this property of his inference rules [32], Ketonen recognized its importance shortly after Gentzen’s work. Indeed, Ketonen restructured Gentzen’s LK calculus around invertible rules, which enabled him to establish certain decidability and independence results for classical provability [18, 19]. Maximizing the presence of invertible inference rules within a proof system stands as a central goal of the widely used G3 two-sided sequent calculus proof system [37].

An intriguing property of linear logic is that the right introduction of a connective is invertible if and only if the right introduction of its dual connective is not invertible. (Note that linear negation is not considered a logical connective in this context.) This observation naturally leads to the concept of polarity. Following Girard [13] and Andreoli [1], a connective is defined as negative if its right-introduction rule is invertible, and positive otherwise. Consequently, a non-atomic formula is defined as negative (positive) if its top-level connective is negative (resp., positive). To extend this notion of polarity to all formulas, a polarity must also be assigned to atomic formulas. While this assignment can be arbitrary, we follow Andreoli’s convention [1] and assign all atomic formulas the negative polarity.

In linear logic, the logical connectives $\top ,\&,\perp ,,\forall ,?$ are negative and $\text{0},\oplus ,\text{1},\otimes ,\exists ,!$ are positive. We follow [26] in presenting linear logic with both linear implication $⊸$ and intuitionistic implication $\Rightarrow$ as primitive. When $\Rightarrow$ is not a primitive, it is usually defined so that $A\Rightarrow B$ is $!A⊸B$. As a result of using $\Rightarrow$, we will not take $!$ as a primitive. Since these implications have invertible right-introduction rules, they are both negative connectives.

In this paper, we develop the proof theory for full linear logic by employing only negative connectives. We slice full linear logic into the following three classes of connectives:

• $\mathrm{■}$

  ${ℒ}_0$ captures the core of intuitionistic logic using the linear logic connectives $\{\top ,\&,\Rightarrow ,\forall \}$.

• $\mathrm{■}$

  ${ℒ}_1$ extends ${ℒ}_0$ by including $⊸$ and corresponds to linear intuitionistic logic.

• $\mathrm{■}$

  ${ℒ}_2$ extends ${ℒ}_1$ by including $\perp$ and $$, forming a complete set of connectives for linear logic.

Thus, the sets of connectives are defined as follows: ${ℒ}_0=\{\top ,\&,\Rightarrow ,\forall \}$, ${ℒ}_1={ℒ}_0\cup \{⊸\}$, and ${ℒ}_2={ℒ}_1\cup \{\perp ,\}$. For $i\in \{0,1,2\}$, we define an ${ℒ}_i$-formula as a formula where all connectives occurring in it are from ${ℒ}_i$. In this paper, $\forall$ denotes a first-order quantifier.

Proof systems that use only negative connectives are common in the literature on intuitionistic logic. For instance, the connectives in ${ℒ}_0$ are primarily the ones discussed in the first half of Girard’s textbook [14]. The positive connectives, such as disjunction, falsehood, and existential quantification, are only briefly mentioned in Chapter 10. Similarly, those studying the normalization procedure for natural deduction in Prawitz’s book [34] will observe how straightforward the treatment of negative connectives is compared to the complexity involved in handling positive connectives.

As the following equivalences reveal, the set ${ℒ}_2$ is a complete set of connectives. (Here, $A\equiv B$ is defined as the judgment that the formula $(A⊸B)\&(B⊸A)$ is provable.)

The set ${ℒ}_2$ is redundant since $BC$ is equivalent to both $(B⊸\perp )⊸(C⊸\perp )⊸\perp$ and to $(B⊸\perp )⊸C$. We shall find it convenient to keep $$ in ${ℒ}_2$, particularly when we discuss multiset rewriting in Section 3.1. When a positive connective appears on the left of an implication, the curry/uncurry equivalences can be employed as below (hence, avoiding the double-negation expressions above).

The main theoretical tools used in this paper are the $\Downarrow {ℒ}_2$ focused proof system and its extension ${\Downarrow }^{+}{ℒ}_2$ that includes (versions of) the cut rule. A sequent is an ${ℒ}_i$ sequent ($i\in \{0,1,2\}$) if all formulas occurring in it are ${ℒ}_i$ formulas.

While this paper presents different ways to present several known results in structural proof theory, it also contains the following novelties.

1. 1.

   $\Downarrow {ℒ}_2$ proofs of ${ℒ}_0$ and ${ℒ}_1$ formulas have the usual intuitionistic structure: i.e., they are necessarily single-conclusion. Classical proof structure only appears once the $\perp$ and $$ connectives are admitted.

2. 2.

   As we shall demonstrate, parallel rule application is captured through multifocusing. Multifocused proofs based on ${ℒ}_0$ and ${ℒ}_1$ formulas are, in fact, single-focused. As a result, such proofs do not permit the parallel application of rules. Non-single-focused proofs are possible with ${ℒ}_2$-sequents.

3. 3.

   Our proof of cut elimination in ${\Downarrow }^{+}{ℒ}_2$ (Theorem 10) contains some technical novelties.

4. 4.

   The admissibility of cut in $\Downarrow {ℒ}_2$ provides a new proof of the completeness of $\Downarrow {ℒ}_2$: earlier completeness proofs relied on permutation arguments within cut-free proofs [2, 26].

5. 5.

   We provide an improved treatment of disjunction and existential quantification within the LJT intuitionistic proof system of [15] and use it to motivate a parallel elimination rule for $\vee$ and $\exists$ in natural deduction proofs for intuitionistic logic.

It is well known that while cut elimination can be challenging to prove given the many cases that need to be considered, once it is proved many important results follow immediately (witness the fact that Gentzen was able to prove the consistency of classical and intuitionistic logic using a one-line proof that invoked his Hauptsatz). We have placed the cut-elimination theorem for $\Downarrow {ℒ}_2$ in the extended version of this paper [27] and in [28, Chapter 7]: as a result, this paper focuses on consequences of cut elimination rather than on that result.

The inference rules in Figure 1 involve two kinds of sequents, namely, $\mathrm{\Sigma }:\mathrm{\Psi };\mathrm{\Gamma }⊢\mathrm{\Delta }$ and $\mathrm{\Sigma }:\mathrm{\Psi };\mathrm{\Gamma }\Downarrow \mathrm{\Theta }⊢{\mathrm{\Theta }}^{\prime }\Downarrow \mathrm{\Delta }$. The signature of these sequents $\mathrm{\Sigma }$ is a binder of eigenvariables within the scope of the sequent. Any variable free in any formula occurring in any zone of the sequent must be explicitly bound (and typed) in $\mathrm{\Sigma }$. The other components of sequents – the left-unbounded zone $\mathrm{\Psi }$, the left-bounded zone $\mathrm{\Gamma }$, the right-bounded zone $\mathrm{\Delta }$, the left-focused zone $\mathrm{\Theta }$, and the right-focused zone ${\mathrm{\Theta }}^{\prime }$ – are all multisets of formulas. We write multiset union as $\uplus$.

The ${\text{decide}}_m$ rule contains the two schema variables ${\mathrm{\Psi }}_2$ and ${\widehat{\mathrm{\Psi }}}_2$: we require these two variables to be instantiated with multisets of formulas in such a way that every formula with a non-zero multiplicity in one of them also has a non-zero multiplicity (not necessarily equal) in the other. The ${\text{decide}}_m$ rule is also constrained so that the multiset union ${\widehat{\mathrm{\Psi }}}_2,{\mathrm{\Gamma }}_2$ is non-empty. If we make no further restrictions on the ${\text{decide}}_m$ inference rule, we call the proof system in Figure 1 the near-focused proof system for ${ℒ}_2$. The $\Downarrow {ℒ}_2$ proof system is the result of requiring that the schema variable $\mathrm{\Delta }$ in the ${\text{decide}}_m$ be a multiset of atomic formulas. Given that restriction on the ${\text{decide}}_m$ rule, it is the case that all instances of the left-phase rules are such that the right-bounded zone contains only atomic formulas. Thus, in $\Downarrow {ℒ}_2$ proofs, the init rule takes place between two occurrences of the same atomic formula.

Although this paper is limited to first-order quantification, it is worth noting that near-focused proofs are stable under higher-order substitution. Specifically, if a predicate within a near-focused proof is substituted with a $\lambda$-term that may contain logical connectives, the resulting instantiation will also be a near-focused proof [28, Chapter 9]. In contrast, an analogous statement does not hold for $\Downarrow {ℒ}_2$ proofs since such substitutions can transform an atomic formula into a non-atomic formula.

The ${\Downarrow }^{+}{ℒ}_2$ proof system is the result of adding the following two cut rules to $\Downarrow {ℒ}_2$.

The formula $B$ is the cut-formula in both of these rules. We say that a $\mathrm{\Sigma }$-formula $B$ has an $\Downarrow {ℒ}_2$ proof if the sequent $\mathrm{\Sigma }:\cdot ;\cdot ⊢B$ has an $\Downarrow {ℒ}_2$ proof.

The site of an inference rule is a set of formula occurrences in the conclusion of that rule, defined as follows: $(i)$ the site for an introduction rule contains just the formula occurrence being introduced, $(ii)$ the site of an init rule contains the two formula occurrences labeled by $B$ in Figure 1, and $(iii)$ the site of the rules release, ${\text{decide}}_m$, $\text{cut}!$, and ${\text{cut}}_l$ are all empty. An occurrence of a formula in the conclusion of an inference rule is a side-formula occurrence if it is not in the site of that rule. For example, all formula occurrences in the conclusion of release, ${\text{decide}}_m$, $\text{cut}!$, and ${\text{cut}}_l$ are side-formula occurrences. Side-formula occurrences can appear in any zone in the two different styles of sequents.

The inference rules of the $\Downarrow {ℒ}_2$ proof system are classified as multiplicative and additive depending on how the rule treats bounded side-formula occurrences. All inference rules treat side-formula occurrences in the unbounded zone the same: formulas occurring in the unbounded zone of the conclusion occur in the unbounded zone of every premise. An inference rule is additive if every side-formula occurrence in a bounded zone in the rule’s conclusion has an occurrence in the same bounded zone in every premise of the rule. An inference rule is multiplicative if every side-formula occurrence in a bounded zone in the rule’s conclusion has an occurrence in exactly one premise and that occurrence is within the same kind of bounded zone. (Here, the left and right-focused zones are also considered to be bounded zones.) Note that all right phase rules are additive, all left rules are multiplicative, and all phase switching rules are additive and multiplicative.

Proofs in $\Downarrow {ℒ}_2$ are multifocused proofs. If every occurrence of the ${\text{decide}}_m$ rule in a proof selects exactly one formula, we say that the proof is single-focused. Similarly, proofs in $\Downarrow {ℒ}_2$ are multiple-conclusion proofs. If every sequent in a proof has exactly one formula on its right-hand side, we say that the proof is a single-conclusion proof.

The focused proof system $\Downarrow {ℒ}_2$ can be used to build large-scale inference rules by abstracting away from some of the details in the exact order introductions are applied, as described next. A border sequent is a sequent of the form $\mathrm{\Sigma }:\mathrm{\Psi };\mathrm{\Gamma }⊢\mathrm{\Delta }$ where $\mathrm{\Delta }$ is a multiset of atomic formulas. Above a border sequent is a ${\text{decide}}_m$ rule and above that is a left phase. Open premises of the left phase are either the left premise of $\Rightarrow$L or the conclusion of a release rule; above these are right phases. Open premises of these right phases must again be border sequents. Such a collection of inference rules that have border sequents as (open) premises, a border sequent as the conclusion, and exactly one instance of the ${\text{decide}}_m$ rule is called a bipole. The synthetic rule justified by such a bipole is the result of deleting all the internal inference rules of the left and right phases and simply maintaining the border sequents as premises and conclusion.

The following soundness theorem is straightforward to prove since every inference rule in $\Downarrow {ℒ}_2$ is derivable in linear logic: when translating the zoned sequents used in $\Downarrow {ℒ}_2$ to linear logic, simply place the exponential $!$ on all formulas in the unbounded zone and then replace the semicolon and the two occurrences of $\Downarrow$ with commas.

We illustrate in this section how multifocused proofs can capture parallel rule application.

The multiplicative false $\perp$ separates the intuitionistic frameworks $\Downarrow {ℒ}_0$ and $\Downarrow {ℒ}_1$, where proofs are single-conclusion and single-focused, from the full linear logic framework $\Downarrow {ℒ}_2$. (As mentioned earlier, $$ can be defined using ${ℒ}_1$ and $\perp$.) Once $\perp$ is present, it is natural to deal with the notion of linear negation, which can be encoded in $\Downarrow {ℒ}_2$ using the “implies false” construction. In the following pairs of sequents, the first sequent has a $\Downarrow {ℒ}_2$ proof if and only if the second also has a $\Downarrow {ℒ}_2$ proof.

If “implies false” was a logical connective, its introduction rules on the left and the right are invertible, thus giving it both positive and negative polarities.

We define the delay operator $\partial (B)$ to be $(B⊸\perp )⊸\perp$. While $B$ and $\partial (B)$ are provably equivalent, their roles within $\Downarrow {ℒ}_2$ proofs can differ. Consider the following derivation.

Thus, the following is an admissible rule

although we do not generally have the rule

This latter rule is a form of contraction that is not immediately associated with focusing (as is the case with the ${\text{decide}}_m$ rule).

Let Neg be the negative intuitionistic connectives $\{\text{t},\wedge ,\supset ,\forall \}$ and let Pos be the positive intuitionistic connectives $\{\text{f},\vee ,\exists \}$. We map intuitionistic logic formulas over the connectives in Neg to formulas in linear logic connectives using the following obvious translation: $A^{\circ }=A$ for atomic formulas and

Let ${\text{LJT}}^{-}$ be the proof system in Figure 4 for intuitionistic logic over the connectives in Neg that results from renaming the ${ℒ}_0$ connectives in Figure 3 with the corresponding connectives in Neg. The implication-only fragment of this proof system is exactly the LJT proof system of Herbelin in [15]. The following proposition has an immediate proof, given the structural properties we have seen of $\Downarrow {ℒ}_2$ proofs of ${ℒ}_0$ sequents.

To the extent that maximal multifocused proofs are candidates for canonical proofs, we can conclude that ${\text{LJT}}^{-}$ proofs are canonical for the negative connectives since all multifocused proofs are single-focused, and, hence, are maximal multifocused.

We now extend the mapping of intuitionistic logic formulas into ${ℒ}_2$ formulas in a rather natural fashion in order to treat also the positive connectives: ${\text{f}}^{\circ }=\top ⊸\perp$, ${(B\vee C)}^{\circ }=((B^{\circ }\Rightarrow \perp )\&(C^{\circ }\Rightarrow \perp ))⊸\perp$, and ${(\exists x.B)}^{\circ }=(\forall x.(B^{\circ }\Rightarrow \perp ))⊸\perp$. To make for a stronger result, we add the positive truth ${\text{t}}^{+}$ and the positive conjunction ${\wedge }^{+}$ to our intuitionistic logic. These connectives are superfluous since we will be able to prove the formulas $\text{t}$ and ${\text{t}}^{+}$ and the formulas $B\wedge C$ and $B{\wedge }^{+}C$ are equivalent (in intuitionistic logic). Nonetheless, we shall map them into linear logic differently: ${({\text{t}}^{+})}^{\circ }=\perp ⊸\perp$ and ${(B{\wedge }^{+}C)}^{\circ }=(B^{\circ }\Rightarrow C^{\circ }\Rightarrow \perp )⊸\perp$. We shall also derive different inference rules for them. Note two things about this extension: First, the results of such translations are much richer than for the negative connectives: for example, one occurrence of $\vee$ yields seven occurrences of linear logic connectives. Second, this translation uses $\perp$, which leaves open the possibility to have multifocused proofs that are not single-focused.

The soundness of this translation (Proposition 16) is proved by a simple induction on the structure of ${\text{LJT}}^{\pm }$ proofs; the proof of completeness (Proposition 17) is in Appendix A.3.

Given the work of Herbelin [15], Espírito Santo [8], and others, the connection between focused proofs and natural deduction using only negative connectives is well established. It is also well known that the natural deduction treatment of the positive connectives is challenged by some of the same issues experienced by the sequent calculus: elimination rules for the positive connectives can permute over each other without changing the essential nature of the proof. As a result, dealing with normal-form proofs is complicated. In [14], Girard says “one tends to think that natural deduction should be modified to correct such atrocities.” We illustrate one approach to making such a correction, but the cost will be an inference rule that can have a large number of premises. This approach is motivated by the treatment of left-introduction rules for the positive connectives in ${\text{LJT}}^{\pm }$ proofs.

A positive formula is in disjunctive normal form if it is of the form

The formula $N_{i,j_i}$ must be either atomic or have a negative connective as its top level connective. It is easy to show the following facts about disjunctive normal forms.

1. 1.

   These normal forms are unique up to renaming the existentially bound variables and the ordering of conjuncts and disjuncts (i.e., modulo commutativity and identity for these binary connectives).

2. 2.

   The disjunctive normal form of a formula can be exponentially larger than the formula.

3. 3.

   The following invariant holds for rules in ${\text{LJT}}^{\pm }$: if a rule has $\Uparrow \mathrm{\Gamma }⊢$ in the conclusion and the premises contain $\Uparrow {\mathrm{\Gamma }}_1⊢,\mathrm{\dots },\Uparrow {\mathrm{\Gamma }}_n⊢$, then both ${\bigwedge }^{+}\mathrm{\Gamma }$ and $({\bigwedge }^{+}{\mathrm{\Gamma }}_1)\vee \mathrm{\cdots }\vee ({\bigwedge }^{+}{\mathrm{\Gamma }}_n)$ have the same disjunctive normal form.

The disjunctive normal form can be used to describe the following parallel elimination for the positive connectives, which can be given as the figure on the left.

Here, $P_1,\mathrm{\dots },P_p$ ($p\ge 1$) are positive formulas and the disjunctive normal form of $P_1{\wedge }^{+}\mathrm{\cdots }{\wedge }^{+}{P}_p$ is given by $(\ast )$ above. The formula $D$ can be restricted to being either a positive formula or an atomic formula. In this inference rule, $x_1,\mathrm{\dots },x_p$ are treated as (new) eigenvariables. A drawback of this rule is that the number of hypothetical premises can be an exponential in the number of occurrences of logical connectives in the formulas $P_1,\mathrm{\dots },P_p$.

Following Gentzen’s approach to defining the intuitionistic proof system LJ from the classical proof system LK, Schellinx [35] defined the ILL proof system for intuitionistic logic to be the single-conclusion restriction of the multiple-conclusion CLL proof system for full (classical) linear logic. He then studied situations where CLL is not conservative over ILL. In particular, he showed that there are formulas composed of only $⊸$ and the additive false $0$ that are provable in CLL and not in ILL. He also showed that Girard’s translation of LJ into CLL is conservative, a result that shows a different approach to relating ${ℒ}_0$ to ${ℒ}_2$. Laurent [21] continued the study of ILL and CLL and provided several generalizations and extensions to Schellinx’s paper.

As we mentioned at the start of Section 2, the $\Downarrow {ℒ}_2$ proof system assumes that atomic formulas have negative polarity. Since this assumption is baked into the design of $\Downarrow {ℒ}_2$, it is unclear how one might accommodate atoms with a positive polarity. Nonetheless, having atomic formulas with positive polarity has been used at the level of term representation [12, 31, 41, 40], where explicit sharing of term structures is enabled, and at the proof search level [4], where forward chaining (in contrast to backward chaining) is the major inference form. In the setting of intuitionistic and classical logics, the proof systems LKQ [6] and LJQ [7] assume that all atomic formulas are positive. The LKF and LJF proof system [23] go further and allow positive and negative atomic formulas within the same proof. It is interesting to consider modifying $\Downarrow {ℒ}_2$ to allow mixing both positive and negative polarized atomic formulas.

Extending this work to include higher-order quantification is a natural next step to consider given the successful higher-order extensions of $\Downarrow {ℒ}_0$ in [10] and LKQ and LKT in [6].

Whether or not this work can be extended to account for different cut-elimination strategies, such as those inspired by call-by-value and call-by-name [33] and call-by-push-value [22] is currently an open question.

This paper presents the proof theory of full linear logic through an intuitionistic orientation rather than the classical orientation based on De Morgan dualities, proof nets, and one-sided sequent calculi. Linear logic is dissected into ${ℒ}_0$, a core intuitionistic logic, and ${ℒ}_1$, which incorporates linear implication, and finally ${ℒ}_2$, which extends ${ℒ}_1$ with multiplicative falsity $\perp$ and disjunction $$.

Central to our analysis is the multifocused, multiple-conclusion proof system $\Downarrow {ℒ}_2$ for full linear logic. We demonstrate how $\Downarrow {ℒ}_2$ subsumes existing focused proof systems for ${ℒ}_0$ and ${ℒ}_1$, while also introducing a formal definition of parallel rule application via multifocusing. Crucially, we show that this form of parallelism, which is non-trivial in $\Downarrow {ℒ}_2$, is absent in proofs involving only ${ℒ}_0$ or ${ℒ}_1$ formulas. Furthermore, our work revisits and refines existing results, offering a new treatment of disjunction and existential quantification within intuitionistic sequent calculus and natural deduction. These innovations lead to more intuitive and modular proof systems. The cut elimination theorem, detailed in the appendix of the extended version of this paper [27], provides the essential foundation for the results presented in this paper.