# Linear logic using negative connectives: extended version

Dale Miller

► To cite this version:

Dale Miller. Linear logic using negative connectives: extended version. FSCD 2025 - 10th International Conference on Formal Structures for Computation and Deduction, Jul 2025, Birmingham, United Kingdom. pp.26:1-26:26, 10.4230/LIPIcs.FSCD.2025.26 . hal-05067259

HAL Id: hal-05067259

https://hal.science/hal-05067259v1

Submitted on 14 May 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Linear logic using negative connectives: extended version

Dale Miller

<figure><img src="image_2.png" /></figure>

ID

Inria Saclay & LIX Institut Polytechnique de Paris, France

## Abstract

In linear logic, the invertibility of a connective's right-introduction rule is equivalent to the non-invertibility of its left-introduction rule. This duality motivates the concept of *polarity*: a connective is termed *negative* if its right-introduction rule is invertible, and *positive* otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes of *goal-reduction* and *backchaining*, respectively. These phases are formalized here using the framework of *multifocused proofs*. We analyze linear logic by dissecting it into three sublogics: $\mathcal{L}_0$ (first-order intuitionistic logic with conjunction, implication, and universal quantification); $\mathcal{L}_1$ (an extension of $\mathcal{L}_0$ incorporating linear implication which preserves its intuitionistic nature); and $\mathcal{L}_2$ (which includes multiplicative falsity $\perp$ and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of $\mathcal{L}_0$ and $\mathcal{L}_1$. While multifocused proofs of $\mathcal{L}_2$ sequents can accommodate parallel applications of left-introduction rules, proofs of $\mathcal{L}_0$ and $\mathcal{L}_1$ sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic.

**2012 ACM Subject Classification** Theory of computation $\rightarrow$ Proof theory; Theory of computation $\rightarrow$ Linear logic

**Keywords and phrases** Linear logic, multifocused proofs, sequent calculus

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2025.26

# 1 Introduction

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 [33], 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 [38].

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$, $\not\top$, $\top$, $\&$, $\top$, $\exists$, $\neg$ are negative and $0$, $\oplus$, $1$, $\otimes$, $\exists$, $\neg$ are positive. We follow [26] in presenting linear logic with both linear implication $\neg\circ$ and

<figure><img src="image_3.png" /></figure>

© Dale Miller;

licensed under Creative Commons License CC-BY 4.0

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025).

Editor: Maribel Fernández; Article No. 26; pp. 26:1–26:26

<figure><img src="image_4.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 26:2 Linear logic using negative connectives: extended version

intuitionistic implication $\Rightarrow$ as primitive. When $\Rightarrow$ is not a primitive, it is usually defined so that $A \Rightarrow B$ is $!A \neg \neg 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:

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

- $\mathcal{L}_1$ extends $\mathcal{L}_0$ by including $\neg$ and corresponds to linear intuitionistic logic.

- $\mathcal{L}_2$ extends $\mathcal{L}_1$ by including $\perp$ and $\not\exists$, forming a complete set of connectives for linear logic.

Thus, the sets of connectives are defined as follows: $\mathcal{L}_0 = \{\top, \& , \Rightarrow, \forall\}$, $\mathcal{L}_1 = \mathcal{L}_0 \cup \{\neg\}$, and $\mathcal{L}_2 = \mathcal{L}_1 \cup \{\perp, \not\exists\}$. For $i \in \{0, 1, 2\}$, we define an $\mathcal{L}_i$-formula as a formula where all connectives occurring in it are from $\mathcal{L}_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 $\mathcal{L}_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 [35] 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 $\mathcal{L}_2$ is a complete set of connectives. (Here, $A \equiv B$ is defined as the judgment that the formula $(A \neg \neg B) \& (B \neg \neg A)$ is provable.)

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
\mathbf{0} & \equiv \top \neg \bot & !B \equiv (B \Rightarrow \bot) \neg \bot & B \oplus C \equiv ((B \neg \bot) \& (C \neg \bot)) \neg \bot \\
\mathbf{1} & \equiv \bot \neg \bot & ?B \equiv (B \neg \bot) \Rightarrow \bot & B \otimes C \equiv (B \neg \bot) \neg (C \neg \bot) \neg \bot \\
& & \exists x.B \equiv (\forall x.B \neg \bot) \neg \bot
\end{array}
$$

The set $\mathcal{L}_2$ is redundant since $B \not\exists C$ is equivalent to both $(B \neg \bot) \neg (C \neg \bot) \neg \bot$ and to $(B \neg \bot) \neg C$. We shall find it convenient to keep $\not\exists$ in $\mathcal{L}_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).

$$ 
\begin{array}{l@{\qquad}l}
\mathbf{1} & \neg H \equiv H \quad (B \otimes C) \neg H \equiv B \neg C \neg H \quad (B \oplus C) \neg H \equiv (B \neg H) \& (C \neg H) \\
\mathbf{0} & \neg H \equiv \top \quad (\exists x.Bx) \neg H \equiv \forall x.(Bx \neg H)
\end{array}
$$

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

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

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

2. As we shall demonstrate, parallel rule application is captured through *multifocusing*. Multifocused proofs based on $\mathcal{L}_0$ and $\mathcal{L}_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 $\mathcal{L}_2$-sequents.

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

4. The admissibility of cut in $\Downarrow \mathcal{L}_2$ provides a new proof of the completeness of $\Downarrow \mathcal{L}_2$: earlier completeness proofs relied on permutation arguments within cut-free proofs [2, 26].
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 $\lor$ 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\mathcal{L}_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.

## 2 The focused proof systems $\Downarrow\mathcal{L}_2$ and $\Downarrow^+\mathcal{L}_2$

The inference rules in Figure 1 involve two kinds of sequents, namely, $\Sigma: \Psi; \Gamma \vdash \Delta$ and $\Sigma: \Psi; \Gamma \Downarrow \Theta \vdash \Theta' \Downarrow \Delta$. The *signature* of these sequents $\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 $\Sigma$. The other components of sequents—the *left-unbounded zone* $\Psi$, the *left-bounded zone* $\Gamma$, the *right-bounded zone* $\Delta$, the *left-focused zone* $\Theta$, and the *right-focused zone* $\Theta'$—are all multisets of formulas. We write multiset union as $\cup$.

The *decide*<sub>m</sub> rule contains the two schema variables $\Psi_2$ and $\hat{\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 *decide*<sub>m</sub> rule is also constrained so that the multiset union $\hat{\Psi}_2, \Gamma_2$ is non-empty. If we make no further restrictions on the *decide*<sub>m</sub> inference rule, we call the proof system in Figure 1 the *near-focused proof system* for $\mathcal{L}_2$. The $\Downarrow\mathcal{L}_2$ proof system is the result of requiring that the schema variable $\Delta$ in the *decide*<sub>m</sub> be a multiset of atomic formulas. Given that restriction on the *decide*<sub>m</sub> 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\mathcal{L}_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\mathcal{L}_2$ proofs since such substitutions can transform an atomic formula into a non-atomic formula.

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

$$ \frac{\Sigma: \Psi; \vdash B \qquad \Sigma: \Psi, B; \Gamma \vdash \Delta \qquad \Sigma: \Psi; \Gamma_1 \vdash B, \Delta_1 \qquad \Sigma: \Psi; \Gamma_2, B \vdash \Delta_2}{\Sigma: \Psi; \Gamma \vdash \Delta} \quad \text{cut!} $$ $$ \frac{\Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2} \quad \text{cut}_l $$

The formula $B$ is the *cut-formula* in both of these rules. We say that a $\Sigma$-formula $B$ has an $\Downarrow\mathcal{L}_2$ proof if the sequent $\Sigma: \cdot; \cdot \vdash B$ has an $\Downarrow\mathcal{L}_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*, *decide*<sub>m</sub>, *cut*!, and *cut*<sub>l</sub> 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
selects exactly one formula, we say that the proof is *single-focused*. Similarly, proofs in $\Downarrow \mathcal{L}_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 \mathcal{L}_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 $\Sigma: \Psi; \Gamma \vdash \Delta$ where $\Delta$ is a multiset of atomic formulas. Above a border sequent is a *decide*<sub>m</sub> 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 *decide*<sub>m</sub> 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.

**► Example 1.** Let $a, b, c$ be propositional constants and assume that $\Psi$ contains the formula $a \dashv b \dashv c$. We have the following bipole and the synthetic inference rule it justifies.

$$ \frac{\frac{\Sigma: \Psi; \Gamma_1 \vdash a, \Delta_1 \quad \Sigma: \Psi; \Gamma_2 \vdash b, \Delta_2 \quad \text{release} \quad \Sigma: \Psi; \Gamma_2 \Downarrow \vdash b \Downarrow \Delta_2}{\Sigma: \Psi; \Gamma_1 \Downarrow \vdash a \Downarrow \Delta_1} \quad \text{release} \quad \Sigma: \Psi; \Gamma_1 \vdash c, \Delta_1, \Delta_2}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash c, \Delta_1, \Delta_2} \quad \text{decide}_m \quad \text{init} \quad \dashv \times 2 $$

$$ \frac{\Sigma: \Psi; \Gamma_1 \vdash a, \Delta_1 \quad \Sigma: \Psi; \Gamma_2 \vdash b, \Delta_2}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash c, \Delta_1, \Delta_2} $$

If instead we assume that $\Psi$ contains the formula $a \Rightarrow b \Rightarrow c$ then we have the following bipole and the synthetic inference rule it justifies.

$$ \frac{\Sigma: \Psi; \vdash a, \cdot \quad \Sigma: \Psi; \vdash b \quad \Sigma: \Psi; \Downarrow \cdot c \vdash \cdot \Downarrow c}{\Sigma: \Psi; \Downarrow \cdot a \Rightarrow b \Rightarrow c \vdash \cdot \Downarrow c} \stackrel{\text{init}}{\Rightarrow} \times 2 \quad \frac{\Sigma: \Psi; \vdash a \quad \Sigma: \Psi; \vdash b}{\Sigma: \Psi; \vdash c} $$

The following soundness theorem is straightforward to prove since every inference rule in $\Downarrow \mathcal{L}_2$ is derivable in linear logic: when translating the zoned sequents used in $\Downarrow \mathcal{L}_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.

**► Theorem 2 (Soundness of $\Downarrow \mathcal{L}_2$ proofs).** If $\Sigma: \cdot; \cdot \vdash B$ has a $\Downarrow \mathcal{L}_2$ proof then B is a theorem of linear logic.

## 2.1 Deriving $\Downarrow \mathcal{L}_0$ and $\Downarrow \mathcal{L}_1$ from $\Downarrow \mathcal{L}_2$

One of the important features of the $\Downarrow \mathcal{L}_2$ proof system is that if we are interested in proving an $\mathcal{L}_1$ or an $\mathcal{L}_0$ formula, then various features of $\Downarrow \mathcal{L}_2$ proofs are not used, and that proof system can be greatly simplified when proving such formulas. The following propositions will allow us to justify such simplifications of $\Downarrow \mathcal{L}_2$.

**► Lemma 3.** There is no $\Downarrow \mathcal{L}_2$ proof of an $\mathcal{L}_1$ sequent with an empty right side.
**Proof.** Assume that there is a $\Downarrow \mathcal{L}_2$ proof of a sequent with an empty right side and with only $\mathcal{L}_1$ formulas on the left side. Let $\Xi$ be such a proof of minimal height. Consider the last inference rule of $\Xi$. This last inference rule cannot be a right-introduction rule since these require a non-empty right side. Similarly, the last rule is not $decide_m$ since that would yield a premise with an empty right side and with a shorter proof. Thus, the endsequent of $\Xi$ must be of the form $\Sigma: \Psi; \Gamma \Downarrow \Theta \vdash \cdot \Downarrow \cdot$ where $\Psi, \Gamma$, and $\Theta$ are multisets of $\mathcal{L}_1$ formulas over $\Sigma$. However, a check of all possible left-introduction rules ($\perp L$ and $\not\gamma L$ are not possible) and the release rule yields at least one premise with an empty right side which has a shorter proof. This contradicts the choice of $\Xi$. ◀

**Proposition 4.** If $\Xi$ is a $\Downarrow \mathcal{L}_2$ proof of a single-conclusion $\mathcal{L}_1$-sequent then $\Xi$ is a single-conclusion proof.

**Proof.** We proceed by induction on the structure of the $\Downarrow \mathcal{L}_2$ proof $\Xi$. By considering all the possible last inference rules of $\Xi$, we need to show that a single-conclusion sequent in the conclusion will guarantee that all premises are also single-conclusion: the inductive hypothesis then completes the proof. The only case that is not immediate is the case for the $\neg \circ L$ rule, namely,

$$ \frac{\Sigma: \Psi; \Gamma_1 \Downarrow \Theta_1 \vdash \Theta_3, B \Downarrow \Delta_1 \quad \Sigma: \Psi; \Gamma_2 \Downarrow C, \Theta_2 \vdash \Theta_4 \Downarrow \Delta_2}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \Downarrow B \neg \circ C, \Theta_1, \Theta_2 \vdash \Theta_3, \Theta_4 \Downarrow \Delta_1, \Delta_2} \quad \neg \circ L $$

and where $\Theta_3 \uplus \Theta_4 \uplus \Delta_1 \uplus \Delta_2$ is a singleton multiset. By Lemma 3, we know that $\Theta_4 \uplus \Delta_2$ is not empty. As a result, $\Theta_3 \uplus \Delta_1$ must be empty. Thus, both premises of this inference rule are single-conclusion sequents. ◀

**Proposition 5.** If $\Xi$ is a $\Downarrow \mathcal{L}_2$ proof of a single-conclusion $\mathcal{L}_1$ sequent then $\Xi$ is single-focused.

**Proof.** Assume that there is a $\Downarrow \mathcal{L}_2$ proof of an $\mathcal{L}_1$ sequent that is not single-focused, and let $\Xi$ be chosen as such a proof of minimal height. The endsequent of $\Xi$ must be a $\Downarrow$-sequent with the focused zones containing at least two formulas. Consider the last inference rule in $\Xi$. That rule is not *init*. By Proposition 4, it is not *release*. Because of the minimality assumption, that rule is not $\forall L$, $\&L$, or $\Rightarrow L$. The only remaining case is when that rule is $\neg \circ L$. Thus, the last inference figure in $\Xi$ is of the form

$$ \frac{\Sigma: \Psi; \Gamma_1 \Downarrow \Theta_1 \vdash \Theta_3, B \Downarrow \Delta_1 \quad \Sigma: \Psi; \Gamma_2 \Downarrow C, \Theta_2 \vdash \Theta_4 \Downarrow \Delta_2}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \Downarrow B \neg \circ C, \Theta_1, \Theta_2 \vdash \Theta_3, \Theta_4 \Downarrow \Delta_1, \Delta_2} \quad \neg \circ L, $$

where at least one of the multisets $\Theta_1, \dots, \Theta_4$ must be non-empty. Thus, one of the premises must have a focused zone with two or more members, which contradicts the minimal height assumption about $\Xi$. ◀

Let $\Xi$ be a $\Downarrow \mathcal{L}_2$ proof of the sequent $\Sigma: \cdot; \cdot \vdash B$, where $B$ is an $\mathcal{L}_1 \Sigma$-formula. By Proposition 4, all sequents in $\Xi$ are single-conclusion and by Proposition 5, every $\Downarrow$ sequent has a focus zone (combining the left and right parts) containing exactly one formula. The proof system in Figure 2 can describe all such proofs; this proof system arises from $\Downarrow \mathcal{L}_2$ by taking the following steps:

- Delete the inference rules that introduce $\perp$ and $\not\gamma$.

- Simplify all sequents to have only one formula on the right side.
$$ \frac{\Sigma: \Psi; \Gamma \vdash B \quad \Sigma: \Psi; \Gamma \vdash C}{\Sigma: \Psi; \Gamma \vdash \top} \quad \top R \quad \frac{\Sigma: \Psi; \Gamma \vdash B \ \& \ C}{\Sigma: \Psi; \Gamma \vdash \top} \quad \& R $$

$$ \frac{\Sigma: \Psi; B, \Gamma \vdash C}{\Sigma: \Psi; \Gamma \vdash B \to C} \quad \to R \quad \frac{\Sigma: B, \Psi; \Gamma \vdash C}{\Sigma: \Psi; \Gamma \vdash B \Rightarrow C} \quad \Rightarrow R \quad \frac{y: \tau, \Sigma: \Psi; \Gamma \vdash B[y/x]}{\Sigma: \Psi; \Gamma \vdash \forall_{\tau} x.B} \quad \forall R $$

$$ \frac{\Sigma: \Psi; \Gamma \vdash B_i \vdash A}{\Sigma: \Psi; \Gamma \vdash B_1 \ \& \ B_2 \vdash A} \quad \& L_i \quad \frac{\Sigma: \Psi; \Gamma \vdash B[t/x] \vdash A}{\Sigma: \Psi; \Gamma \vdash \forall_{\tau} x.B \vdash A} \quad \forall L \quad \frac{\Sigma: \Psi; \Gamma \vdash A}{\Sigma: \Psi; \Gamma \vdash B \ \& \ C \vdash A} \quad \text{init} $$

$$ \frac{\Sigma: \Psi; \Gamma \vdash B \quad \Sigma: \Psi; \Gamma \vdash C \vdash A}{\Sigma: \Psi; \Gamma \vdash B \Rightarrow C \vdash A} \quad \Rightarrow L \quad \frac{\Sigma: \Psi; \Gamma_1 \vdash B \quad \Sigma: \Psi; \Gamma_2 \vdash C \vdash A}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash B \to C \vdash A} \quad \to L $$

$$ \frac{\Sigma: \Psi, B; \Gamma \vdash B \vdash A}{\Sigma: \Psi, B; \Gamma \vdash A} \quad \text{decide!} \quad \frac{\Sigma: \Psi; \Gamma \vdash B \vdash A}{\Sigma: \Psi; \Gamma, B \vdash A} \quad \text{decide}_l $$

Figure 2 The $\vdash \mathcal{L}_1$ proof system

- Modify the decide rule to select exactly one formula by splitting it into $decide_l$ (to select a formula from the left-bounded zone) and $decide$! (to select a formula from the left-unbounded zone).

- Drop the release rule since it can be merged into the left premise of $\to L$. As a result, all $\vdash$ sequents no longer need their right-focused zone.

The resulting simplification of the $\vdash \mathcal{L}_2$ proof system is the $\vdash \mathcal{L}_1$ proof system in Figure 2. It is simple to show that if $B$ is an $\mathcal{L}_1$ formula then there is a $\vdash \mathcal{L}_2$ proof of $B$ if and only if there is a $\vdash \mathcal{L}_1$ proof of $B$. Thus, the multiple-conclusion and the multifocus features of $\vdash \mathcal{L}_2$ proofs are not usable for $\mathcal{L}_1$ sequents. Note that in other presentations of proof systems for intuitionistic linear logic, the use of single-conclusion sequents is a requirement [11, 21, 36, 39], while in our setting, it is a consequence of the choice of connectives.

If we now turn our attention to proofs of $\mathcal{L}_0$ formulas, we find that an additional feature of $\vdash \mathcal{L}_1$ and $\vdash \mathcal{L}_2$ proofs is not needed.

**Proposition 6.** If $B$ is an $\mathcal{L}_0$ $\Sigma$-formula and $\Xi$ is a $\vdash \mathcal{L}_2$-proof of $\Sigma: \vdash; \Gamma \vdash B$, then $\Xi$ is a single-focused and single-conclusion proof in which all left-bounded zones are empty.

**Proof.** Let $B$ be an $\mathcal{L}_0$ $\Sigma$-formula, and let $\Xi$ be a $\vdash \mathcal{L}_2$-proof of $\Sigma: \vdash; \Gamma \vdash B$. By the two preceding propositions, $\Xi$ can be viewed as a $\vdash \mathcal{L}_1$ proof. An easy induction on the structure of such proofs reveals that if $B$ does not contain $\to$, then the left-bounded zone for all sequents in $\Xi$ is empty. $\quad$

This proposition justifies introducing the $\vdash \mathcal{L}_0$ proof system in Figure 3, where the inference rules introducing $\to$ are dropped, and the left-bounded zone is removed (since it will always be empty). The $\vdash \mathcal{L}_0$ proof system is also known as LJT [15, 16] and as uniform proofs with backchaining [29]. We will return to $\vdash \mathcal{L}_0$ when we discuss the LJT$^-$ proof system in Section 5.

It is worth noting here that while $\vdash \mathcal{L}_2$ is a multiple-conclusion proof system, both $\vdash \mathcal{L}_0$ and $\vdash \mathcal{L}_1$ are single-conclusion proof systems. This characteristic of $\vdash \mathcal{L}_0$ and $\vdash \mathcal{L}_1$ is not an imposition on the more general multiple-conclusion proof system (as Gentzen needed to impose on LK to get the LJ proof system [11]) but rather it is simply a consequence of using fewer logical connectives.
**26:8 Linear logic using negative connectives: extended version**

<figure><img src="image_5.png" /><figcaption>Figure 3 The rules that result from restricting ⇓ ℒ₂ to ℒ₀ sequents.</figcaption></figure>

**2.2 Paths in formulas**

Given a sequent of the form $\Sigma: \Psi; \Gamma \vdash \Delta$ there is a unique right phase with that conclusion: the right phase can be seen as a *function* that takes such a sequent and returns a multiset of sequents of the form $\Sigma, \Sigma': \Psi, \Psi'; \Gamma, \Gamma' \vdash A$ (where $A$ is a multiset of atomic formulas), which forms the premises of that right-introduction phase. On the other hand, the left-introduction phase yields a nondeterministic *relation* between its endsequent, say, $\Sigma: \Psi; \Gamma \Downarrow \Theta \vdash \cdot \Downarrow A$, and the multiset of sequents of the form $\Sigma: \Psi; \Gamma' \Downarrow \cdot \vdash \Theta' \Downarrow \Delta'$ that are the premises of a left-introduction phase. As Propositions 7 and 8 will show, the following notion of *paths* in $\mathcal{L}_2$ formulas can be used to calculate those functions and relations.

Let $B$ be an $\mathcal{L}_2$-formula. The paths in $B$ are those formulas $P$ for which the following two-place relation $B \uparrow P$ is provable.

<figure><img src="image_6.png" /></figure>

It is easy to prove $B \equiv \&_{B\uparrow P} P$ by using the following distributivity properties and quantifier movement rules:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
C \to (B_1 \& B_2) \equiv (C \to B_1) \& (C \to B_2) & C \nparallel (B_1 \& B_2) \equiv (C \nparallel B_1) \& (C \nparallel B_2) & \\
C \Rightarrow (B_1 \& B_2) \equiv (C \Rightarrow B_1) \& (C \Rightarrow B_2) & \forall x. (B_1 \& B_2) \equiv (\forall x. B_1) \& (\forall x. B_2) &
\end{array}
$$

Paths have a simple normal form. Using the equivalences (where $x$ is not free in $B$)

$$ B \nparallel \forall x.C \equiv \forall x.(B \nparallel C), \quad B \to \forall x.C \equiv \forall x.(B \to C), \quad \text{and} \quad B \Rightarrow \forall x.C \equiv \forall x.(B \Rightarrow C), $$

a path can be written in the form $\forall x_1 \dots \forall x_n.P'$ where $n \ge 0$, and every occurrence of $\forall$ in $P'$ occurs to the left of either $\to$ or $\Rightarrow$. Similarly, using the equivalences

$$ 
\begin{array}{l@{\qquad}l}
(B \to C_1) \nparallel C_2 \equiv B \to (C_1 \nparallel C_2), & B \to C \Rightarrow D \equiv C \Rightarrow B \to D, \\
(B \Rightarrow C_1) \nparallel C_2 \equiv B \Rightarrow (C_1 \nparallel C_2), & \perp \nparallel B \equiv B \nparallel \perp \equiv B
\end{array}
$$

and the commutativity of $\nparallel$, paths can be put into the normal form

$$ \forall \bar{x} [C_1 \Rightarrow \dots \Rightarrow C_n \Rightarrow B_1 \to \dots \to B_m \to A_1 \nparallel \dots \nparallel A_p], $$
where $\forall \bar{x}$ is a list of universal quantifiers, $n, m, p$ are non-negative integers, $A_1, \dots, A_p$ are atomic formulas, and $B_1, \dots, B_m, C_1, \dots, C_n$ are $\mathcal{L}_2$ formulas. If a path $P$ has the normal form above, then we say that the multiset $\{C_1, \dots, C_n\}$ is its intuitionistic arguments, the multiset $\{B_1, \dots, B_m\}$ is its linear arguments, and the multiset $\{A_1, \dots, A_p\}$ is its targets. Finally, $\bar{x}$ is the list of bound variables of $P$ (we assume that all these bound variables are distinct and subject to $\alpha$-conversion). Since these various components of the normal form of a path are multisets, this decomposition of a path is unique. We shall also display this normal form as the associated sequent $\bar{x}: C_1, \dots, C_n; B_1, \dots, B_m \vdash A_1, \dots, A_p$. Paths can be used to describe both left and right phases in a more abstract setting than by appealing to introduction rules.

**Proposition 7.** Consider a $\downarrow\mathcal{L}_2$-proof $\Xi$ of the sequent $\Sigma: \Psi; \Gamma \vdash G, \Delta$. There is a $\downarrow\mathcal{L}_2$-proof $\Xi'$ of this same sequent that differs only in permutations of right-introduction rules such that the formula $G$ is decomposed first. More specially, that right-introduction phase can be written as

$$ \frac{\displaystyle\frac{\Xi_i}{\Sigma: \Psi; \Gamma \vdash G, \Delta} \quad \text{where the path } P_i \text{ is associated with the sequent } \Sigma_i: \Psi_i; \Gamma_i \vdash A_i \text{ and where } \Xi_i \text{ is the right phase of the } i^{\text{th}} \text{ premise.}} $$

Concerning left phases in single-focused proofs with endsequent $\Sigma: \Psi; \Gamma \downarrow B \vdash \cdot \downarrow A$ we note that in every left rule application, the signature and the left-unbounded zone in the conclusion is the same in every premise.

**Proposition 8.** Let $\Xi$ be a $\downarrow\mathcal{L}_2$-proof of the sequent $\Sigma: \Psi; \Gamma \downarrow B \vdash \cdot \downarrow A$. The left-introduction phase at the bottom of $\Xi$, which has a multiset of premises $\mathcal{M}$, can be described as follows. There is a path $P$ in $B$ with the associated sequent $\Sigma': C_1, \dots, C_n; B_1, \dots, B_m \vdash A_1, \dots, A_p$ and there is a substitution $\theta$ that maps the variables in $\Sigma'$ to $\Sigma$-terms such that

1. $A$ is equal to the multiset union $\{A_1\theta, \dots, A_p\theta\} \uplus A_1 \uplus \dots \uplus A_m$;

2. $\Gamma$ is the multiset union $\Gamma_1 \uplus \dots \uplus \Gamma_m$; and

3. $\mathcal{M}$ is the multiset union $\{\Sigma: \Psi; \cdot \vdash C_i\theta\}_{i=1}^n \uplus \{\Sigma: \Psi; \Gamma_i \vdash B_i\theta, A_i\}_{i=1}^m$.

This use of paths to characterize the two focusing phases is a generalization of the use of game moves in [30] and patterns in [43].

## 2.3 Cut elimination and completeness for $\downarrow\mathcal{L}_2$

One method for proving the (relative) completeness of $\downarrow\mathcal{L}_2$ is to first prove that the general form of the initial rule and the cut rule are admissible. These two admissibility results are more formally stated as the following two theorems.

**Theorem 9 (Admissibility of the generalized initial rule).** Let $B$ be an $\mathcal{L}_2$ $\Sigma$-formula. The sequent $\Sigma: \cdot; B \vdash B$ has a $\downarrow\mathcal{L}_2$ proof.

**Theorem 10 (Cut elimination for $\downarrow^+\mathcal{L}_2$).** Let $B$ be an $\mathcal{L}_2$ $\Sigma$-formula. If the sequent $\Sigma: \cdot; \cdot \vdash B$ has an $\downarrow^+\mathcal{L}_2$ proof then it has a $\downarrow\mathcal{L}_2$ proof.

A proof of Theorem 9 is in Appendix A.1 and a proof of Theorem 10 is in the extended version of this paper [27] and in [28, Chapter 7]. Below, we highlight the main novelty of our cut-elimination proof. We first introduce the following key cut inference rule.

$$ \frac{\Sigma: \Psi; \Gamma_1 \vdash B, \Delta \quad \Sigma: \Psi; \Gamma_2 \downarrow B \vdash \cdot \downarrow A \quad \text{cut}_k}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash \Delta, A} $$
**26:10 Linear logic using negative connectives: extended version**

When we allow this inference rule within a focused proof, we know that the right premise is proved by using a left-phase rule on B, while the left premise is proved by a right-introduction rule (and via permutation of right-introduction rules) on B.

Consider the following instance of cut! in a single-focused proof Ξ.

$$ \frac{\begin{array}{c} \Xi_l \\ \Sigma: \Psi; \vdash B \end{array} \quad \begin{array}{c} \Xi_r \\ \Sigma: \Psi, B; \Gamma \vdash \Delta \end{array}}{\Sigma: \Psi; \Gamma \vdash \Delta} \quad \text{cut!} $$

Consider also a subderivation of Ξ<sub>r</sub> that ends in *decide*<sub>m</sub>, such as

$$ \frac{\begin{array}{c} \Xi_0 \\ \Sigma, \Sigma': \Psi, \Psi', B; \Gamma' \vdash B \vdash \Delta \end{array}}{\Sigma, \Sigma': \Psi, \Psi', B; \Gamma' \vdash \Delta} \quad \text{decide}_m, $$

where the variables bound in Σ' are not bound in Σ and where Ψ' and Γ' are multisets. This inference rule can be converted to the derivation

$$ \frac{\begin{array}{c} \hat{\Xi}_l \\ \Sigma, \Sigma': \Psi, \Psi'; \vdash B \end{array} \quad \begin{array}{c} \Xi_0 \\ \Sigma, \Sigma': \Psi, \Psi', B; \Gamma' \vdash B \vdash \Delta \end{array}}{\Sigma, \Sigma': \Psi, \Psi', B; \Gamma' \vdash \Delta} \quad \text{cut}_k. $$

Here, $\hat{\Xi}_l$ is the result of weakening $\Xi_l$ (using Proposition 20 in Appendix A.2). We can thus remove all occurrences of $decide_m$ on B in $\Xi_r$ to obtain the proof $\Xi'_r$ of $\Sigma: \Psi, B; \Gamma \vdash \Delta$. Since B is no longer used in this subproof, $\Xi'_r$ can be strengthened (using Proposition 22 in Appendix A.2) to get a proof of $\Sigma: \Psi; \Gamma \vdash \Delta$. This proof can now replace our original instance of cut! Similarly, an occurrence of cut$_l$ can be used to rewrite instances of $decide_m$ into a key cut. The argument for eliminating key cuts follows the usual pattern of matching a left-introduction rule with a right-introduction rule.

One can draw some analogies between the proof theory of $\vdash \mathcal{L}_2$ and the meta-theory of typed λ-calculi. This connection is well developed for the $\vdash \mathcal{L}_0$ calculus (see Section 5). More generally, Theorems 9 and 10 are closely related to η-expansion and β-reduction in typed λ-calculi, and Theorem 10 corresponds to a weak normalization theorem.

The completeness of $\vdash \mathcal{L}_2$ proofs for linear logic is now a simple consequent of this cut-elimination theorem since it is possible to prove that all the rules in an unfocused proof system for linear logic are admissible in $\vdash^{\mathcal{L}_2}$.

**► Theorem 11 (Completeness of $\vdash \mathcal{L}_2$).** Let B be an $\mathcal{L}_2$ Σ-formula provable in linear logic. The sequent $\Sigma: \vdash \cdot \vdash B$ has a $\vdash \mathcal{L}_2$-proof.

Several completeness proofs exist for focused proof systems. The first such proof, given by Andreoli [1], transformed cut-free proofs into focused proofs via permutation of inference rules. The completeness of $\vdash \mathcal{L}_2$ is proved in [26] by mapping the formulas and focused proofs used by Andreoli to those in $\vdash \mathcal{L}_2$. An alternative proof, based directly on phases rather than introduction rules, is given by Bruscoli and Guglielmi [2]. Other completeness proofs leveraged the cut rule and cut elimination, rather than the direct manipulation of cut-free proofs. Examples of this approach can be found in [5, 20, 37, 43] for various fragments of linear and intuitionistic logic, and in [24] for classical logic. Theorem 11, which relies on Theorems 9 and 10, falls into this latter category.

**3 Parallel rule application within proofs**

We illustrate in this section how multifocused proofs can capture parallel rule application.
26:12 Linear logic using negative connectives: extended version

► **Example 14.** Assume that $a, b, c, d, l$ are atomic formulas and that the two formulas $b \not\sim l \dashv a \not\sim l$ and $d \not\sim l \dashv c \not\sim l$ are members of $\Psi$. The atomic formula $l$ serves as a kind of lock, and this lock makes it impossible for there to be a parallel application of these two rules unless there are two occurrences of the lock. The following is a synthetic inference rule

$$ \frac{\Sigma: \Psi; \Gamma \vdash b, d, l, l, \Delta \qquad \text{while the following is not a synthetic rule}}{\Sigma: \Psi; \Gamma \vdash a, c, l, l, \Delta} \qquad \text{(assuming that } \Delta \text{ does not contain } l). $$

$$ \frac{\Sigma: \Psi; \Gamma \vdash b, d, l, \Delta}{\Sigma: \Psi; \Gamma \vdash a, c, l, \Delta} $$

The Lolli logic programming language [17] is based on the logic $\mathcal{L}_1$ and the only form of multiset rewriting it provided followed the indirect style described in Example 12. The Forum [26] extension to Lolli is based on $\mathcal{L}_2$ and it can encode multiset rewriting in the more direct style of Example 13, although it did not provide for parallel rewriting steps since it was described using a single-focused proof system. The LolliMon logic programming language [25] and the Concurrent LF [40] extended $\mathcal{L}_1$ by allowing some occurrences of the positive linear logic connectives 1, $\otimes$, $!$, and $\exists$ and positively polarized atomic formulas. In that system, a direct form of multiset rewriting was also possible using the multiset encoded in the left-bounded zone. The Concurrent LF did not permit multifocusing, but it did provide an equality theory within its dependently-type setting that could equate different non-overlapping rewrites occurring in different order.

## 3.2 Multifocusing as parallel rule application

Two notable aspects of the $\Downarrow \mathcal{L}_2$ proof system make it possible to deal with parallel rule application within a sequent calculus setting.

First, focusing makes it possible to hide the sequential nature of the construction of synthetic inference rules. The order in which left introduction rules are applied within a multifocused proof is irrelevant since every order leads to the same result. The same applies to the order in which right-introduction rules are applied in multiple-conclusion proofs. Thus, the reliance on phases and synthetic rules means that the particular details of how a phase is constructed are hidden away.

Second, the $\Downarrow \mathcal{L}_2$ proof system contains a subtle feature: namely, the interaction between the zone on the right located between the $\vdash$ and the $\Downarrow$ and the use of the *release* rule to merge that zone with the rest of the right-hand context. Consider modifying sequents so that the right-hand zone between $\vdash$ and $\Downarrow$ is removed and rewriting the $\dashv \neg L$ inference rule as

$$ \frac{\Sigma: \Psi; \Gamma_1 \Downarrow \Theta_1 \vdash B, \Delta_1 \quad \Sigma: \Psi; \Gamma_2 \Downarrow C, \Theta_2 \vdash \Delta_2}{\Sigma: \Psi; \Gamma_1, \Gamma_2 \Downarrow B \dashv \neg C, \Theta_1, \Theta_2 \vdash \Delta_1, \Delta_2} \qquad \neg L^*. $$

The inference rule in Example 14 that we argued should not exist as a synthetic rule can now be constructed with the rule $\neg L^*$.

*Maximally multifocused proofs* have been proposed as a way to describe canonical proofs in the sequent calculus: in particular, they have been shown to correspond to expansion proofs in classical logic [3] and proof nets in MALL [4]. To the extent that we are using multifocusing to capture parallel rule application, a $\Downarrow \mathcal{L}_2$ proof of a sequent that does not mention $\perp$ and $\not\sim$ will not exhibit this kind of parallelism.

# 4 Linear negation in proofs

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

$$ \Sigma: \Psi; \Gamma, B \dashv \perp \vdash \Delta \quad \dashv \quad \Sigma: \Psi; \Gamma \vdash B, \Delta $$

$$ \Sigma: \Psi, (B \Rightarrow \perp) \dashv \perp; \Gamma \vdash \Delta \quad \dashv \quad \Sigma: \Psi; \Gamma, (B \Rightarrow \perp) \dashv \perp \vdash \Delta $$

$$ \Sigma: \Psi, B; \Gamma \vdash \Delta \quad \dashv \quad \Sigma: \Psi; \Gamma, (B \Rightarrow \perp) \dashv \perp \vdash \Delta $$

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 \dashv \perp) \dashv \perp$. While $B$ and $\partial(B)$ are provably equivalent, their roles within $\llcorner \mathcal{L}_2$ proofs can differ. Consider the following derivation.

$$ \frac{\Sigma: \Psi, \partial(B); \Gamma, B \vdash \Delta \qquad \Sigma: \Psi, \partial(B); \Gamma, B \vdash \perp, \Delta \qquad \Sigma: \Psi, \partial(B); \Gamma \vdash B \dashv \perp, \Delta}{\Sigma: \Psi, \partial(B); \Gamma \llcorner \partial \vdash B \dashv \perp \llcorner \Delta} \qquad \Sigma: \Psi, \partial(B); \llcorner \partial \vdash \perp \vdash \llcorner \partial \cdot \llcorner \partial \Delta} $$

Thus, the following is an admissible rule

$$ \frac{\Sigma: \Psi, \partial(B); \Gamma, B \vdash \Delta, \quad \text{although we do not generally have the rule}}{\Sigma: \Psi, \partial(B); \Gamma \vdash \Delta} \qquad \frac{\Sigma: \Psi, B; \Gamma, B \vdash \Delta}{\Sigma: \Psi, B; \Gamma \vdash \Delta} $$

This latter rule is a form of contraction that is not immediately associated with focusing (as is the case with the *decide*<sub>*m*</sub> rule).

# 5 The LJT<sup>±</sup> proof system for intuitionistic logic

Let Neg be the negative intuitionistic connectives {$t, \wedge, \supset, \forall$} and let Pos be the positive intuitionistic connectives {$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

$$ t^\circ = \top, \quad (B \wedge C)^\circ = B^\circ \& C^\circ, \quad (B \supset C)^\circ = B^\circ \Rightarrow C^\circ, \quad (\forall x.B)^\circ = \forall x.B^\circ $$

Let LJT<sup>-</sup> be the proof system in Figure 4 for intuitionistic logic over the connectives in Neg that results from renaming the $\mathcal{L}_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 $\llcorner \mathcal{L}_2$ proofs of $\mathcal{L}_0$ sequents.

**Proposition 15.** Let $B$ be an intuitionistic formula over the connectives in Neg. The sequent $\Sigma: \cdot; \vdash B^\circ$ is provable in $\llcorner \mathcal{L}_2$ if and only if the sequent $\Sigma: \cdot \vdash B$ has an LJT<sup>-</sup> proof.

To the extent that maximal multifocused proofs are candidates for canonical proofs, we can conclude that LJT<sup>-</sup> proofs are canonical for the negative connectives since all multifocused proofs are single-focused, and, hence, are maximal multifocused.
26:14 Linear logic using negative connectives: extended version

$$
\begin{array}{r@{\quad}l@{\quad}l@{\quad}l@{\quad}l}
\begin{array}{c} \Sigma: \Psi \vdash t \\ \hline \Sigma: \Psi \vdash t \end{array} & \mathrm{tR} & \begin{array}{c} \Sigma: \Psi \vdash B & \Sigma: \Psi \vdash C \\ \hline \Sigma: \Psi \vdash B \wedge C & \wedge R \end{array} & \begin{array}{c} \Sigma: B, \Psi \vdash C \\ \hline \Sigma: \Psi \vdash B \supset C & \supset R \end{array} & \begin{array}{c} y: \tau, \Sigma: \Psi \vdash B[y/x] \\ \hline \Sigma: \Psi \vdash \forall_{\tau} x.B & \forall R \end{array} \\[1.5em]
\begin{array}{c} \Sigma: \Psi, N \vdash N \\ \hline \Sigma: \Psi, N \vdash P_a \end{array} & \text{decide}_m & \begin{array}{c} \Sigma: \Psi \vdash A \\ \hline \Sigma: \Psi \vdash A \supset A \end{array} & \text{init} \\[1.5em]
\begin{array}{c} \Sigma: \Psi \vdash B_i \\ \hline \Sigma: \Psi \vdash B_1 \wedge B_2 \\ \hline \Sigma: \Psi \vdash B_1 \wedge B_2 \supset A \end{array} & \wedge L_i & \begin{array}{c} \Sigma: \Psi \vdash B[t/x] \\ \hline \Sigma: \Psi \vdash \forall_{\tau} x.B \\ \hline \Sigma: \Psi \vdash A \\ \hline \Sigma: \Psi \vdash A \supset A \end{array} & \forall L \\[1.5em]
\begin{array}{c} \Sigma: \Psi \vdash B \\ \hline \Sigma: \Psi \vdash B_1 \wedge B_2 \supset A \end{array} & \wedge L_i & \begin{array}{c} \Sigma: \Psi \vdash B \\ \hline \Sigma: \Psi \vdash C \\ \hline \Sigma: \Psi \vdash B \supset C \\ \hline \Sigma: \Psi \vdash B \supset C \supset A \end{array} & \supset L
\end{array}
$$

Figure 4 The LJT<sup>-</sup> proof system

$$
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c@{\quad}c}
\begin{array}{c} \Sigma: \Psi \vdash B_i \\ \hline \Sigma: \Psi \vdash B_1 \vee B_2 \end{array} & \forall R & \begin{array}{c} \Sigma: \Psi \vdash B[t/x] \\ \hline \Sigma: \Psi \vdash \exists x.B \end{array} & \forall R & \begin{array}{c} \Sigma: \Psi \vdash B & \Sigma: \Psi \vdash C \\ \hline \Sigma: \Psi \vdash B \wedge^+ C \end{array} \\
\begin{array}{c} \Sigma: \Psi, P \upharpoonright P \\ \hline \Sigma: \Psi, P \vdash P_a \end{array} & \text{invert} & \begin{array}{c} \Sigma: \Psi, N \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright N \vdash P_a \end{array} & \text{done} \\
\begin{array}{c} \Sigma: \Psi \upharpoonright B, \Gamma \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright C, \Gamma \vdash P_a \end{array} & \forall L & \begin{array}{c} \Sigma: \Psi \upharpoonright f, \Gamma \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright f, \Gamma \supset P_a \end{array} & fL \\
\begin{array}{c} \Sigma: \Psi \upharpoonright B, C, \Gamma \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright B \wedge^+ C, \Gamma \vdash P_a \end{array} & \wedge^+ L & \begin{array}{c} \Sigma: \Psi \upharpoonright \Gamma \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright t^+, \Gamma \vdash P_a \end{array} & t^+L \\
\begin{array}{c} \Sigma: \Psi \upharpoonright B, C, \Gamma \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright B \wedge^+ C, \Gamma \vdash P_a \end{array} & \wedge^+ L & \begin{array}{c} \Sigma: \Psi \upharpoonright B[t/x], \Gamma \vdash P_a \\ \hline \Sigma: \Psi \upharpoonright \exists x.B, \Gamma \vdash P_a \end{array} & \exists L
\end{array}
$$

Here, $P_A$ ranges over either positive formulas or atomic formulas, and $\mathcal{P}$ (in the *invert* rule) is a non-empty multiset of positive formulas.

Figure 5 The additional rules for the LJT<sup>±</sup> proof system.

We now extend the mapping of intuitionistic logic formulas into $\mathcal{L}_2$ formulas in a rather
natural fashion in order to treat also the positive connectives: $f^\circ = \top \to \bot$, $(B \vee C)^\circ =$
(($B^\circ \Rightarrow \bot$) & ($C^\circ \Rightarrow \bot$)) $\to$ $\bot$, and $(\exists x.B)^\circ = (\forall x.(B^\circ \Rightarrow \bot))$ $\to$ $\bot$.
To make for a stronger result, we add the positive truth $t^+$ and the positive conjunction $\wedge^+$ to our intuitionistic logic.
These connectives are superfluous since we will be able to prove the formulas $t$ and $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: ($t^+)^\circ = \bot \to \bot$ and $(B \wedge^+ C)^\circ = (B^\circ \Rightarrow C^\circ \Rightarrow \bot) \to \bot$.
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 $\bot$, 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 LJT<sup>±</sup> proofs; the proof of completeness (Proposition 17) is in Appendix A.3.

► **Proposition 16** (Soundness of $(\cdot)^\circ$). Let $B$ be a formula over the connectives in $\text{Neg} \cup \text{Pos}$.
If $B$ is provable in $\text{LJT}^\pm$, then $B^\circ$ is provable in linear logic.

► **Proposition 17** (Completeness of $(\cdot)^\circ$). Let $B$ be a formula over the connectives in $\text{Neg} \cup \text{Pos}$.
If $B^\circ$ is provable in linear logic, then $B$ is provable in the LJT$^\pm$ proof system.

► **Example 18.** The formula $(a \vee b) \supset p \supset p$ is clearly provable in intuitionistic logic. The
LJF proof system [23] treats disjunctions and existentials on the left in a linear fashion: when such formulas appear on the left, they are introduced exactly once. Thus, the formula above has exactly one LJF proof, and that proof includes a (harmless) case analysis. In LJT<sup>±</sup>, there are possibly many proofs of this formula, one for every invocation of the *invert* rule on a disjunctive assumption. This is similar to the proof system in [9] based on a polarized intuitionistic proof system that uses a “negation translation” for the disjunction.

## 6 Revisiting natural deduction

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 LJT<sup>±</sup> proofs.

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

$$ \exists x_1 \dots \exists x_p \left( \bigvee_{i=1}^{n} \bigwedge_{j_i=1}^{m_i} N_{i,j_i} \right). \quad (*) $$

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. 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. The disjunctive normal form of a formula can be exponentially larger than the formula.

3. The following invariant holds for rules in LJT<sup>±</sup>: if a rule has $\Uparrow \Gamma \vdash$ in the conclusion and the premises contain $\Uparrow \Gamma_1 \vdash, \dots, \Uparrow \Gamma_n \vdash$, then both $\bigwedge^+ \Gamma$ and $(\bigwedge^+ \Gamma_1) \vee \dots \vee (\bigwedge^+ \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, \dots, P_p$ ($p \ge 1$) are positive formulas and the disjunctive normal form of $P_1 \wedge^+ \dots \wedge^+ P_p$ is given by (*) above. The formula $D$ can be restricted to being either a positive formula or an atomic formula. In this inference rule, $x_1, \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, \dots, P_p$.

**► Example 19.** Assume that $p \ge 1$ and that $a_1, \dots, a_p, b_1, \dots, b_p$ are atomic formulas. A special case of the parallel elimination rule for positive formulas is the following.

$$ \frac{a_1 \lor b_1 \cdots a_p \lor b_p \quad \left( \begin{array}{c} \{a_i \mid i \in I\} \cup \{b_j \mid i \notin I\} \\ \vdots \\ D \end{array} \right)_{I \subseteq \{1, \dots, p\}}}{D} \qquad \text{This rule has } p + 2^p \text{ premises.} $$
# 7 Related and Future work

Following Gentzen's approach to defining the intuitionistic proof system LJ from the classical proof system LK, Schellinx [36] 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 $\neg$ 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 $\mathcal{L}_0$ to $\mathcal{L}_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 $\vdash \mathcal{L}_2$ proof system assumes that atomic formulas have negative polarity. Since this assumption is baked into the design of $\vdash \mathcal{L}_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, 42, 41], 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 $\vdash \mathcal{L}_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 $\vdash \mathcal{L}_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 [34] and call-by-push-value [22] is currently an open question.

# 8 Conclusion

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 $\mathcal{L}_0$, a core intuitionistic logic, and $\mathcal{L}_1$, which incorporates linear implication, and finally $\mathcal{L}_2$, which extends $\mathcal{L}_1$ with multiplicative falsity $\perp$ and disjunction $\Join$.

Central to our analysis is the multifocused, multiple-conclusion proof system $\vdash \mathcal{L}_2$ for full linear logic. We demonstrate how $\vdash \mathcal{L}_2$ subsumes existing focused proof systems for $\mathcal{L}_0$ and $\mathcal{L}_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 $\vdash \mathcal{L}_2$, is absent in proofs involving only $\mathcal{L}_0$ or $\mathcal{L}_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.

**Acknowledgments** I thank the reviewers of this paper for their comments and Jui-Hsuan Wu and Beniamino Accattoli for insightful discussions on topics related to this paper.
References

1 Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. *J. of Logic and Computation*, 2(3):297-347, 1992. doi:10.1093/logcom/2.3.297.

2 Paola Bruscoli and Alessio Guglielmi. On structuring proof search for first order linear logic. *Theoretical Computer Science*, 360(1-3):42-76, 2006. doi:10.1016/j.tcs.2005.11.047.

3 Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A multi-focused proof system isomorphic to expansion proofs. *J. of Logic and Computation*, 26(2):577-603, 2016. doi:10.1093/logcom/exu030.

4 Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, editors, *Fifth International Conference on Theoretical Computer Science*, volume 273 of IFIP, pages 383-396. Springer, sep 2008. doi:10.1007/978-0-387-09680-3_26.

5 Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. *J. of Automated Reasoning*, 40(2-3):133-177, 2008. doi:10.1007/s10817-007-9091-0.

6 V. Danos, J.-B. Joinet, and H. Schellinx. LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, *Advances in Linear Logic*, number 222 in London Mathematical Society Lecture Note Series, pages 211-224. Cambridge University Press, 1995. doi:10.1017/CBO9780511629150.

7 R. Dyckhoff and S. Lengrand. LJQ: a strongly focused calculus for intuitionistic logic. In A. Beckmann and et al., editors, *Computability in Europe 2006*, volume 3988 of LNCS, pages 173-185. Springer, 2006. doi:10.1007/11780342_19.

8 José Espírito Santo. Completing Herbelin's programme. In Simona Ronchi Della Rocca, editor, *Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings*, volume 4583 of LNCS, pages 118-132. Springer, 2007. doi:10.1007/978-3-540-73228-0_10.

9 José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic. In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, *26th International Conference on Types for Proofs and Programs (TYPES 2020)*, LIPIcs, pages 4:1-4:24, 2020. doi:10.4230/LIPIcs.TYPES.2020.4.

10 Amy Felty. Encoding the calculus of constructions in a higher-order logic. In M. Vardi, editor, *8th Symp. on Logic in Computer Science*, pages 233-244. IEEE, jun 1993. doi:10.1109/LICS.1993.287584.

11 Gerhard Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, *The Collected Papers of Gerhard Gentzen*, pages 68-131. North-Holland, Amsterdam, 1935. Translation of articles that appeared in 1934-35. Collected papers appeared in 1969. doi:10.1007/BF01201353.

12 Ulysse Gérard and Dale Miller. Separating functional computation from relations. In Valentin Goranko and Mads Dam, editors, *26th EACSL Annual Conference on Computer Science Logic (CSL 2017)*, volume 82 of LIPIcs, pages 23:1-23:17, 2017. doi:10.4230/LIPIcs.CSL.2017.23.

13 Jean-Yves Girard. A new constructive logic: classical logic. *Math. Structures in Comp. Science*, 1:255-296, 1991. doi:10.1017/S0960129500001328.

14 Jean-Yves Girard, Paul Taylor, and Yves Lafont. *Proofs and Types*. Cambridge University Press, 1989.

15 Hugo Herbelin. A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In *Computer Science Logic, 8th International Workshop, CSL '94*, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer, 1995. doi:10.1007/BFb0022247.

16 Hugo Herbelin and Gyesik Lee. Forcing-based cut-elimination for gentzen-style intuitionistic sequent calculus. In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, *Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009*,
26:18 Linear logic using negative connectives: extended version

Tokyo, Japan, June 21-24, 2009. Proceedings, volume 5514 of LNCS, pages 209-217. Springer, 2009. doi:10.1007/978-3-642-02261-6.

17 Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327-365, 1994. doi:10.1006/inco.1994.1036.

18 Oiva Ketonen. Untersuchungen zum Prädikatenkalkul. Annales Academiae Scientiarum Fennicae, series A, I. Mathematica-physica 23, 1944.

19 Oiva Ketonen. Investigations into the Predicate Calculus. College Publications, 2022. Ed. by S. Negri and J. von Plato.

20 Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, may 2004.

21 Olivier Laurent. Around classical and intuitionistic linear logics. In LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 629-638, jul 2018. doi:10.1145/3209108.3209132.

22 Paul Blain Levy. Call-by-push-value: A subsuming paradigm (extended abstract). In J.-Y. Girard, editor, *Typed Lambda Calculi and Applications (TLCA 1999)*, volume 1581 of lncs. Springer, 1999.

23 Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. *Theoretical Computer Science*, 410(46):4747-4768, 2009. Abstract Interpretation and Logic Programming: A Special Issue in Honor of Professor Giorgio Levi. doi:10.1016/j.tcs.2009.07.041.

24 Chuck Liang and Dale Miller. Focusing Gentzen's LK proof system. In Thomas Piecha and Kai Wehmeier, editors, *Peter Schroeder-Heister on Proof-Theoretic Semantics*, Outstanding Contributions to Logic, pages 275-313. Springer, 2024. doi:10.1007/978-3-031-50981-0_9.

25 Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concurrent linear logic programming. In Pedro Barahona and Amy P. Felty, editors, *Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP)*, pages 35-46. ACM, 2005. doi:10.1145/1069778.

26 Dale Miller. Forum: A multiple-conclusion specification logic. *Theoretical Computer Science*, 165(1):201-232, 1996. doi:10.1016/0304-3975(96)00045-X.

27 Dale Miller. Linear logic using negative connectives: extended version. Technical report, Inria Saclay, 2025. Extended version of a paper appearing in FSCD 2025.

28 Dale Miller. *Proof Theory and Logic Programming: Computation as Proof Search*. Cambridge University Press, 2025. To appear. Preprint available at https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/.

29 Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. *Annals of Pure and Applied Logic*, 51(1-2):125-157, 1991. doi:10.1016/0168-0072(91)90068-W.

30 Dale Miller and Alexis Saurin. A game semantics for proof search: Preliminary results. In M. Escardó, A. Jung, and M. Mislove, editors, *Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)*, volume 155 of ENTCS, pages 543-563. Elsevier, 2005. doi:10.1016/j.entcs.2005.11.072.

31 Dale Miller and Jui-Hsuan Wu. A positive perspective on term representations. In Bartek Klin and Elaine Pimentel, editors, *31st EACSL Annual Conference on Computer Science Logic (CSL 2023)*, volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPIcs.CSL.2023.3.

32 Grigorii E. Mints. Finite investigations of transfinite derivations. In Selected papers in proof theory, pages 17-71. Bibliopolis, 1992.

33 Jan von Plato. Proof theory of classical and intuitionistic logic. In Leila Haaparanta, editor, *The Development of Modern Logic*. Oxford University Press, 2009.

34 Gordin Plotkin. Call-by-name, call-by-value and the λ-calculus. *Theoretical Computer Science*, 1(1):125-159, 1976.
35 Dag Prawitz. *Natural Deduction*. Almqvist & Wiksell, Uppsala, 1965.

36 Harold Schellinx. Some syntactical observations on linear logic. *J. of Logic and Computation*, 1(4):537–559, sep 1991. doi:10.1093/logcom/1.4.537.

37 Robert J. Simmons. Structural focalization. *ACM Trans. on Computational Logic*, 15(3):21, 2014. doi:10.1145/2629678.

38 A. S. Troelstra and H. Schwichtenberg. *Basic Proof Theory*. Cambridge University Press, 2nd edition, 2000.

39 Anne S. Troelstra. *Lectures on Linear Logic*. CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.

40 Keven Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: The propositional fragment. In *Post-proceedings of TYPES 2003 Workshop*, number 3085 in LNCS, pages 355–377. Springer, 2003. doi:10.1007/978-3-540-24849-1_23.

41 Jui-Hsuan Wu. *Proof theory, syntactic representations, logic, and sharing*. PhD thesis, Institut Polytechnique de Paris, dec 2023.

42 Jui-Hsuan Wu. Proofs as terms, terms as graphs. In Chung-Kil Hur, editor, *Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings*, volume 14405 of *Lecture Notes in Computer Science*, pages 91–111. Springer, 2023. doi:10.1007/978-981-99-8311-7_5.

43 Noam Zeilberger. Focusing and higher-order abstract syntax. In George C. Necula and Philip Wadler, editors, *Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008*, pages 359–369. ACM, 2008. doi:10.1145/1328897.1328482.
**A Some omitted proofs**

We limit the $\Downarrow \mathcal{L}_2$ proofs we reason about in this appendix to single-focused proofs. This restriction does not limit the main results, which are essentially about *provability*. Dealing with the nature of, say, cut-elimination with multifocused proofs is an interesting project, but one that would only complicate the results we prove here.

**A.1 The generalized initial rule**

◀ **Theorem 9 (Admissibility of the generalized initial rule)** Let $B$ be an $\mathcal{L}_2$ $\Sigma$-formula. The sequent $\Sigma: \vdash; B \vdash B$ has a $\Downarrow \mathcal{L}_2$ proof.

**Proof.** Let $\Psi \uplus \{B\}$ be a multiset of $\mathcal{L}_2$ $\Sigma$-formulas. We describe how to build an $\Downarrow \mathcal{L}_2$ proof of $\Sigma: \Psi; B \vdash B$ by induction on the structure of the formula $B$. By Proposition 7, there is a right phase with endsequent $\Sigma: \Psi; B \vdash B$ and with one premise for every path $P$ in $B$. In particular, if the associated sequent for $P$ is $\Sigma': C_1, \dots, C_n; B_1, \dots, B_m \vdash A_1, \dots, A_p$, then the premise of the right-introduction phase that corresponds to this path is $\Sigma, \Sigma': C_1, \dots, C_n; B, B_1, \dots, B_m \vdash A_1, \dots, A_p$. We can now use the *decide*$_m$ rule to select the occurrence of $B$ in the left-bounded context. By Proposition 8, there is a left-introduction phase corresponding to $P$ such that the sequents

$$ \{\Sigma, \Sigma': \Psi, C_1, \dots, C_n; \dots \vdash C_i\}_{i=1}^n \uplus \{\Sigma, \Sigma': \Psi, C_1, \dots, C_n; B_i \vdash B\}_{i=1}^m $$

must all be provable (the $\theta$ in Proposition 8 is set to the identity substitution on the variables in $\Sigma'$). The inductive assumption proves the second group of sequents, and the first group is proved using the *decide*$_m$ rule on $C_i$. The inductive assumption completes this proof. ◀

**A.2 Proofs with cuts in $\Downarrow^{+}\mathcal{L}_2$**

Section 2 introduced two cut rules involving $\Downarrow \mathcal{L}_2$ sequents. We call those two cut rules the *regular cut rules* since we now introduce a new cut rule called the *key cut*.

$$ \frac{\begin{array}{l} \Sigma: \Psi; \Gamma_1 \vdash B, \Delta \quad \Sigma: \Psi; \Gamma_2 \Downarrow B \vdash \Delta \Downarrow \mathcal{A} \\ \Sigma: \Psi; \Gamma_1, \Gamma_2 \vdash \Delta, \mathcal{A} \end{array}}{\text{cut}_k} $$

Here, $\mathcal{A}$ is a multiset (possibly empty) of atomic formulas. The key cut is the only cut rule containing a $\Downarrow$-sequent. The formula $B$ is the *cut-formula* in this rule. To help prove the cut-elimination theorem, we extend the $\Downarrow^{+}\mathcal{L}_2$ proof system to include the key cut. A proof is *cut-free* if it has no occurrences of these three cut rules.

The cut-elimination argument uses various measurements attached to occurrences of both regular and key-cut rules. A *thread* in the $\Downarrow^{+}\mathcal{L}_2$ proof $\Xi$ is a list of sequent occurrences $S_1, \dots, S_n$ in $\Xi$ such that $n \ge 1$, $S_1$ is the conclusion of an *init* rule, $S_n$ is the endsequent of $\Xi$, and, for $i = 1, \dots, n-1$, there is an inference rule occurrence of $\Xi$ that has $S_i$ as a premise and $S_{i+1}$ as its conclusion. Such a thread is said to have length $n$.

The *rank* of $\Xi$ is the maximal number of occurrences of *decide* and *cut* rules in threads in $\Xi$ that do not contain a sequent occurrence that is the left premise of a *cut*$_l$, *cut*$_!$, or *cut*$_k$. The *degree* of a formula is the number of occurrences of logical connectives in that formula.

Every occurrence of a *cut* rule in a given proof is given a *measure* as follows. Let $\Xi$ be the subproof determined by having that occurrence of *cut* as its last inference rule. We define $|\Xi|$ to be the pair of natural numbers $\langle d, w \rangle$, where $d$ is the degree of its *cut* formula, and
$w$ is the rank of $Ξ$. Such pairs are well-ordered using the lexicographic ordering on pairs. This measure plays an important role in the termination of the cut-elimination procedure described in Appendix A.4 of [27]. The following two propositions are proved by simple inductions on the structure of $↓^+\mathcal{L}_2$ proofs.

**Proposition 20 (Weakening $↓^+\mathcal{L}_2$ proofs).** Let $\Sigma'$ be a signature disjoint from $\Sigma$, and let $\Psi'$ be a multiset of $\Sigma, \Sigma'$-formulas. If $\Sigma: \Psi; \Gamma \vdash A$ has a $↓^+\mathcal{L}_2$ proof $Ξ$ then $\Sigma, \Sigma': \Psi, \Psi'; \Gamma \vdash A$ has a $↓^+\mathcal{L}_2$ proof $Ξ'$. Furthermore, every instance of a cut rule in $Ξ$ corresponds to an instance of cut in $Ξ'$ and they have the same measure.

**Proposition 21 (Substitution into $↓^+\mathcal{L}_2$ proofs).** Let $\Sigma$ be a signature, $x$ be a variable not declared in $\Sigma$, $\tau$ be a primitive type, and $t$ be a $\Sigma$-term of type $\tau$. If $\Sigma, x : \tau : \Psi; \Gamma \vdash A$ has a $↓^+\mathcal{L}_2$ proof $Ξ$ then $\Sigma : \Psi[t/x]; \Gamma[t/x] \vdash A[t/x]$ has a $↓^+\mathcal{L}_2$ proof $Ξ'$. Furthermore, every instance of a cut rule in $Ξ$ corresponds to an instance of cut in $Ξ'$ and they have the same measure.

The following proposition states that if a formula occurrence in the unbounded zone of a sequent is never decided on within the proof of that sequent, then that occurrence can be removed from its zone. This proposition is proved by a simple induction on the structure of $↓^+\mathcal{L}_2$ proofs.

**Proposition 22 (Strengthening $↓^+\mathcal{L}_2$ proofs).** Assume that we have a $↓^+\mathcal{L}_2$ proof $Ξ$ of $\Sigma: \Psi, B; \Gamma \vdash \Delta$ (resp. $\Sigma: \Psi, B; \Gamma \llcorner D \vdash \llcorner \Delta$) in which there is no occurrence of decider $m$ applied to the formula $B$. Then there is a $↓^+\mathcal{L}_2$ proof $Ξ'$ of $\Sigma: \Psi; \Gamma \vdash \Delta$ (respectively, $\Sigma: \Psi; \Gamma \llcorner D \vdash \llcorner \Delta$). Furthermore, every instance of a cut rule in $Ξ$ corresponds to an instance of cut in $Ξ'$, and they have the same measure.

### A.3 The completeness of $(\cdot)^\circ$

For convenience, define $B^\bullet$ for positive intuitionistic formulas $B$ as follows: $f^\bullet = \top$, $(B \vee C)^\bullet = (B^\circ \Rightarrow \bot)$ & $(C^\circ \Rightarrow \bot)$, $(\exists x.B)^\bullet = \forall x.(B^\circ \Rightarrow \bot)$, $(t^+)^\bullet = \bot$, $(B \wedge C)^\bullet = B^\circ \Rightarrow C^\circ \Rightarrow \bot$. Thus, for $B$ a positive intuitionistic formula, $B^\circ$ is the same formula as $B^\bullet \dashv \bot$.

**Proposition 17 (Completeness of $(\cdot)^\circ)$** Let $B$ be a formula over the connectives in $\text{Neg} \cup \text{Pos}$. If $B^\circ$ is provable in linear logic, then $B$ is provable in the $LJT^\pm$ proof system.

**Proof.** Let $B$ be a formula over the connectives in $\text{Neg} \cup \text{Pos}$. If $B^\circ$ is provable in linear logic, then $\Sigma: \cdot; \cdot \vdash B^\circ$ has a $↓^+\mathcal{L}_2$ proof. There are a few different kinds of sequents that can appear in such a $↓^+\mathcal{L}_2$ proof, and we need to consider $↓^+\mathcal{L}_2$ proofs of sequents which are in one of the following shapes: $\Sigma: \Psi^\circ; \cdot \vdash B^\circ$ or $\Sigma: \Psi^\circ; B^\bullet \vdash \cdot$ or $\Sigma: \Psi^\circ; \llcorner B^\circ \vdash \cdot \llcorner A$ or $\Sigma: \Psi^\circ; \llcorner B^\bullet \vdash \cdot \llcorner \cdot$. Note that if the left-bounded zone is non-empty, then that zone contains one formula which is the result of $(\cdot)^\bullet$ of a positive formula, and the right zone is empty.

**Remark:** If the sequent $\Sigma: \Psi; B^\bullet \llcorner (C)^\circ \vdash \cdot \llcorner \cdot$ has a proof (when $B$ is a positive formula) then $C$ is also positive. This remark is easily proved by induction on the structure of $C$.

We can now translate $↓^+\mathcal{L}_2$ proofs of these four kinds of sequents directly into $LJT^\pm$ proofs. We proceed by induction on the structure of an $↓^+\mathcal{L}_2$ proof $Ξ$ of these kinds of sequents.

**Case:** $Ξ$ is a proof of $\Sigma: \Psi^\circ; \cdot \vdash B^\circ$. If $B$ is positive, then $Ξ$ has a subproof of $\Sigma: \Psi^\circ; B^\bullet \vdash \cdot$ the translation of that proof (see below) is the needed $LJT^\pm$ proof. If $B$ is negative, we consider the last inference rule of $Ξ$, which is either $\top R$, $\&R$, $\Rightarrow R$, or $\forall R$. In each of these cases, the translation is achieved by first translating the immediate subproof(s) and then adding the corresponding $LJT^\pm$ rules of $tR$, $\wedge R$, $\supset R$, and $\forall R$. The right introduction rules for the negative connectives arise this way.
**Case:** Ξ is a proof of Σ: Ψ°; B• ⊢ ·, where B is a positive formula. This sequent is the conclusion of a decide rule that selects either B• or a member of Ψ°. The former case is considered below. In the latter case, this is only possible (by the remark above) if the selected member C of Ψ is a positive formula. Ξ contains a subproof of the sequent Σ: Ψ°; B• ⇓ C• — ⊥ ⊢ · ⇓ · and this has a subproof of Σ: Ψ°; B• ⊢ C•. By considering all cases for the positive formula C, Ξ will contain subproofs of the shape Σ': Ψ'°; B• ⊢ ·. The translation of those subproofs and the corresponding left-introduction rules, yields the required translation.

**Case:** Ξ is a proof of Σ: Ψ°; · ⇓ B° ⊢ · ⇓ A. If B is a negative formula, then Ξ must be the right introduction rule of either ⊤, &, ⇒, or ∀. The required LJT<sup>±</sup> proof results from applying the right introduction rules for t, ∧, ∨, or ∀ to the transformations of the associated subproofs of Ξ. If B is a positive formula, then Ξ must end with

$$ \frac{\Sigma: \Psi^\circ; \vdash B^\bullet, A \\ \Sigma: \Psi^\circ; \vdash \vdash B^\bullet \vdash A \quad \Sigma: \Psi^\circ; \vdash \vdash \vdash \vdash \\ \Sigma: \Psi^\circ; \vdash B^\bullet \quad \begin{array}{l} \sim \top \vdash \vdash A \end{array}}{\quad} $$

If we now consider each case for the positive formula B, we see that invertibility will yield direct translations of the corresponding left introduction rule. For example, if B is $B_1 \lor B_2$ then the Ξ proof of Σ: Ψ°; · ⇓ ($B_1 \lor B_2$)° ⊢ · ⇓ A contains a subproof of

$$ \Sigma: \Psi^\circ; \vdash (B_1^\circ \Rightarrow \perp) \& (B_2^\circ \Rightarrow \perp), A, $$

which in turn contains subproofs of Σ: Ψ°, $B_i^\circ$; · ⊢ A, for $i \in \{1, 2\}$. The full translation uses the $\lor L$ rule of LJT<sup>±</sup>.

**Case:** Ξ is a proof of Σ: Ψ°; · ⇓ B• ⊢ · ⇓ ·. This case emulates the right introduction rule of LJT<sup>±</sup> for the positive connectives. For example, if B is $B_1 \lor B_2$ then Ξ must have the form Σ: Ψ°; · ⇓ ($B_1^\circ \Rightarrow \perp$) & ($B_2^\circ \Rightarrow \perp$) ⊢ · ⇓ · and this means that there must be a subproof of Ξ of Σ: Ψ°; · ⊢ $B_i^\circ$.

Note that the abstraction mechanism of synthetic inference rules allows hiding the internal presence of multiple-conclusion sequents even within an intuitionistic proof. ◀

## A.4 The cut-elimination theorem for ⇓ L<sub>2</sub>

We single out instances of atomic cut<sub>k</sub> rules for special treatment. Note that the right premise of an atomic cut<sub>k</sub> rule can only be proved using init, for example:

$$ \frac{\Sigma: \Psi; \Gamma \vdash \Delta, A \quad \overline{\Sigma: \Psi; \cdot \Downarrow A \vdash \cdot \Downarrow A} \quad \begin{array}{l} \text{init} \\ \text{cut}_k \end{array}}{\Sigma: \Psi; \Gamma \vdash \Delta, A} $$

This derivation can be written more simply as

$$ \frac{\Sigma: \Psi; \Gamma \vdash \Delta, A}{\Sigma: \Psi; \Gamma \vdash \Delta, A} \quad \begin{array}{l} \text{Rep.} \\ \text{cut}_k. \end{array} $$

which resembles the *repetition rule* used by Mints [32] to prove a cut-elimination theorem for a different logic. An important feature of atomic key cut rules is that their measure is always ⟨0, 1⟩ since the proof structure in their left premise is not part of the measure. Ultimately, our cut-elimination procedure will eliminate all cuts except for atomic key cuts. After those eliminations are made, a second procedure will eliminate all atomic key cuts.
A $\Downarrow^+\mathcal{L}_2$ proof is called a $\Downarrow^a\mathcal{L}_2$-proof if the only occurrences of cut rules in it are atomic key cuts. A redex is a $\Downarrow^+\mathcal{L}_2$ proof where the last inference rule is a regular or key cut and where that rule's two premises are $\Downarrow^a\mathcal{L}_2$-proofs. A redex is classified as atomic or non-atomic depending on whether the cut formula of its final cut rule is atomic or non-atomic. A redex is also classified by the kind of cut rule it has as its final rule.

It is easy to prove that the side-formulas on the right-bounded zone for the Rep rule (the schematic variable $\Delta$ above) can be restricted to contain only atomic formulas: that is, the conclusion of such rules can be assumed to be border sequents. As a result, Proposition 7 can be used to characterize additionally the right-introduction phase of $\Downarrow^a\mathcal{L}_2$-proofs.

We now provide several lemmas that show how various redexes can be replaced with proofs involving strictly smaller redexes.

**Lemma 23 (Replace cut! with cut<sub>k</sub>)**. Let $\Xi$ be a cut! redex. Then there exists a proof of the same endsequent in which the only instances of cut rules are either cut<sub>l</sub> or atomic cut<sub>k</sub>, and all such instances of cuts have a measure strictly less than $|\Xi|$.

*Proof.* Consider the following cut!-redex $\Xi$.

$$ \frac{\begin{array}{c} \Xi_l \\ \Sigma: \Psi; \vdash B \end{array} \quad \begin{array}{c} \Xi_r \\ \Sigma: \Psi, B; \Gamma \vdash \Delta \end{array}}{\Sigma: \Psi; \Gamma \vdash \Delta} \quad \text{cut!} $$

Here, the only occurrences of cut rules in the subproofs $\Xi_l$ and $\Xi_r$ are atomic key cuts. Consider a subderivation of $\Xi_r$ that ends in $decide_m$, such as

$$ \frac{\begin{array}{c} \Xi_0 \\ \Sigma, \Sigma': \Psi, \Psi', B; \Gamma \Downarrow B \vdash \Delta \end{array}}{\Sigma, \Sigma': \Psi, \Psi', B; \Gamma \vdash \Delta} \quad \text{decide}_m, $$

where the variables bound in $\Sigma'$ are not bound in $\Sigma$ and where $\Psi'$ is a multiset. This inference rule can be converted to the derivation

$$ \frac{\begin{array}{c} \hat{\Xi}_l \\ \Sigma, \Sigma': \Psi, \Psi', \vdash B \end{array} \quad \begin{array}{c} \Xi_0 \\ \Sigma, \Sigma': \Psi, \Psi', B; \Gamma \Downarrow B \vdash \Delta \end{array}}{\Sigma, \Sigma': \Psi, \Psi', B; \Gamma \vdash \Delta} \quad \text{cut}_k, $$

where $\hat{\Xi}_l$ is the result of weakening $\Xi_l$ using Proposition 20. In this way, we can remove all occurrences of $decide_m$ on $B$ in $\Xi_r$ to obtain the proof $\Xi'_r$ of $\Sigma: \Psi, B; \Gamma \vdash \Delta$. By Proposition 22, we can strengthen $\Xi'_r$ to get a proof $\Xi''_r$ of $\Sigma: \Psi; \Gamma \vdash \Delta$. This proof can now replace our original redex. Since all new occurrences of cuts have $B$ as their cut formula and since the rank part of the measure of redexes does not consider the subproof of the left premise of cut! and cut<sub>l</sub>, the measure of the cut-rules in $\Xi''_l$ is strictly smaller than $|\Xi|$. $\llap{\quad}$

The previous lemma removed a cut! by converting some $decide_m$ rules into cut<sub>k</sub> rules. The treatment of the cut<sub>l</sub> rule is not so easily handled. In particular, we will use the following lemma to show that the “side cut” case can be treated by moving a cut<sub>l</sub> rule over an entire left-introduction phase.

**Lemma 24 (Side cut<sub>l</sub> case).** Let $\Xi$ be a cut<sub>l</sub>-redex such that a decide rule is the last inference rule of the proof of the right premise. If the formula selected is not the cut formula, then there exists a $\Downarrow^+\mathcal{L}_2$ proof with the same endsequent in which all instances of cuts have a measure strictly less than $|\Xi|$.
**Proof.** The decide rule that ends the proof of the right premise must select its focus from either the bounded or unbounded zone on the left. We consider these two cases below.

**Case:** The decide rule selects from the bounded zone. Let $Ξ$ be the following proof.

$$ \frac{\Xi_l \quad \frac{\Sigma: \Psi; \Gamma', C \Downarrow B \vdash \Delta \quad \Xi_r}{\Sigma: \Psi; \Gamma' \vdash B, C \vdash A} \quad \text{decide}_m}{\Sigma: \Psi; \Gamma, \Gamma', B \vdash \Delta, A} \quad \text{cut}_l $$

Here, the only occurrences of cut rules in the subproofs $Ξ_l$ and $Ξ_r$ are atomic key cuts, and $A$ is a multiset of atomic formulas. By Proposition 8,<fnref n="1" /> the sequent $\Sigma: \Psi; \Gamma', C \Downarrow B \vdash \Delta A$ is the endsequent of a left-introduction phase with a multiset of premises $M$ such that there is a path $P$ in $B$ with the associated sequent

$$ \Sigma': C_1, \dots, C_n; B_1, \dots, B_m \vdash A_1, \dots, A_p, $$

and there is a substitution $\theta$ that maps the variables in $\Sigma'$ to $\Sigma$-terms such that

1. $A$ is equal to the multiset union $\{A_1\theta, \dots, A_p\theta\} \uplus A_1 \uplus \dots \uplus A_m$;

2. $\Gamma' \uplus \{C\}$ is the multiset union $\Gamma_1 \uplus \dots \uplus \Gamma_m$; and

3. $M$ is $\{\Sigma: \Psi; \vdash C_i\theta\}_{i=1}^n \uplus \{\Sigma: \Psi; \Gamma_i \vdash B_i\theta, A_i\}_{i=1}^m$.

Since the left-phase is multiplicative, there is a unique $k \in \{1, \dots, m\}$ such that $C$ occurs in $\Gamma_k$. Let $\Gamma'_k$ be the result of removing one occurrence of $C$ from $\Gamma_k$. Thus, one of the premises in $M$ is $\Sigma: \Psi; \Gamma'_k, C \vdash B_k\theta, A_k$. By using the $cut_l$ rule we have, together with a proof of the above sequent, the following proof.

$$ \frac{\Xi_l \quad \frac{\Sigma: \Psi; \Gamma' \vdash C, A \quad \Sigma: \Psi; \Gamma'_k, C \vdash B_k\theta, A_k}{\Sigma: \Psi; \Gamma', \Gamma'_k \vdash B_k\theta, A_k, A} \quad \text{cut}_l}{\Sigma: \Psi; \Gamma, \Gamma' \vdash \Delta, A} $$

By using the same path above, we can move this left-introduction phase below the $cut_l$ rule. Thus, the original $cut_l$ rule has been moved up, and its measure has decreased.

**Case:** The decide rule selects from the unbounded zone. Let $Ξ$ be the following proof, and assume that $B$ is a member of $\Psi$.

$$ \frac{\Xi_l \quad \frac{\Sigma: \Psi; \Gamma', C \Downarrow B \vdash \Delta \quad \Xi_r}{\Sigma: \Psi; \Gamma' \vdash B, C \vdash A} \quad \text{decide}_m}{\Sigma: \Psi; \Gamma, \Gamma' \vdash \Delta, A} \quad \text{cut}_l $$

Here, the only occurrences of cut rules in the subproofs $Ξ_l$ and $Ξ_r$ are atomic key cuts, and $A$ is a multiset of atomic formulas. This case is treated the same as the previous case. ◀

**Remark:** Let $Ξ$ be a $\Downarrow^+\mathcal{L}_2$ proof of $\Sigma: \Psi; \Gamma, B \vdash \Delta$. If $\Delta$ contains a logical connective, then this proof is of the form displayed to the right. Here, $A_i$ is a multiset of atomic formulas; $\Gamma$ is a sub-multiset of $\Gamma_i$; $\Psi$ is a sub-multiset of $\Psi_i$; all the inference rules elided here are either

$$ \frac{\Xi_i \quad \dots \quad \Sigma_i: \Psi_i; \Gamma_i, B \vdash A_i \quad \dots}{\vdots} \quad \Sigma: \Psi; \Gamma, B \vdash \Delta $$

<footnote n="1">¹ While Proposition 8 was proved for $\Downarrow^+\mathcal{L}_2$ proofs, it also holds in the presence of cut rules since no cut rule contains a $\Downarrow$ in its conclusion.</footnote>
right-introduction rules or atomic key cuts; and the last inference rule of the subproofs $\Xi_i$'s are one of the decide rules. An instance of $cut_l$ on $B$ in the endsequent can then be lifted to several instances of $cut_l$ with $\Xi_i$. This does not change the measure of any cuts. Next we resolve the cut/decide pairing as described in the following proof.

**Lemma 25** (Replace $cut_l$ with $cut_k$). Let $\Xi$ be a $cut_l$ redex. Then there exists a proof of the same endsequent in which the only instances of cut rules are $cut_k$, and all such instances of cuts have a measure strictly less than $|\Xi|$.

**Proof.** Consider the following $cut_l$-redex $\Xi$.

$$ \frac{\frac{\Xi_l}{\Sigma: \Psi; \Gamma_1 \vdash B, \Delta_1} \quad \Xi_r}{\Sigma: \Psi; \Gamma_2, B \vdash \Delta_2} \quad cut_l $$

Here, the only occurrences of cut rules in the subproofs $\Xi_l$ and $\Xi_r$ are atomic key cuts. Given the remark above, we only need to consider the situation where the right-bounded context contains only atomic formulas and that the last inference rule of $\Xi_r$ is a decide rule.

If the $decide_m$ rule selects $B$ as its focus, then the proof $\Xi_r$ has the form

$$ \frac{\Xi'_r}{\Sigma: \Psi; \Gamma'_2 \Downarrow B \vdash \Delta'_2} \quad decide_m. $$

This instance of the $cut_l$ rule above can be replaced with the following instance of $cut_k$.

$$ \frac{\frac{\Xi_l}{\Sigma: \Psi; \Gamma_1 \vdash B, \Delta_1} \quad \Xi'_r}{\Sigma: \Psi; \Gamma_2 \Downarrow B \vdash \Delta_2} \quad cut_k $$

If the formula selected for the focus is some other formula than $B$, then the proof $\Xi_r$ has the form ($\Gamma_2$ is of the form $C, \Gamma'_2$)

$$ \frac{\Xi'_r}{\Sigma: \Psi; \Gamma'_2, B \Downarrow C \vdash \Delta_2} \quad decide_m. $$

We now use Lemma 24 to construct a $\Downarrow^+\mathcal{L}_2$ proof of $\Sigma: \Psi; \Gamma'_2, C \vdash \Delta_2$ of lower rank. ◀

**Lemma 26** (Reduce $cut_k$). Let $\Xi$ be a non-atomic $cut_k$ redex. Then there exists a proof of the same endsequent in which the redexes it has are $cut_l$ and $cut_l$-redexes all with a measure strictly less than $|\Xi|$.

**Proof.** Consider a $cut_k$-redex $\Xi$ of the form

$$ \frac{\frac{\Xi_l}{\Sigma: \Psi; \Gamma_1 \vdash B, \Delta} \quad \Xi_r}{\Sigma: \Psi; \Gamma_2 \Downarrow B \vdash \Delta} \quad cut_k, $$

where $\Xi_l$ and $\Xi_r$ are $\Downarrow^a\mathcal{L}_2$ proofs. Since $B$ is not atomic, $\Xi_l$ ends in a right-introduction phase and $\Xi_r$ ends in a left-introduction phase. By Proposition 8, there is a path $P$ in $B$ that has the associated sequent representation

$$ \Sigma': C_1, \dots, C_n; B_1, \dots, B_m \vdash A_1, \dots, A_p, $$
and there is a substitution $\theta$ that maps the variables in $\Sigma'$ to $\Sigma$-terms such that $\mathcal{A}$ is the multiset union $\{A_1\theta, \dots, A_p\theta\} \cup \mathcal{A}_1 \cup \dots \cup \mathcal{A}_m$, $\Gamma$ is the multiset union $\Gamma_1 \cup \dots \cup \Gamma_m$, and this phase has $n+m$ premises $\{\Sigma: \Psi; \vdash C_i\theta\}_{i=1}^n \cup \{\Sigma: \Psi; \Gamma_i \vdash B_i\theta, \mathcal{A}_i\}_{i=1}^m$. By Proposition 7, $\Xi_l$ ends with a right-introduction phase that contains a premise of the form

$$ \Xi_0 \qquad \Sigma, \Sigma': \Psi, C_1, \dots, C_n; \Gamma, B_1, \dots, B_m \vdash \mathcal{A}', A_1, \dots, A_p. $$

By repeated application of Proposition 21, we know that the sequent

$$ \Xi'_0 \qquad \Sigma: \Psi, C_1\theta, \dots, C_n\theta; \Gamma, B_1\theta, \dots, B_m\theta \vdash \mathcal{A}', A_1\theta, \dots, A_p\theta $$

has a $\Downarrow^\mathcal{L}_2$ proof. We can take $\Xi'_0$ and use $cut_l$ and $cut$! with the proofs of the $n+m$ premises above to yield a proof with $n+m$ occurrences of these cut rules to provide a proof without occurrences of $cut_k$ of the endsequent $\Sigma: \Psi; \Gamma, \Gamma' \vdash \Delta, \mathcal{A}$. Note that the size of each of the cut formulas $C_1\theta, \dots, C_n\theta, B_1\theta, \dots, B_m\theta$ is strictly smaller than the size of the original cut formula $B$. $\quad$

We are now in a position to prove the cut-elimination theorem for $\Downarrow^\mathcal{L}_2$ proofs.

**▲ Theorem 10 (Cut elimination for $\Downarrow^\mathcal{L}_2$)** *Let $B$ be an $\mathcal{L}_2$-$\Sigma$-formula. If the sequent $\Sigma:.; \vdash B$ has a $\Downarrow^\mathcal{L}_2$ proof, then it has an $\Downarrow^\mathcal{L}_2$ proof.*

**Proof.** We divide this proof into two parts. The first part proves that if a sequent has a $\Downarrow^\mathcal{L}_2$ proof, then it has a $\Downarrow^\mathcal{L}_2$-proof. The second part proves that if a sequent has a $\Downarrow^\mathcal{L}_2$-proof then it has a (cut-free) $\Downarrow^\mathcal{L}_2$ proof.

Thus, assume that we have a $\Downarrow^\mathcal{L}_2$ proof. We proceed by induction on the number of occurrences of cut rules in that proof that are not atomic key cuts. If the number of such redexes is zero, we are finished with the first part of this proof. Otherwise, select a redex $\Xi$ that is not an atomic key cut redex. We prove by induction on the measure $|\Xi|$ that this redex can be replaced by a $\Downarrow^\mathcal{L}_2$-proof of the same endsequent. If $\Xi$ is a cut!-redex then apply Lemma 23; if $\Xi$ is a cut$_l$-redex then apply Lemma 25; and, finally, if $\Xi$ is a non-atomic cut$_k$-redex then apply Lemma 26. The results of such applications are proofs of the same endsequent as $\Xi$ in which all redexes have a measure strictly less than $|\Xi|$. Thus, by induction, all of these can be replaced by $\Downarrow^\mathcal{L}_2$-proofs.

To complete the second part of this proof, we proceed to prove by induction that if the $\Downarrow^\mathcal{L}_2$-proof $\Xi$ contains $n \ge 0$ occurrences of atomic key cuts, then there is a $\Downarrow^\mathcal{L}_2$ proof of the same endsequent. Pick any atomic key cut occurrence in $\Xi$. That occurrence resembles the Rep rule, which is trivial to remove. $\quad$

More details on proving cut-elimination for $\Downarrow^\mathcal{L}_2$ is contained in [28, Chapter 7].