# Splitting and Focusing for Full Propositional Linear Logic in the Calculus of Structures

Kaustuv Chaudhuri, Nicolas Guenot, Mikheil Rukhaia, Lutz Strassburger

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

## To cite this version:

Kaustuv Chaudhuri, Nicolas Guenot, Mikheil Rukhaia, Lutz Strassburger. Splitting and Focusing for Full Propositional Linear Logic in the Calculus of Structures. 2017. hal-05493721

HAL Id: hal-05493721

https://inria.hal.science/hal-05493721v1

Preprint submitted on 5 Feb 2026

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_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Splitting and Focusing for Full Propositional Linear Logic in the Calculus of Structures

Kaustuv Chaudhuri

Nicolas Guenot

Mikheil Rukhaia

Lutz Straßburger

May 4, 2018

## Abstract

The *calculus of structures* is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but there are two drawbacks: first, the standard techniques of proving proof normalization do not work, and second, the proof presentation is too permissive, allowing too many proofs. In this paper, we address both points for the case of linear logic. First, we give a full proof of the splitting lemma, which allows to use standard reduction steps to prove normalization, and second, we transplant the focusing theorem from the sequent calculus to the calculus of structures. For this, the key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof.

## 1 Introduction

Logic has traditionally been seen as a means of representing and systematizing mathematical knowledge, but it is increasingly being used to encode and reason about formal systems—programming languages, process calculi, transition systems, etc.—that are inherently computational. In this use of logic, the syntax of proofs is important to build correspondences between the proofs in logic and the computations of the encoded systems, also known as the problem of *representational adequacy*. An adequate encoding is not only manifestly correct, i.e., it represents all and only the computations of the encoded system, but is also useful as a device to automate the reasoning in and about the encoded system. In standard proof systems such as Gentzen's *sequent calculus*, it is usually impossible to construct adequate encodings: there are more proofs than computational traces, because the inference rules are more non-deterministic than the computational steps.

In recent years the *focusing* theorem of Andreoli [1] has been used to create certain “normal forms” of sequent proofs where the question of representational adequacy becomes considerably easier, often trivial, for focused proofs. Focusing was originally developed for (classical) linear logic but has since been extended to a wide spectrum of logics [3, 10, 17, 19]. The essential observation of focusing is that sequent rules have certain natural permutative affinities that can be exploited to fuse logical connectives into larger *synthetic connectives*; for example, the synthetic connective $-\otimes-(\oplus-)$ behaves as a ternary connective instead of as a composition of two binary connectives. The problem of representational adequacy is reduced to that of encoding the computational steps in such a way that they correspond exactly to the synthetic connectives.

This technique has been successful for the standard classical, intuitionistic, and linear logics where the sequent calculus is most natural. The sequent calculus is, however, inherently limited in its expressivity: it cannot be used to give *analytic* (i.e., cut-free) proof systems for many modal and non-commutative logics that have been used for program safety, operational semantics, or linguistics. The common feature of many of these logics is that they rely on *deep inference* or the ability to perform deduction inside a formula. Proof systems for many such logics need to generalize the sequent calculus; some popular generalizations include: hypersequents [2], nested sequents [5], or the display calculus [4]. The most permissive, and therefore most expressive, of such generalizations is the *calculus of structures* [14, 15, 6] that does not differentiate between formulas and sequents and can therefore perform deduction anywhere inside a formula. Besides the increased expressivity [15, 25], proofs in the calculus of structures can
also exploit features that are not available in the other shallower formalisms; for example, they can be exponentially smaller than sequent proofs [7], or they can be decomposed in a number of ways [24, 26].

A main distinguishing feature of the calculus of structures is that it divides the sequent rules into smaller components, thereby introducing more non-deterministic choices. The sequent calculus operates on entire (multi-)sets of formulas, with a single sequent rule able to split whole contexts multiplicatively or test for the absence of certain elements. The rules of the calculus of structures, on the other hand, perform such operations incrementally on fragments of contexts. Some of the inessential choices introduced by this incremental nature can be removed by restricting the syntactic congruence in the original formulation of the calculus [14, 15], leading to the system LS for classical propositional linear logic (outlined in Section 2), which can be seen as a variant of the original formulation in [21, 22] that is more amenable to automation. One important feature of LS is that contraction is the sole rule that makes proofs unbounded, and it permutes below all other rules (Proposition 6), a property that is crucial for the cut-elimination result for LS (also presented in Section 2.2). The contraction-free fragment of LS is therefore decidable.

There are two main contributions about LS in this paper. First, we give a full proof of the splitting lemma for LS (in Section 2.3 and Section 2.4), which is considerably simpler than the one presented in [22]. The splitting lemma is an important ingredient for an internal cult elimination proof for LS inside the calculus of structures (i.e., without translation into the sequent calculus). Recently it has been shown by Aler Tubella in [26] that splitting can be proved independently from the particular proof system, as long as the rules follow a certain pattern. Unfortunately, LS does not (yet) follow this pattern because of the presence of the exponentials ? and !. However, we hope that with the help of our work the result of Aler Tubella can eventually be generalized to include modalities.

The second main contribution of this paper is to present a focused variant of LS, that we call LSF. More precisely, we tame LS in the same way that the sequent system LLK (without cut) for linear logic (Figure 1) was tamed to produce the focused system LLKF (Figure 3). For the purely multiplicative fragment, this issue has already been investigated in [12], but the strategy there seems difficult to generalize. The system LSF for full classical propositional linear logic that we construct in this paper uses the technical device of polarized formulas [16]; polarities make the synthetic connectives manifest in the syntax, and the rules of LSF are organized to respect polarity, i.e., to never introduce a polarity change that did not already exist. Synthetic connectives are thus preserved in LSF proofs.

To show LSF complete with respect to LS in its own right, i.e., that any LS proof can be turned into an LSF proof, we build an equivalent synthetic variant of LSF called LSS (see Section 3.2). A special rule that breaks the polarity restriction is added to LSS to represent unfocused LS proofs directly, and then this rule is shown to be admissible in LSS. We thus have a simple internal proof of completeness of LSS (and hence of LSF) with respect to LS. This style of showing completeness of focusing for the calculus of structures can pave the way for focused variants of other logics that lack an analytic sequent system. Although we limit our attention to classical propositional linear logic in this paper, we consider it an important future work to extend our focusing result to logics for which focusing in terms of the sequent calculus is inapplicable. In particular, recently our techniques have been successfully employed for designing focused nested sequent systems for classical modal logics [10] and intuitionistic modal logics [11]. We hope to be able to extend our methods also to other logics that seem to require deep inference systems. This includes logics like BV [14, 25] and the logic of bunched implications [20].

In this paper, we also compare LSF and LLKF by first showing that any LLKF proof can be simulated in LSF (in Section 4.1), i.e., that LSF is powerful enough to represent focused sequent proofs. Then we also give an algorithm to extract an LLKF proof from any LSF proof that is unique up to permutations between negative rules (in Section 4.2). These two results justify the use of the adjective “focused” for LSF. Together with the completeness of LSF for LS, this result can be used to give an alternative proof of completeness of LLKF for LLK.

This paper is an extended version of [9], including full proofs of all theorems (in particular, the proof of the splitting lemma for LS) and a refined translation between the focused systems LLKF and LSF.

# 2 Linear Logic in the Calculus of Structures

## 2.1 LLK: Sequent Calculus for Linear Logic

Let us first quickly review the standard sequent calculus and the focusing theorem for classical propositional linear logic whose formulas $(A, B, ...)$ have the following grammar:

$$A, B ::= a \mid A \otimes B \mid 1 \mid A \oplus B \mid 0 \mid !A \mid \bar{a} \mid A \ominus B \mid \bot \mid A \& B \mid \top \mid ?A$$
<figure><img src="image_3.png" /><figcaption>Figure 1: LLK: a one-sided single-zoned sequent calculus for classical propositional linear logic</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 2: SLS, a symmetric calculus of structures for classical propositional linear logic. The fragment containing the first four rows is called LS.</figcaption></figure>

The atoms $(a, b, \dots)$ are drawn from some countably infinite set. Formulas are in negation normal form, with the negation of $a$ written as $\bar{a}$, and negation of formulas $(-)^{\perp}$ as follows:

$$ (a)^{\perp} = \bar{a} \quad (A \otimes B)^{\perp} = (A)^{\perp} \otimes (B)^{\perp} \quad (1)^{\perp} = \perp \quad (A \oplus B)^{\perp} = (A)^{\perp} \& (B)^{\perp} \quad (0)^{\perp} = \top \quad (!A)^{\perp} = ?(A)^{\perp} \\ (\bar{a})^{\perp} = a \quad (A \otimes B)^{\perp} = (A)^{\perp} \otimes (B)^{\perp} \quad (\perp)^{\perp} = 1 \quad (A \& B)^{\perp} = (A)^{\perp} \oplus (B)^{\perp} \quad (\top)^{\perp} = 0 \quad (?A)^{\perp} = ! (A)^{\perp} $$

The standard sequent calculus for linear logic, called LLK and shown in Figure 1, is given in terms of one-sided single-zoned sequents of the form $\vdash \Gamma$ where $\Gamma$ is a context (a multi-set of formulas).

**Theorem 1** (cut elimination). *The cut rule is admissible in LLK \ {cut}. □*

## 2.2 SLS: Calculus of Structures for Linear Logic

The calculus of structures is based on the observation that the connectives of linear logic preserve logical entailment, and therefore, any valid implication in the logic can be turned into a rewrite step on any subformula. Hence, there is no need to maintain a distinction between the connectives used in formulas, and structural meta-connectives such as the comma used to write sequents, or the meta conjunction among the premises of a binary rule. The original formulations of the calculus of structures [14, 15, 6] used structures, which are formulas modulo a syntactic congruence. We deviate from this tradition and
use just the formulas, i.e., we remove the syntactic congruence. Then, inference rules are allowed to operate on any subformula. These rules are therefore written in terms of formula contexts (ξ, ζ, ...), which are formulas with a single hole (written {}), i.e., they have the following grammar:

$$ \xi, \zeta ::= \{ } | A \star \xi | \xi \star A | !\xi | ?\xi \qquad (\text{Formula Contexts}) $$

where $\star$ can stand for any binary connective ($\otimes$, $\oplus$, $\ominus$, or $\&$). We write $\xi\{A\}$ for the formula formed by replacing the single occurrence of {} in $\xi$ with the formula A. For example, if $\xi$ is !($a \& (\{ } \otimes b)$) $\ominus$ ?c and A is $\bar{a} \oplus b$, then $\xi\{A\}$ is !($a \& ((\bar{a} \oplus b) \otimes b)$) $\ominus$ ?c.

A derivation $\mathcal{D}$ in a system S with premise A and conclusion B is a rewriting path from A to B, using the rules in S. It is usually depicted as $s \parallel_{\mathcal{D}}$. A proof $\mathcal{P}$ in a system S, depicted as $s \parallel_{B}^{\mathcal{P}}$, is a derivation in S with premise 1.

The inference rules of the system SLS, which is a symmetric calculus of structures presentation of classical linear logic, are given in Figure 2. The first two columns constitute the multiplicative fragment, the next two columns the exponential fragment, and the last two columns the additive fragment. The multiplicative and exponential fragment constitute system SELS, which is a variant of the system studied in [23]. The first four rows in Figure 2 constitute the down fragment of SLS, denoted by SLS↓, and the last four rows the up fragment, denoted by SLS↑. The down fragment corresponds to the cut-free version of the system, and following the tradition, we will call it LS. Each rule in either fragment is the dual of some rule in the other fragment, where the duals of a rule are formed by exchanging the premise and conclusion and negating both. Note that the two rules sl and sr (read switch left and switch right) are self-dual and therefore part of both fragments.<fnref n="1" /> The rules $ai_↓$ and $ai_↑$, called atomic identity and atomic cut, have the following general versions:

$$ i_{\downarrow} \frac{\xi\{1\}}{\xi\{A \ominus (A)^{\perp}\}} \qquad i_{\uparrow} \frac{\xi\{(A)^{\perp} \otimes A\}}{\xi\{\perp\}} $$

Like in the sequent calculus, the general identity rule is derivable. By duality the same is true for the general cut rule. We have the following proposition, which is standard for systems in the calculus of structures (see. e.g., [21]).

**Proposition 2.** *The rule $i_{\downarrow}$ is derivable in SLS↓, and the rule $i_{\uparrow}$ is derivable in SLS↑. Furthermore, every rule in SLS↑ is derivable in SLS↓ + $i_{\uparrow}$, and dually, every rule in SLS↓ is derivable in SLS↑ + $i_{\downarrow}$. □*

By an easy induction on the size of the proofs, one can show the following implications, expressing the relation to the sequent calculus.

**Proposition 3.** *A formula A is provable in LLK with cut if and only if it is provable in SLS. And if A is provable in LLK without cut, then it is provable in LS. □*

We can now use Theorem 1 to show that provability in SLS implies provability in LS and that provability in LS, implies provability in LLK without cut. The proof is standard for systems in the calculus of structures that have a corresponding sequent calculus, e.g., [6, 21, 23, 13].

**Theorem 4** (cut elimination). *If a formula A is provable in SLS then it is provable in LS. □*

**Corollary 5.** *The rule $i_{\uparrow}$ is admissible for LS. □*

The proof given in [21] for Theorem 4 relies on the sequent calculus and Theorem 1. In the following, we present a proof that is internal to SLS, i.e., not using the sequent calculus. First, observe that in any derivation $\mathcal{D}$ in LS, all the instances of the contraction rule can be permuted to the bottom. This can be shown by an easy inductive argument.

**Proposition 6.** *For every derivation $\mathcal{L}_S \parallel_{\mathcal{D}}$ there is a formula $B'$ such that $\mathcal{L}_S\{\text{ct}_\downarrow\} \parallel_{\mathcal{D}'}$ and $\text{ct}_\downarrow \parallel_{\mathcal{D}''}$. □*

<footnote n="1">¹Note that our system SLS is slightly different from the presentation in [21, 22]. The reason for the differences is that we get stronger results (e.g., the down fragment does not need associativity for $\otimes$, $\oplus$, and $\&$), their proofs become simpler, and the relation to the focused systems is more evident.</footnote>
## 2.3 Splitting

For the internal cut-elimination proof of SLS, we will use a technique called splitting, first used in [14]. The central ingredients are Lemmas 8 – 10 and Lemma 13 below. Lemmas 8 – 10 say how the connectives behave in a shallow context, and Lemma 13 says how a general deep context can be reduced to a shallow one. For formally stating these lemmas, we need the notions of linear killing context and killing context, denoted by $\lambda\langle\rangle$ and $\kappa\langle\rangle$, respectively, and generated by this grammar:

$$ \lambda ::= \top | \{ \} | \lambda \& \lambda | \lambda \otimes 1 | 1 \otimes \lambda \qquad (\text{Linear Killing Contexts}) $$

$$ \kappa ::= 1 | \top | \{ \} | \kappa \& \kappa | \kappa \otimes 1 | 1 \otimes \kappa | !\kappa \qquad (\text{Killing Contexts}) $$

We write $\lambda\langle\rangle^n$ (resp. $\kappa\langle\rangle^n$) to indicate that there are exactly $n$ occurrences of $\{ \}$. Then, we write $\lambda\langle A_1, \dots, A_n \rangle$ (resp. $\kappa\langle A_1, \dots, A_n \rangle$) for the formula obtained from $\lambda\langle\rangle^n$ (resp. $\kappa\langle\rangle^n$) by replacing, from left to right, the $n$ occurrences of $\{ \}$ by the formulas $A_1, \dots, A_n$. The two main properties of killing contexts are summarized in the following lemma. From now on we assume that $L \in \{\text{LS}, \text{LS} \setminus \{\text{ct}_\downarrow\}\}$.

**Lemma 7.** Let $A, B_1, \dots, B_n$, and $\lambda\langle\rangle^n$ and $\kappa\langle\rangle^n$ be given.

1. If $B_1, \dots, B_n$ are provable in $L$, then so are $\lambda\langle B_1, \dots, B_n \rangle$ and $\kappa\langle B_1, \dots, B_n \rangle$.

2. There are derivations
$$ \begin{array}{ccc} \lambda\langle A \succ B_1, \dots, A \succ B_n \rangle & & \kappa\langle?A \succ B_1, \dots, ?A \succ B_n \rangle \\ \mathbf{L}\parallel\parallel_{\mathcal{D}_\lambda} & \text{and} & \mathbf{L}\parallel\parallel_{\mathcal{D}_\kappa} \\ A \succ \lambda\langle B_1, \dots, B_n \rangle & & ?A \succ \kappa\langle B_1, \dots, B_n \rangle \end{array} $$

*Proof.* The first statement follows by using the rules $!\downarrow$, $\&\downarrow$, $\top\downarrow$, and $\otimes\downarrow$. For the second statement, $\mathcal{D}_\lambda$ is obtained using the rules $gc_\downarrow$, $com_\downarrow$, $asc_\downarrow$, $sl$, $sr$ and $dt_\downarrow$; and $\mathcal{D}_\kappa$ is obtained additionally using the rules $\top\downarrow$, $?\downarrow$ and $pr_\downarrow$. $\square$

We can now state the splitting lemmas.

**Lemma 8 (binary splitting).** Let $A, B$, and $K$ be formulas.

1. If $(A \& B) \succ K$ is provable in $L$, then so are $A \succ K$ and $B \succ K$.

2. If $(A \oplus B) \succ K$ is provable in $L$, then there is an $n \ge 0$ and $K_1, \dots, K_n$ and $\lambda\langle\rangle^n$, such that

$$ \lambda\langle K_1, \dots, K_n \rangle \qquad \mathbf{L}\parallel\parallel_K \qquad \text{and} \qquad \text{for all } i \le n \text{ we have } \mathbf{L}\parallel\parallel_{A \succ K_i} \text{ or } \mathbf{L}\parallel\parallel_{B \succ K_i} . $$

3. If $(A \otimes B) \succ K$ is provable in $L$, then there are $n \ge 0$ and $K_{A1}, K_{B1}, \dots, K_{An}, K_{Bn}$ and $\lambda\langle\rangle^n$, such that

$$ \lambda\langle K_{A1} \succ K_{B1}, \dots, K_{An} \succ K_{Bn} \rangle \qquad \mathbf{L}\parallel\parallel_K \qquad \text{and} \qquad \text{for all } i \le n \text{ we have } \mathbf{L}\parallel\parallel_{A \succ K_{Ai}} \text{ and } \mathbf{L}\parallel\parallel_{B \succ K_{Bi}} . $$

*Proof.* We proceed by induction on the length of the proof and on the size of the conclusion. For simplicity, we consider commutativity and associativity of the $\succ$ connective and do not use the $com_\downarrow$ and $asc_\downarrow$ rules explicitly. We make a case analysis on the bottommost rule applied in the given derivation.

1. Assume $(A \& B) \succ K$ is provable in $L$. There are three cases to consider:

(a) The last rule $r$ is applied inside $A, B$ or $K$. If it is applied inside $K$ then we have

$$ r \frac{\mathbf{L}\parallel\parallel_{\mathcal{D}_A}}{(A \& B) \succ K'} \qquad \text{from which we get} \qquad r \frac{\mathbf{L}\parallel\parallel_{\mathcal{D}_B}}{A \succ K'} \qquad \text{and} \qquad r \frac{\mathbf{L}\parallel\parallel_{\mathcal{D}_B}}{B \succ K'} $$

where $\mathcal{D}_A$ and $\mathcal{D}_B$ exist by induction hypothesis. The other cases, when $r$ is applied inside $A$ or $B$ are similar: on the last step $r$ is applied to the proof of $A' \succ K$ or $B' \succ K$ respectively.

(b) The last rule $r$ operates on a subformula containing $A \& B$. We distinguish between the following cases:
i. $r = sl$ and $K = K_1 \oslash (K_2 \otimes K_3) \oslash K_4$, i.e.

$$sl \frac{\mathfrak{l}\mathfrak{l}}{((A \oplus B) \oslash K_1 \oslash K_2) \otimes K_3) \oslash K_4} \frac{(A \oplus B) \oslash K_1 \oslash (K_2 \otimes K_3) \oslash K_4}{(A \oplus B) \oslash K_1 \oslash (K_2 \otimes K_3) \oslash K_4}$$

By induction hypothesis there are $n \ge 0$ and $G_{11}, G_{21}, \dots, G_{1n}, G_{2n}$ and $\lambda\langle \rangle^n$, such that

$$\lambda\langle G_{11} \oslash G_{21}, \dots, G_{1n} \oslash G_{2n} \rangle \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_4} \quad \text{and} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{AB}} \quad \text{and} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_3} \quad (A \oplus B) \oslash K_1 \oslash K_2 \oslash G_{1i} \quad \text{and} \quad K_3 \oslash G_{2i}$$

for all $i \le n$. Applying induction hypothesis to $\mathcal{D}_{AB}$ gives us

$$A \oslash K_1 \oslash K_2 \oslash G_{1i} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_A} \quad \text{and} \quad B \oslash K_1 \oslash K_2 \oslash G_{1i} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_B}$$

Now we can build:

$$\begin{array}{ccc}
\otimes_{\downarrow} \frac{1}{1 \otimes 1} & & \otimes_{\downarrow} \frac{1}{1 \otimes 1} \\
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_A} & & \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_B} \\
(A \oslash K_1 \oslash K_2 \oslash G_{1i}) \otimes 1 & \text{and} & (B \oslash K_1 \oslash K_2 \oslash G_{1i}) \otimes 1 \\
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_3} & & \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_3} \\
\text{sl, sr} \frac{(A \oslash K_1 \oslash K_2 \oslash G_{1i}) \otimes (K_3 \oslash G_{2i})}{A \oslash K_1 \oslash (K_2 \otimes K_3) \oslash G_{1i} \oslash G_{2i}} & & \text{sl, sr} \frac{(B \oslash K_1 \oslash K_2 \oslash G_{1i}) \otimes (K_3 \oslash G_{2i})}{B \oslash K_1 \oslash (K_2 \otimes K_3) \oslash G_{1i} \oslash G_{2i}}
\end{array}$$

from which we can form

$$\begin{array}{l}
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_0} \\
\lambda\langle A \oslash K_1 \oslash (K_2 \otimes K_3) \oslash G_{11} \oslash G_{21}, \dots, A \oslash K_1 \oslash (K_2 \otimes K_3) \oslash G_{1n} \oslash G_{2n} \rangle \\
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_1} \\
A \oslash K_1 \oslash (K_2 \otimes K_3) \oslash \lambda\langle G_{11} \oslash G_{21}, \dots, G_{1n} \oslash G_{2n} \rangle \\
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_4} \\
A \oslash K_1 \oslash (K_2 \otimes K_3) \oslash K_4
\end{array}$$

where $\mathcal{D}_0, \mathcal{D}_1$ exists by Lemma 7. The proof of $B \oslash K_1 \oslash (K_2 \otimes K_3) \oslash K_4$ is formed analogously.

The case for $r = sr$ is symmetric.

ii. $r = dt_{\downarrow}$ and $K = K_1 \oslash (K_2 \oplus K_3) \oslash K_4$, i.e.

$$dt_{\downarrow} \frac{\mathfrak{l}\mathfrak{l}}{((A \oplus B) \oslash K_1 \oslash K_2) \oplus ((A \oplus B) \oslash K_1 \oslash K_3)) \oslash K_4} \frac{(A \oplus B) \oslash K_1 \oslash (K_2 \oplus K_3) \oslash K_4}{(A \oplus B) \oslash K_1 \oslash (K_2 \oplus K_3) \oslash K_4}$$

By induction hypothesis there are

$$\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_2} \quad \text{and} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_3} \\
(A \oplus B) \oslash K_1 \oslash K_2 \oslash K_4 \quad (A \oplus B) \oslash K_1 \oslash K_3 \oslash K_4$$

Applying the induction hypothesis again to $\mathcal{D}_2$ and $\mathcal{D}_3$ gives us

$$\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{2A}} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{2B}} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{3A}} \quad \mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{3B}} \\
A \oslash K_1 \oslash K_2 \oslash K_4 \quad B \oslash K_1 \oslash K_2 \oslash K_4 \quad A \oslash K_1 \oslash K_3 \oslash K_4 \quad B \oslash K_1 \oslash K_3 \oslash K_4$$

From this we can get

$$\begin{array}{l}
\&_{\downarrow} \frac{1}{1 \& 1} \\
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{2A}} \\
(A \oslash K_1 \oslash K_2 \oslash K_4) \& 1 \\
\mathfrak{l}\mathfrak{l}\mathfrak{l}_{\mathcal{D}_{3A}} \\
\frac{(A \oslash K_1 \oslash K_2 \oslash K_4) \& (A \oslash K_1 \oslash K_3 \oslash K_4)}{A \oslash K_1 \oslash (K_2 \oplus K_3) \oslash K_4}
\end{array}$$

Analogously we get a proof for $B \oslash K_1 \oslash (K_2 \oplus K_3) \oslash K_4$.
(c) The last rule $r$ decomposes the subformula $A \& B$. There is only one case to consider, namely $r = dt_{\downarrow}$ and $K = K_1 \succ K_2$, i.e.,

$$ \frac{\mathfrak{l} \parallel ((A \succ K_1) \& (B \succ K_1)) \succ K_2}{(A \& B) \succ K_1 \succ K_2} $$

Then immediately by induction hypothesis we get proofs for $A \succ K_1 \succ K_2$ and $B \succ K_1 \succ K_2$.

2. Assume $(A \oplus B) \succ K$ is provable in $L$. There are three cases to consider:

(a) The last rule $r$ is applied inside $A, B$ or $K$. Similar to (1a).

(b) The last rule $r$ operates on a subformula containing $A \oplus B$. We distinguish between the following cases:

i. $r = sl$ and $K = K_1 \succ (K_2 \otimes K_3) \succ K_4$, i.e.

$$ \frac{\mathfrak{l} \parallel ((((A \oplus B) \succ K_1 \succ K_2) \otimes K_3) \succ K_4)}{(A \oplus B) \succ K_1 \succ (K_2 \otimes K_3) \succ K_4} $$

By induction hypothesis there are $m \ge 0$ and $G_{11}, G_{21}, \dots, G_{1m}, G_{2m}$ and $\lambda' \langle \rangle^m$, such that

$$ \frac{\lambda' \langle G_{11} \succ G_{21}, \dots, G_{1m} \succ G_{2m} \rangle}{\mathfrak{l} \parallel_{\mathcal{D}_4} K_4} \quad \text{and} \quad \frac{\mathfrak{l} \parallel_{\mathcal{D}_{AB_i}} (A \oplus B) \succ K_1 \succ K_2 \succ G_{1i}}{K_4} \quad \text{and} \quad \frac{\mathfrak{l} \parallel_{\mathcal{D}_{2i}} K_3 \succ G_{2i}}{K_3} $$

for all $i \le m$. Applying induction hypothesis to $\mathcal{D}_{AB_i}$ gives us that there are $m_i \ge 0$ and $G_{1i1}, \dots, G_{1im_i}$ and $\lambda_i \langle \rangle^{m_i}$, such that

$$ \frac{\lambda_i \langle G_{1i1}, \dots, G_{1im_i} \rangle}{\mathfrak{l} \parallel_{\mathcal{D}_{1i}} K_1 \succ K_2 \succ G_{1i}} \quad \text{and for all } j_i \le m_i \text{ we have either } \frac{\mathfrak{l} \parallel_{A \succ G_{1ij_i}}}{A \succ G_{1ij_i}} \text{ or } \frac{\mathfrak{l} \parallel_{B \succ G_{1ij_i}}}{B \succ G_{1ij_i}}. $$

Now take $n = m_1 + \dots + m_m$ and $\lambda \langle \rangle^n = \lambda' \langle \lambda_1 \langle \rangle^{m_1} \otimes 1, \dots, \lambda_m \langle \rangle^{m_m} \otimes 1 \rangle$, from which we can get

$$ \frac{\lambda \langle G_{111}, \dots, G_{11m_1}, \dots, G_{1mm_m} \rangle}{\mathfrak{l} \parallel_{\mathcal{D}_{11}, \dots, \mathcal{D}_{1m}} \lambda' \langle (K_1 \succ K_2 \succ G_{11}) \otimes 1, \dots, (K_1 \succ K_2 \succ G_{1m}) \otimes 1 \rangle} \frac{\lambda' \langle (K_1 \succ K_2 \succ G_{11}) \otimes (K_3 \succ G_{21}), \dots, (K_1 \succ K_2 \succ G_{1m}) \otimes (K_3 \succ G_{2m}) \rangle}{\mathfrak{l} \parallel_{\mathcal{D}_{21}, \dots, \mathcal{D}_{2m}} \lambda' \langle K_1 \succ (K_2 \otimes K_3) \succ G_{11} \succ G_{21}, \dots, K_1 \succ (K_2 \otimes K_3) \succ G_{1m} \succ G_{2m} \rangle} \frac{\mathfrak{l} \parallel_{\mathcal{D}_0} K_1 \succ (K_2 \otimes K_3) \succ \lambda' \langle G_{11} \succ G_{21}, \dots, G_{1m} \succ G_{2m} \rangle}{\mathfrak{l} \parallel_{\mathcal{D}_4} K_1 \succ (K_2 \otimes K_3) \succ K_4} $$

where $\mathcal{D}_0$ exists by Lemma 7.

The case for $r = sr$ is symmetric.

ii. $r = dt_{\downarrow}$ and $K = K_1 \succ (K_2 \& K_3) \succ K_4$, i.e.

$$ \frac{\mathfrak{l} \parallel ((((A \oplus B) \succ K_1 \succ K_2) \& ((A \oplus B) \succ K_1 \succ K_3)) \succ K_4)}{(A \oplus B) \succ K_1 \succ (K_2 \& K_3) \succ K_4} $$

By induction hypothesis there are

$$ \frac{\mathfrak{l} \parallel_{\mathcal{D}_2}}{(A \oplus B) \succ K_1 \succ K_2 \succ K_4} \quad \text{and} \quad \frac{\mathfrak{l} \parallel_{\mathcal{D}_3}}{(A \oplus B) \succ K_1 \succ K_3 \succ K_4}. $$
Applying induction hypothesis again to $\mathcal{D}_2$ and $\mathcal{D}_3$ gives us that there are $m_1, m_2 \ge 0$ and $G_{11}, \dots, G_{1m_1}, G_{21}, \dots, G_{2m_2}$ and $\lambda_1(\rangle^{m_1}, \lambda_2(\rangle^{m_2})$, such that

$$ \lambda_1 \langle G_{11}, \dots, G_{1m_1} \rangle \\ \mathbf{L} \|_{\mathcal{D}_{K_2}} \quad \text{and} \quad \lambda_2 \langle G_{21}, \dots, G_{2m_2} \rangle \\ K_1 \succ K_2 \succ K_4 \\ \mathbf{L} \|_{\mathcal{D}_{K_3}} \quad \text{and} \quad K_1 \succ K_3 \succ K_4 $$

and for all $i \le m_1, j \le m_2$ we have

$$ \mathbf{L} \|_{A \succ G_{1i}} \quad \text{or} \quad \mathbf{L} \|_{B \succ G_{1i}} \quad \text{and} \quad \mathbf{L} \|_{A \succ G_{2j}} \quad \text{or} \quad \mathbf{L} \|_{B \succ G_{2j}} $$

Now take $n = m_1 + m_2$ and $\lambda(\rangle^n = \lambda_1(\rangle^{m_1} \& \lambda_2(\rangle^{m_2})$, from which we can get

$$ \lambda \langle G_{11}, \dots, G_{1m_1}, G_{21}, \dots, G_{2m_2} \rangle \\ \mathbf{L} \|_{\mathcal{D}_{K_2}, \mathcal{D}_{K_3}} \\ \frac{\mathrm{d}t_{\downarrow} \frac{(K_1 \succ K_2 \succ K_4) \& (K_1 \succ K_3 \succ K_4)}{K_1 \succ (K_2 \& K_3) \succ K_4}}{K_1 \succ (K_2 \& K_3) \succ K_4} $$

(c) The last rule $r$ decomposes the subformula $A \oplus B$. There are two cases to consider. Assume $r = \oplus \downarrow$, i.e.

$$ \mathbf{L} \| \\ \oplus \downarrow \frac{A \succ K}{(A \oplus B) \succ K} $$

Then take $n = 1$, $\lambda(\rangle^n = \{\} \text{ and } K_1 = K$.

The case for $r = \oplus \downarrow$ is similar.

3. Assume $(A \otimes B) \succ K$ is provable in $L$. There are three cases to consider:

(a) The last rule $r$ is applied inside $A, B$ or $K$. Similar to (1a).

(b) The last rule $r$ operates on a subformula containing $A \otimes B$. We distinguish between the following cases:

i. $r = \mathbf{sl}$ and $K = K_1 \succ (K_2 \otimes K_3) \succ K_4$, i.e.

$$ \mathbf{sl} \| \frac{((A \otimes B) \succ K_1 \succ K_2) \otimes K_3) \succ K_4}{(A \otimes B) \succ K_1 \succ (K_2 \otimes K_3) \succ K_4} $$

By induction hypothesis there are $m \ge 0$ and $G_{11}, G_{21}, \dots, G_{1m}, G_{2m}$ and $\lambda'(\rangle^m)$, such that

$$ \lambda' \langle G_{11} \succ G_{21}, \dots, G_{1m} \succ G_{2m} \rangle \\ \mathbf{L} \|_{\mathcal{D}_4} \quad \text{and} \quad (A \otimes B) \succ K_1 \succ K_2 \succ G_{1i} \quad \text{and} \quad \mathbf{L} \|_{\mathcal{D}_{2i}} \quad \text{and} \quad K_3 \succ G_{2i} $$

for all $i \le m$. Applying induction hypothesis to $\mathcal{D}_{ABi}$ gives us that there are $m_i \ge 0$ and $G_{1iA1}, G_{1iB1}, \dots, G_{1iAm_i}, G_{1iBm_i}$ and $\lambda_i(\rangle^{m_i})$, such that

$$ \lambda_i \langle G_{1iA1} \succ G_{1iB1}, \dots, G_{1iAm_i} \succ G_{1iBm_i} \rangle \\ \mathbf{L} \|_{\mathcal{D}_{1i}} \quad \text{and} \quad \mathbf{L} \|_{A \succ G_{1iAj_i}} \quad \text{and} \quad \mathbf{L} \|_{B \succ G_{1iBj_i}} $$

for all $j_i \le m_i$. Now take $n = m_1 + \dots + m_m$ and $\lambda(\rangle^n = \lambda'(\lambda_1(\rangle^{m_1} \otimes 1, \dots, \lambda_m(\rangle^{m_m} \otimes 1))$, from which we can get

$$ \lambda \langle G_{11A1} \succ G_{11B1}, \dots, G_{11Am_1} \succ G_{11Bm_1}, \dots, G_{1mAm_m} \succ G_{1mBm_m} \rangle \\ \mathbf{L} \|_{\mathcal{D}_{11}, \dots, \mathcal{D}_{1m}} \\ \lambda' \langle (K_1 \succ K_2 \succ G_{11}) \otimes 1, \dots, (K_1 \succ K_2 \succ G_{1m}) \otimes 1 \rangle \\ \mathbf{L} \|_{\mathcal{D}_{21}, \dots, \mathcal{D}_{2m}} \\ \frac{\lambda' \langle (K_1 \succ K_2 \succ G_{11}) \otimes (K_3 \succ G_{21}), \dots, (K_1 \succ K_2 \succ G_{1m}) \otimes (K_3 \succ G_{2m}) \rangle}{\lambda' \langle K_1 \succ (K_2 \otimes K_3) \succ G_{11} \succ G_{21}, \dots, K_1 \succ (K_2 \otimes K_3) \succ G_{1m} \succ G_{2m} \rangle} \\ \mathbf{L} \|_{\mathcal{D}_0} \\ K_1 \succ (K_2 \otimes K_3) \succ \lambda' \langle G_{11} \succ G_{21}, \dots, G_{1m} \succ G_{2m} \rangle \\ \mathbf{L} \|_{\mathcal{D}_4} \\ K_1 \succ (K_2 \otimes K_3) \succ K_4 $$
where $\mathcal{D}_0$ exists by Lemma 7.

The case for $r = sr$ is symmetric.

ii. $r = dt_↓$ and $K = K_1 \succ (K_2 \& K_3) \succ K_4$, i.e.

$$dt_↓ \frac{\mathbf{L} \Vert}{((A \otimes B) \succ K_1 \succ K_2) \& ((A \otimes B) \succ K_1 \succ K_3) \succ K_4}$$

By induction hypothesis there are

$$\mathbf{L} \Vert_{\mathcal{D}_2} \quad \text{and} \quad \mathbf{L} \Vert_{\mathcal{D}_3}$$

Applying induction hypothesis again to $\mathcal{D}_2$ and $\mathcal{D}_3$ gives us that there are $m_1, m_2 \ge 0$ and $G_{A1}, G_{B1}, \dots, G_{A_{m_1}}, G_{B_{m_1}}, G'_{A1}, G'_{B1}, \dots, G'_{A_{m_2}}, G'_{B_{m_2}}$ and $\lambda_1(\rangle^{m_1}, \lambda_2(\rangle^{m_2})$, such that

$$\lambda_1 \langle G_{A1} \succ G_{B1}, \dots, G_{A_{m_1}} \succ G_{B_{m_2}} \rangle \quad \text{and} \quad \lambda_2 \langle G'_{A1} \succ G'_{B1}, \dots, G'_{A_{m_2}} \succ G'_{B_{m_2}} \rangle$$

and for all $i \le m_1, j \le m_2$ we have

$$\mathbf{L} \Vert \quad A \succ G_{Ai}, \quad \mathbf{L} \Vert \quad B \succ G_{Bi}, \quad \mathbf{L} \Vert \quad A \succ G'_{Aj}, \quad \mathbf{L} \Vert \quad B \succ G'_{Bj}$$

Now take $n = m_1 + m_2$ and $\lambda(\rangle^n = \lambda_1(\rangle^{m_1} \& \lambda_2(\rangle^{m_2})$, from which we can get

$$\lambda \langle G_{A1} \succ G_{B1}, \dots, G_{A_{m_1}} \succ G_{B_{m_1}}, G'_{A1} \succ G'_{B1}, \dots, G'_{A_{m_2}} \succ G'_{B_{m_2}} \rangle \quad \mathbf{L} \Vert_{\mathcal{D}_{K_2}, \mathcal{D}_{K_3}} \quad dt_↓ \frac{(K_1 \succ K_2 \succ K_4) \& (K_1 \succ K_3 \succ K_4)}{K_1 \succ (K_2 \& K_3) \succ K_4}$$

(c) The last rule $r$ decomposes the subformula $A \otimes B$. There are two cases to consider. First, assume $r = sl$ and $K = K_1 \succ K_2$, i.e.

$$sl \frac{\mathbf{L} \Vert}{((A \succ K_1) \otimes B) \succ K_2}$$

By induction hypothesis there are $n \ge 0$ and $G_{11}, G_{21}, \dots, G_{1n}, G_{2n}$ and $\lambda(\rangle^n$, such that

$$\lambda \langle G_{11} \succ G_{21}, \dots, G_{1n} \succ G_{2n} \rangle \quad \mathbf{L} \Vert_{\mathcal{D}} \quad \text{and} \quad A \succ K_1 \succ G_{1i} \quad \text{and} \quad \mathbf{L} \Vert_{\mathcal{D}} \quad B \succ G_{2i}$$

for all $i \le n$. From this we can get

$$\lambda \langle K_1 \succ G_{11} \succ G_{21}, \dots, K_1 \succ G_{1n} \succ G_{2n} \rangle \quad \mathbf{L} \Vert_{\mathcal{D}_0} \quad K_1 \succ \lambda \langle G_{11} \succ G_{21}, \dots, G_{1n} \succ G_{2n} \rangle \quad \mathbf{L} \Vert_{\mathcal{D}} \quad K_1 \succ K_2$$

where $\mathcal{D}_0$ exists by Lemma 7.

The second case, for $r = sr$ is symmetric.

□

**Lemma 9 (nullary splitting).** Let $x$ be an atom or a negated atom, and let $K$ be a formula.

$$\lambda \langle x^{\perp}, \dots, x^{\perp} \rangle$$
5. If $1 \nmid K$ is provable in $L$, then there is a $\lambda(\ )^n$ and a derivation $\lambda(\perp, \dots, \perp) \overset{\mathcal{L}}{\parallel} K$.

6. If $\perp \nmid K$ is provable in $L$, then so is $K$.

7. If $0 \nmid K$ is provable in $L$, then there is a $\lambda(\ )^n$ and a derivation $\lambda(\top, \dots, \top) \overset{\mathcal{L}}{\parallel} K$.

*Proof.* We proceed analogously to the proof of Lemma 8.

4. Assume $K \nmid \mathfrak{A}$ is provable in $L$. There are three cases to consider:

(a) The last rule $r$ is applied inside $K$. Similar to (1a).

(b) The last rule $r$ operates on a subformula containing $x$. We distinguish between the following cases:

i. $r = sl$ and $K = K_1 \nmid (K_2 \nmid K_3) \nmid K_4$, i.e.

$$sl \overset{\mathcal{L}\parallel}{\frac{((x \nmid K_1 \nmid K_2) \nmid K_3) \nmid K_4}{x \nmid K_1 \nmid (K_2 \nmid K_3) \nmid K_4}}$$

By Lemma 8 there are $m \ge 0$ and $G_{11}, G_{21}, \dots, G_{1m}, G_{2m}$ and $\lambda(\ )^m$, such that

$$\lambda'(G_{11} \nmid G_{21}, \dots, G_{1m} \nmid G_{2m}) \overset{\mathcal{L}\parallel\mathcal{D}_4}{\underset{K_4}{\lambda(\ )^m}} \text{ and } x \nmid K_1 \nmid K_2 \nmid G_{1i} \text{ and } \overset{\mathcal{L}\parallel\mathcal{D}_{2i}}{\underset{K_3}{\lambda(\ )^m}} \nmid G_{2i}$$

for all $i \le m$. Applying induction hypothesis to $\mathcal{D}_{xi}$ gives us that there are $m_i \ge 0$ and $\lambda_i(\ )^{m_i}$, such that

$$\lambda_i(x^{\perp}, \dots, x^{\perp}) \overset{\mathcal{L}\parallel\mathcal{D}_{1i}}{=} K_1 \nmid K_2 \nmid G_{1i}$$

Now take $n = m_1 + \dots + m_m$ and $\lambda(\ )^n = \lambda'(\lambda_1(\ )^{m_1} \nmid 1, \dots, \lambda_m(\ )^{m_m} \nmid 1)$, from which we can get

$$\lambda(x^{\perp}, \dots, x^{\perp}) \overset{\mathcal{L}\parallel\mathcal{D}_{11}, \dots, \mathcal{D}_{1m}}{=} \lambda'(\langle K_1 \nmid K_2 \nmid G_{11} \rangle \otimes 1, \dots, \langle K_1 \nmid K_2 \nmid G_{1m} \rangle \otimes 1) \overset{\mathcal{L}\parallel\mathcal{D}_{21}, \dots, \mathcal{D}_{2m}}{=} \lambda'(\langle K_1 \nmid K_2 \nmid G_{11} \rangle \otimes \langle K_3 \nmid G_{21} \rangle, \dots, \langle K_1 \nmid K_2 \nmid G_{1m} \rangle \otimes \langle K_3 \nmid G_{2m} \rangle) \overset{\mathcal{L}\parallel\mathcal{D}_0}{=} K_1 \nmid (K_2 \otimes K_3) \nmid \lambda'(G_{11} \nmid G_{21}, \dots, G_{1m} \nmid G_{2m}) \overset{\mathcal{L}\parallel\mathcal{D}_4}{=} K_1 \nmid (K_2 \otimes K_3) \nmid K_4$$

where $\mathcal{D}_0$ exists by Lemma 7.

The case for $r = sr$ is symmetric.

ii. $r = dt_{\downarrow}$ and $K = K_1 \nmid (K_2 \& K_3) \nmid K_4$, i.e.

$$dt_{\downarrow} \overset{\mathcal{L}\parallel}{\frac{((x \nmid K_1 \nmid K_2) \& (x \nmid K_1 \nmid K_3)) \nmid K_4}{x \nmid K_1 \nmid (K_2 \& K_3) \nmid K_4}}$$

By Lemma 8 we have

$$\overset{\mathcal{L}\parallel\mathcal{D}_2}{x \nmid K_1 \nmid K_2 \nmid K_4} \text{ and } \overset{\mathcal{L}\parallel\mathcal{D}_3}{x \nmid K_1 \nmid K_3 \nmid K_4}.$$
Applying induction hypothesis to $\mathcal{D}_2$ and $\mathcal{D}_3$ gives us that there are $m_1, m_2 \ge 0$ and $\lambda_1(\rangle^{m_1}, \lambda_2(\rangle^{m_2})$ such that

$$ \lambda_1\langle x^{\perp}, \dots, x^{\perp} \rangle \quad \text{and} \quad \lambda_2\langle x^{\perp}, \dots, x^{\perp} \rangle \\ \text{L}\|_{\mathcal{D}_{K_2}} \qquad \text{L}\|_{\mathcal{D}_{K_3}} \\ K_1 \otimes K_2 \otimes K_4 \qquad K_1 \otimes K_3 \otimes K_4 $$

Now take $n = m_1 + m_2$ and $\lambda(\rangle^n = \lambda_1(\rangle^{m_1} \& \lambda_2(\rangle^{m_2})$, from which we can get

$$ \lambda\langle x^{\perp}, \dots, x^{\perp} \rangle \quad \text{L}\|_{\mathcal{D}_{K_2} \& \mathcal{D}_{K_3}} \\ \text{dt}_{\downarrow} \frac{(K_1 \otimes K_2 \otimes K_4) \& (K_1 \otimes K_3 \otimes K_4)}{K_1 \otimes (K_2 \& K_3) \otimes K_4} $$

(c) The last rule $\mathfrak{r}$ introduces $x$. There is only one case to consider here, namely $\mathfrak{r} = \mathfrak{ai}_{\downarrow}$, i.e.

$$ \mathfrak{ai}_{\downarrow} \frac{L \|}{x \otimes x^{\perp} \otimes K} $$

By induction hypothesis there are $n \ge 0$ and $\lambda(\rangle^n$, such that $\lambda(\perp, \dots, \perp)$. From this we can get

$$ \perp_{\downarrow} \times n \frac{\lambda\langle x^{\perp}, \dots, x^{\perp} \rangle}{\lambda\langle x^{\perp} \perp \perp, \dots, x^{\perp} \perp \perp \rangle} \quad \text{L}\|_{\mathcal{D}_0} \\ x^{\perp} \otimes \lambda\langle \perp, \dots, \perp \rangle \quad \text{L}\|_{\mathcal{D}} \\ x^{\perp} \otimes K $$

where $\mathcal{D}_0$ exists by Lemma 7.

5. Assume $1 \otimes K$ is provable in $\mathfrak{L}$. The proof is similar to the one of (4), with the difference that there is no case (c), since there is no rule in $\mathfrak{L}$ introducing 1.

6. Assume $\perp \otimes K$ is provable in $\mathfrak{L}$. The proof is similar to the one of (4), with the difference that the

case (c) is trivial, i.e., if we have $\perp_{\downarrow} \frac{L \|}{\perp \otimes K}$ then $L \| K$.

7. Assume $0 \otimes K$ is provable in $\mathfrak{L}$. The proof is similar to the one of (4), with the difference that there is no case (c), since there is no rule in $\mathfrak{L}$ introducing 0. $\square$

**Lemma 10 (unary splitting).** Let A and K be formulas.

8. If $A \otimes K$ is provable in $\mathfrak{L}$, then there are $n \ge 0$ and $K_1, \dots, K_n$ and $\lambda(\rangle^n$, such that $\lambda(K_1, \dots, K_n)$ and for all $i \le n$ we have $\perp_{\downarrow} \frac{L \|}{A \otimes K_i}$ with $K_i = \perp$ or $K_i = ?K_{i1} \otimes \dots \otimes ?K_{ih_i}$ for some $h_i \ge 1$.

9. If $A \otimes K$ is provable in $\mathfrak{LS} \setminus \{\text{ct}_{\downarrow}\}$, then either $K$ is provable in $\mathfrak{LS} \setminus \{\text{ct}_{\downarrow}\}$, or there are $n \ge 1$ and $\kappa\langle K_1, \dots, K_n \rangle$ and $K_1, \dots, K_n$ and $\kappa(\rangle^n$, such that $\text{LS}\setminus\{\text{ct}_{\downarrow}\} \| K$ and $A \otimes K_i$ for all $i \le n$.

*Proof.* We proceed analogously to the proof of Lemma 8.

8. Assume $A \otimes K$ is provable in $\mathfrak{L}$. There are three cases to consider:

(a) The last rule $\mathfrak{r}$ is applied inside A or K. Similar to (1a).

(b) The last rule $\mathfrak{r}$ operates on a subformula containing $!A$. We distinguish between the following cases:
Now take $n = m_1 + \dots + m_k$ and $\kappa(\rangle^n = \lambda(\kappa_1(\rangle^{m_1} \otimes 1, \dots, \kappa_k(\rangle^{m_k} \otimes 1, 1 \otimes 1, \dots, 1 \otimes 1))$, from which we can get

$$
\begin{align*}
& \kappa\langle G_{111}, \dots, G_{11m_1}, \dots, G_{1km_k} \rangle \\
& \phantom{\kappa\langle} \llbracket \mathcal{L}\setminus\{ct_\downarrow\} \rrbracket_{\mathcal{D}_{11}, \dots, \mathcal{D}_{1m}} \\
& \lambda\langle (K_1 \otimes K_2 \otimes G_{11}) \otimes 1, \dots, (K_1 \otimes K_2 \otimes G_{1m}) \otimes 1 \rangle \\
& \llbracket \mathcal{L}\setminus\{ct_\downarrow\} \rrbracket_{\mathcal{D}_{21}, \dots, \mathcal{D}_{2m}} \\
& \text{sl, sr} \times m \frac{\lambda\langle (K_1 \otimes K_2 \otimes G_{11}) \otimes (K_3 \otimes G_{21}), \dots, (K_1 \otimes K_2 \otimes G_{1m}) \otimes (K_3 \otimes G_{2m}) \rangle}{\lambda\langle K_1 \otimes (K_2 \otimes K_3) \otimes G_{11} \otimes G_{21}, \dots, K_1 \otimes (K_2 \otimes K_3) \otimes G_{1m} \otimes G_{2m} \rangle} \\
& \llbracket \mathcal{L}\setminus\{ct_\downarrow\} \rrbracket_{\mathcal{D}_0} \\
& K_1 \otimes (K_2 \otimes K_3) \otimes \lambda\langle G_{11} \otimes G_{21}, \dots, G_{1m} \otimes G_{2m} \rangle \\
& \llbracket \mathcal{L}\setminus\{ct_\downarrow\} \rrbracket_{\mathcal{D}_4} \\
& K_1 \otimes (K_2 \otimes K_3) \otimes K_4
\end{align*}
$$

where $\mathcal{D}_0$ exists by Lemma 7.

The case for $r = sr$ is symmetric.

ii. $r = dt_\downarrow$ and $K = K_1 \otimes (K_2 \& K_3) \otimes K_4$, i.e.

$$
\frac{\left\| \mathcal{L}\setminus\{ct_\downarrow\} \right\|}{\mathrm{d}t_\downarrow} \frac{((?A \otimes K_1 \otimes K_2) \& (?A \otimes K_1 \otimes K_3)) \otimes K_4}{?A \otimes K_1 \otimes (K_2 \& K_3) \otimes K_4}
$$

By Lemma 8 we have

$$
\begin{array}{ll}
\mathcal{L}\setminus\{ct_\downarrow\} \| \mathcal{D}_2 & \text{and} \\
?A \otimes K_1 \otimes K_2 \otimes K_4 & \mathcal{L}\setminus\{ct_\downarrow\} \| \mathcal{D}_3
\end{array}
$$

Applying induction hypothesis to $\mathcal{D}_2$ and $\mathcal{D}_3$ gives us either $\mathcal{L}\setminus\{ct_\downarrow\} \|_{\mathcal{D}K_2}$ or there are $m_1 \ge 1$ and $G_{11}, \dots, G_{1m_1}$ and $\kappa_1(\rangle^{m_1}$ such that for all $i \le m_1$ we have

$$
\kappa_1 \langle G_{11}, \dots, G_{1m_1} \rangle \\
\mathcal{L}\setminus\{ct_\downarrow\} \|_{\mathcal{D}_{\kappa_1}} \quad \text{and} \quad \mathcal{L}\setminus\{ct_\downarrow\} \| \\
K_1 \otimes K_2 \otimes K_4 \qquad A \otimes G_{1i}
$$

and analogously, either $\mathcal{L}\setminus\{ct_\downarrow\} \|_{\mathcal{D}K_3}$ or there are $m_2 \ge 1$ and $G_{21}, \dots, G_{2m_2}$ and $\kappa_2(\rangle^{m_2}$ such that for all $j \le m_2$ we have

$$
\kappa_2 \langle G_{21}, \dots, G_{2m_2} \rangle \\
\mathcal{L}\setminus\{ct_\downarrow\} \|_{\mathcal{D}_{\kappa_2}} \quad \text{and} \quad \mathcal{L}\setminus\{ct_\downarrow\} \| \\
K_1 \otimes K_3 \otimes K_4 \qquad A \otimes G_{2j}.
$$

From this we can get either

$$
\frac{1}{\mathrm{ct}_\downarrow} \frac{\mathrm{d}t_\downarrow}{\mathrm{ct}_\downarrow} \frac{(K_1 \otimes K_2 \otimes K_4) \& (K_1 \otimes K_3 \otimes K_4)}{K_1 \otimes (K_2 \& K_3) \otimes K_4}
$$

or take $n = m_1 + m_2$ and $\kappa(\rangle^n = \kappa_1(\rangle^{m_1} \& \kappa_2(\rangle^{m_2}$ or $\kappa(\rangle^{m_l} = \kappa_l(\rangle^{m_l} \& 1$ for $l = 1, 2$ and respectively

$$
\begin{array}{ll}
\kappa\langle G_{11}, \dots, G_{1m_1}, G_{21}, \dots, G_{2m_2} \rangle & \\
\mathcal{L}\setminus\{ct_\downarrow\} \|_{\mathcal{D}_{\kappa_1}, \mathcal{D}_{\kappa_2}} & \text{or} \\
\frac{(K_1 \otimes K_2 \otimes K_4) \& (K_1 \otimes K_3 \otimes K_4)}{K_1 \otimes (K_2 \& K_3) \otimes K_4} & \text{d}t_\downarrow \\
& \frac{(K_1 \otimes K_2 \otimes K_4) \& (K_1 \otimes K_3 \otimes K_4)}{K_1 \otimes (K_2 \& K_3) \otimes K_4}
\end{array}
$$
iii. $r = \mathrm{pr}_\downarrow$ and $K = !K_1 \succ K_2$, i.e.

$$ \frac{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\}^{\|}}{\mathrm{pr}_\downarrow \frac{!(K_1 \succ ?A) \succ K_2}{?A \succ !K_1 \succ K_2}} $$

By induction hypothesis there are $m \ge 0$ and $G_1, \dots, G_m$ and $\lambda(\rangle)^m$, such that

$$ \lambda\langle G_1, \dots, G_m \rangle_{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\} \|_{\mathcal{D}_2}} \quad \text{and} \quad \lambda\langle G_1, \dots, G_m \rangle_{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\} \|_{\mathcal{D}_{Ai}}} $$

for all $i \le m$ with $G_i = \perp$ or $G_i = ?G'_{i1} \succ \dots \succ ?G'_{ih_i}$ for some $h_i \ge 1$. Thus, 0 or $h_i$ applications of the $\mathrm{pr}_\downarrow$ rule to $!(K_1 \succ G_i)$ gives us $!K_1 \succ G_i$.

Applying induction hypothesis to $\mathcal{D}_{Ai}$ gives us either $\lambda\langle G_1, \dots, G_m \rangle_{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\} \|_{\mathcal{D}_{1i}}}$ or there are $m_i \ge 1$ and $G_{i1}, \dots, G_{im_i}$ and $\kappa_i(\rangle)^{m_i}$ such that

$$ \kappa_i\langle G_{i1}, \dots, G_{im_i} \rangle_{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\} \|_{\mathcal{D}_{2i}}} \quad \text{and} \quad \lambda\langle G_1, \dots, G_m \rangle_{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\} \|_{\mathcal{D}_{ij_i}}} $$

for all $j_i \le m_i$. W.l.o.g., assume there is a $k \le m$, such that for all $k < i \le m$, $K_1 \succ G_i$ is provable in $\mathrm{LS} \setminus \{\mathrm{ct}_\downarrow\}$ and for all $i \le k$ the other property holds.

Now take $n = m_1 + \dots + m_k$ and $\kappa(\rangle)^n = \lambda(\!\kappa_1(\rangle)^{m_1}, \dots, \!\kappa_k(\rangle)^{m_k}, !1, \dots, !1\rangle)$, from which we can get

$$ \begin{aligned} & \kappa\langle G_{11}, \dots, G_{1m_1}, \dots, G_{km_k} \rangle \\ & \lambda\langle!K_1 \succ G_1, \dots, !K_1 \succ G_m\rangle \\ & \lambda\langle G_1, \dots, G_m \rangle \\ & \lambda\langle G_1, \dots, G_m \rangle \\ & \lambda\langle G_1, \dots, G_m \rangle \\ & \lambda\langle G_1, \dots, G_m \rangle \end{aligned} $$

where $\mathcal{D}_0$ exists by Lemma 7.

(c) The last rule $r$ decomposes the subformula $?A$. We distinguish between the following cases:

i. $r = \mathrm{wk}_\downarrow$, i.e.,

$$ \frac{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\}^{\|}}{\mathrm{wk}_\downarrow \frac{\perp \succ K}{?A \succ K}} $$

Then by Lemma 9, $K$ is provable in $\mathrm{LS} \setminus \{\mathrm{ct}_\downarrow\}$.

ii. $r = ?_\downarrow$, i.e.,

$$ \frac{\mathrm{LS}\setminus\{\mathrm{ct}_\downarrow\}^{\|}}{?_\downarrow \frac{A \succ K}{?A \succ K}} $$

Then take $n = 1$ and $\kappa(\rangle)^n = \{\}$ and $K_1 = K$. $\square$

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

The purpose of the splitting lemmas is to prove the following lemma, which says that the rules of the up-fragment are admissible in a shallow context.

**Lemma 11.** Let $K$ be a formula and let $r_\uparrow \frac{\xi\{F\}}{\xi\{G\}}$ be a rule in $\mathrm{SLS}_\uparrow$. If $F \succ K$ is provable in $\mathrm{LS}$, then so is $G \succ K$.

*Proof.* We proceed by using splitting to decompose the proof of $F \succ K$ into smaller pieces which can then be rearranged to build a proof of $G \succ K$. We consider only the three most complex cases, the others are similar (and simpler).
1. Let $r_\uparrow = a_i\uparrow$. Apply binary splitting to the proof of $(\bar{a} \otimes a) \succ K$, then there are $n \ge 0$ and $K_{11}, K_{21}, \dots, K_{1n}, K_{2n}$ and $\lambda\langle \rangle^n$, such that

$$ \lambda\langle K_{11} \succ K_{21}, \dots, K_{1n} \succ K_{2n} \rangle \quad \text{and} \quad \frac{\text{LS}\left\|_{\mathcal{D}_K}\right.}{K} \quad \text{and} \quad \frac{\text{LS}\left\|_{\bar{a} \succ K_{1i}}\right.}{a \succ K_{2i}} $$

for all $i \le n$. Now apply nullary splitting to the latter proofs. Then there are $n_{i1}, n_{i2} \ge 0$ and $\lambda_{i1}\langle \rangle^{n_{i1}}, \lambda_{i2}\langle \rangle^{n_{i2}}$, such that

$$ \lambda_{i1}\langle a, \dots, a \rangle \quad \lambda_{i2}\langle \bar{a}, \dots, \bar{a} \rangle \\ \text{LS}\left\|_{\mathcal{D}_{K_{1i}}}\right. \quad \text{and} \quad \text{LS}\left\|_{\mathcal{D}_{K_{2i}}}\right. \\ K_{1i} \qquad K_{2i} $$

Since $a \succ \bar{a}$ is provable in LS, we can get

$$ \begin{array}{l} \text{LS}\left\|_{\mathcal{D}_0}\right. \\ \lambda_{i2}\langle\lambda_{i1}\langle a \succ \bar{a}, \dots, a \succ \bar{a} \rangle, \dots, \lambda_{i1}\langle a \succ \bar{a}, \dots, a \succ \bar{a} \rangle\rangle \\ \text{LS}\left\|_{\mathcal{D}_1}\right. \\ \lambda_{i2}\langle\lambda_{i1}\langle a, \dots, a \rangle \succ \bar{a}, \dots, \lambda_{i1}\langle a, \dots, a \rangle \succ \bar{a} \rangle \\ \text{LS}\left\|_{\mathcal{D}_2}\right. \\ \lambda_{i1}\langle a, \dots, a \rangle \succ \lambda_{i2}\langle \bar{a}, \dots, \bar{a} \rangle \\ \text{LS}\left\|_{\mathcal{D}_{K_{1i}}, \mathcal{D}_{K_{2i}}}\right. \\ K_{1i} \succ K_{2i} \end{array} \quad \text{and thus} \quad \begin{array}{l} \text{LS}\left\|_{\mathcal{D}}\right. \\ \lambda\langle K_{11} \succ K_{21}, \dots, K_{1n} \succ K_{2n} \rangle \\ \text{LS}\left\|_{\mathcal{D}_K}\right. \\ \frac{K}{\perp\downarrow} \frac{\succ K}{\perp\succ K} \end{array} $$

where $\mathcal{D}_0, \mathcal{D}_1, \mathcal{D}_2$ and $\mathcal{D}$ exists by Lemma 7.

2. Let $r_\uparrow = \text{dt}_\uparrow$. Apply binary splitting to the proof of $((A \oplus B) \otimes C) \succ K$, then there are $n \ge 0$ and $K_{11}, K_{21}, \dots, K_{1n}, K_{2n}$ and $\lambda\langle \rangle^n$, such that

$$ \lambda\langle K_{11} \succ K_{21}, \dots, K_{1n} \succ K_{2n} \rangle \quad \text{and} \quad \frac{\text{LS}\left\|_{\mathcal{D}_K}\right.}{K} \quad \text{and} \quad \frac{\text{LS}\left\|_{\mathcal{D}_{A_{B_i}}}\right.}{(A \oplus B) \succ K_{1i}} \quad \text{and} \quad \frac{\text{LS}\left\|_{\mathcal{D}_{C_i}}\right.}{C \succ K_{2i}} $$

for all $i \le n$. Applying binary splitting to $\mathcal{D}_{A_{B_i}}$ gives us that there are $m_i \ge 0$ and $G_{i1}, \dots, G_{im_i}$ and $\lambda_i\langle \rangle^{m_i}$, such that

$$ \lambda_i\langle G_{i1}, \dots, G_{im_i} \rangle \quad \text{and for each } j_i \le m_i \text{ we have either} \quad \text{LS}\left\|_{\mathcal{D}_{A_{ij_i}}}\right. \quad \text{or} \quad \text{LS}\left\|_{\mathcal{D}_{B_{ij_i}}}\right. \\ K_{1i} \qquad G_{ij_i} \qquad G_{ij_i} $$

Using these derivations we build

$$ \begin{array}{c} \otimes_{\downarrow} \frac{1}{1 \otimes 1} \\ \text{LS}\left\|_{\mathcal{D}_{A_{ij_i}}, \mathcal{D}_{C_i}}\right. \\ \oplus_{\downarrow} \frac{\text{sl}, \text{sr} \frac{(A \succ G_{ij_i}) \otimes (C \succ K_{2i})}{((A \otimes C) \succ K_{2i}) \succ G_{ij_i}}}{((A \otimes C) \oplus (B \otimes C)) \succ K_{2i}) \succ G_{ij_i}} \\ \text{or} \\ \oplus_{\downarrow} \frac{\text{sl}, \text{sr} \frac{(B \succ G_{ij_i}) \otimes (C \succ K_{2i})}{((B \otimes C) \succ K_{2i}) \succ G_{ij_i}}}{((A \otimes C) \oplus (B \otimes C)) \succ K_{2i}) \succ G_{ij_i}} \\ \text{LS}\left\|_{\mathcal{D}_{B_{ij_i}}, \mathcal{D}_{C_i}}\right. \\ \text{LS}\left\|_{\mathcal{D}_{C_i}}\right. \\ \text{LS}\left\|_{\mathcal{D}_{K_{1i}}}\right. \end{array} $$

from which we can form

$$ \begin{array}{l} \text{LS}\left\|_{\mathcal{D}_1}\right. \\ \lambda_i\langle((A \otimes C) \oplus (B \otimes C)) \succ K_{2i}) \succ G_{i1}, \dots, ((A \otimes C) \oplus (B \otimes C)) \succ K_{2i}) \succ G_{im_i}\rangle \\ \text{LS}\left\|_{\mathcal{D}_2}\right. \\ ((A \otimes C) \oplus (B \otimes C)) \succ K_{2i}) \succ \lambda_i\langle G_{i1}, \dots, G_{im_i}\rangle \\ \text{LS}\left\|_{\mathcal{D}_{K_{1i}}}\right. \\ \text{com}_\downarrow \times 2, \text{asc}_\downarrow, \text{com}_\downarrow \frac{((A \otimes C) \oplus (B \otimes C)) \succ K_{2i}) \succ K_{1i}}{((A \otimes C) \oplus (B \otimes C)) \succ (K_{1i} \succ K_{2i})} \end{array} $$
and

$$
\begin{align*}
& \text{LS} \parallel \mathcal{D}_0 \\
& \lambda \left\langle \left( (A \otimes C) \oplus (B \otimes C) \right) \gtrdot (K_{11} \gtrdot K_{21}), \dots, ((A \otimes C) \oplus (B \otimes C)) \gtrdot (K_{1n} \gtrdot K_{2n}) \right\rangle \\
& \text{LS} \parallel \mathcal{D} \\
& \left( (A \otimes C) \oplus (B \otimes C) \right) \gtrdot \lambda \left\langle K_{11} \gtrdot K_{21}, \dots, K_{1n} \gtrdot K_{2n} \right\rangle \\
& \text{LS} \parallel \mathcal{D}_K \\
& \left( (A \otimes C) \oplus (B \otimes C) \right) \gtrdot K
\end{align*}
$$

where $\mathcal{D}_1, \mathcal{D}_2$ and $\mathcal{D}_0, \mathcal{D}$ exists by Lemma 7.

3. Let $r_\uparrow = \text{pr}_\uparrow$. Apply binary splitting to the proof of $(?A \otimes !C) \gtrdot K$, then there are $n \ge 0$ and $K_{11}, K_{21}, \dots, K_{1n}, K_{2n}$ and $\lambda \langle \rangle^n$, such that

$$
\lambda \langle K_{11} \gtrdot K_{21}, \dots, K_{1n} \gtrdot K_{2n} \rangle \\
\mathop{\mathrm{LS}}\nolimits\!\left\|_{K}^{\mathcal{D}_{K}}\right. \\
\text{and for all } j_i \le m_i \text{ we have } \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{1i}\right)_{A \gtrdot K_{1i}} \text{ and } \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{2i}\right)_{!C \gtrdot K_{2i}}
$$

for all $i \le n$. Applying unary splitting to $\mathcal{D}_{2i}$ gives us that there are $m_i \ge 0$ and $G_{i1}, \dots, G_{im_i}$ and $\lambda_i \langle \rangle^{m_i}$, such that

$$
\lambda_i \langle G_{i1}, \dots, G_{im_i} \rangle \\
\mathop{\mathrm{LS}}\nolimits\!\left\|_{K_{2i}}^{\mathcal{D}_{K_{2i}}}\right. \quad \text{and for all } j_i \le m_i \text{ we have } \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{j_i}\right)_{C \gtrdot G_{j_i}} \\
\left. \quad \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{j_i}\right)_{C \gtrdot G_{j_i}} \right\rangle
$$

with $G_{ij_i} = \perp$ or $G_{ij_i} = ?G_{ij_i} \gtrdot \dots \gtrdot ?G_{ij_i h_{j_i}}$ for $h_{j_i} \ge 1$. Applying Proposition 6 to $\mathcal{D}_{1i}$ we obtain formulas $?A_{i1}, \dots, ?A_{ik_i}, K'_{1i}$, such that

$$
\mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{\downarrow}\right)_{\mathcal{D}_{1i}}^{\mathcal{D}_{1i}} \quad \text{and} \quad \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{\downarrow}\right)_{\mathcal{D}_{2i}}^{\mathcal{D}_{2i}} \quad \text{for all } l=1\dots k_i \quad \text{and} \quad \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{\downarrow}\right)_{\mathcal{D}_{1i}}^{\mathcal{D}_{1i}} \\
?A_{i1} \gtrdot \dots \gtrdot ?A_{ik_i} \gtrdot K'_{1i} \quad \text{and} \quad ?A_{i1} \gtrdot \dots \gtrdot ?A_{ik_i} \gtrdot K'_{1i}
$$

Now applying Lemma 12 (proved below), $k_i$ times to $\mathcal{D}'_{1i}$ and $\mathcal{D}_{ij_i}$ gives us

$$
\begin{align*}
& \mathop{\mathrm{LS}}\nolimits\!\left(\mathcal{D}_{\downarrow}\right)_{\mathcal{D}_{1i}}^{\mathcal{D}_{1i}} \\
& \quad ?(A_{i1} \otimes !C) \gtrdot \dots \gtrdot ?(A_{ik_i} \otimes !C) \gtrdot K'_{1i} \gtrdot G_{ij_i} \gtrdot \dots \gtrdot G_{ij_i} \\
& \quad \{\mathcal{D}_{\downarrow}, \mathcal{D}_{\downarrow}, \mathcal{D}_{\downarrow}\}^{\mathcal{D}_{1i}} \\
& \quad \quad \quad \quad ((A \otimes !C) \gtrdot K_{1i}) \gtrdot G_{ij_i}
\end{align*}
$$

from which we can form

$$
\begin{align*}
& \text{LS} \parallel \mathcal{D}_1 \\
\lambda_i \left\langle \left( \begin{aligned}[c] & ?(A \otimes !C) \gtrdot K_{1i}) \gtrdot G_{i1}, \dots, ?(A \otimes !C) \gtrdot K_{1i}) \gtrdot G_{im_i} \\ &(A \otimes !C) \gtrdot K_{1i}) \gtrdot \lambda_i \langle G_{i1}, \dots, G_{im_i} \rangle \end{aligned} \right\rangle \\
& \text{LS} \parallel \mathcal{D}_2 \\
& \left( ?(A \otimes !C) \gtrdot K_{1i}) \gtrdot \lambda_i \langle K_{11} \gtrdot K_{21}, \dots, K_{1n} \gtrdot K_{2n} \rangle \right) \\
& \text{LS} \parallel \mathcal{D}_{K_{2i}} \\
& \frac{\text{com}_\downarrow \times 2, \text{asc}_\downarrow, \text{com}_\downarrow}{? (A \otimes !C) \gtrdot (K_{1i} \gtrdot K_{2i})} \\
& \frac{? (A \otimes !C) \gtrdot K_{1i}) \gtrdot K_{2i}}{? (A \otimes !C) \gtrdot (K_{1i} \gtrdot K_{2i})}
\end{align*}
$$

and

$$
\begin{align*}
& \text{LS} \parallel \mathcal{D}_0 \\
\lambda \langle & ?(A \otimes !C) \gtrdot (K_{11} \gtrdot K_{21}), \dots, ?(A \otimes !C) \gtrdot (K_{1n} \gtrdot K_{2n}) \rangle \\
& \text{LS} \parallel \mathcal{D} \\
& ?(A \otimes !C) \gtrdot \lambda \langle K_{11} \gtrdot K_{21}, \dots, K_{1n} \gtrdot K_{2n} \rangle \\
& \text{LS} \parallel \mathcal{D}_K \\
& ?(A \otimes !C) \gtrdot K
\end{align*}
$$

where $\mathcal{D}_1, \mathcal{D}_2$ and $\mathcal{D}_0, \mathcal{D}$ exists by Lemma 7.

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

**Lemma 12.** Let A, C, K and G be formulas, where $G = \perp$ or $G = ?G_1 \gtrdot \dots \gtrdot ?G_h$, for $h \ge 1$. If $A \gtrdot K$ and C $\gtrdot G$ are provable in $\mathrm{LS} \setminus \{\mathrm{ct}_\downarrow\}$, then so is $(?A \otimes !C) \gtrdot K) \gtrdot G$.
*Proof.* Apply unary splitting to the proof of ?A ≁ K. Then either K is provable in $LS \setminus \{ct_↓\}$ and thus

$$ \begin{array}{c} \mathrm{LS}\setminus\{ct_↓\} \\ K \\ \{⊥_↓, \mathrm{wk}_↓, \mathrm{com}_↓, \mathrm{asc}_↓\} \\ \Vert \\ (?(A \otimes !C) ≁ K) ≁ G \end{array} $$

or there are $n \ge 1$ and $K_1, \dots, K_n$ and $\kappa \langle \rangle^n$, such that

$$ \kappa\langle K_1, \dots, K_n \rangle_{LS\setminus\{ct_↓\}} \parallel_{\mathcal{D}_K} \text{ and } \kappa\langle K_1, \dots, K_n \rangle_{LS\setminus\{ct_↓\}} \parallel_{\mathcal{D}_{K_i}} $$

for all $i \le n$. Since $C \nmid G$ is provable in $LS \setminus \{ct_↓\}$, if $G = \perp$, $C$ and thus $!C \nmid G$ are provable in $LS \setminus \{ct_↓\}$ and if $G = ?G_1 \nmid \dots \nmid ?G_h$, applying the $pr_↓$ rule (modulo $com_↓, asc_↓$ rules) $h$ times to the proof of $C \nmid G$ gives us a proof $\mathcal{D}_G$ of $!C \nmid G$ in $LS \setminus \{ct_↓\}$. From this we can form

$$ \begin{array}{c} \otimes_↓, !_↓ \quad \frac{1}{1 \otimes !1} \\ \mathrm{LS}\setminus\{ct_↓\} \parallel_{\mathcal{D}_{K_i}, \mathcal{D}_G} \\ \text{sl, sr} \quad \frac{(A \nmid K_i) \otimes (!C \nmid G)}{((A \otimes !C) \nmid G) \nmid K_i} \\ ?_↓ \quad \frac{((A \otimes !C) \nmid G) \nmid K_i}{(?(A \otimes !C) \nmid G) \nmid K_i} \\ \kappa\langle C \nmid K_1, \dots, C \nmid K_n \rangle_{LS} \parallel_{\mathcal{D}_0} \text{ and } \kappa\langle(?(A \otimes !C) \nmid G) \nmid K_1, \dots, (?(A \otimes !C) \nmid G) \nmid K_n \rangle_{LS} \\ \kappa\langle(?(A \otimes !C) \nmid G) \nmid K_i, \dots, (?(A \otimes !C) \nmid G) \nmid K_n \rangle_{LS} \\ \text{com}_↓, \text{asc}_↓, \text{com}_↓ \quad \frac{(?(A \otimes !C) \nmid G) \nmid K}{(?(A \otimes !C) \nmid K) \nmid G} \\ \mathcal{D}_0, \mathcal{D} \text{ exists by Lemma 7.} \end{array} $$

where $\mathcal{D}_0, \mathcal{D}$ exists by Lemma 7. $\square$

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

## 2.4 Context Reduction

For proving Theorem 4, we need to extend Lemma 11 to general contexts. This is done by the context reduction lemma, whose proof is a straightforward induction on the context, repeatedly applying splitting.

**Lemma 13 (context reduction).** Let $A$ be a formula and $\xi$ be a context in which $\{ \}$ does not appear inside the scope of a $?\text{-modality}$. If $\xi\{A\}$ is provable in $LS$, then there exist an $n \ge 0$, a killing context $\kappa \langle \rangle^n$, and formulas $K_1, \dots, K_n$, such that

$$ \kappa\langle C \nmid K_1, \dots, C \nmid K_n \rangle_{LS} \parallel_{\xi\{C\}} \text{ for every formula } C \text{ and } \kappa\langle K_1, \dots, K_n \rangle_{LS} \parallel_{A \nmid K_i} \text{ for every } i \le n. $$

*Proof.* We proceed by induction on the structure of $\xi$. The base case is trivial. In the inductive step we consider only four cases. All the other cases are special forms of these ones.

1. Assume $\xi = (\xi' \otimes K_1) \nmid K_2$ (the case when $\xi = (K_1 \otimes \xi') \nmid K_2$ is symmetric). Apply the binary splitting lemma to the proof of $(\xi'\{A\} \otimes K_1) \nmid K_2$. Then there are $m \ge 0$ and $G_{11}, G_{21}, \dots, G_{1m}, G_{2m}$ and $\lambda \langle \rangle^m$, such that

$$ \lambda\langle G_{11} \nmid G_{21}, \dots, G_{1m} \nmid G_{2m} \rangle_{LS} \parallel_{\mathcal{D}_{K_2}} \text{ and } \lambda\langle K_1 \nmid G_{1i} \rangle_{LS} \parallel_{\mathcal{D}_{A_i}} \text{ and } \lambda\langle G_{1i} \nmid G_{2i} \rangle_{LS} \parallel_{A \nmid G_{1ij}} $$

for all $i \le m$. Applying induction hypothesis to $\mathcal{D}_{A_i}$ gives us that there are $m_i \ge 0$ and $G_{1i1}, \dots, G_{1im_i}$ and $\kappa_i \langle \rangle^{m_i}$, such that for an arbitrary formula $C$

$$ \kappa_i\langle C \nmid G_{1i1}, \dots, C \nmid G_{1im_i} \rangle_{LS} \parallel_{\xi'\{C\} \nmid G_{1i}} \text{ and } \kappa_i\langle G_{1i1}, \dots, G_{1im_i} \rangle_{LS} \parallel_{A \nmid G_{1ij}} $$
form

$$
\begin{align*}
& \kappa \langle C \oslash G_{11}, \dots, C \oslash G_{1m_1}, \dots, C \oslash G_{km_k} \rangle \\
& \oplus l_{\downarrow} \times k, \oplus r_{\downarrow} \times m - k \frac{\lambda \langle \xi' \{C\} \oslash G_1, \dots, \xi' \{C\} \oslash G_k, K_1 \oslash G_{k+1}, \dots, K_1 \oslash G_m \rangle}{\lambda \langle (\xi' \{C\} \oplus K_1) \oslash G_1, \dots, (\xi' \{C\} \oplus K_1) \oslash G_m \rangle} \\
& \phantom{\lambda \langle \xi' \{C\} \oslash G_1, \dots, \xi' \{C\} \oslash G_k, K_1 \oslash G_{k+1}, \dots, K_1 \oslash G_m \rangle} \frac{\lambda \langle \xi' \{C\} \oplus K_1) \oslash \lambda \langle G_1, \dots, G_m \rangle}{\lambda \langle \xi' \{C\} \oplus K_1) \oslash K_2} \\
& \phantom{\lambda \langle \xi' \{C\} \oslash G_1, \dots, \xi' \{C\} \oslash G_k, K_1 \oslash G_{k+1}, \dots, K_1 \oslash G_m \rangle} \frac{\lambda \langle \xi' \{C\} \oplus K_1) \oslash K_2 \rangle}{\lambda \langle \xi' \{C\} \oplus K_1) \oslash K_2 \rangle}
\end{align*}
$$

where $\mathcal{D}_0$ exists by Lemma 7.

4. Assume $\xi = !\xi' \oslash K$. Apply the unary splitting lemma to the proof of $!\xi' \{A\} \oslash K$. Then there are $m \ge 0$ and $K_1, \dots, K_m$ and $\lambda \langle \rangle^m$, such that

$$
\begin{array}{c}
\lambda \langle K_1, \dots, K_m \rangle \\
\mathbf{LS} \|_{\mathcal{D}_K} \\
K
\end{array}
\quad \text{and for all } i \le m \text{ we have} \quad
\mathbf{LS} \|_{\mathcal{D}_{A_i}} \\
\xi' \{A\} \oslash K_i
$$

with $K_i = \perp$ or $K_i = ?K'_{i1} \oslash \cdots \oslash ?K'_{ih_i}$ for some $h_i \ge 1$. Thus, $!\xi' \{A\} \oslash K_i$ is derivable from $!(\xi' \{A\} \oslash K_i)$ using the $pr_\downarrow$ rule 0 or $h_i$ times. Applying induction hypothesis to $\mathcal{D}_{Ai}$ gives us that there are $m_i \ge 0$ and $K_{i1}, \dots, K_{im_i}$ and $\kappa_i \langle \rangle^{m_i}$, such that for an arbitrary formula $C$,

$$
\kappa_i \langle C \oslash K_{i1}, \dots, C \oslash K_{im_i} \rangle \quad \text{and} \quad \mathbf{LS} \|_{\mathcal{D}_{K_i}} \quad A \oslash K_{ij_i}
$$

for every $j_i \le m_i$. Now take $n = m_1 + \dots + m_m$ and $\kappa \langle \rangle^n = \lambda \langle !\kappa_1 \langle \rangle^{m_1}, \dots, !\kappa_m \langle \rangle^{m_m} \rangle$, from which we can form

$$
\begin{align*}
& \kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle \\
& \phantom{\kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle} \mathbf{LS} \|_{\mathcal{D}_{K_1}, \dots, \mathcal{D}_{K_m}} \\
& \phantom{\kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle} \lambda \langle !\xi' \{C\} \oslash K_1, \dots, !\xi' \{C\} \oslash K_m \rangle \\
& \phantom{\kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle} \mathbf{LS} \|_{\mathcal{D}_0} \\
& \phantom{\kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle} !\xi' \{C\} \oslash \lambda \langle K_1, \dots, K_m \rangle \\
& \phantom{\kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle} \mathbf{LS} \|_{\mathcal{D}_K} \\
& \phantom{\kappa \langle C \oslash K_{11}, \dots, C \oslash K_{1m_1}, \dots, C \oslash K_{mm_m} \rangle} !\xi' \{C\} \oslash K
\end{align*}
$$

where $\mathcal{D}_0$ exists by Lemma 7.

□

**Lemma 14.** Let $r_\uparrow \frac{\xi\{F\}}{\xi\{G\}}$ be a rule in SLS$\uparrow$ and let $\xi$ be a context in which $\{\}$ does not appear inside the scope of a $\neg$-modality. If $\xi\{F\}$ is provable in LS, then so is $\xi\{G\}$.

*Proof.* The general idea is to decompose the given proof via context reduction and then apply Lemma 11 and Lemma 7. We illustrate this on the case of $ai_\uparrow$ rule, the other cases are similar.

Assume $\xi \{ \bar{a} \otimes a \}$ is provable in LS. Applying context reduction to the proof of $\xi \{ \bar{a} \otimes a \}$ gives us that there are $n \ge 0$ and $K_1, \dots, K_n$ and $\kappa \langle \rangle^n$, such that for every formula $C$

$$
\begin{align*}
& \kappa \langle C \oslash K_1, \dots, C \oslash K_n \rangle \\
& \mathbf{LS} \| \\
& \xi \{ C \}
\end{align*}
\quad \text{and} \quad
\begin{gathered}
\mathbf{LS} \|_{\mathcal{D}_{ai}} \\
(\bar{a} \otimes a) \oslash K_i, \quad \text{but then} \\
\mathbf{LS} \|_{\mathcal{D}_{\perp}} \\
\xi \{ \perp \}
\end{gathered}
$$

Applying Lemma 11 to $\mathcal{D}_{ai}$ gives us that for all $i \le n$ we have

$$
\mathbf{LS} \|_{\mathcal{D}_i} \quad \text{and} \quad \kappa \langle \perp \oslash K_1, \dots, \perp \oslash K_n \rangle \\
\mathbf{LS} \|_{\mathcal{D}_{\perp}} \quad \xi \{ \perp \}
$$

where $\mathcal{D}_0$ exists by Lemma 7.

□
In order to deal with ?-contexts, we use the following lemma, proved by a simple rule permutation argument: any rule applied inside the scope of a ? can be permuted up until it leaves the scope of the ?-modality.

**Lemma 15** (?-reduction). For every proof $\mathcal{P}$ in SLS there is a proof $\mathcal{P}'$ in SLS with the same conclusion as $\mathcal{P}$, such that in $\mathcal{P}'$ no inference rule is applied inside the scope of a ?-modality.

*Proof.* If we have one of the following cases

$$ 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
\mathrm{wk}_{\downarrow} \\ 
r 
\end{array} 
\quad 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
\mathrm{?}_{\downarrow} \\ 
r 
\end{array} 
\quad 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
\mathrm{pr}_{\uparrow} \\ 
r 
\end{array} 
\quad 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
r' \\ 
r 
\end{array} 
\end{array} 
$$

then we get, respectively

$$ 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
\mathrm{wk}_{\downarrow} \\ 
r 
\end{array} 
\quad 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
\mathrm{?}_{\downarrow} \\ 
r' 
\end{array} 
\quad 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
\mathrm{pr}_{\uparrow} \\ 
r' 
\end{array} 
\quad 
\begin{array}{c} 
\begin{array}{c} 
\mathrm{SLS} \\ 
\mathrm{\parallel} 
\end{array} \\ 
r' \\ 
r' 
\end{array} 
$$

For the other cases use induction hypothesis. $\square$

Now Theorem 4 can be shown by first applying Lemma 15 and then eliminating all up-rules, starting with the topmost one, using Lemma 14.

# 3 Focusing

## 3.1 LLKF: Polarized and Focused Variant of LLK

In order to build the focused variant of LLK, called LLKF, linear formulas are divided into two *polarity* classes—*positive* and *negative*—based on the permutation properties of their sequent rules. The negative formulas have invertible rules, i.e., rules that may be applied whenever the formula occurs in the context, while the rules for the positive formulas are sensitive to the order of application of rules and are therefore generally non-invertible. Following [16], we syntactically distinguish these two classes and mediate between them by a pair of *shift* connectives (↓ and ↑):

$P, Q ::= a \mid P \otimes Q \mid 1 \mid P \oplus Q \mid 0 \mid !N \mid \downarrow N$ (Positive Formulas)

$N, M ::= \bar{a} \mid N \ominus M \mid \perp \mid N \& M \mid \top \mid ?P \mid \uparrow P$ (Negative Formulas)

Here, $\downarrow N)^{\perp} = \uparrow N)^{\perp}$ and $(\uparrow P)^{\perp} = \downarrow (P)^{\perp}$. We use the following contexts for LLKF:

$\Gamma ::= \cdot \mid \Gamma, P$ (Positive Sequent Contexts)

$\Delta ::= \cdot \mid \Delta, N$ (Negative Sequent Contexts)

$\Pi ::= \cdot \mid \Pi, \uparrow P \mid \Pi, \bar{a}$ (Reactive Sequent Contexts)

LLKF proofs consist of alternating maximal *phases* based on the polarity of the principal formulas. These two phases are represented by two different sequent forms, given below. We follow Andreoli's original two-zoned (*dyadic*) convention for presenting the system because it is the most common style in presenting focused proof systems.

$\vdash \Gamma ; \Delta$ (Negative Sequents)

$\vdash \Gamma ; \Pi, [P]$ (Positive Sequents)

The sequent $\vdash \Gamma ; \cdot, [P]$ is abbreviated as $\vdash \Gamma ; [P]$.

The focused rules of inference are shown in Figure 3. The most important rules are the *decision* rules wdc and dc that begin<fnref n="2" /> a positive phase; in this phase, the focused formula (written inside `[ ]`) is principal, and the focus persists on the principal operands if they are of the same polarity. All essential choices are confined to this phase; they include: disjunctive choice (for ⊕), multiplicative choice (for ⊗),

<footnote n="2">²As usual, the intended reading of sequent rules is from conclusion to premises.</footnote>
<figure><img src="image_8.png" /><figcaption>Figure 3: **LLKF**: a two-zoned focused variant of cut-free LLK</figcaption></figure>

possible failures (for atoms, 1, and !, if the context is not of the correct form), and guaranteed failure (for 0, which has no rules). The positive phase switches to the negative phase with the rules for ↓ or !. Observe that in the negative phase the rules can be applied in any order, and none of the negative rules can fail to apply. When no more negative rules can apply, a decision rule must be applied to restart the cycle. There are no structural rules of weakening or contraction because the rules treat the *unrestricted context* Γ as a set; in particular, contraction is part of the wdc rule.

The soundness of LLKF with respect to cut-free LLK is straightforward: forgetting the polarities, the focusing distinctions in sequents, and the rules {dc, ↓}; prefixing the elements of Γ with ? and using ct and wk to account for its additive treatment in the ⊗, 1 and id rules; and replacing wdc with the sequence ct then ? on the focused formula produces valid LLK proofs from LLKF proofs.

**Notation 16.** Write $\lfloor P \rfloor$ (resp. $\lfloor N \rfloor$) for the unpolarized formula obtained from $P$ (resp. $N$) by erasing all occurrences of $\downarrow$ and $\uparrow$. Similarly we define $\lfloor \Delta \rfloor$.

**Theorem 17 (completeness of focusing).** If $\vdash [\Delta]$ in LLK, then $\vdash \cdot ; \Delta$ in LLKF.

There are many ways to prove this theorem; we refer the interested reader to one of the standard approaches [17, 19]. One interesting feature of all such proofs is their unusual complexity forced by the rigidity of the focusing calculus. It is easier to show the completeness of focusing in the sequent calculus with more synthetic approaches [8].

## 3.2 LSF and LSS: Polarized, Focused, and Synthetic Variants of LS

In this section we study two complete polarized and focused variants of LS. Like in Andreoli's original formulation of focusing in the sequent calculus [1], we keep the general form of the rules of LS but modify them to respect polarity. The resulting calculus, called LSF, can be seen to be related to LS in the same way that LLKF is related to LLK. (In Section 4 below, we formalize the comparison between LLKF and LSF.) Just as in the sequent calculus, the proofs of completeness of the focusing restriction will become more manageable in a synthetic formulation of LSF, that we call LSS, which we present immediately after LSF.

Because LSF uses polarized formulas, the contexts in LSF are sensitive to the polarity of their holes. We use $\pi$ and $\rho$ for positive formula contexts, i.e., $\pi\{P\}$ is a well-formed polarized formula for any positive formula $P$. Likewise, we use $\nu$ and $\mu$ for negative formula contexts. Note that the polarity of $\pi\{P\}$ (resp. $\nu\{N\}$) need not itself be positive (resp. negative). For example, $\pi\{\}$ = ($N \& ?\{\}$) $\succcurlyeq$ $M$ is a positive formula context, but the polarity of the formula $\pi\{P\} = (N \& ?P) \succcurlyeq M$ is negative.

Inside positive contexts, we will use a notational device to mark the foci. To motivate this notation, consider the properties of the foci in LLKF sequents: they *interact* with the context by splitting it (for $\otimes$), by testing it for emptiness (for 1 and !), or by checking for the presence of negated atoms (for id). For LSF, these interactions need to be made incremental—formula by formula—because the formulas of the corresponding sequent context may not (yet) be present in a $\succcurlyeq$ relation at the point of the switch rules.
<figure><img src="image_9.png" /><figcaption>Figure 4: LSF: a polarized and focused variant of LS</figcaption></figure>

**Definition 18.** An *interaction formula* (or simply an *interaction*) is a positive formula of the form $P \otimes L$. We call $P$ in $P \otimes L$ the *focus* of the interaction, and $L$ its *spine*.

Here, we use $L$ to stand for *reactive formulas*, which correspond to the formulas that occur in LLKF sequents $\vdash \Gamma$; $\Pi$, which are precisely those sequents that are introduced by the decision rules wdc and dc. Recall that such sequents represent formulas of the form $\mathcal{G}(?\Gamma, \Pi)$. Reactive formulas, and their duals, the *active formulas*, therefore have this grammar:

$$ \begin{array}{l@{\hspace{2em}}l} R & ::= \ a \mid !N \mid \downarrow N \qquad (\text{Active Formulas}) \\ L & ::= \ \bar{a} \mid ?P \mid \uparrow P \qquad (\text{Reactive Formulas}) \end{array} $$

Figure 4 lists the inference rules of LSF. A proof in LSF is a derivation with premise 1 or $\uparrow 1$. The start rules in Figure 4 define what it means to finish an LSF proof. The first start rule removes a pair of shifts from a 1, and the other four are polarized versions of the rules $\otimes\downarrow$, $!\downarrow$, $\&\downarrow$, and $\uparrow\downarrow$ of LS (Figure 2). Interactions are created by the $\text{int}_F$ rule, which corresponds to dc in LLKF. When the focus of the interaction involves a polarity shift, the interaction dissipates into an ordinary $\mathcal{G}$ using $\text{pc}_F$, which is the analogue of the $\downarrow$ rule of LLKF. In order to remain true to the spirit of LS, we keep contraction and decision as separate rules instead of building a specialized version of $\text{int}_F$ that incorporates contraction. This lets us preserve the permutability of contraction (Proposition 6) even in the focused setting. To retain completeness, the $?_F$ rule derelicts a $?$ to a $\uparrow$. The remaining rules for interactions follow the shape of the focus of the interaction, just as in the sequent calculus. For example, for $\otimes$, the rules $\text{sl}_F$ and $\text{sr}_F$ (that are the focused versions of the $\text{sl}$ and $\text{sr}$ rules of LS) send the spine of the interaction into one of the components of the focus. The remaining (non-interaction) rules are simply the direct polarity-respecting translations of the LS rules.

**Theorem 19 (soundness).** For any $N$, if $N$ is provable in LSF, then $[N]$ is provable in LS.

*Proof.* Just replace $P \otimes L$ with $P \mathcal{G} L$ and erase the polarity shifts. $\square$

To show completeness, we will now move to a synthetic variant of LSF, called LSS, that keeps a sequence of interactions on subformulas of a focus together. While the correspondence with LLKF is clearer in LSF without this synthetic step, the proof of completeness is drastically simplified with synthetic formulations, a phenomenon that has also been observed for focusing in the sequent calculus [8].

The key observation needed to produce a synthetic variant of LSF is the following: in an interaction formula $P \otimes L$, the spine $L$ is switched (using $\text{sl}_F$ and $\text{sr}_F$) *deep inside* $P$ until the focus of the interaction becomes active. During this switching, any $\mathcal{G}$-formulas in the focus are destructed by removing (using $\oplus\text{I}_F$ and $\oplus\text{R}_F$) one of its operands. Thus, we can define a special *tensor context*, written using $\pi_{\otimes}$ and $\rho_{\otimes}$, with this grammar:
$$ \pi_{\otimes} ::= \{ \} | \pi_{\otimes} \otimes P | P \otimes \pi_{\otimes} \qquad (Tensor Contexts) $$

Note that, because $\pi_{\otimes}$ contains no shift or exponential connectives, any substitution $\pi_{\otimes}\{P\}$ is itself positive. Tensor contexts allow us to write the following synthetic forms of the interaction rules:

$$ \mathit{sai}_F \frac{\nu\{\uparrow\pi_{\otimes}\{1\}\}}{\nu\{\uparrow\pi_{\otimes}\{a\} \upharpoonright \bar{a}\}} \qquad \mathit{spc}_F \frac{\nu\{\uparrow\pi_{\otimes}\{\downarrow(N \upharpoonright L)\}\}}{\nu\{\uparrow\pi_{\otimes}\{\downarrow N\} \upharpoonright L\}} \qquad \mathit{spr}_F \frac{\nu\{\uparrow\pi_{\otimes}\{! (N \upharpoonright ?P)\}\}}{\nu\{\uparrow\pi_{\otimes}\{!N\} \upharpoonright ?P\}} $$

**Definition 20.** The system LSS is LSF $\setminus \{\mathrm{int}_F, \mathrm{ai}_F, \mathrm{sl}_F, \mathrm{sr}_F, \mathrm{pc}_F, \mathrm{pr}_F\} \cup \{\mathrm{sai}_F, \mathrm{spc}_F, \mathrm{spr}_F\}$.

**Theorem 21.** Any formula is provable in LSS if and only if it is provable in LSF.

*Proof.* Each instance of $\mathrm{sai}_F$, $\mathrm{spc}_F$, or $\mathrm{spr}_F$ can be derived by one of

$$ \begin{array}{ccc} \mathrm{ai}_F & \frac{\nu\{\uparrow\pi_{\otimes}\{1\}\}}{\nu\{\uparrow\pi_{\otimes}\{a \upharpoonright \bar{a}\}\}} & \mathrm{pc}_F \frac{\nu\{\uparrow\pi_{\otimes}\{\downarrow(M \upharpoonright L)\}\}}{\nu\{\uparrow\pi_{\otimes}\{\downarrow M \upharpoonright L\}\}} & \mathrm{pr}_F \frac{\nu\{\uparrow\pi_{\otimes}\{! (M \upharpoonright ?P)\}\}}{\nu\{\uparrow\pi_{\otimes}\{! M \upharpoonright ?P\}\}} \\ \{\mathrm{sl}_F, \mathrm{sr}_F\} \parallel \mathcal{D} & & \{\mathrm{sl}_F, \mathrm{sr}_F\} \parallel \mathcal{D} & \{\mathrm{sl}_F, \mathrm{sr}_F\} \parallel \mathcal{D} \\ \mathrm{int}_F & \frac{\nu\{\uparrow(\pi_{\otimes}\{a\} \upharpoonright \bar{a})\}}{\nu\{\uparrow\pi_{\otimes}\{a\} \upharpoonright \bar{a}\}} & \mathrm{int}_F \frac{\nu\{\uparrow(\pi_{\otimes}\{\downarrow M\} \upharpoonright L)\}}{\nu\{\uparrow\pi_{\otimes}\{\downarrow M\} \upharpoonright L\}} & \mathrm{int}_F \frac{\nu\{\uparrow(\pi_{\otimes}\{!M\} \upharpoonright ?P)\}}{\nu\{\uparrow\pi_{\otimes}\{!M\} \upharpoonright ?P\}} \end{array} $$

where $\mathcal{D}$ can be constructed by a straightforward induction on $\pi_{\otimes}$.

In the other direction, if an LSF proof is given, the idea is to show that there is a possibility to reorder $\mathrm{int}_F$, $\mathrm{ai}_F$, $\mathrm{sl}_F$, $\mathrm{sr}_F$, $\mathrm{pc}_F$, $\mathrm{pr}_F$ rules inside the proof in such a way, that their application sequence can be replaced by $\mathrm{sai}_F$, $\mathrm{spc}_F$, or $\mathrm{spr}_F$. Note that $\upharpoonright 1$ is not commutative, i.e., the order of the spines is fixed in iterations of $\upharpoonright 1$. We can therefore permute any LSF proof to guarantee that the focus of any interaction isn't itself an interaction. Considering, that interactions are introduced by $\mathrm{ai}_F$, $\mathrm{sl}_F$, $\mathrm{sr}_F$, $\mathrm{pc}_F$, $\mathrm{pr}_F$, we permute all instances of $\upharpoonright 1$ and $\downarrow ?$ as low as possible in the LSF proof so that all interactions are introduced only by $\mathrm{ai}_F$, $\mathrm{pc}_F$ or $\mathrm{pr}_F$. The synthetic rules $\mathrm{sai}_F$, $\mathrm{spc}_F$ and $\mathrm{spr}_F$ can now be easily recovered in a similar way as it is shown above for the first direction. $\square$

For giving the proof of completeness of LSS with respect to LS, we proceed by inductive transformation of LS proofs in three steps. First, we rewrite the instances of the switch rules in LS to respect the restriction of the spines to reactive formulas, which corresponds to applying negative rules eagerly like in LLKF. Second, we use an auxiliary rule, called $\mathrm{ps}_F$, that breaks the polarity restrictions by means of an extra pair of shifts in the premise. This rule allows us to transform any LS proof into a proof in LSS $\cup \{\mathrm{ps}_F\}$. And third, we show that $\mathrm{ps}_F$ can be eliminated from LSS $\cup \{\mathrm{ps}_F\}$.

For the first step, let $\mathrm{LS}^r$ stand for LS where the rules $\mathrm{sl}$ and $\mathrm{sr}$ (see Figure 2) are replaced by the following rules $\mathrm{sl}^r$ and $\mathrm{sr}^r$, respectively:

$$ \mathrm{sl}^r \frac{\xi\{(A \upharpoonright \lfloor L \rfloor) \otimes B\}}{\xi\{(A \otimes B) \upharpoonright \lfloor L \rfloor\}} \qquad \mathrm{sr}^r \frac{\xi\{A \otimes (B \upharpoonright \lfloor L \rfloor)\}}{\xi\{(A \otimes B) \upharpoonright \lfloor L \rfloor\}} $$

Recall that $L$ stands for reactive formulas. The following can be shown by an easy induction:

**Lemma 22.** *The rules*

$$ \mathrm{cc}_{\downarrow} \frac{\xi\{(A \& B) \otimes C\}}{\xi\{(A \otimes C) \& (B \otimes C)\}} \qquad \mathrm{ga}_{\downarrow} \frac{\xi\{\top \otimes A\}}{\xi\{\top\}} \qquad \bar{\bot}_{\downarrow} \frac{\xi\{A \upharpoonright \bot\}}{\xi\{A\}} \qquad \bar{\mathrm{d}}_{\downarrow} \frac{\xi\{(A \& B) \upharpoonright C\}}{\xi\{(A \upharpoonright C) \& (B \upharpoonright C)\}} \qquad \bar{\mathrm{g}}_{\downarrow} \frac{\xi\{\top \upharpoonright C\}}{\xi\{\top\}} $$

are admissible in $\mathrm{LS}^r$.

*Proof.* We proceed by induction on the length of the proof of the rule premises and make a case analysis on the bottommost rule $r \in \mathrm{LS}^r$ applied in the given derivation.

If $r$ is applied inside the context or inside the active formulas, then we simply use induction hypothesis and $r$, to construct the desired proof. Thus we only consider the cases, when $r$ modifies the active formulas.

$(\mathrm{cc}_{\downarrow})$. Assume $\xi\{(A \& B) \otimes C\}$ is provable in $\mathrm{LS}^r$. If $r = \mathrm{sl}^r$, i.e.

$$ \mathrm{sl}^r \frac{\mathrm{LS}^r \parallel \mathcal{D}}{\xi\{(A \& B) \upharpoonright \lfloor L \rfloor\} \otimes C} \qquad \xi\{(A \& B) \otimes C\} \upharpoonright \lfloor L \rfloor $$
Applying induction hypothesis twice to $\mathcal{D}$ gives us that $\xi\{(A \otimes \lfloor L \rfloor) \otimes C\} \& ((B \otimes \lfloor L \rfloor) \otimes C)\}$ is provable in $LS^r$. From this we get

$$sl^r \times 2 \frac{\overset{LS^r \Vert \mathcal{D}'}{\xi\{(A \otimes \lfloor L \rfloor) \otimes C\} \& ((B \otimes \lfloor L \rfloor) \otimes C)\}}{\overset{\text{dL}}{\xi\{(A \otimes C) \otimes \lfloor L \rfloor\} \& ((B \otimes C) \otimes \lfloor L \rfloor)\}}} \frac{\overset{LS^r \Vert \mathcal{D}'}{\xi\{(\top \otimes \lfloor L \rfloor) \otimes A\}}}{\overset{\text{dL}}{\xi\{(\top \otimes A) \otimes \lfloor L \rfloor\}}}}$$

Analogously, if $r = sr^r$, we apply induction hypothesis only once, then the $sr^r$ rule twice and finally the $dL$ rule.

(ga↓). Assume $\xi\{\top \otimes A\}$ is provable in $LS^r$. If $r = \top↓$, then immediately $\xi\{\top\}$ is provable in $LS^r$. If $r = sl^r$, i.e.

$$sl^r \frac{\overset{LS^r \Vert \mathcal{D}'}{\xi\{(\top \otimes \lfloor L \rfloor) \otimes A\}}}{\overset{\text{dL}}{\xi\{(\top \otimes A) \otimes \lfloor L \rfloor\}}}}$$

Applying induction hypothesis twice to $\mathcal{D}$ gives us that $\xi\{\top\}$ is provable in $LS^r$. From this we get

$$gc↓ \frac{\overset{LS^r \Vert \mathcal{D}'}{\xi\{\top \otimes \lfloor L \rfloor\}}}{\overset{\text{dL}}{\xi\{\top \otimes \lfloor L \rfloor\}}}}$$

Analogously, if $r = sr^r$, we apply induction hypothesis only once and then the $gc↓$ rule.

($\bar{\text{L}}$↓). Assume $\xi\{A \otimes \perp\}$ is provable in $LS^r$. If $r = \perp↓$, then immediately $\xi\{A\}$ is provable in $LS^r$. If $r = sl^r$, i.e.

$$sl^r \frac{\overset{LS^r \Vert \mathcal{D}'}{\xi\{(A_1 \otimes \perp) \otimes A_2\}}}{\overset{\text{dL}}{\xi\{(A_1 \otimes A_2) \otimes \perp\}}}}$$

Applying induction hypothesis to $\mathcal{D}$ immediately gives us that $\xi\{A_1 \otimes A_2\}$ is provable in $LS^r$. The cases for $r = sr^r$ and $r = asc↓$ are similar.

($\bar{\text{dL}}$↓). Assume $\xi\{(A \& B) \otimes C\}$ is provable in $LS^r$. If $r = dL↓$, then immediately $\xi\{(A \otimes C) \& (B \otimes C)\}$ is provable in $LS^r$.

($\bar{\text{gc}}$↓). Assume $\xi\{\top \otimes C\}$ is provable in $LS^r$. If $r = gc↓$, then immediately $\xi\{\top\}$ is provable in $LS^r$. If $r = sl^r$, i.e.

$$sl^r \frac{\overset{LS^r \Vert \mathcal{D}'}{\xi\{(C_1 \otimes \top) \otimes C_2\}}}{\overset{\text{dL}}{\xi\{(C_1 \otimes C_2) \otimes \top\}}}} \quad \text{Applying induction hypothesis twice to} \quad \overset{LS^r \Vert \mathcal{D}'}{\text{com}_↓ \frac{\xi\{(C_1 \otimes \top) \otimes C_2\}}{\xi\{(\top \otimes C_1) \otimes C_2\}}}}$$

gives us that $\xi\{\top\}$ is provable in $LS^r$. The cases for $r = sr^r$ and $r = asc↓$ are similar.

□

**Lemma 23.** If a formula A is provable in LS, then it is also provable in $LS^r$.

*Proof.* Let the size of an instance of sl or sr with conclusion $\xi\{(A \otimes B) \otimes C\}$ be defined as the number of symbols used in C. For transforming an LS proof into an $LS^r$ proof we take two steps:

$$\overset{\text{dL}}{\text{LS}^r \Vert \mathcal{D}_1} \longrightarrow \overset{\text{dL}}{\text{LS}^r \cup \{cc↓, ga↓, \bar{\text{L}}↓, \bar{\text{dL}}↓, \bar{\text{gc}}↓\} \Vert \mathcal{D}_2} \longrightarrow \overset{\text{Lemma 22}}{\text{LS}^r \Vert \mathcal{D}_3} \longrightarrow \overset{\text{dL}}{\text{LS}^r \Vert \mathcal{D}_1}$$

For the first step, proceed by induction on the multi-set of the sizes of all switch instances in $\mathcal{D}_1$, under multi-set ordering, showing that all instances of sl and sr can be reduced to $sl^r$ and $sr^r$. Any instance of
sl but not of sl' can be replaced by one of the following derivations, reducing the size. (Note that we omitted some instances of asc↓ and com↓.)

$$
\begin{align*}
\frac{\mathrm{sl} \frac{(B \otimes G(G \otimes H)) \otimes C}{((B \otimes G) \otimes C) \otimes H}}{(B \otimes C) \otimes (G \otimes H)} &\qquad \frac{\bar{\mathrm{sl}} \frac{(B \otimes \perp) \otimes C}{B \otimes C}}{\perp \frac{\bar{\mathrm{sl}} \frac{(B \otimes \perp) \otimes C}{(B \otimes C) \otimes \perp}}{(B \otimes C) \otimes \perp}} \\
&\qquad \frac{\bar{\mathrm{cc}} \frac{\bar{\mathrm{dt}} \frac{(B \otimes G(G \& H)) \otimes C}{((B \otimes G) \otimes C) \& ((B \otimes H) \otimes C)}}{\mathrm{sl} \frac{\bar{\mathrm{dt}} \frac{(B \otimes G) \otimes C}{((B \otimes G) \otimes C) \& ((B \otimes C) \otimes H)}}{\mathrm{sl} \frac{\bar{\mathrm{dt}} \frac{\bar{\mathrm{dc}} \frac{(B \otimes G) \otimes C}{((B \otimes G) \otimes C) \otimes H}}{(B \otimes C) \otimes (G \otimes H)}}} \\
&\qquad \frac{\bar{\mathrm{g}} \frac{\bar{\mathrm{c}} \frac{(B \otimes \top) \otimes C}{\top \otimes C}}{\mathrm{ga} \frac{\bar{\mathrm{g}} \frac{\bar{\mathrm{c}} \frac{(B \otimes \top) \otimes C}{(B \otimes C) \otimes \top}}{\mathrm{g} \frac{\bar{\mathrm{c}} \frac{(B \otimes \top) \otimes C}{(B \otimes C) \otimes \top}}{\mathrm{g}}}}}{\mathrm{g} \frac{\bar{\mathrm{c}} \frac{(B \otimes \top) \otimes C}{(B \otimes C) \otimes \top}}{\mathrm{g} \frac{\bar{\mathrm{c}} \frac{(B \otimes \top) \otimes C}{(B \otimes C) \otimes \top}}{\mathrm{g}}}}
\end{align*}
$$

The cases for sr are similar.

□

The second step of the transformation of LS proofs to LSS proofs involves the following *partial switch* synthetic rule:

$$
\mathrm{ps}_F \frac{\nu\{\uparrow\pi_\otimes\{\downarrow(\uparrow P \otimes L)\}\}}{\nu\{\uparrow\pi_\otimes\{P\} \otimes L\}}
$$

This rule has more shifts in the premise than in the conclusion and is therefore not derivable in LSS. It can permute above any rule in LSS \ {saIF, spcF, sprF}. Before we can show that psF can always be eliminated from any proof of LSS, we need a lemma stating that $\downarrow\uparrow$ can be removed from an LSS proof with the use of psF.

**Lemma 24.** If there is a proof $\mathcal{D}$ of a negative formula $\pi\{\downarrow\uparrow P\}$ in LSS $\cup \{\text{ps}_F\}$, then there is a proof of $\pi\{P\}$ in LSS $\cup \{\text{ps}_F\}$ of at most the same height as $\mathcal{D}$.

*Proof.* Proceed by induction on the height of $\mathcal{D}$. In the base case, $\pi\{\downarrow\uparrow P\}$ is $\uparrow\downarrow\uparrow 1$ and the result is immediate. In the general case, consider the bottommost rule instance $r$ in $\mathcal{D}$; in most cases the induction hypothesis is directly applicable so the pair of shifts can simply be removed. The only interesting case is where $r$ is a matching instance of $\text{spc}_F$. We replace it by an instance of $\text{ps}_F$ as follows:

$$
\mathrm{spc}_F \frac{\nu\{\uparrow\pi_\otimes\{\downarrow(\uparrow P \otimes L)\}\}}{\nu\{\uparrow\pi_\otimes\{\downarrow\uparrow P\} \otimes L\}} \rightarrow \mathrm{ps}_F \frac{\nu\{\uparrow\pi_\otimes\{\downarrow(\uparrow P \otimes L)\}\}}{\nu\{\uparrow\pi_\otimes\{P\} \otimes L\}}
$$

□

**Remark 25.** Note that we also have the converse: if there is a proof of $\pi\{P\}$ in LSS $\cup \{\text{ps}_F\}$, then there is also a proof of $\pi\{\downarrow\uparrow P\}$ in LSS $\cup \{\text{ps}_F\}$.

**Lemma 26.** For every $N$, if $\lfloor N \rfloor$ is provable in $LS^r$, then $N$ is provable in $LSS \cup \{ps_F\}$.

*Proof.* Proceed by induction on the height of the LS' proof $\mathcal{D}$ of $\lfloor N \rfloor$ to build a proof of $N$ in LSS $\cup \{\text{ps}_F\}$. The base case, where $\lfloor N \rfloor$ is 1, is trivial. Now make a case analysis for the bottommost rule instance $r$ in $\mathcal{D}$. In most cases, we can simply replace $r$ with the corresponding rule in LSS, and appeal to the induction hypothesis on the proof above $r$. The four interesting cases involve $r$ being an instance of $\mathrm{ai}_\downarrow$, $\mathrm{sl}^r$, $\mathrm{sr}^r$, or $\mathrm{pr}_\downarrow$. We can apply the induction hypothesis to the proof above $r$ and glue the result to one the following rule instances depending on the case:

$$
\mathrm{saIF} \frac{\nu\{\uparrow 1\}}{\nu\{\uparrow a \otimes \bar{a}\}} \qquad \mathrm{psF} \frac{\nu\{\uparrow(\downarrow(\uparrow P \otimes L) \otimes Q)\}}{\nu\{\uparrow(P \otimes Q) \otimes L\}} \qquad \mathrm{psF} \frac{\nu\{\uparrow(P \otimes \downarrow(\uparrow Q \otimes L))\}}{\nu\{\uparrow(P \otimes Q) \otimes L\}} \qquad \mathrm{sprF} \frac{\nu\{\uparrow!(N \otimes ?P)\}}{\nu\{\uparrow!N \otimes ?P\}}
$$

If the premises and conclusions do not match (because of extra $\downarrow\uparrow$ pairs) we appeal to Lemma 24 and
Remark 25 above.

$\square$

**Lemma 27.** The rule ps<sub>F</sub> is height-preserving admissible in LSS.

*Proof.* Given a proof $\mathcal{D}$ of a negative formula $N$ in LSS $\cup \{\text{ps}_F\}$, we prove by induction on the height of $\mathcal{D}$ that there is a proof of $N$ in LSS of at most the same height as $\mathcal{D}$. In the base case, $N$ is $\uparrow 1$ and we are done. In the general case, we case-analyze the bottommost rule instance $r$ in $\mathcal{D}$. If this is not an instance of $\text{ps}_F$, we appeal to the induction hypothesis on the proof above $r$ and compose the result with $r$. In the case where $r$ is an instance of $\text{ps}_F$, we consider the rule instance $r_1$ above $r$ in $\mathcal{D}$, and consider the cases for $r_1$. If $r_1$ is not a synthetic rule, then we can permute $r$ up above $r_1$ and then appeal to the induction hypothesis on the proof now above $r_1$. If $r_1$ was an instance of $\text{ct}_F$ or $\text{dt}_F$, then we need to appeal to the induction hypothesis twice, which is possible because our reduction does not increase the height of $\mathcal{D}$. If
$r_1$ was $wk_F$ or $gc_F$, we do not need to appeal to the induction hypothesis. If $r_1 \in \{sai_F, spc_F, spr_F\}$, we merge $r$ and $r_1$ by replacing them with a new instance of $r_1$, as follows:

$$ \frac{\nu\{\uparrow\pi_{\otimes}\{\downarrow\uparrow\rho_{\otimes}\{1\}\}\}}{\nu\{\uparrow\pi_{\otimes}\{\downarrow\uparrow\rho_{\otimes}\{a\} \otimes \bar{a}\}\}} \downarrow $$

$$ \frac{\nu\{\uparrow\pi_{\otimes}\{\downarrow\uparrow\rho_{\otimes}\{\downarrow(M \otimes L)\}\}}{\nu\{\uparrow\pi_{\otimes}\{\downarrow\uparrow\rho_{\otimes}\{\downarrow M\} \otimes L\}\}} \downarrow $$

$$ \frac{\nu\{\uparrow\pi_{\otimes}\{\downarrow\uparrow\rho_{\otimes}\{!(M \otimes ?P)\}\}}{\nu\{\uparrow\pi_{\otimes}\{\downarrow\uparrow\rho_{\otimes}\{!M\} \otimes ?P\}\}} \downarrow $$

$$ \frac{\nu\{\uparrow\pi_{\otimes}\{\rho_{\otimes}\{1\}\}\}}{\nu\{\uparrow\pi_{\otimes}\{\rho_{\otimes}\{a\} \otimes \bar{a}\}\}} $$

$$ \frac{\nu\{\uparrow\pi_{\otimes}\{\rho_{\otimes}\{\downarrow(M \otimes L)\}\}}{\nu\{\uparrow\pi_{\otimes}\{\rho_{\otimes}\{\downarrow M\} \otimes L\}\}} $$

$$ \frac{\nu\{\uparrow\pi_{\otimes}\{\rho_{\otimes}\{!(M \otimes ?P)\}\}}{\nu\{\uparrow\pi_{\otimes}\{\rho_{\otimes}\{!M\} \otimes ?P\}\}} $$

Now we apply Lemma 24 to the proof above $r_1$ to get a proof $\mathcal{D}'$, with a conclusion matching the premise of the new instances resulting from the merge. We appeal to the induction hypothesis on $\mathcal{D}'$ and plug the result above the merged instance. Lastly, if $r_1$ is also an instance of $ps_F$, then we appeal to the induction hypothesis on the proof above $r_1$ and apply the technique used for the other cases. □

We now have all the ingredients for the completeness theorem for LSS.

**Theorem 28.** For any $N$, if $\lfloor N \rfloor$ is provable in LS, then $N$ is provable in LSS.

*Proof.* Let a proof of $\lfloor N \rfloor$ in LS be given. By Lemma 23, there is a proof of $\lfloor N \rfloor$ in LS'. By Lemma 26, we have a proof of $N$ in LSS $\cup \{ps_F\}$, and thus by Lemma 27 also in LSS. □

Note that since LSS and LSF are equivalent, Theorem 28 also proves the completeness of LSF with respect to LS.

# 4 Comparing Sequent and Structural Focusing

In order to justify the adjective “focused” for LSF, it is important to give a precise comparison with LLKF. In this section we shall prove that every LLKF proof can be simulated in LSF, and, conversely, every LSF proof has a corresponding LLKF proof. Both results are surprising, as there is no reason a priori that the two systems should have a close correspondence. Indeed, there are significant differences such as the treatment of weakening and contraction and the incremental splitting of contexts around $\otimes$.

## 4.1 Simulating LLKF in LSF

First, let us simulate LLKF proofs in LSF, i.e., show that LSF is adequate with respect to LLKF. The two proof systems are not isomorphic, so we use an abstraction.

**Definition 29.** For a non-empty LLKF sequent $\sigma$ and a polarized formula $A$, we say that $A$ is a structural interpretation of $\sigma$, written $A \approx \sigma$, iff it can be derived from these rules:

$$ \frac{P \approx (\vdash \cdot ; [P])}{\phantom{\approx}} $$

$$ \frac{Q \approx (\vdash \Gamma ; \Pi, [P])}{(Q \circled{0} L) \approx (\vdash \Gamma ; \Pi, L, [P])} $$

$$ \frac{Q \approx (\vdash \Gamma, P ; \Pi, [P'])}{(Q \circled{0} ?P) \approx (\vdash \Gamma, P ; \Pi, [P'])} $$

$$ \frac{Q \approx (\vdash \Gamma ; \Pi, [P'])}{Q \approx (\vdash \Gamma, P ; \Pi, [P'])} $$

$$ \frac{N \approx (\vdash \cdot ; N)}{\phantom{\approx}} $$

$$ \frac{M \approx (\vdash \Gamma ; \Delta)}{(M \otimes N) \approx (\vdash \Gamma ; \Delta, N)} $$

$$ \frac{M \approx (\vdash \Gamma, P ; \Delta)}{(M \otimes ?P) \approx (\vdash \Gamma, P ; \Delta)} $$

$$ \frac{M \approx (\vdash \Gamma ; \Delta)}{M \approx (\vdash \Gamma, P ; \Delta)} $$

In other words, structural interpretations can arbitrarily reorder the LLKF sequent and potentially erase or duplicate the unrestricted formulas, but they must preserve the multiplicities of the linear formulas. The simulation theorem shows that LSF can preserve the structural interpretations of each rule of LLKF.

**Theorem 30 (simulation).** For any $\Gamma$, $\Delta$, $\Pi$, and $P$,

* If $\vdash \Gamma ; \Pi, [P]$ in LLKF, then there is a $Q \approx (\vdash \Gamma ; \Pi, [P])$ such that $\frac{1}{Q} \| \text{LSF} \|$.

* If $\vdash \Gamma ; \Delta$ in LLKF, then there is a $N \approx (\vdash \Gamma ; \Delta)$ such that $\frac{1}{N} \| \text{LSF} \|$.

*Proof.* By structural induction on the given LLKF proofs. We show here a few representative cases for the final rule in the LLKF proof.
1. One of the structural rules wdc or dc. For instance:

$$ \frac{\vdash \Gamma, P ; \Pi, [P]}{\vdash \Gamma, P ; \Pi} $$

By the inductive hypothesis, there is a $Q \approx (\vdash \Gamma, P ; \Pi, [P])$ such that $\|_{\text{LSF}}^1$. Note that $Q$ must be of the form $P \circled A_1 \circled \dots \circled A_n$ such that $(A_1 \gtrdot \dots \gtrdot A_n) \approx (\vdash \Gamma, P ; \Pi)$. If there is a $k \in 1..n$ such that $A_k = ?P$, then we have:

$$ \begin{array}{l} 1 \\ \|^{\text{i.h.}} \\ P \circled A_1 \circled \dots \circled A_n \\ ?_{\Gamma, \text{int}_F} \\ ?P \gtrdot A_1 \gtrdot \dots \gtrdot A_n \\ \text{congruence} \\ A_1 \gtrdot \dots \gtrdot ?P \gtrdot A_k \gtrdot \dots \gtrdot A_n \\ \text{ct}_F \\ A_1 \gtrdot \dots \gtrdot ?P \gtrdot \dots \gtrdot A_n \end{array} $$

Otherwise, we have:

$$ \begin{array}{l} 1 \\ \|^{\text{i.h.}} \\ P \circled A_1 \circled \dots \circled A_n \\ ?_{\Gamma, \text{int}_F} \\ ?P \gtrdot A_1 \gtrdot \dots \gtrdot A_n \end{array} $$

In each case, the conclusion $\approx (\vdash \Gamma, P ; \Pi)$.

2. A positive rule such as $\otimes$:

$$ \otimes \frac{\vdash \Gamma ; \Pi_1, [P_2] \quad \vdash \Gamma ; \Pi_2, [P_2]}{\vdash \Gamma ; \Pi_1, \Pi_2, [P_1 \otimes P_2]} $$

By the induction hypothesis, there are LSF-derivable $Q_1 \approx (\vdash \Gamma ; \Pi_1, [P_1])$ and $Q_2 \approx (\vdash \Gamma ; \Pi_1, [P_2])$. Again, note that $Q_1$ must be of the form $P_1 \circled A_1 \circled \dots \circled A_m$ and $Q_2$ must be of the form $P_2 \circled B_1 \circled \dots \circled B_n$ where $(A_1 \gtrdot \dots \gtrdot A_m) \approx (\vdash \Gamma ; \Pi_1)$ and $(B_1 \gtrdot \dots \gtrdot B_n) \approx (\vdash \Gamma ; \Pi_2)$. We then have:

$$ \begin{array}{l} \frac{1}{1 \otimes 1} \\ \|^{\text{i.h.}} \\ (P_1 \circled A_1 \circled \dots \circled A_m) \otimes (P_2 \circled B_1 \circled \dots \circled B_n) \\ \text{sl}_{\Gamma, \text{sr}_{\Gamma}} \\ (P_1 \otimes P_2) \circled A_1 \circled \dots \circled A_m \circled B_1 \circled \dots \circled B_n \end{array} $$

It is easy to see that the conclusion $\approx (\vdash \Gamma ; \Pi_1, \Pi_2, [P_1 \otimes P_2])$.

3. A negative rule, such as $\&$.

$$ \& \frac{\vdash \Gamma ; \Delta, M_1 \quad \vdash \Gamma ; \Delta, M_2}{\vdash \Gamma ; \Delta, M_1 \& M_2} $$

By the induction hypothesis, there are LSF-derivable $N_1 \approx (\vdash \Gamma ; \Delta, M_1)$ and $N_2 \approx (\vdash \Gamma ; \Delta, M_2)$. By definition, $N_1$ and $N_2$ must be of the form $M_1 \gtrdot A_1 \gtrdot \dots \gtrdot A_m$ and $M_2 \gtrdot B_1 \gtrdot \dots \gtrdot B_n$, respectively, where both $(A_1 \gtrdot \dots \gtrdot A_m)$ and $(B_1 \gtrdot \dots \gtrdot B_n) \approx (\vdash \Gamma ; \Delta)$. Therefore, there are $C_1, \dots, C_u$ such that $\{A_1, \dots, A_m\} \subseteq \text{multiset } \{C_1, \dots, C_u\}$, $\{B_1, \dots, B_n\} \subseteq \text{multiset } \{C_1, \dots, C_u\}$, and $(C_1 \gtrdot \dots \gtrdot C_u) \approx (\vdash \Gamma ; \Delta, M_1)$.
Γ ; Δ). Note that {$C_1, \dots, C_u$} \ {$A_1, \dots, A_m$} and {$C_1, \dots, C_u$} \ {$B_1, \dots, B_n$} must be only ?-formulas. Thus, we have:

$$
\begin{array}{c}
\frac{\uparrow 1}{\uparrow 1 \& \uparrow 1} \\
\| \text{i.h.} \\
(M_1 \mathring{\omega} A_1 \mathring{\omega} \cdots \mathring{\omega} A_m) \& (M_2 \mathring{\omega} B_1 \mathring{\omega} \cdots \mathring{\omega} B_n) \\
\mathring{w}_{k_F} \\
\| \\
(M_1 \mathring{\omega} C_1 \mathring{\omega} \cdots \mathring{\omega} C_u) \& (M_2 \mathring{\omega} C_1 \mathring{\omega} \cdots \mathring{\omega} C_u) \\
\mathring{d}_{t_F} \\
\| \\
(M_1 \& M_2) \mathring{\omega} C_1 \mathring{\omega} \cdots \mathring{\omega} C_u
\end{array}
$$

The conclusion is manifestly $\approx (\vdash \Gamma ; \Delta, M_1 \& M_2)$.

☐

**Corollary 31 (completeness).** If $\vdash P_1, \dots, P_m$; $N_1, \dots, N_n$ is provable in LLKF, then $N_1 \mathring{\omega} \dots \mathring{\omega} N_n \mathring{\omega} ? P_1 \mathring{\omega} \dots \mathring{\omega} ? P_m$ is provable in LSF.

*Proof.* We have:

$$
\begin{array}{c}
\frac{}{\displaystyle\uparrow 1} \\
\left\| \vphantom{\begin{array}{@{}c@{}}\displaystyle\text{Theorem 30}\\
\text{\scriptsize\textbf{~~$\|\|$}}\end{array}} \right. \\
N_1 \mathring{\omega} \cdots \mathring{\omega} N_n \mathring{\omega}^{u_1} ? P_1 \mathring{\omega}^{u_2} \cdots \mathring{\omega}^{u_m} ? P_m \\
\mathring{c}_{t_F, w_{k_F}} \\
\| \\
N_1 \mathring{\omega} \cdots \mathring{\omega} N_n \mathring{\omega} ? P_1 \mathring{\omega} \cdots \mathring{\omega} ? P_m
\end{array}
$$

where $M_1 \mathring{\omega}^u M_2$ stands for $M_1 \mathring{\omega} \underbrace{(M_2 \mathring{\omega} \cdots \mathring{\omega} M_2)}_{u \text{ times}}$ if $u \ge 1$, and for $M_1$ if $u = 0$. ☐

☐

**4.2 Extracting LLKF Proofs from LSF Proofs**

Let an LSF proof $\mathcal{D}$ with conclusion $N_0$ be given. We present here an algorithm that extracts an LLKF
proof of $\vdash \cdot ; N_0$ that has the same focusing behaviour as the LSF proof, i.e. make the same decisions
in the LLKF proof as the instances of $\text{int}_F$ in the LSF proof, and splitting the formulas in the same was
as the instances of $\text{sl}_F$ and $\text{sr}_F$ in the LSF proof. The strategy we will use is to do guided focused proof
search in LLKF from the end-sequent upwards, using information in the LSF proof as an oracle at every
choice point. There are, in fact, only the following “don’t know” choices in an LLKF proof (cf. Figure 3).

* Which formula to decide on using wdc or dc;

• How to divide the context in the $\otimes$ rule; and

• Which of $\oplus l$ or $\oplus r$ to use.

These correspond to the following choice points in an LSF proof:

* In the int<sub>F</sub> rule which ↑P to select for focus, and in the ?<sub>F</sub> rule which ?P to derelict to a ↑P;

• Which of sl<sub>F</sub> or sr<sub>F</sub> to use;

• Which of $\oplus l_F$ or $\oplus r_F$ to use; and

• When to use ct<sub>F</sub> or wk<sub>F</sub>.

The first three points of each case are aligned, but the fourth point is a peculiarity of LSF. In fact ct<sub>F</sub>
and dt<sub>F</sub> are the only rules that copy a formula in the conclusion into two copies in the premise, while wk<sub>F</sub>
and gc<sub>F</sub> are the only rules that can delete an arbitrary formula in the conlcusion.

We will now present an algorithm to use the LSF proof as an oracle.

It will consist of two steps. First, the instances of contraction (ct<sub>F</sub>) are moved to the bottom of the LSF derivation, and a precise record of the sequence of contractions is produced by labelling the active and reactive formulas. This phase determines the formulas that are to be decided on in the extracted LLKF proof. Next, in the contraction-free upper half of the proof, we compute a dependency relation between the labelled (contracted copies of) the active and reactive formulas. The goal of this second step is to extract an order of focusing decisions (wdc and dc) in the LLKF proof. This phase is not entirely trivial in the presence of additive connectives, because in the two additive branches of a & it is entirely possible to focus on the same formulas in different orders. Therefore, we will need to further annotate the LSF proof with information about additive *slices*.
**Definition 32.** An infinite set $\mathcal{L}$ of atomic labels is fixed. A label (written $\alpha, \beta, \dots$) is a pair of the form $(\sigma, \alpha)$ where $\alpha$ is an atomic label and $\sigma: \mathcal{L} \to \{1, 2\}$ is an assignment of the constants 1 or 2 to a subset of atomic labels. The two components of the label will be called the *slice* and the *decision*, respectively. We will use $\Lambda$ to denote a multi-set of labels.

We modify the grammar of formulas as follows to allow labelling the (re)active and $\&$-formulas.

$$ P, Q ::= a_{\alpha} \mid !_{\alpha} N \mid \downarrow_{\alpha} N \mid P \otimes Q \mid 1 \mid P \oplus Q \mid 0 \mid P \diamond N $$
$$ N, M ::= \bar{a}_{\alpha} \mid ?_{\alpha} P \mid \uparrow_{\alpha} P \mid N \&_{\alpha} M \mid \top \mid N \ominus M \mid \bot $$

We use $A_{\alpha}$ to denote that the formula $A$ has label $\alpha$ for its top-level connective; we will not use this notation in situations where the top-level

connective is not labelled.

The rules of LSF $\setminus \{ct_F\}$ (Figure 4) are modified to be label-sensitive. The labelling is only an annotation: it does not change the soundness and completeness of the calculus with respect to the unlabelled LSF $\setminus \{ct_F\}$. Let us call a formula *well-labelled* if all the labels that occur in it are pairwise distinct, and let us assume that the end-formula $N_0$ is well-labelled. Besides contraction, there is only a single rule in LSF that copies an entire subformula and therefore breaks well-labelling: $dt_F$. Let us quickly talk about the remaining rules: most of these rules are not specific to the structure of active and reactive formulas and are therefore unaltered from their unlabelled versions. Here are the ones that do analyze the structure of an active or a reactive formula.

$$ \text{int}_{\text{F}} \frac{\nu\{\uparrow_{\alpha}(P \oplus L_{v})\}}{\nu\{\uparrow_{\alpha}P \ominus L_{v}\}} \quad \text{ai}_{\text{F}} \frac{\pi\{1\}}{\pi\{a_{\alpha} \oplus \bar{a}_{\beta}\}} \quad \text{pc}_{\text{F}} \frac{\pi\{\downarrow_{\alpha}(N \ominus L_{\beta})\}}{\pi\{\downarrow_{\alpha}N \oplus L_{\beta}\}} \quad \text{pr}_{\text{F}} \frac{\pi\{!_{\alpha}(N \ominus ?_{\beta}P)\}}{\pi\{!_{\alpha}N \oplus ?_{\beta}P\}} \quad ?_{\text{F}} \frac{\nu\{\uparrow_{\alpha}P\}}{\nu\{?_{\alpha}P\}} \quad \text{wk}_{\text{F}} \frac{\nu\{\bot\}}{\nu\{?_{\alpha}P\}} $$

The fix to the $dt_F$ rule that makes it preserve well-labelling requires a fairly straightforward definition.

**Definition 33.** Given a labelled formula $A$, we write

In order to modify $dt_F$ to preserve well-labelling, we us the slice string portions of the labels. Let us write $1 \cdot A$ (respectively, $2 \cdot A$) to stand for the formula that modifies every label $\alpha$ in $A$ to $1\alpha$ (respectively, to $2\alpha$). Note that if $A$ is well-labelled, then so is $1 \cdot A \ominus 2 \cdot A$. This leads directly to the version of $dt_F$ that preserves well-labelling.

$$ \text{dt}_{\text{F}} \frac{\nu\{(M_1 \ominus 1 \cdot N) \& (M_2 \ominus 2 \cdot N)\}}{\nu\{(M_1 \& M_2) \ominus N\}} $$

Observe that, since the slice labels are prefixed to the side-formula in the rule, the order in which the $\&$s are decomposed is immaterial. To illustrate, consider the following pair of derivations of $(M_1 \& M_2) \ominus (N_1 \& N_2)$; up to congruence, we obtain the same premise regardless of which $\&$ is analyzed first.

$$ \frac{(1 \cdot M_1 \& 1 \cdot N_1) \& (2 \cdot N_1 \& 1 \cdot M_2) \& (1 \cdot N_2 \& 2 \cdot N_1) \& (2 \cdot N_2 \& 2 \cdot N_2)}{(M_1 \& 1 \cdot (N_1 \& N_2)) \& (M_2 \& 2 \cdot (N_1 \& N_2))} $$

For $ct_F$, the labels $u_1$ and $u_2$ in the premise are assumed to be different from each other and from all labels in the conclusion of the rule. It is easy to see that the $ct_F$ rule preserves well-labelling when read from conclusion to premise. Thus, the formula that interpolates between the contraction and the contraction-free phase of the modified LSF proof will also be well-labelled.

The rules $\{\text{int}_F, \text{ai}_F, \text{pr}_F, \text{pc}_F\}$ in the first line above induce an ordering, written $<$, among the labels, with $u < v$ in each case. The rules $ct_F$ and $wk_F$ induce a rewrite relation $\rightsquigarrow$ on multi-sets of labels that tracks the exponential uses of $?$-formulas. We assume that if $u < v$ and $\{v\} \rightsquigarrow \Lambda, w$, then $u < w$. We label all active and reactive formulas in $N_0$ with unique labels and label every rule instance in $\mathcal{D}$ as above. Let us use LLSF to denote this labelled version of LSF.

**Theorem 34.** The relation $\leq$, which is the reflexive-transitive closure of the induced $<$, is a partial order.

*Proof.* The bases cases of $<$ induced by the LLSF derivation $\square$

Note that the reflexive-transitive closure of this label ordering, written $\leq$, is a partial order.

Our algorithm will extract a labelled LLKF proof of $\vdash \cdot ; N_0$ where the unrestricted contexts contain positive formulas annotated with a multi-set of labels, i.e., their elements will be of the form $P_{\Lambda}$. The
wdc rule is modified to consume one of the available labels in this multi-set; if this multi-set is empty, then the rule is inapplicable. Likewise, the dc rule consumes the label of the linear reactive formula. Finally, in the ? rule, the label of the ? is normalized with respect to ↝.

$$ \begin{array}{c} \text{wdc} \\ \vdash \Gamma, P_{\Lambda} ; \Pi, [P] \\ \vdash \Gamma, P_{\Lambda,u} ; \Pi \end{array} \qquad \begin{array}{c} \text{dc} \\ \vdash \Gamma ; \Pi, [P] \\ \vdash \Gamma ; \Pi, \uparrow_u P \end{array} \qquad ? \frac{\{u\} \stackrel{\sim}{\Lambda}) \vdash \Gamma, P_{\Lambda} ; \Delta \\ \vdash \Gamma ; \Delta, ?_u P} \end{array} $$

The remaining rules of LLKF (Figure 3) can be modified to use labelled formulas in a straightforward manner. We say that a label is available in a labelled LLKF sequent if it is the label of some top-level formula in the sequent. The extraction of the labelled LLKF proof of $\vdash \cdot ; N_0$ proceeds by backwards proof search (i.e., proof search from this goal sequent upwards by applying LLKF rules from conclusion to premises) with some constraints:

* For a negative sequent for which there are available negative rules (i.e., rules in the negative phase in Figure 3), we apply one of these rules. The choice and order of the application of these rules is immaterial.

* From a negative sequent where no negative rules apply, we pick the unique $\leq$-smallest label from the available labels, and use wdc or dc as appropriate. Each pair of formulas in such a sequent has a corresponding pair of formulas in a $\omega$-relation in $\mathcal{D}$. Because we normalize with respect to $\rightsquigarrow$, every surviving available label in this sequent is involved in some instance of $\text{int}_F$ with another available label of the sequent in $\mathcal{D}$. Thus, the available labels are $\leq$-connected, and, because there is a sub-proof in $\mathcal{D}$ of the $\omega$-formula corresponding to this sequent, there is always a unique $\leq$-smallest label.

* For the $\otimes$ rule of LLKF focused on $P \otimes Q$, we send those side formulas to the premise involving $P$ whose labels are $\leq$-larger than some label of a subformula of $P$, and the rest to the premise involving $Q$. There is no splitting ambiguity: the sets of labels in subformulas of $P$ and $Q$ are disjoint because the labelling is unique.

* For $\oplus$, we repeat the same choices made in $\mathcal{D}$.

This algorithm is deterministic and always succeeds: it has no choice points that require backtracking. There are no labels in any subformula of 1, so no formula will ever be sent to a branch of a $\otimes$ that has focus on 1, guaranteeing that its LLKF rule will succeed. Similarly, the sole formula that can be sent to a branch with focus on $a_u$ will be a formula $\bar{a}_v$ with $u < v$, and therefore the id rule of LLKF will succeed. Lastly, the only formulas that have labels $\leq$-greater than a $!$-formula are $?$-formulas, as ensured by the $\text{pr}_F$ rule in LSF, so the corresponding $!$ rule of LLKF succeeds. The algorithm terminates because each decision rule consumes one of the finitely many labels of $\mathcal{D}$. We can erase the labels from the computed labelled LLKF proofs as a post-processing step.

## References

[1] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. *J. of Logic and Computation*, 2(3):297–347, 1992.

[2] Arnon Avron. The method of hypersequents in the proof theory of propositional non-classical logics. In *Logic: from foundations to applications: European logic colloquium*, pages 1–32. Clarendon Press, 1996.

[3] David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In N. Dershowitz and A. Voronkov, editors, *International Conference on Logic for Programming and Automated Reasoning (LPAR)*, volume 4790 of *Lecture Notes in Computer Science*, pages 92–106, 2007.

[4] Nuel D. Belnap, Jr. Display logic. *J. of Philosophical Logic*, 11:375–417, 1982.

[5] Kai Brünnler. Deep sequent systems for modal logic. *Archive for Mathematical Logic*, 48(6):551–577, 2009.

[6] Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors, *LPAR 2001*, volume 2250 of *LNAI*, pages 347–361. Springer, 2001.
[7] Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. *ACM Trans. on Computational Logic*, 10(2), 2009.

[8] Kaustuv Chaudhuri. Focusing strategies in the sequent calculus of synthetic connectives. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, *LPAR: International Conference on Logic, Programming, Artificial Intelligence and Reasoning*, volume 5330 of *Lecture Notes in Computer Science*, pages 467–481. Springer, November 2008.

[9] Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The focused calculus of structures. In Marc Bezem, editor, *CSL'11*, volume 12 of *LIPIcs*, pages 159–173. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2011.

[10] Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Focused and synthetic nested sequents. In Bart Jacobs and Christof Löding, editors, *Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)*, volume 9634 of *Lecture Notes in Computer Science*, April 2016.

[11] Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. In *FSCD 2016 - 1st International Conference on Formal Structures for Computation and Deduction*, Porto, Portugal, June 2016.

[12] Nicolas Guenot. Focused proof search for linear logic in the calculus of structures. In Manuel V. Hermenegildo and Torsten Schaub, editors, *Technical Communications of the 26th International Conference on Logic Programming (ICLP 2010)*, volume 7 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 84–93, Edinburgh, United Kingdom, July 2010. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.

[13] Nicolas Guenot and Lutz Strassburger. Symmetric normalisation for intuitionistic logic. In Tom Henzinger and Dale Miller, editors, *Proceedings of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, 2014.

[14] Alessio Guglielmi. A system of interaction and structure. *ACM Trans. on Computational Logic*, 8(1):1–64, 2007.

[15] Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, *Computer Science Logic, CSL 2001*, volume 2142 of LNCS, pages 54–68. Springer-Verlag, 2001.

[16] Olivier Laurent. *Etude de la Polarisation en Logique*. PhD thesis, Univ. Aix-Marseille II, 2002.

[17] Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, May 2004.

[18] Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. *Theoretical Computer Science*, 410(46):4747–4768, 2009.

[19] Dale Miller and Alexis Saurin. From proofs to focused proofs: a modular proof of focalization in linear logic. In J. Duparc and T. A. Henzinger, editors, *CSL 2007: Computer Science Logic*, volume 4646 of Lecture Notes in Computer Science, pages 405–419. Springer, 2007.

[20] P. O'Hearn and D. Pym. The logic of bunched implications. *Bulletin of Symbolic Logic*, 5(2):215–244, June 1999.

[21] Lutz Straßburger. A local system for linear logic. In Matthias Baaz and Andrei Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002*, volume 2514 of LNAI, pages 388–402. Springer-Verlag, 2002.

[22] Lutz Straßburger. *Linear Logic and Noncommutativity in the Calculus of Structures*. PhD thesis, Technische Universität Dresden, 2003.

[23] Lutz Straßburger. MELL in the Calculus of Structures. *Theoretical Computer Science*, 309(1–3):213–285, 2003.

[24] Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: The exponentials and decomposition. *ACM Trans. Comput. Log.*, 12(4):23, 2011.
[25] Alwen Fernanto Tiu. A system of interaction and structure II: The need for deep inference. *Logical Methods in Computer Science*, 2(2):1-24, 2006.

[26] Andrea Aler Tubella. *A study of normalisation through subatomic logic*. PhD thesis, University of Bath, 2017.