# Light logics with inductive and coinductive types: a uniform account of cut-elimination

Esaïe Bauer, Alexis Saurin

► To cite this version:

Esaïe Bauer, Alexis Saurin. Light logics with inductive and coinductive types: a uniform account of cut-elimination. 2024. hal-04692386

HAL Id: hal-04692386

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

Preprint submitted on 9 Sep 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Light logics with inductive and coinductive types: a uniform account of cut-elimination

Esâie BAUER & Alexis SAURIN

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

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

Université Paris Cité & CNRS & INRIA, Pl. Aurélie Nemours, 75013 Paris, France

## Abstract

In this paper, we explore the connection between fixed-point and parametrized modalities in linear logic. We tackle this by examining a broad range of systems, taking inspiration from the subexponential system from Nigam and Miller and the super exponential system from Bauer and Laurent. Our work is inspired by Baillot's research on light linear logics with recursive types, but also extends to systems with multiple modalities not necessarily exponential, like Bauer and Saurin's modal calculus-based linear system. Unlike Baillot's approach, we focus on inductive and coinductive types in a non-wellfounded context, rather than finite recursive types. We introduce a new non-wellfounded system, $\mu$-superLL, which is a variant of superLL with fixed-point, and prove a syntactic cut-elimination for it using methods from non-wellfounded linear logic.

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

**Keywords and phrases** linear logic, proof theory, sequent calculus, cut elimination, fixed-points, non-wellfounded proofs, exponential modalities, subexponentials

## 1 Introduction

**On the redundancy of cut-elimination proofs.** While cut-elimination is certainly a cornerstone of structural proof theorem since Gentzen's introduction of the sequent calculus, an annoying fact is that a slight change in a proof system induce the need to reprove globally the cut-elimination property and that such re-proofs are usually quite boring and fastiduous, often lacking any new insight: cut-elimination results lack modularity. There are mainly two directions to try and make cut-elimination results more uniform.

The first option consists in proving a new cut-elimination results from a previously obtains theorem by means of translation between proof systems, allowing to reduce the cut-elimination property of a given system to that of another one for which the property is already known. Very frequent in term-calculi such as the variants of the $\lambda$-calculus, such an approach is also applied in proof theory for instance in translations between classical, intuitionistic and linear logics [10, 11]. A more recent application of this approach is Saurin's proof of cut-elimination for the circular system of linear logic extended with least and greatest fixed-points, $\mu LL^\infty$, which is proved [18] by a reduction to the cut-elimination property of the exponential-free fragment of the logic [2].

The second option consists in abstracting properties ensuring that cut-elimination holds in a sequent calculus, and to provide sufficient condition for cut-elimination to hold. For instance, after Miller and Nigam's work on subexponentials [16] providing a family of logic extending LL with exponential admitting various structural rules, Bauer and Laurent provided a systematic and generic setting that captures most of the light logics to be found in the literature [12, 14], superLL, for which they provided a uniform proof of cut-elimination based on an axiomatization stating a set of sufficient conditions for cut-elimination to hold [6].

We will see in the present paper that both approaches can be mixed in an efficient way, providing a uniform cut-elimination proofs for a large family of logics that we call $\mu$superLL$^\infty$ and that extends both $\mu LL^\infty$ and super exponentials: we shall obtain a single proof for a large class of proof systems and, by relying on a proof translation-method, we shall not need
## 2 Super exponentials with fixed-points

do design a new termination measure, simply rely on simulation results from one logic to another.

**Light logics with least and greatest fixed points.** Modifying linear logic with new exponential connectives allows us to get complexity bounds on the cut-elimination process [12, 14]. Adding fixpoints in such logic enriches the study of complexity classes [3, 7, 17, 8], as well as the study of light $\lambda$-calculus enriched with fixpoints as in [4].

In [3], enriching *elementary affine logic* with fixpoints allows one to refine the complexity results from ELL, and to characterize a hierarchy of the elementary complexity classes. In [15], it is even shown that the fixpoint-free version of this logic gets a very different characterization of complexity bounds for similar types.

The systems we define in this article differ from those discussed in the previous paragraph: they use a wider variety of types, while our system allows infinite derivation trees. However, the principal type used to prove complexity bounds that uses fixpoints is the Scott binary words type, which is: $\mu\beta, \forall\alpha, (\beta \to \alpha) \to (\beta \to \alpha) \to (\alpha \to \alpha)$. Here, the fixpoint variable $\beta$ is always in a positive position, meaning that it is a valid type in our system. Moreover, assigning to $\mu$ the role of least fixed-points ensures that a proof of such type remains finite. This makes a stronger link between our systems and light systems from the literature.

**Linear modal $\mu$-calculus** The study of proof theory for certain logical systems via translations has been explored in [5]. Linear logic offers powerful tools for proof theory and translating systems like $\mu LK^\infty$ from [18] and $\mu LK_\Box^\infty$ [13] into linear systems makes the transfer of these tools to other systems efficient. In [5], a non-wellfounded linear version of the modal $\mu$-calculus, $\mu LL_\Box^\infty$, is defined as a target for a linear translation of $\mu LK_\Box^\infty$. This system is an instance of our $\mu$**superLL**$^\infty$ system.

**Organization and contributions of the paper.** The main contribution of this paper is a syntactic proof of cut-elimination of a large variety of parametrized linear systems. In Section 2, we recall some definitions and results about infinitary rewriting theory in linear logic; we also give definitions of a variant of super exponentials from [6]. We give in Section 3 a definition of our parametrized system, $\mu$**superLL**$^\infty$, which is **superLL** augmented with fixed-points. Finally, in Section 4, we define the (cut)-steps and provide the proof of our main theorem, the cut-elimination of $\mu$**superLL**$^\infty$, through an encoding into $\mu LL^\infty$.

## 2 Background

### 2.1 Linear logic and non-wellfounded proofs

In this paper, we will study proof theory of different systems of linear logic. It is much more convenient to work on one-sided sequents systems as proofs as well as the description of these systems are half the size compared to a two-sided sequents version. However, we can easily retrieve results from the one-sided systems on the two-sided system with translations between them as in [18] for instance.

#### 2.1.1 Formulas

We first give a definition of the (pre-)formulas of linear logic with the addition of fixed-points:

$$F, G ::= a \in \mathcal{A} \mid a^{\perp} \mid X \in \mathcal{V} \mid \mu X.F \mid \nu X.F \mid F \intercal G \mid F \otimes G \mid \perp \mid 1 \mid F \oplus G \mid F \& G \mid 0 \mid \top \mid ?F \mid !F.$$

Formulas of $\mu LL^\infty$ are such closed pre-formulas ($\mu$ and $\nu$ being binders for variables in $\mathcal{V}$). By considering the $\mu, \nu, X$-free formulas of this system, we get LL, the usual formulas of
<figure><img src="image_4.png" /><figcaption>Figure 1 one sided MALL rules</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 2 one sided exponential fragment of LL</figcaption></figure>

linear logic [11]. By considering the !,?-free formulas of it, we get the formulas $\mu\text{MALL}^{\infty}$ the multiplicative and additive linear logic with fixed points [2]. By considering the intersection of these two subset of formulas, we get the formulas of MALL the multiplicative and additive linear logic. The ?, !-fragment is called the exponential fragment of linear logic.

**► Definition 1 (Negation).** We define $(-)^{\perp}$ to be the involution on formulas satisfying:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \bot^{\perp} = 1 & X^{\perp} = X & (A_1 \otimes A_2)^{\perp} = A_1^{\perp} \not\approx A_2^{\perp} & (A_1 \& A_2)^{\perp} = A_1^{\perp} \oplus A_2^{\perp} \\ \top^{\perp} = 0 & a^{\perp} = a & (\mu X.F)^{\perp} = \nu X.F^{\perp} & (?F)^{\perp} = !F^{\perp} \end{array} $$

## 2.1.2 Sequent calculi

Before defining inference rules, we need the definition of a sequent:

**► Definition 2 (Sequent).** A sequent is a list of formulas $\Gamma$, that we usually write $\vdash \Gamma$.

**► Remark 1 (Derivation rules & ancestor relation).** Usually, in the literature, derivation rules are defined as a scheme of one conclusion sequent and a list of hypotheses sequents. In our system, the derivation rules come with an ancestor relation linking one formula of the conclusion to zero, one or several formulas of the hypotheses. When defining our rules, we provide this link by drawing the ancestor relation with colors.

Rules for MALL are defined in figure 1. We add rules of figure 2 to those of MALL to get the rules of LL. We add rules of figure 3 to MALL and LL to get the fixed-point versions of these systems: $\mu\text{MALL}^{\infty}$ and $\mu\text{LL}^{\infty}$. The exchange rule (ex) from figure 1 allows one to derive the rule $\frac{\vdash \sigma(\Gamma)}{\vdash \Gamma} \text{ex}(\sigma)$ for any permutation $\sigma$ of $[[1, \#(\Gamma)]]$, where $\sigma(\Gamma)$ designate the action of $\sigma$ on the list $\Gamma$. In the rest of the article, we will intentionally forget to write the exchange rule explicitely, the reader can consider that each of our rules are preceded and followed by a finite number of rule (ex).

Proofs of non fixed-point systems, MALL, LL, are the trees inductively generated by the corresponding set of rules of each of these systems. To define non-wellfounded proofs for fixed-point logics, we first need a definition:

**► Definition 3 (Pre-proofs).** Given a set of derivation rules, we define pre-proofs to be the trees co-inductively generated by rules of each of those systems.

$$ \frac{\vdash F[X := \mu X.F], \Gamma}{\vdash \mu X.F, \Gamma} \mu \qquad \frac{\vdash F[X := \nu X.F], \Gamma}{\vdash \nu X.F, \Gamma} \nu $$

<caption>Figure 3 Rules for the fixed-point fragment</caption>
4 Super exponentials with fixed-points

► **Example 1** (Regular proof). *Regular pre-proofs are those pre-proofs having a finite number of sub-proofs. We represent them with back-edges. We give an example of circular proof:*

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

► **Definition 4** (Active & Principal occurrence of a rule). *We define active occurrences (resp. principal formula) of the rules of figures 1, 2 and 3 to be the first occurrence (resp. formula) of each conclusion sequent of that rule except for:*

- the rule (ex) which does not contain any active occurrences nor principal rules;

- the rule (cut) does not contain active occurrences but has F as principal formula;

From that, we define the proofs as a subset of the pre-proofs:

► **Definition 5** (Validity and proofs). *Let $b = (s_i)_{i \in \omega}$ be a sequence of sequents defining an infinite branch in a pre-proof $\pi$. A thread of $b$ is a sequence $(F_i \in s_i)_{i>n}$ of occurrences such that for each $j$, $F_j$ and $F_{j+1}$ are satisfying the ancestor relation. We say that a thread of $b$ is valid if the minimal recurring formula of this sequence, for sub-formula ordering, exists and is a $\nu$-formula and that the formulas of this threads are infinitely often active. A branch $b$ is valid if there exists a valid thread of $b$. A pre-proof is valid and is a proof if each of its infinite branches is valid.*

2.1.3 Cut-elimination for linear logic with fixed-point

Cut-elimination holds for $\mu\mathrm{MALL}^{\infty}$ and $\mu\mathrm{LL}^{\infty}$. To prove cut-elimination, we use a new rule (mcut) corresponding to an abstraction of several cuts.

Details
in
ap-
pendix A.1.

► **Definition 6** (Multicut rule). *The multicut rule has an arbitrary number of hypotheses: $\frac{\vdash \Gamma_1 \dots \vdash \Gamma_n}{\vdash \Gamma}$ mcut($\iota, \perp$). The ancestor relation $\iota$ sends one formula of the conclusion to exactly one formula of the hypotheses; whereas the $\perp$-relation links cut-formulas together.*

► **Example 2.** *We give the example of the (cut/mcut) step, representing graphically $\iota$ in red*

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

To define the (mcut) reduction step we need a last definition, that will be also useful when defining the reduction step of the super exponential system:

► **Definition 7** (Restriction of a multicut context). *Let $\frac{C}{s}$ mcut($\iota, \perp$) be a multicut occurrence such that $C = s_1 \dots s_n$ and let $s_i := \vdash F_1, \dots, F_{k_i}$, we define $C_{F_j}$ to be the sequents linked to the formula $F_j$ with the $\perp$-relation. We extend this definition to contexts.*

Details
in
ap-
pendix A.2

Cut-elimination for $\mu\mathrm{MALL}^{\infty}$ and $\mu\mathrm{LL}^{\infty}$ is proved syntactically with a rewriting system for (mcut), which steps are given in appendix A.3. We then consider reduction sequences with one (mcut) at the root of the proof. In an infinite setting, we want to prove that our reduction sequences are infinitarily normalizing, meaning that they converge to a valid proof. This is not enough to prove *cut-elimination*, as some infinite sequences of reduction might converge to a proof which still contains cut: by letting some (mcut) infinitely untouched. In order to have a infinitary strong-normalization theorem, we restrict our notion of reductions to reductions that interact with every (mcut) of the proofs:
**► Definition 8 (Fair reduction sequences [2, 1]).** A reduction sequence $(\pi_i)_{i \in \omega}$ is fair, if for each $\pi_i$ such that there is a reduction $\mathcal{R}$ to a proof $\pi'$, there exist a $j > i$ such that $\pi_j$ does not contain any residual of $\mathcal{R}$.

We then have a first theorem of cut-elimination for $\mu\text{MALL}^{\infty}$ proved in [1, 2]:

**► Theorem 1.** Each fair (mcut) reduction sequences of $\mu\text{MALL}^{\infty}$ converges to a cut-free (valid) proof.

In [18], exponential formulas, proofs and cut-steps are encoded into $\mu\text{MALL}^{\infty}$, following $(?A)^{\bullet} = \mu X.(A^{\bullet} \oplus (\perp \oplus (X \nparallel X)))$ $(!A)^{\bullet} = \nu X.(A^{\bullet} \& (1 \& (X \otimes X)))$. Then Theorem 1 is used to prove the following theorem:

**► Theorem 2.** Each fair (mcut) reduction sequences of $\mu\text{LL}^{\infty}$ converges to a cut-free proof.

## 2.2 Super exponentials

In this section, we define a family of parameterized logical systems, following the methodology of [6] and using the formalism from the previous section. The rules of Bauer and Laurent's system [6] only include functorial promotion and one needs to use the digging rule to get the usual *Girard's promotion* rule. As we do not cover the digging rule in our system, we use an alternative *superLL* formalization. We give adaptation of the proofs of [6] in A.6.

The first parameters of these systems will allow us to define formulas:

**► Definition 9 (Exponential signature).** An exponential signature $\sigma$, is a Boolean function on the set of rule names: $\{?_{m_i} | i \in \mathbb{N}\} \cup \{?_{c_i} | i \ge 2\}$.

We consider sets of exponential names $\mathcal{E}$, which is an arbitrary set $\mathcal{E}_{\text{name}}$ endowed with a function $f_{\mathcal{E}_{\text{name}}}$ in a set of exponential signatures. Each exponentials will be signed by an element of $\mathcal{E}$ that will determine which rules with names from $\{?_{m_i} | i \in \mathbb{N}\} \cup \{?_{c_i} | i \ge 2\}$ can be applied on it. For the sake of clarity, we will write $\sigma$ instead of $f_{\mathcal{E}_{\text{name}}}(\sigma)$, omitting $f_{\mathcal{E}_{\text{name}}}$ throughout the remainder of the paper.

Let $\mathcal{E}$ be a set of exponential names, formulas of superLL($\mathcal{E}$) are the formulas of MALL together with exponential connectives subscripted by an element $\sigma$ of $\mathcal{E}$:

$$F, G ::= a \in \mathcal{A} \mid a^{\perp} \mid F \nparallel G \mid F \otimes G \mid \perp \mid 1 \mid F \oplus G \mid F \& G \mid 0 \mid \top \mid ?_{\sigma} F \mid !_{\sigma} F$$

The orthogonal $(-)^{\perp}$ is defined as the smallest involution satisfying the same conditions as in Definition 1 but with the addition of: $(!_{\sigma} A)^{\perp} = ?_{\sigma} A^{\perp}$.

**► Notation 1 (List of exponential signatures).** Let $\Delta = A_1, \dots, A_n$ be a list of n formulas, and let $\vec{\sigma} = \sigma_1, \dots, \sigma_n$ be a list of n exponential signatures. We write $?_{\vec{\sigma}} \Delta$ for the list of formulas $?_{\sigma_1} A_1, \dots, ?_{\sigma_n} A_n$. Moreover, given a relation $R$ on exponential signatures, and given two lists of exponential signatures $\vec{\sigma} = \sigma_1, \dots, \sigma_m$ and $\vec{\sigma}' = \sigma'_1, \dots, \sigma'_n$, we write $\vec{\sigma}R\vec{\sigma}'$ for $\bigwedge_{1 \le i \le m} \sigma_i R \sigma'_j$.

$$1 \le i \le m \\ 1 \le j \le n$$

For one set of signatures $\mathcal{E}$, we define many systems, parametrized by three binary relations on $\mathcal{E}$: $\le_g$, $\le_f$ and $\le_u$. Rules for this system are the rules of MALL from Figure 1 in combination with rules of Figure 4. Note that the multiplexing rule, $?_{m_i}$, is $(?_w)$ for $i = 0$ and $(?_d)$ for $i = 1$. Proofs from superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) are those trees inductively generated by the rules of this system.

Not all instances of superLL eliminate cuts: one needs to impose conditions on them, so that cut can indeed be eliminated. The two following definitions aim at formulating these conditions in a suitable way.
## 6 Super exponentials with fixed-points

<figure><img src="image_8.png" /><figcaption>Figure 4 Exponential fragment of $\mu$superLL$^\infty$</figcaption></figure>

<table><tr><td>σ ≤<sub>g</sub> σ' ⇒ σ(?<sub>m<sub>i</sub></sub>) ⇒ ¯σ'(?<sub>c<sub>i</sub></sub>)</td><td>i ≥ 0</td><td>(axgmpx)</td></tr><tr><td>σ ≤<sub>s</sub> σ' ⇒ σ(?<sub>m<sub>i</sub></sub>) ⇒ ¯σ'(?<sub>m<sub>i</sub></sub>)</td><td>i ≥ 0 and s ≠ g</td><td>(axfumpx)</td></tr><tr><td>σ ≤<sub>s</sub> σ' ⇒ σ(?<sub>c<sub>i</sub></sub>) ⇒ ¯σ'(?<sub>c<sub>i</sub></sub>)</td><td>i ≥ 2</td><td>(axcontr)</td></tr><tr><td>σ ≤<sub>s</sub> σ' ⇒ σ' ≤<sub>s</sub> σ'' ⇒ σ ≤<sub>s</sub> σ''</td><td></td><td>(axTrans)</td></tr><tr><td>σ ≤<sub>g</sub> σ' ⇒ σ' ≤<sub>s</sub> σ'' ⇒ σ ≤<sub>g</sub> σ''</td><td></td><td>(axleqgs)</td></tr><tr><td>σ ≤<sub>f</sub> σ' ⇒ σ' ≤<sub>u</sub> σ'' ⇒ σ ≤<sub>f</sub> σ''</td><td></td><td>(axleqfu)</td></tr><tr><td>σ ≤<sub>f</sub> σ' ⇒ σ' ≤<sub>g</sub> σ'' ⇒ (σ ≤<sub>g</sub> σ'' ∧ (σ ≤<sub>f</sub> σ'' ⇒ (σ ≤<sub>g</sub> σ'' ∧ σ'''(?<sub>m<sub>1</sub></sub>))))</td><td></td><td>(axleqfg)</td></tr><tr><td>σ ≤<sub>u</sub> σ' ⇒ σ' ≤<sub>s</sub> σ'' ⇒ σ ≤<sub>s</sub> σ''</td><td></td><td>(axlequs)</td></tr></table>

with $s \in \{g, f, u\}$, all the axioms are universally quantified.

For convenience, we use the notation $?_{c_0} := ?_{m_0}$ and set $\bar{\sigma}(?_{c_1}) = \text{true}$ for all $\sigma$.

<caption>Table 1 Cut-elimination axioms</caption>

**Definition 10 (Derivability closure).** Given a signature $\sigma$, we define the derivability closure $\bar{\sigma}$ to be the signature inductively defined by:

$$ \begin{gathered} \sigma(r) \Rightarrow \bar{\sigma}(r) \qquad \bar{\sigma}(?_{c_i}) \Rightarrow \bar{\sigma}(?_{c_j}) \Rightarrow \bar{\sigma}(?_{c_{i+j-1}}) \\ \text{For } i, j \neq 0, \quad \sigma(?_{c_2}) \Rightarrow \bar{\sigma}(?_{m_i}) \Rightarrow \bar{\sigma}(?_{m_j}) \Rightarrow \bar{\sigma}(?_{m_{i+j}}) \qquad \sigma(?_{m_1}) \Rightarrow \bar{\sigma}(?_{c_i}) \Rightarrow \bar{\sigma}(?_{m_i}) \end{gathered} $$

Derivability closure comes with the following property, proved by induction on $\bar{\sigma}(r)$:

**Proposition 1.** If $\bar{\sigma}(r)$ is true, then $(r)$ is derivable for a principal formula with principal connective $?_{\sigma}$ using only $?_{m_i}$ and $?_{c_i}$ rules.

**Notation 2.** We name $?_{\bar{\sigma}_{c_i}}$ (resp. $?_{\bar{\sigma}_{m_i}}$), for $i \in \mathbb{N}$, any derivation using only $(?_{c_j})$ and $(?_{m_j})$ rules and having the same conclusion and hypothesis than $?_{c_i}$ (resp. $?_{m_i}$).

We take the notation $\bar{\sigma}(?_{c_0}) := \bar{\sigma}(?_{m_0})$, and we set $\bar{\sigma}(?_{c_1}) := \text{true}$ for all $\sigma$ and $?_{c_1}^{(e)}$ to be the empty derivation.

To help us define a cut-elimination rewriting system, we consider cut-elimination axioms defined in Table 1. In superLL-systems each axiom corresponds to one step of cut-elimination. However, as our reduction systems is based on the (mcut)-rule, which corresponds to the concatenation of many cuts, some axioms will be used in more than one case of reduction.

In the original system [6], axiom expansion and cut-elimination property hold. We state here cut-elimination and postpone the axiom expansion property to Appendix A.5.

**Theorem 3 (Cut Elimination).** As soon as the 8 cut-elimination axioms of Table 1 are satisfied, cut elimination holds for superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$).

Many existing linear logic systems are instances of superLL. We give the example of ELL [12]:

**Example 3 (Elementary Linear Logic).** Elementary Linear Logic (ELL) [12, 9] is a variant of LL where we remove $(?_d)$ and $(!_g)$ and add the functorial promotion: $\vdash A, \Gamma \vdash !_A, ?\Gamma$ !_f This
system is captured as the instance of superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) system with $\mathcal{E} = \{\bullet\}$, defined by $\bullet(?(c_2)) = \bullet(?(m_0)) = true$ (and $(\bullet)(r) = false$ otherwise), $\le_g = \le_u = \emptyset$ and $\bullet \le_f \bullet$. This superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) instance is ELL and satisfies the cut-elimination axioms and the expansion axiom defined in A.5.

Details
in ap-
pendix
A.7

As argued in [6], The superLL-systems subsume many more existing linear logic systems such as SLL [14], LLL [12], seLL [16]. The last two are particularly interesting as they require more than one exponential signature to be formalized. In the following section, we will look at such an example but for the fixed-point version of $\mu$superLL$^{\infty}$.

### 3 Super exponentials with fixed-points

In this section, we define $\mu$superLL$^{\infty}$ the non-wellfounded version of superLL and give some interesting instances of it.

#### 3.1 Definition of $\mu$superLL$^{\infty}$

##### 3.1.1 Formulas

Let $\mathcal{E}$ be an exponential names, pre-formulas of $\mu$superLL$^{\infty}(\mathcal{E})$ are the formulas of superLL($\mathcal{E}$) with the addition of fixed-point variables and a least and a greatest fixed-point:

$$F, G ::= a \in \mathcal{A} \mid a^{\perp} \mid X \in \mathcal{V} \mid F \mathcal{N} G \mid F \otimes G \mid \perp \mid 1 \mid F \oplus G \mid F \& G \mid 0 \mid \top \mid ?_{\sigma} F \mid !_{\sigma} F \mid \mu X.F \mid \nu X.F$$

Formulas of $\mu$superLL$^{\infty}(\mathcal{E})$ are the closed pre-formulas. Negation is defined as the smallest involution on formulas satisfying the relations of Definition 1 as well as: $(?_{\sigma}F)^{\perp} := !F^{\perp}$.

##### 3.1.2 Rules and proofs

Again, for one set of signatures $\mathcal{E}$ we define many systems, each parametrized with $\le_g$, $\le_f$ and $\le_u$. Rules for this system are the rules of superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) together with the fixed-point fragment of Figure 3. Pre-proofs of $\mu$superLL$^{\infty}(\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) are the trees coinductively generated by the rules of $\mu$superLL$^{\infty}(\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$), validity is defined the same way as $\mu$LL$^{\infty}$.

### 3.2 Some instances of $\mu$superLL$^{\infty}$

In this subsection, we give some interesting instances of $\mu$superLL$^{\infty}$.

#### 3.2.1 A linear modal $\mu$-calculus

Super exponentials were usually designed to prove cut-elimination for a lot of instances of light linear logic. Another utility of this system can be found in [5]. The system $\mu$LL$^{\infty}$ is an instance of $\mu$superLL$^{\infty}$ with two exponential names. However, one of this names does not represent exponential modalities but represent the modalities from the modal $\mu$-calculus. Formulas of $\mu$LL$^{\infty}$ are the formulas of $\mu$LL$^{\infty}$ with the additions of two modalities: $\diamond F \ \square F$. Rules of $\mu$LL$^{\infty}$ are the rules of $\mu$LL$^{\infty}$ where the promotion is extended with $\diamond$-contexts. Rules on modalities are a functorial promotion (called the modal rule) and a contraction and a weakening on $\diamond$-formulas:

$$\frac{\vdash F, ?\Gamma, \diamond\Delta}{\vdash !F, ?\Gamma, \diamond\Delta} \vDash_P \frac{\vdash F, \Gamma}{\vdash \Box F, \diamond\Gamma} \Box_P \frac{\vdash \diamond F, \diamond F, \Gamma}{\vdash \diamond F, \Gamma} \diamond_c \frac{\vdash \Gamma}{\vdash \diamond F, \Gamma} \diamond_w$$

The system $\mu$LL$^{\infty}$ is the system $\mu$superLL$^{\infty}(\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) such that:
- The set of signatures contains two elements $\mathcal{E} := \{\bullet, \star\}$.

- $?_{c_2}(\bullet) = ?_{c_2}(\star) = \text{true} \ ?_{m_1}(\bullet) = \text{true}, ?_{m_0}(\bullet) = ?_{m_0}(\star) = \text{true}$, and all the other elements have value false for both signatures.

- $\bullet \le_g \bullet$ ; $\bullet \le_g \star, \star \le_f \star$, and all couples for the three relations $\le_g, \le_f$ and $\le_u$ being false. This system is $\mu LL_\square^\infty$ when taking: $?_{\bullet} := ?$, $!_{\bullet} := !$, $?_{\star} := \diamond$ and $!_{\star} := \Box$. Moreover, the system satisfy cut-elimination axioms of figure 1

3.2.2 ELL with fixed point

In [3], an affine version of second-order ELL with recursive types, called EAL<sub>μ</sub>, is introduced.
this system allows only finite proofs. Affine means weakening applies to any formulas.
Fixpoints are added to a two-sided version with —o and (-)⊥ formulas, without any condition
on the fixpoint variables, unlike the positivity condition induced by our one-sided sequent
version. The paper proves EAL<sub>μ</sub> cut-elimination and refines complexity bounds from ELL.

Considering $\mu$ELL$^{\infty}$, an instance of Example 3 with fixpoints, gives us a typing system similar to EAL$_{µ}$. Namely, consider $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$) with the same E, $\le_g$, $\le_f$, and $\le_u$ as in Example 3. Since the axioms in Table 1 only concern E, $\le_g$, $\le_f$, and $\le_u$, they are also satisfied by this instance of $\mu$superLL$^{\infty}$.

Our systems differ in two ways: (i) the condition of positivity on fixed-point variables, and (ii) the infinite nature of our proofs. Thus, our cut-elimination theorem may not apply due to (i), and even if it did, it might not ensure finite proofs because of (ii). However, in [3], only fixed-point variables in positive positions are used when proving complexity bounds, addressing (i). Additionally, using only $\mu$-fixed-points to encode fixpoints ensures that cut-free proofs remain finite, resolving the incompatibility induced by (ii) by preventing infinite branches.

► **Remark 2.** *Note that there are no proof of the conclusion sequent of Example 1 in *µELL*<sup>*∞*</sup>.*

4 Cut-elimination

In this section, we only consider instances of $\mu\mathit{superLL}^\infty$ satisfying the axioms of Table 1.

**4.1 (mcut)-elimination steps**

Here, we define the (mcut)-elimination steps of instances of $\mu\mathit{superLL}^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$. To define (mcut)-elimination steps, it is suitable to have a specific notation for the contexts containing only proofs concluded by a promotion. We use notations similar to the notations used in $\mu LL^\infty$ cut-elimination proof [18]:

► **Notation 3** ((!)-contexts). $C^!$ denotes a list of $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-proofs which are all concluded by some promotion rule ($!_g$; $!_f$ or $!_u$). Given $s \in \{g, f, u\}$, $C^!_s$ denotes a list of $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-proofs which are all concluded by an ($!_s$)-rule. In both cases, $C$ denotes the list of $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-proofs formed by gathering the immediate subproofs of the last promotion (being either $C^!$, or $C^!_s$).

We now give a series of lemmas that will be used to justify the (mcut)-reduction steps defined in figures 5 and 6. We write some conditions on the proofs of these figure in their corresponding lemma. We only give a proof sketch of lemma 3, and give complete proofs of each lemma in appendix C.1. We start by the commutation cases of the different promotions. Commutation cases for the multiplexing and the contraction rules were give in section 4.1. The case (comm<sub>g</sub>) covers all the case where (!<sub>g</sub>) commute under the cut:
**Lemma 1 (Justification for step (comm<sub>!_g</sub>)).** If
$$ \frac{\begin{array}{c} \pi \\ \vdash A, ?\bar{\tau}\Delta \\ \vdash !_\sigma A, ?\bar{\tau}\Delta \\ \vdash !_\sigma A, ?\bar{\rho}\Gamma \end{array} \sigma \le_g \bar{\tau} !_g C^!}{\begin{array}{c} C^! \\ \vdash A, ?\bar{\tau}\Delta \\ \vdash A, ?\bar{\rho}\Gamma \end{array}} \text{mcut}(\iota, \perp) $$
is a $\mu$superLL<sup>∞</sup>(*E*, $\le_g$, $\le_f$, $\le_u$)-proof then
$$ \frac{\begin{array}{c} \pi \\ \vdash A, ?\bar{\tau}\Delta \\ \vdash A, ?\bar{\rho}\Gamma \end{array} C^!}{\begin{array}{c} \text{mcut}(\iota, \perp) \\ \sigma \le_g \bar{\rho} !_g \end{array}} \text{is also} $$
a $\mu$superLL<sup>∞</sup>(*E*, $\le_g$, $\le_f$, $\le_u$)-proof.

The case (comm<sub>!_f</sub>) covers the case of commutation of an (!_f)-promotion but where only (!_g)-rules with empty contexts appears in the hypotheses of the multi-cut. Note that an (!_g) occurrence with empty context could be seen as an (!_f) occurrence (with empty context).

Details
in ap-
pendix,
lemma 17

**Lemma 2 (Justification for step (comm<sub>!_f</sub>))**. If
$$ \frac{\begin{array}{c} \pi \\ \vdash A, \Delta \\ \vdash !_\sigma A, ?\bar{\tau}\Delta \\ \vdash !_\sigma A, ?\bar{\rho}\Gamma \end{array} \sigma \le_f \bar{\tau} !_f C^!}{\begin{array}{c} C^! \\ \vdash A, \Delta \\ \vdash A, \Gamma \end{array}} \text{mcut}(\iota, \perp) $$
is
a $\mu$superLL<sup>∞</sup>(*E*, $\le_g$, $\le_f$, $\le_u$)-proof with $C^!$ such that each sequents concluded by an (!_g) have
an empty context, then
$$ \frac{\begin{array}{c} \pi \\ \vdash A, \Delta \\ \vdash !_\sigma A, ?\bar{\rho}\Gamma \end{array} C^! \sigma \le_f \bar{\rho} !_f}{\begin{array}{c} \text{mcut}(\iota, \perp) \\ \sigma \le_g \bar{\rho} !_g \end{array}} $$
is a $\mu$superLL<sup>∞</sup>(*E*, $\le_g$, $\le_f$, $\le_u$)-proof.

We then have the following case where we commute an (!_f)-rule, but where there is one (at least) (!_g)-promotion with a non-empty context in the premisses of the multicut rule:

Details
in ap-
pendix,
lemma 18

**Lemma 3 (Justification for step (comm<sub>!_g</sub><sup>2</sup>))**. If
$$ \frac{\begin{array}{c} \pi \\ \vdash A, \Delta \\ \vdash !_\sigma A, ?\bar{\tau}\Delta \\ \vdash !_\sigma A, ?\bar{\rho}\Gamma \end{array} \sigma \le_f \bar{\tau} !_f C^!}{\begin{array}{c} C^! \\ \vdash A, ?\bar{\tau}\Delta \\ \vdash A, ?\bar{\rho}\Gamma \end{array}} \text{mcut}(\iota, \perp) $$
is
a $\mu$superLL<sup>∞</sup>(*E*, $\le_g$, $\le_f$, $\le_u$)-proof with $C^1_g$ containing a sequent conclusion of an (!_g)-rule
with at least one formula in the context, then
$$ \frac{\begin{array}{c} \pi \\ \vdash A, \Delta \\ \vdash A, ?\bar{\tau}\Delta \\ \vdash A, ?\bar{\rho}\Gamma \end{array} \tau(?_{m_1}) ?_{m_1} C^! \sigma \le_g \bar{\rho} !_g}{\begin{array}{c} C^! \\ \sigma \le_g \bar{\rho} !_g \end{array}} $$
is also a $\mu$superLL<sup>∞</sup>(*E*, $\le_g$, $\le_f$, $\le_u$)-proof.

**Proof sketch (details in appendix, lemma 19).** The proof is done in two steps:

1. Starting from $\vdash !_\sigma A, ?\bar{\tau}\Delta$ we run through sequents until reaching one $\vdash !_\sigma A, ?\bar{\tau}', \Delta'$ conclusion of an (!_g)-rule, for each signature $\sigma'$ in these sequents, we prove that $\sigma \le_f \sigma'$ using axiom (axTrans) or (axleqfu). Then we use axiom (axleqfg) to prove that $\bar{\tau}(?_{m_1})$ and $\sigma \le_g \bar{\tau}$.

2. We run through all the sequents and using axiom (axleqgs), we prove that $\sigma \le_g \sigma''$ for each signature $\sigma''$ we encounter.

We therefore get that $\sigma \le_g \bar{\rho}$ as signatures from $\bar{\rho}$ are contained on hypotheses of the mcut. And we use first step for the condition of application of $(?_{m_1})$. $\quad$

We then cover the cases where we commute an (!_u)-rule with the multi-cut. The first case is where there are only a list of (!_u)-rules in the hypotheses of the multi-cut:
► **Lemma 4 (Justification for step (comm<sup>1</sup><sub>u</sub>))**. If $\frac{\frac{\pi}{\vdash A, C \quad \sigma \leq_u \tau} !_u}{\frac{\vdash !_\sigma A, ?_\tau C}{\vdash !_\sigma A, ?_\rho B}} C^!_u$ is

$\pi$

The second case of (!_u)-commutation is where we have an (!_f)-rule and where the hypotheses concluded by an (!_g)-rule have empty contexts.

► **Lemma 5 (Justification for step (comm<sup>2</sup><sub>u</sub>))**. Let $\frac{\frac{\pi}{\vdash A, B \quad \sigma \leq_u \tau} !_u}{\frac{\vdash !_\sigma A, ?_\tau B}{\vdash !_\sigma A, ?_\rho \Gamma}} C^!_u$ mcut($\iota, \perp$)

be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof with $C$ containing at least one proof concluded by an (!_f)-promotion; and such that for each sequent conclusion of an (!_g)-promotion has empty context.

We have that $\frac{\frac{\pi}{\vdash A, B \quad C \quad mcut(\iota, \perp)} \sigma \leq_f \vec{\rho}}{\vdash A, \Gamma \quad mcut(\iota, \perp)} !_f$ is also a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof.

The following lemma deals with the case where there are sequents concluded by an (!_g)-rule with non-empty context and where the first rule encountered is an !_f-rule.

► **Lemma 6 (Justification for step (comm<sup>3</sup><sub>u</sub>))**. Let $\frac{\frac{\pi_1}{\vdash A, B \quad \sigma \leq_u \tau} !_u}{\frac{\vdash !_\sigma A, ?_\tau B}{\vdash !_\sigma A, ?_\rho \Gamma}} C_1^{!u} \quad \frac{\pi_2}{\vdash C, \Delta \quad \sigma' \leq_f \vec{\tau}'} !_f}$ mcut($\iota, \perp$)

be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof, such that $C_2^1$ contains a sequent conclusion of an (!_g) rule with non-empty context; $C := \{\vdash !_\sigma A, ?_\tau B\} \cup C_1^{!u} \cup \{\vdash !_\sigma C, ?_\tau' \Delta\}$ are a cut-connected subset of sequents; and $C' := \{\vdash !_\sigma C, ?_\tau' \Delta\} \cup C_2^1$ another one. We have that

$\frac{\pi_1}{\vdash A, B \quad C_1} \frac{\frac{\vdash C, \Delta \quad \vec{\tau}'(?_{m_1})}{\vdash C, ?_{\tau'} \Delta} ?_{m_1}}{\vdash A, ?_\rho \Gamma} C_2^1$ is also a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof.

The last lemma of promotion commutation is about the case where we commute an (!_u)-promotion but when first meeting an (!_g)-promotion.

► **Lemma 7 (Justification for step (comm<sup>4</sup><sub>u</sub>))**. Let $\frac{\frac{\pi_1}{\vdash A, B \quad \sigma \leq_u \tau} !_u}{\frac{\vdash !_\sigma A, ?_\tau B}{\vdash !_\sigma A, ?_\rho \Gamma}} C_1^{!u} \quad \frac{\pi_2}{\vdash C, ?_\tau' \Delta \quad \sigma' \leq_g \vec{\tau}'} !_g}$ mcut($\iota, \perp$)

be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof such that $C := \{\vdash !_\sigma A, ?_\tau B\} \cup C_1^{!u} \cup \{\vdash !_\sigma C, ?_\tau' \Delta\}$ are a cut-connected subset of sequents; and $C' := \{\vdash !_\sigma C, ?_\tau' \Delta\} \cup C_2^1$ another one. Then,

$\frac{\pi_1}{\vdash A, B \quad C_1} \frac{\pi_2}{\vdash A, ?_\rho \Gamma} \frac{C_2^1}{\vdash A, ?_\rho \Gamma}$ is also a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof.
Then we have the principal cases, starting with the contraction:

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

Before giving the case for the multiplexing, we need a definition:

Details
in ap-
pendix,
lemma 24

**Definition 11.** Let $S^!$ be a sequent of a $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-context $C^!$, such that $C^!$ is a tree with respect to a cut-relation $\perp$. We define a $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-context $\mathcal{O}_{mpx_S}(C^!)$ by induction on this relation taking $S^!$ as the root. We take advantage of this induction definition to define two sets of sequent $S_{C^!_1,S^!1}^{?m}$ and $S_{C^!_1,S^!n}^{?c}$. Let $C_1^!...C_n^!$ be the sons of $S^!$, such that $C^! = (S^!,(C_1^!...,C_n^!))$, we have two cases:

- $S^! = S^!_g$, then we define $\mathcal{O}_{mpx_S}(C^!):= (S,(C_1^!...,C_n^!))$; $S_{C^!_1,S^!}^{?m} = \emptyset$; $S_{C^!_1,S^!}^{?c} := C^!$.

- $S^! = S^!_f$ ou $S^! = S^!_u$, then let the root of $C_i^!$ be $S_i^!$, we define $\mathcal{O}_{mpx_S}(C^!):= (S,\mathcal{O}_{mpx_S^1}(C_1^!),...,\mathcal{O}_{mpx_S^n}(C_n^!))$; $S_{C^!_1,S^!}^{?m} := \{S^!\} \cup S_{C^!_i,S_i^!}^{?m}$; $S_{C^!_1,S^!}^{?c} := \cup S_{C^!_i,S_i^!}^{?c}$

A graphical representation of this definition is given in appendix, definition 14. Finally, we have the multiplexing principal case:

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

## 4.2 Translating $\mu$superLL$^\infty$ into $\mu$LL$^\infty$

We now give a translation of $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ into $\mu$LL$^\infty$ using directly the results of [18] to deduce $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ cut-elimination in a more modular way:

Details
in ap-
pendix,
lemma 25
12 Super exponentials with fixed-points

$$ \frac{\pi \quad \sigma \leq_g \vec{\tau} \quad !_g}{\frac{\vdash A, ?_{\vec{\tau}} \Delta}{\vdash !_\sigma A, ?_{\vec{\tau}} \Delta} \quad C^!} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad C^!}{\frac{\vdash A, ?_{\vec{\tau}} \Delta}{\vdash A, ?_{\vec{\rho}} \Gamma} \quad mcut(\iota, \perp)} \quad \sigma \leq_g \vec{\rho} \quad !_g \quad \text{(comm}_1^g) $$

$$ \frac{\pi \quad \sigma \leq_f \vec{\tau} \quad !_f}{\frac{\vdash A, \Delta}{\vdash !_\sigma A, ?_{\vec{\tau}} \Delta} \quad C^!} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad C}{\frac{\vdash A, \Delta}{\vdash A, \Gamma} \quad mcut(\iota, \perp)} \quad \sigma \leq_f \vec{\rho} \quad !_f \quad \text{(comm}_1^f) $$

$$ \frac{\pi \quad \sigma \leq_f \vec{\tau} \quad !_f}{\frac{\vdash A, \Delta}{\vdash !_\sigma A, ?_{\vec{\tau}} \Delta} \quad C^!} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad \vec{\tau}(?_{m_1})}{\frac{\vdash A, ?_{\vec{\tau}} \Delta}{\vdash A, ?_{\vec{\rho}} \Gamma} \quad C^!} \quad ?_{m_1} \quad \text{(comm}_2^g) $$

$$ \frac{\pi \quad \sigma \leq_u \tau \quad !_u}{\frac{\vdash A, C}{\vdash !_\sigma A, ?_\tau C} \quad C^!} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad C}{\frac{\vdash A, C}{\vdash A, B} \quad mcut(\iota, \perp)} \quad \sigma \leq_u \rho \quad !_u \quad \text{(comm}_1^u) $$

$$ \frac{\pi \quad \sigma \leq_u \tau \quad !_u}{\frac{\vdash A, B}{\vdash !_\sigma A, ?_\tau B} \quad C^!} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad C}{\frac{\vdash A, B}{\vdash A, \Gamma} \quad mcut(\iota, \perp)} \quad \sigma \leq_f \vec{\rho} \quad !_f \quad \text{(comm}_2^u) $$

$$ \frac{\pi_1 \quad \sigma \leq_u \tau \quad !_u}{\frac{\vdash A, B}{\vdash !_\sigma A, ?_\tau B} \quad C_1^!} \quad \frac{\pi_2 \quad \sigma' \leq_f \vec{\tau}' \quad !_f}{\frac{\vdash C, \Delta}{\vdash !_\sigma C, ?_{\vec{\tau}} \Delta} \quad C_2^!} \quad \text{mcut}(\iota, \perp) $$

$$ \rightsquigarrow \frac{\pi_1 \quad C_1}{\frac{\vdash A, B \quad C_1}{\vdash A, ?_{\vec{\rho}} \Gamma}} \quad \frac{\pi_2 \quad \vec{\tau}'(?_{m_1})}{\frac{\vdash C, \Delta \quad C_2^!}{\vdash A, ?_{\vec{\tau}} \Delta}} \quad ?_{m_1} \quad \text{(comm}_3^g) $$

$$ \frac{\pi_1 \quad \sigma \leq_u \tau \quad !_u}{\frac{\vdash A, B}{\vdash !_\sigma A, ?_\tau B} \quad C_1^!} \quad \frac{\pi_2 \quad \sigma' \leq_g \vec{\tau}' \quad !_g}{\frac{\vdash C, ?_{\vec{\tau}} \Delta}{\vdash !_\sigma C, ?_{\vec{\tau}} \Delta} \quad C_2^!} \quad \text{mcut}(\iota, \perp) $$

$$ \rightsquigarrow \frac{\pi_1 \quad C_1}{\frac{\vdash A, B \quad C_1}{\vdash A, ?_{\vec{\rho}} \Gamma}} \quad \frac{\pi_2 \quad C_2^!}{\frac{\vdash C, ?_{\vec{\tau}} \Delta}{\vdash !_\sigma A, ?_{\vec{\rho}} \Gamma}} \quad \text{mcut}(\iota, \perp) \quad \sigma \leq_g \vec{\rho} \quad !_g \quad \text{(comm}_4^g) $$

$$ \text{ Elimination steps: } \rightsquigarrow \frac{\pi \quad \sigma(\mu_{m_i})}{\frac{\vdash A, \dots, A, \Delta}{\vdash ?_\sigma A, \Delta} \quad C} \quad ?_{m_i} \quad \text{(comm}_5^g) $$

$$ \text{ Elimination steps: } \rightsquigarrow \frac{\pi \quad \sigma(\mu_{c_i})}{\frac{\vdash ?_\sigma A, \dots, ?_\sigma A, \Delta}{\vdash ?_\sigma A, \Delta} \quad C} \quad ?_{c_i} \quad \text{(comm}_6^g) $$

<caption>Figure 5 Commutative cut-elimination steps of the exponential fragment of $\mu$superLL$^\infty$</caption>
<figure><img src="image_11.png" /></figure>

with $S$ being the sequent cut-connected to $?_{\sigma}A, \Delta$ on the formula $?_{\sigma}A$.

<caption>**Figure 6** Principal cut-elimination steps of the exponential fragment of $\mu$superLL$^{\infty}$</caption>

**► Definition 12** ((-)$^{\circ}$-translation). We define (-)$^{\circ}$ by induction on formulas (c is any non-exponential connective): $c(F_1, \dots, F_n)^{\circ} := c(F_1^{\circ}, \dots, F_n^{\circ})$; $X^{\circ} := X$; $\forall \sigma, (?_{\sigma}A)^{\circ} := ?A^{\circ}$; $a^{\circ} := a$; $(!_{\sigma}A)^{\circ} := !A^{\circ}$. We define translations for exponential rules of $\mu$superLL$^{\infty}(\mathcal{E}, \le_g)$, $\le_f, \le_u$) in Figure 7. Other rules have their translations equal to themselves. Proof translation $\pi^{\circ}$ of $\pi$ is the proof coinductively defined on $\pi$ from rule translations.

The following lemma is immediate and comes from the fact that fixed-points are not affected by the translation:

**► Lemma 10** (Robustness of the (-)$^{\circ}$ translation to validity). Valid pre-proofs $\pi$ translates to valid pre-proofs $\pi^{\circ}$. Conversely, if $\pi^{\circ}$ is a valid pre-proof, then $\pi$ is also a valid pre-proof.

The goal of this section is to prove that each fair reductions sequences converges to a cut-free proof. We have to make sure (mcut)-reduction sequences are robust under this translation. In our proof of the final theorem, we also need one-step reduction-rules to be simulated by a finite number of reduction steps in the translation, which is the objective of the following lemma. We only give a proof sketch here, full proof can be found in appendix C.3.

**► Lemma 11.** Let $\pi_0$ be a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ proof and let $\pi_0 \rightsquigarrow \pi_1$ be a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ step of reduction. There exist a finite number of $\mu$LL$^{\infty}$ proofs $\theta_0, \dots, \theta_n$ such that $\theta_0 \to \dots \to \theta_n$, $\pi_0^{\circ} = \theta_0$ and $\theta_n = \pi_1^{\circ}$ up to a finite number of rule permutations, done only on rules that just permuted down the (mcut).

**Proof sketch.** Non exponential cases are immediate. Commutations of promotions translates to commutation of promotions and derelictions and promotion/dereliction key-case. We must

Details
in ap-
pendixapp:detailsredSeqTr
**► Theorem 4.** Every fair (mcut)-reduction sequence of $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ converges to a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ cut-free proof.

**Proof sketch, see full proof in appendix, Theorem 6.** Consider a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ fair reduction sequence $(\pi_i)_{i \in 1+\lambda}$ ($\lambda \in \omega + 1$). If the sequence is finite, we use lemma 11 and we are done. If the sequence is infinite, using corollary 1 we get a fair infinite $\mu$LL$^{\infty}$ reduction sequence $(\theta_i)_{i \in \omega}$. By theorem 2, we know that $(\theta_i)_{i \in \omega}$ converges to a cut-free proof $\theta$ of $\mu$LL$^{\infty}$. We prove that $(\pi_i)_{i \in \omega}$ converges to a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ pre-proof using the fact that $(\theta_i)_i$ is the translation of $(\pi_i)_i$ and that it is productive.

We then prove validity of the limit $\pi$ of $(\pi_i)_i$ by proving that the translation of $\pi$ is equal to $\theta$ up to rule- permutation (the permutation of one particular rule being finite). From Lemma 10 and Proposition 2, we get that these two operations preserves validity, therefore $\pi$ is valid which concludes the proof. ◀

We obtain another proof of the result of [6]:

**► Corollary 2 (Cut Elimination for superLL).** *Cut elimination holds for superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) as soon as the 8 cut-elimination axioms of definition 1 are satisfied.*

This result not only gives another way of proving cut-elimination for superLL-systems but the sequences of reduction we build in it are generally different from the one that are built in [6]. Indeed, we are eliminating cuts from the bottom of the proof using the multicut rule whereas in [6] the deepest cuts in the proof are eliminated first.

See
proof
in ap-
pendix,
Corol-
lary 4

# 5 Conclusion

We introduced a family of logical systems, $\mu$superLL$^{\infty}$, and proved a syntactic cut-elimination theorem for them. Our system encompasses various fixed-point extensions of existing linear logic systems, including well-known light logics extended with least and greatest fixed-points and a non-well-founded proof system. We provide a relatively simple and uniform proof of cut-elimination for these extensions. Additionally, $\mu$superLL$^{\infty}$ captures a linear logic version of the modal $\mu$-calculus, where modalities are used in a quite different way than exponential modalities from linear logic.

The $\mu$superLL$^{\infty}$ system, as defined in this paper, does not include the digging rule. Incorporating this rule would enable us to cover the super exponential version from [6]. It could also be relevant for modal calculus, as the digging rule for modal formulas is equivalent to axiom 4 of modal logic. Other modal logic axioms, such as axiom T and co-dereliction rules from differential linear logic, can be viewed as rules in linear logic.

Another natural future work would be to explore linear translations of affine linear logic and/or intuitionistic/classical translations of these systems, facilitating the study of proof theory closer to [3].

# References

1. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533375.
2 David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In *CSL 2016*, volume 62 of LIPIcs, pages 42:1–42:17, 2016. URL: http://drops.dagstuhl.de/opus/volltexte/2016/6582, doi:10.4230/LIPIcs.CSL.2016.42.

3 Patrick Baillot. On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy. *Information and Computation*, 241:3–31, 2015. URL: https://www.sciencedirect.com/science/article/pii/S0890540114001369, doi:https://doi.org/10.1016/j.ic.2014.10.005.

4 Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. *Information and Computation*, 261:55–77, 2018. Developments in Implicit Computational Complexity (DICE) 2014 and 2015. URL: https://www.sciencedirect.com/science/article/pii/S0890540118300774, doi:https://doi.org/10.1016/j.ic.2018.05.005.

5 Esaïe Bauer and Alexis Saurin. On the cut-elimination of the modal μ-calculus: Linear Logic to the rescue. working paper or preprint, July 2024. URL: https://hal.science/hal-04659700.

6 Esaïe Bauer and Olivier Laurent. Super exponentials in linear logic. *Electronic Proceedings in Theoretical Computer Science*, 353:50–73, December 2021. URL: http://dx.doi.org/10.4204/EPTCS.353.3, doi:10.4204/eptcs.353.3.

7 Aloïs Brunel and Kazushige Terui. Church => scott = ptime: an application of resource sensitive realizability. In Patrick Baillot, editor, *Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010*, volume 23 of *EPTCS*, pages 31–46, 2010. doi:10.4204/EPTCS.23.3.

8 Ugo Dal Lago and Patrick Baillot. On light logics, uniform encodings and polynomial time. *Mathematical Structures in Computer Science*, 16(4):713–733, 2006.

9 Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. 183(1):123–137, May 2003. doi:10.1016/S0890-5401(03)00010-5.

10 Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: Linear logic. *J. Symb. Log.*, 62(3):755–807, 1997. doi:10.2307/2275572.

11 Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

12 Jean-Yves Girard. Light linear logic. 143(2):175–204, June 1998. doi:10.1006/inco.1998.2700.

13 Dexter Kozen. Results on the propositional mu-calculus. *Theor. Comput. Sci.*, 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.

14 Yves Lafont. Soft linear logic and polynomial time. *Theoretical Computer Science*, 318(1–2):163–180, June 2004. doi:10.1016/j.tcs.2003.10.018.

15 Lê Thành Dũng Nguyen. On the elementary affine lambda-calculus with and without fixed points. *Electronic Proceedings in Theoretical Computer Science*, 298:15–29, August 2019. URL: http://dx.doi.org/10.4204/EPTCS.298.2, doi:10.4204/eptcs.298.2.

16 Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In *PPDP 2009*, page 129–140, New York, NY, USA, 2009. ACM. doi:10.1145/1599410.1599427.

17 Luca Roversi and Luca Vercelli. Safe recursion on notation into a light logic by levels. In Patrick Baillot, editor, *Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010*, volume 23 of *EPTCS*, pages 63–77, 2010. doi:10.4204/EPTCS.23.5.

18 Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points. TABLEAUX '23. Springer, 2023. URL: https://hal.science/hal-04169137.
A Details on Section 2

A.1 Details on the multicut rule (Definition 6)

The multi-cut rule is a rule with an arbitrary number of hypotheses:

$$ \frac{\Gamma_1 \vdash \Delta_1 \quad \dots \quad \Gamma_n \vdash \Delta_n}{\Gamma \vdash \Delta} \quad \text{mcut}(\iota, \perp) $$

Let $C_1 := \{(1, i, j) \mid i \in [1, n], j \in [1, \#\Gamma_i]\}, C_2 := \{(2, i, j) \mid i \in [1, n], j \in [1, \#\Delta_i]\}, \iota$ is a map from $(1, [1, \#\Gamma_i]) \cup (2, [1, \#\Delta_i])$ to $C = C_1 \cup C_2$ and $\perp$ is a relation on $C$:

- Elements of $(k, n)$ are sent on $C_k$;

- The map $\iota$ is injective;

- If $(k, i, j) \perp (k', i', j')$ then $k \neq k'$;

- The relation $\perp$ is defined for $C \setminus \iota$, and is total for this set;

- The relation $\perp$ is symmetric;

- Each index can be related at most once to another one;

- If $(1, i, j) \perp (2, i', j')$, then the $\Gamma_i[j] = \Delta_{i'}[j]$;

- The projection of $\perp$ on the second element is acyclic and connected.

A.2 Details on the restriction of a multicut context (Definition 7)

► **Definition 13** (Restriction of a multicut context). Let $\frac{C}{s}$ mcut($\iota, \perp$) be a multicut occurrence such that $C = s_1 \dots s_n$ and let $s_i := F_1, \dots, F_{k_i} \vdash G_1, \dots, G_{r_i}$, we define $C_{F_j}$ (resp. $C_{G_j}$) with $F_j \in s_i$ (resp. $G_j \in s_i$) to be the least sub-context of $C$ such that:

- The sequent $s_i$ is in $C_{F_j}$ (resp. $C_{G_j}$);

- If there exists $l$ such that $(1, i, j) \perp (2, k, l)$ or $(2, i, j) \perp (1, k, l)$ then $s_k \in C_{F_j}$ (resp. $s_k \in C_{G_j}$);

- For any $k \neq i$, if there exists $l$ such that $(1, k, l) \perp (2, k', l')$ or $(2, k, l) \perp (1, k', l')$ and that $s_k \in C_{F_j}$ (resp. $s_k \in C_{G_j}$) then $s_{k'} \in C_{F_j}$ ($s_{k'} \in C_{G_j}$).

We then extend the notation to contexts, setting $C_\emptyset := \emptyset$ and $C_{F,\Gamma} := C_F \cup C_\Gamma$.

A.3 One-step multicut-elimination for $\mu MALL^\infty$

Commutative one-step reductions for $\mu MALL^\infty$ are given in Figure 8 whereas principal reductions in Figure 9.

A.4 One-step multicut-elimination for $\mu LL^\infty$

Commutative one-step reductions for $\mu LL^\infty$ are steps from $\mu MALL^\infty$ together with the reduction of the exponential fragment given in Figure 10.

A.5 Proof of Axiom Expansion property

► **Lemma 13** (Axiom Expansion). One-step axiom expansion holds for formulas $?_\sigma A$ and $!_\sigma A$ in superLL($\mathcal{E}$, $\le_g, \le_f, \le_u$) if $\sigma$ satisfies the following expansion axiom:

$$ \sigma \le_u \sigma \lor \sigma \le_f \sigma \lor (\sigma \le_g \sigma \land \sigma(?_{m_1})). $$

The axiom expansion holds in superLL($\mathcal{E}$, $\le_g, \le_f, \le_u$) if all $\sigma$ satisfy the expansion axiom.

**Proof.** We start by proving the first part of the theorem. We distinguish three cases depending on which branch of the disjunction holds for $\sigma$:
<figure><img src="image_12.png" /><figcaption>■ **Figure 8** Commutative one-step reduction rules for $\mu$MALL$^{∞}$</figcaption></figure>
$$
\begin{align*}
& \frac{\mathcal{C} \quad \overline{\vdash F, F^{\perp}}^{\text{ax}} \quad \text{mcut}(i, \perp)}{\Gamma} \rightsquigarrow \frac{\mathcal{C} \quad \text{mcut}(i', \perp')}{\Gamma} \\
& \frac{\mathcal{C} \quad \overline{\vdash F, \Gamma'} \quad \overline{\vdash F^{\perp}, \Delta} \quad \text{cut}}{\Gamma} \rightsquigarrow \frac{\mathcal{C} \quad \overline{\vdash F, \Gamma'} \quad \overline{\vdash F^{\perp}, \Delta} \quad \text{mcut}(i', \perp')}{\Gamma} \\
& \frac{\mathcal{C} \quad \overline{\vdash F, G, \Delta} \quad \mathfrak{F} \quad \overline{\vdash F^{\perp}, \Gamma_1} \quad \overline{\vdash G^{\perp}, \Gamma_2} \quad \text{\(\otimes\)}}{\Gamma} \rightsquigarrow \frac{\text{mcut}(i, \perp)}{\Gamma} \\
& \frac{\mathcal{C} \quad \overline{\vdash F, G, \Delta} \quad \overline{\vdash F^{\perp}, \Gamma_1} \quad \overline{\vdash G^{\perp}, \Gamma_2}}{\Gamma} \rightsquigarrow \frac{\text{mcut}(i', \perp')}{\Gamma} \\
& \frac{\mathcal{C} \quad \overline{\vdash F_i, \Delta} \quad \oplus_i \quad \overline{\vdash F_1^{\perp}, \Gamma'} \quad \overline{\vdash F_2^{\perp}, \Gamma'}}{\Gamma} \text{\(\&\)} \rightsquigarrow \frac{\text{mcut}(i, \perp)}{\Gamma} \\
& \frac{\mathcal{C} \quad \overline{\vdash F_i, \Delta} \quad \overline{\vdash F_i^{\perp}, \Gamma'}}{\Gamma} \text{\(\&\)} \text{mcut}(i', \perp') \\
& \frac{\mathcal{C} \quad \overline{\vdash F[X := \mu X.F], \Delta} \quad \mu \quad \overline{\vdash F[X := \nu X.F], \Delta'} \quad \nu}{\Gamma} \rightsquigarrow \frac{\text{mcut}(i, \perp)}{\Gamma} \\
& \frac{\mathcal{C} \quad \overline{\vdash F[X := \mu X.F], \Delta} \quad \overline{\vdash \Gamma} \quad \overline{\vdash F[X := \nu X.F], \Delta'}}{\Gamma} \text{\(\&\)} \text{mcut}(i, \perp) \\
& \frac{\mathcal{C} \quad \overline{\vdash 1} \quad \overline{\vdash \Gamma'} \quad \perp}{\Gamma} \text{\(\&\)} \text{mcut}(i, \perp) \rightsquigarrow \frac{\mathcal{C} \quad \overline{\vdash \Gamma'} \quad \text{mcut}(i', \perp')}{\Gamma}
\end{align*}
$$

<caption>Figure 9 Principal one-step reduction rules for $\mu$MALL$^\infty$</caption>
$$ \frac{\pi \quad \frac{\vdash A, ?\Delta}{\vdash !A, ?\Delta} !_p C^!}{\vdash !A, ?\Gamma} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad \frac{\vdash A, ?\Delta}{\vdash !A, ?\Gamma} C^!}{\vdash !A, ?\Gamma} !_p \text{mcut}(\iota, \perp) $$

$$ \frac{\pi \quad \frac{\vdash \Delta}{\vdash ?A, \Delta} ?_w C}{\vdash ?A, \Gamma} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad \frac{\vdash \Delta}{\vdash \Gamma} C}{\vdash ?A, \Gamma} ?_w \text{mcut}(\iota', \perp') $$

$$ \frac{\pi \quad \frac{\vdash A, \Delta}{\vdash ?A, \Delta} ?_d C}{\vdash ?A, \Gamma} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad \frac{\vdash A, \Delta}{\vdash A, \Gamma} C}{\vdash ?A, \Gamma} ?_d \text{mcut}(\iota', \perp') $$

$$ \frac{\pi \quad \frac{\vdash ?A, ?A, \Delta}{\vdash ?A, \Delta} ?_c C}{\vdash ?A, \Gamma} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\pi \quad \frac{\vdash ?A, ?A, \Delta}{\vdash ?A, ?A, \Gamma} C}{\vdash ?A, \Gamma} ?_c \text{mcut}(\iota', \perp') $$

$$ \frac{C_{\Delta} \quad \frac{\vdash \Delta}{\vdash ?A, \Delta} ?_w C'_{?A}}{\vdash \Gamma, ?\Gamma'} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{C_{\Delta} \quad \frac{\vdash \Delta}{\vdash \Gamma} C}{\vdash \Gamma, ?\Gamma'} ?_w \text{mcut}(\iota', \perp') $$

$$ \frac{\vdash A, \Delta}{\vdash ?A, \Delta} ?_d \quad \frac{\vdash A^{\perp}, ?\Delta'}{\vdash !A^{\perp}, ?\Delta'} !_p C}{\vdash \Gamma} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{\vdash A, \Delta}{\vdash \Gamma} \quad \frac{\vdash A^{\perp}, ?\Delta'}{\vdash ?\Gamma', ?\Gamma'} C}{\vdash \Gamma, ?\Gamma'} \text{mcut}(\iota', \perp') $$

$$ \frac{C_{\Delta} \quad \frac{\vdash ?A, ?A, \Delta}{\vdash ?A, \Delta} ?_c C'_{?A}}{\vdash \Gamma, ?\Gamma'} \text{mcut}(\iota, \perp) \rightsquigarrow \frac{C_{\Delta} \quad \frac{\vdash ?A, ?A, \Delta}{\vdash ?\Gamma', ?\Gamma', \Gamma} C^!_{?A} C'_{?A}}{\vdash \Gamma, ?\Gamma'} ?_c \text{mcut}(\iota', \perp') $$

<caption>■ Figure 10 Multicut-elimination steps of the exponential fragment of $\mu$superLL$^\infty$</caption>
■ If $\sigma \le_u \sigma$ is true, then we have:

$$ \frac{\vdash A^{\perp}, A \quad \overline{\sigma \le_u \sigma} !_u}{\vdash !_{\sigma} A^{\perp}, ?_{\sigma} A} $$

■ If $\sigma \le_f \sigma$ is true, it is similar to the previous case:

$$ \frac{\vdash A^{\perp}, A \quad \overline{\sigma \le_f \sigma} !_f}{\vdash !_{\sigma} A^{\perp}, ?_{\sigma} A} $$

■ And if $\sigma \le_g \sigma$ and $\overline{(\sigma)(?_{m_1})}$:

$$ \frac{\vdash A^{\perp}, A \quad \overline{(\sigma)(?_{m_1})} ?_{m_1} \quad \overline{\sigma \le_g \sigma} !_g}{\vdash A^{\perp}, ?_{\sigma} A \quad \overline{\sigma \le_f \sigma} !_f} $$

The second part of the theorem is proved by induction on the size of the formula, using the first part of the theorem. ◀

## A.6 Proof of cut-elimination of superLL (Theorem 3)

We first need three lemmas called the substitution lemmas:

**Lemma 14 (Girard Substitution Lemma).** Let $\sigma_1$ be a signature and $\vec{\sigma}_2$ a list of signatures such that $\sigma_1 \le_g \vec{\sigma}_2$. Let $A$ be a formula, and let $\Delta$ be a context, such that for all $\Gamma$, if $\vdash A, \Gamma$ is provable without using any cut then $\vdash ?_{\vec{\sigma}_2} \Delta, \Gamma$ is provable without using any cut.

Then we have that for all $\Gamma$, if $\vdash \underbrace{?_{\sigma_1} A, \dots, ?_{\sigma_1} A}_{n} \Gamma$ is provable without using any cut then $\vdash \underbrace{?_{\vec{\sigma}_2} \Delta, \dots, ?_{\vec{\sigma}_2} \Delta}_{n} \Gamma$.

**Proof.** First we can notice that for any $\Gamma$ the following rule:

$$ \vdash \begin{array}{c} A, \dots, A, \Gamma \\ ?_{\vec{\sigma}_2} \Delta, \dots, ?_{\vec{\sigma}_2} \Delta, \Gamma \end{array} S_g $$

is admissible in the system without cuts (by an easy induction on the number of $A$).

Now we show the lemma by induction on the proof of $\vdash ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma$. We distinguish cases according to the last rule:

■ If it is a rule on a formula of $\Gamma$ which is not a promotion:

$$ \frac{\pi \qquad IH(\pi)}{\vdash_{?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma'} r \qquad \vdash_{?_{\vec{\sigma}_2} \Delta, \dots, ?_{\vec{\sigma}_2} \Delta, \Gamma'} r} $$

■ If it is a Girard's style promotion, thanks to the axiom (axTrans), we have:

$$ \frac{\pi \qquad \frac{\vdash B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_1} A, \dots, ?_{\sigma_1} A \quad \sigma_0 \le_g \vec{\sigma}_3 \quad \sigma_0 \le_g \sigma_1}{\vdash !_{\sigma_0} B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_1} A, \dots, ?_{\sigma_1} A} !_g}{\vdash B, ?_{\vec{\sigma}_3} \Gamma', ?_{\vec{\sigma}_2} \Delta, \dots, ?_{\vec{\sigma}_2} \Delta \quad \sigma_0 \le_g \vec{\sigma}_3 \quad \frac{\sigma_0 \le_g \sigma_1 \quad \sigma_1 \le_g \vec{\sigma}_2}{\sigma_0 \le_g \vec{\sigma}_2} !_g} (\text{axTrans}) \qquad \vdash !_{\sigma_0} B, ?_{\vec{\sigma}_3} \Gamma', ?_{\vec{\sigma}_2} \Delta, \dots, ?_{\vec{\sigma}_2} \Delta$$
**► Lemma 15 (Functorial Substitution Lemma).** Let $\sigma_1$ be a signature and $\vec{\sigma}_2$ a list of signatures such that $\sigma_1 \leq_f \vec{\sigma}_2$. Let $A$ be a formula, and let $\Delta$ be a context, such that for all $\Gamma$, if $\vdash A, \Gamma$ is provable without using any cut then $\vdash \Delta, \Gamma$ is provable without using any cut. Then we have that for all $\Gamma$, if $\vdash \overbrace{\sigma_1 A, \dots, \sigma_1 A}^n, \Gamma$ is provable without using any cut then $\vdash \overbrace{\sigma_2 \Delta, \dots, \sigma_2 \Delta}^n, \Gamma$ as well.

**Proof.** First we can notice that for any $\Gamma$ the following rule:

$$ \vdash \begin{array}{cccc} A, \dots, A, \Gamma \\ \bar{\vdash} \bar{\Delta}, \dots, \bar{\Delta}, \bar{\Gamma} \end{array} S_f $$

is admissible in the system without cuts (by an easy induction on the number of $A$). Now we show the lemma by induction on the proof of $\vdash \sigma_1 A, \dots, \sigma_1 A, \Gamma$. We distinguish cases according to the last applied rule:

■ If it is a rule on a formula of $\Gamma$ which is not a promotion:

$$ \frac{\begin{array}{c} \pi \\ \vdash \sigma_1 A, \dots, \sigma_1 A, \Gamma' \\ \vdash \sigma_1 A, \dots, \sigma_1 A, \Gamma \end{array} r}{\vdash \sigma_1 B, \dots, \sigma_1 B} \rightsquigarrow \frac{\begin{array}{c} IH(\pi) \\ \vdash \sigma_2 \Delta, \dots, \sigma_2 \Delta, \Gamma' \\ \vdash \sigma_2 \Delta, \dots, \sigma_2 \Delta, \Gamma \end{array} r}{\vdash \sigma_2 B, \dots, \sigma_2 B} $$

■ If it is a Girard's style promotion. Thanks to the axiom (axleqgs), we have:

$$ \frac{\begin{array}{c} \pi \\ \vdash B, \sigma_3 \Gamma', \sigma_1 A, \dots, \sigma_1 A \\ \vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_1 A, \dots, \sigma_1 A \end{array} !_g}{\vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_1 A, \dots, \sigma_1 A} \rightsquigarrow \frac{\begin{array}{c} IH(\pi) \\ \vdash B, \sigma_3 \Gamma', \sigma_2 \Delta, \dots, \sigma_2 \Delta \\ \vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_2 \Delta, \dots, \sigma_2 \Delta \end{array} !_g}{\vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_2 \Delta, \dots, \sigma_2 \Delta} \quad \text{(axleqgs)} $$

■ If it is a unary promotion, we use axiom (axlequs):

$$ \frac{\begin{array}{c} \pi \\ \vdash B, A \\ \vdash \sigma_0 B, \sigma_1 A \end{array} !_u}{\vdash \sigma_0 B, \sigma_1 A} \\ \frac{\begin{array}{c} \pi \\ \vdash B, A \\ \vdash \sigma_0 \leq_u \sigma_1 \\ \vdash \bar{B}, \bar{\Delta} \\ \vdash \sigma_0 \leq_f \bar{\sigma}_2 \end{array} S_f}{\vdash \sigma_0 B, \sigma_2 \Delta} !_f $$

■ If it is a functorial promotion, thanks to the axiom (axTrans) we have:

$$ \frac{\begin{array}{c} \pi \\ \vdash B, \Gamma', A, \dots, A \\ \vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_1 A, \dots, \sigma_1 A \end{array} !_f}{\vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_1 A, \dots, \sigma_1 A} \rightsquigarrow \frac{\begin{array}{c} IH(\pi) \\ \vdash B, \Gamma', A, \dots, A \\ \vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_2 \Delta, \dots, \sigma_2 \Delta \\ \vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_2 \Delta, \dots, \sigma_2 \Delta \end{array} !_f}{\vdash \sigma_0 B, \sigma_3 \Gamma', \sigma_2 \Delta, \dots, \sigma_2 \Delta} \quad \text{(axTrans)} $$
■ If it is a contraction $(?_{c_i})$ on $?_{\sigma_1} A$, we use axiom (axfumpx):

$$ \frac{\pi}{\vdash, \overbrace{?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma}^{n+i-1} (\sigma_1)(?_{c_i})} \overset{?_{c_i}}{\leadsto} \frac{\vdash ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma}{\overbrace{\sigma_1 \leq_f \vec{e}_2}^{\text{IH}(\pi)}} $$

$$ \frac{\pi}{\vdash \overbrace{?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta, \Gamma}^{n+i-1} (\sigma_1)(?_{c_i})} \overset{?_{c_i}}{\leadsto} \frac{\overbrace{(\sigma_1)(?_{c_i})}^{\text{IH}(\pi)} \quad \overbrace{\sigma_1 \leq_f \vec{e}_2}^{\text{axfumpx}}}{\vdash \overbrace{?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta, \Gamma}^{\text{IH}(\pi)}} $$

■ If it is a multiplexing $(?_{m_i})$ on $?_{\sigma_1} A$, we use axiom (axfumpx):

$$ \frac{\pi}{\vdash ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \overbrace{A, \dots, A}^{i}, ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma} (\sigma_1)(?_{m_i}) \overset{?_{m_i}}{\leadsto} \frac{\vdash ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma}{\overbrace{\sigma_1 \leq_f \vec{e}_2}^{\text{IH}(\pi)}} $$

$$ \frac{\pi}{\vdash ?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta, \overbrace{A, \dots, A}^{i}, ?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta, \Gamma} S_f \frac{(\sigma_1)(?_{m_i})}{\overbrace{(\sigma_1)(?_{m_i})}^{\text{IH}(\pi)}} \quad \overbrace{\sigma_1 \leq_f \vec{e}_2}^{\text{axfumpx}} \quad (\sigma_2)(?_{m_i}) \quad \overbrace{?_{m_i}}^{\text{IH}(\pi)} $$

■ If it is an (ax) rule on $?_{\sigma_1} A$. Then $\Gamma = !_{\sigma_1} A^{\perp}$ and we have:

$$ \frac{\overbrace{\vdash A^{\perp}, A}^{\text{ax}} S_f}{\overbrace{\vdash A^{\perp}, \Delta}^{\text{ax}}} \quad \overbrace{\sigma_1 \leq_f \vec{e}_2}^{\text{IH}(\pi)} !_f \quad \vdash !_{\sigma_1} A^{\perp}, ?_{\sigma_2} \Delta $$

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

**Lemma 16 (Unary Functorial Substitution Lemma).** Let $\sigma_1$ and $\sigma_2$ be two exponential signatures such that $\sigma_1 \leq_u \sigma_2$. Let A and B be formulas, such that for all $\Gamma$, if $\vdash A, \Gamma$ is provable without using any cut then $\vdash B, \Gamma$ is provable without using any cut. Then we have that for all $\Gamma$, if $\vdash \overbrace{?_{\sigma_1} A, \dots, ?_{\sigma_1} A}^{n}, \Gamma$ is provable without using any cut then $\vdash \overbrace{?_{\sigma_2} B, \dots, ?_{\sigma_2} B}^{n}, \Gamma$ as well, with $k_i$ positive integers.

**Proof.** This lemma is proven the same way as Lemma 15.

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

Finally we prove cut-elimination theorem 3:

**Theorem 5 (Cut Elimination).** Cut elimination holds for superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) as soon as the 8 cut-elimination axioms of Table 1 are satisfied.

**Proof.** We prove the result by induction on the couple $(t, s)$ with lexicographic order, where $t$ is the size of the cut formula and $s$ is the sum of the sizes of the premises of the cut. We distinguish cases depending on the last rules of the premises of the cut:

■ If one of the premises does not end with a rule acting on the cut formula, we apply the induction hypothesis with the premise(s) of this rule.
■ If both last rules act on the cut formula which does not start with an exponential connective, we apply the standard reduction steps for non-exponential cuts leading to cuts involving strictly smaller cut formulas. We conclude by applying the induction hypothesis.

■ If we have an exponential cut for which the cut formula $!_{\sigma_1} A^{\perp}$ is not the conclusion of a promotion rule introducing $!_{\sigma_1}$, the rule above $!_{\sigma_1} A^{\perp}$ cannot be a promotion rule, and we apply the induction hypothesis to its premise(s).

■ If we have an exponential cut for which the cut formula $!_{\sigma_1} A^{\perp}$ is the conclusion of an (!_g)-rule. We can apply:

$$ \frac{\vdash A^{\perp}, ?_{\sigma_2} \Delta \qquad \sigma_1 \leq_g \sigma_2}{\vdash !_{\sigma_1} A^{\perp}, ?_{\sigma_2} \Delta} !_g \qquad \vdash ?_{\sigma_1} A, \Gamma \qquad \sigma_1 \leq_g \sigma_2 \qquad \text{Lem. 14} \\ \text{cut} \qquad \vdash ?_{\sigma_2} \Delta, \Gamma \qquad \text{cut} \qquad \vdash ?_{\sigma_2} \Delta, \Gamma \qquad \text{Lem. 14} $$

We have that A and Δ are such that for every Γ such that $\vdash A, \Gamma$ is provable without cuts, $\vdash ?_{\sigma_2} \Delta, \Gamma$ too. Indeed, A and Δ are such that $\vdash A^{\perp}, ?_{\sigma_2} \Delta$ is provable without cuts and we can apply the induction hypothesis ($\#(A) < \#(\sigma_1 A)$). Therefore, we can apply Lemma 14 on $\vdash ?_{\sigma_1} A, \Gamma$ and obtain that $\vdash ?_{\sigma_2} \Delta, \Gamma$ is provable without cut.

■ If we have an exponential cut for which the cut formula $!_{\sigma_1} A^{\perp}$ is the conclusion of an (!_f)-rule. We can apply:

$$ \frac{\vdash A^{\perp}, \Delta \qquad \sigma_1 \leq_f \sigma_2}{\vdash !_{\sigma_1} A^{\perp}, ?_{\sigma_2} \Delta} !_f \qquad \vdash ?_{\sigma_1} A, \Gamma \qquad \sigma_1 \leq_f \sigma_2 \qquad \text{Lem. 15} \\ \text{cut} \qquad \vdash ?_{\sigma_2} \Delta, \Gamma \qquad \text{cut} \qquad \vdash ?_{\sigma_2} \Delta, \Gamma \qquad \text{cut} $$

We have that A and Δ are such that for every Γ such that $\vdash A, \Gamma$ is provable without cuts, $\vdash \Delta, \Gamma$ too. Indeed, A and Δ are such that $\vdash A^{\perp}, \Delta$ is provable without cuts and we can apply the induction hypothesis. Therefore, we can apply Lemma 15 on $\vdash ?_{\sigma_1} A, \Gamma$ and obtain that $\vdash ?_{\sigma_2} \Delta, \Gamma$ is provable without cut.

■ If we have an exponential cut for which the cut formula $!_{\sigma_1} A^{\perp}$ is the conclusion of an (!_u)-rule, this case is treated in the exact same way as (!_f), using Lemma 16.

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

## A.7 Details on ELL as instance of superLL

### A.7.0.1 Elementary Linear Logic.

Elementary Linear Logic (ELL) [12, 9] is a variant of LL where we remove (?_d) and (!_g) and add the functorial promotion:

$$ \frac{\vdash A, \Gamma}{\vdash !A, ?\Gamma} !_f $$

It is the superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) system with $\mathcal{E} = \{\bullet\}$, defined by $\bullet(?_{c_2}) = \bullet(?_{m_0}) = \text{true}$ (and $(\bullet)(r) = \text{false}$ otherwise), $\leq_g = \leq_u = \emptyset$ and $\bullet \leq_f \bullet$. This superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) instance is ELL and satisfies the cut-elimination axioms and the expansion axiom:

■ The rule (?_{m_0}) is the weakening rule (?_w), (?_{c_2}) is the contraction rule (?_c), and we can always apply promotion (!_f) as $\leq_f$ is the plain relation on $\mathcal{E}$:

$$ \frac{\vdash A, \Gamma \quad \overline{\bullet \leq_f \bullet}}{\vdash ! \bullet A, ? \bullet \Gamma} !_f \qquad \text{Lem. 16} $$

We have that (!_g) is a restriction of (!_f) in ELL and (!_u) is non-existent.
Moreover, the cut-elimination axioms are satisfied. As $\mathcal{E}$ is a singleton, axioms (axgmpx), (axfumpx), (axcontr), (axTrans), (axleqgs), (axleqfu), (axlequs) hold. Axiom (axleqfg) is vacuously satisfied.

The expansion axiom is satisfied since $\le_f$ is reflexive.

## B Details on Section 3

### B.1 Details on $\mu LL_{\square}^{\infty}$ as an instance of $\mu superLL^{\infty}$

The system $\mu LL_{\square}^{\infty}$ is the system $\mu superLL^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ such that:

The set of signatures contains two elements $\mathcal{E} := \{\bullet, \star\}$.

$?_{c_2}(\bullet) = ?_{c_2}(\star) = \text{true} \ ?_{m_1}(\bullet) = \text{true}, ?_{m_0}(\bullet) = ?_{m_0}(\star) = \text{true}, \text{ and all the other elements have value false for both signatures.}$

$\bullet \le_g \bullet; \bullet \le_g \star, \star \le_f \star, \text{ and all couples for the three relations } \le_g, \le_f \text{ and } \le_u \text{ being false.}$
This system is $\mu LL_{\square}^{\infty}$ when taking:

$$?_{\bullet} := ?, !_{\bullet} := !, ?_{\star} := \diamond \text{ and } !_{\star} := \square.$$

Moreover, the system satisfy cut-elimination axioms of figure 1:

Hypotheses of axiom (axcontr) are only true for $i = 2$ in two cases: for $\sigma = \sigma' = \bullet$, in that case $\bar{\sigma}(?_{c_2})$ is true because $\sigma(?_{c_2})$ is; or for $\sigma = \bullet$ and $\sigma' = \star$, in that case the axiom is satisfied as $\sigma'(?_{c_2})$ is true.

Hypotheses of axiom (axgmpx) are true for $i = 0$ when $\sigma = \sigma' = \bullet$, or for $\sigma = \bullet$ and $\sigma' = \star$, in both cases we have that $\bar{\sigma}'(?_{c_0})$ is true because $\sigma'(?_{m_0})$ is true.

Axiom (axgmpx) is always true for $i = 1$.

Hypotheses of axiom (axgmpx) are not satisfied for $i > 1$.

Hypotheses of axiom (axfumpx) are satisfied only for $\sigma = \sigma' = \star$ and so easily satisfied.

Axiom (axTrans) is satisfied as $\le_g$ and $\le_f$ are transitive.

Hypotheses of axiom (axleqgs) are only satisfied for $\sigma = \bullet$ and $\sigma' = \sigma'' = \star$, and in this case the conclusion is one of the hypothesis.

Hypotheses of the other axioms are never fully satisfied.

## C Details on Section 4

### C.1 Details on the justification of (mcut)-steps

The case $(\text{comm}_{!g})$ covers all the case where $(!_g)$ commute under the cut:

► Lemma 17 (Justification for step (comm$_!g$)). If

$$\frac{\pi \quad \vdash A, ?_{\vec{\tau}}\Delta \quad \sigma \le_g \vec{\tau} \quad !_g \quad C' \quad \text{mcut}(\iota, \perp)}{\vdash !_{\sigma} A, ?_{\vec{\tau}}\Delta \quad \vdash !_{\sigma} A, ?_{\vec{\rho}}\Gamma}$$

is a $\mu superLL^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$-proof then

$$\frac{\pi \quad \vdash A, ?_{\vec{\tau}}\Delta \quad C' \quad \text{mcut}(\iota, \perp) \quad \sigma \le_g \vec{\rho} \quad !_g}{\vdash A, ?_{\vec{\rho}}\Gamma \quad \vdash !_{\sigma} A, ?_{\vec{\rho}}\Gamma}$$

is also a $\mu superLL^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$-proof.
**Proof.** We prove that for each sequent $\vdash !_{\sigma'} A', ?_{\vec{\tau}'} \Delta'$ of $C' := C^! \cup \{\vdash !_{\sigma} A, ?_{\vec{\tau}} \Delta\}$, we have that $\sigma \le_g ?_{\vec{\tau}'}$.

The $\perp$-relation extended to sequent defines a tree on $C'$. Taking $\vdash !_{\sigma} A, ?_{\vec{\tau}} \Delta$ as the root, the ancestor relation of this tree is a well-founded relation. We can therefore do a proof by induction:

- The base case is given by the condition of application of (!_g) in the proof.

- For heredity, we have that there is a sequent $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta'', ?_{\sigma'}(A'^{\perp})$ of $C'$, connected on !_\sigma A' to our sequent. By induction hypothesis, we have that $\sigma \le_g \sigma'$. The rule on top of $\vdash !_{\sigma'} A', ?_{\vec{\tau}'} \Delta'$ is a promotion. We have two cases:

- If it's an (!_g)-promotion, we can use axiom (axTrans) with the application condition of the promotion, to get $\sigma \le_g ?_{\vec{\tau}'}$.

- If it's an (!_f)-promotion or an (!_u)-promotion, we can use axiom (axleqgs) with the application condition of the promotion, to get $\sigma \le_g ?_{\vec{\tau}'}$.

We conclude by induction and use the inequalities to prove that $\sigma \le_g ?_{\vec{\rho}}$.

The case (comm<sub>!_f</sub><sup>1</sup>) covers the case of commutation of an (!_f)-promotion but where only (!_g)-rules with empty contexts appears in the hypotheses of the multi-cut. Note that an (!_g) occurrence with empty context could be seen as an (!_f) occurrence (with empty context).

**► Lemma 18 (Justification for step (comm<sub>!_f</sub><sup>1</sup>)).** If

$$ \frac{\displaystyle\frac{\pi}{\vdash A, \Delta} \quad \sigma \le_f ?_{\vec{\tau}} !_f}{\displaystyle\frac{\vdash !_{\sigma} A, ?_{\vec{\tau}} \Delta !_f}{\vdash !_{\sigma} A, ?_{\vec{\rho}} \Gamma}} C^! \quad \text{mcut}(\iota, \perp)} $$

is a $\mu$superLL<sup>\infty</sup>(&#x1d540;, &le;<sub>g</sub>, &le;<sub>f</sub>, &le;<sub>u</sub>)-proof with $C^!$ such that each sequents concluded by an (!_g) have an empty context, then

$$ \frac{\pi}{\displaystyle\frac{\vdash A, \Delta C}{\vdash A, \Gamma}} \text{mcut}(\iota, \perp) \quad \sigma \le_f ?_{\vec{\rho}} !_f $$

is a $\mu$superLL<sup>\infty</sup>(&#x1d540;, &le;<sub>g</sub>, &le;<sub>f</sub>, &le;<sub>u</sub>)-proof.

**Proof.** We prove that for each sequent $\vdash !_{\sigma'} A', ?_{\vec{\tau}'} \Delta'$ of $C' := C^!_g \cup \{\vdash !_{\sigma} A, ?_{\vec{\tau}} \Delta\}$, $\sigma \le_f ?_{\vec{\tau}'}$.

The $\perp$-relation extended to sequent defines a tree on $C'$. Taking $\vdash !_{\sigma} A, ?_{\vec{\tau}} \Delta$ as the root, the ancestor relation of this tree is a well-founded relation. We can therefore do an induction proof:

- The base case is given by the condition of application of (!_f) in the proof.

- For heredity, we have that there is a sequent $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta'', ?_{\sigma'}(A'^{\perp})$ of $C'$, connected on !_\sigma A' to our sequent. By induction hypothesis, we have that $\sigma \le_f \sigma'$. The rule on top of $\vdash !_{\sigma'} A', ?_{\vec{\tau}'} \Delta'$ is a promotion. We have three cases:

- If it's an (!_g)-promotion, then the context is empty and the proof is easily satisfied.

- If it's an (!_f)-promotion, we can use axiom (axTrans) with the application condition of the promotion to get $\sigma \le_f ?_{\vec{\tau}'}$.

- If it's an (!_u)-promotion, we can use axiom (axleqfu) with the application condition of the promotion to get $\sigma \le_f ?_{\vec{\tau}'}$.

We conclude by induction and use the inequalities to prove that $\sigma \le_f ?_{\vec{\rho}}$.

We then have the following case where we commute an (!_f)-rule, but where there is one (at least) (!_g)-promotion with a non-empty context in the premisses of the multicut rule:
► Lemma 19 (Justification for step (comm<sub>l</sub><sup>2</sup>)). If

$$
\frac{\pi}{\frac{\vdash A, \Delta \qquad \sigma \leq_f \vec{\tau}}{\vdash !_\sigma A, ?_{\vec{\tau}} \Delta} !_f} \frac{C^!}{\vdash !_\sigma A, ?_{\vec{\rho}} \Gamma} \text{mcut}(\iota, \perp)
$$

is a µsuperLL<sup>∞</sup>(E, ≤<sub>g</sub>, ≤<sub>f</sub>, ≤<sub>u</sub>)-proof with C<sup>!g</sup> containing a sequent conclusion of an (!<sub>g</sub>)-rule
with at least one formula in the context, then

$$
\frac{\pi}{\frac{\vdash A, \Delta \quad \vec{\tau}(?_{m_1})}{\vdash A, ?_{\vec{\tau}} \Delta}} ?_{m_1} \frac{C^!}{\frac{\vdash A, ?_{\vec{\rho}} \Gamma}{\vdash !_{\sigma} A, ?_{\vec{\rho}} \Gamma}} \sigma \leq_g \vec{\rho} !_g
$$

is also a µsuperLL<sup>∞</sup>(E, ≤<sub>g</sub>, ≤<sub>f</sub>, ≤<sub>u</sub>)-proof.

**Proof.** We prove that for each sequent $\vdash !_{\sigma'} A', ?_{\tau'} \Delta'$ of $C^! := C_1^{!g} \cup C_2^{!f} \cup C_3^{!u} \cup \{\vdash !_{\sigma} A, ?_{\tau} \Delta\}$,
we have that $\sigma \leq_g \tau'$. Moreover, we prove that $\vec{\tau}(?_{m_1})$. We prove that in two steps:

1. There is a sequent $\vdash !_{\sigma'} A', ?_{\tau'} \Delta'$, with $\Delta'$ being non-empty, which is conclusion of an ($!_g$)-rule. Let's suppose without loss of generality, that this sequent is the closest such sequent to $S := \vdash !_{\sigma} A, ?_{\tau} \Delta$. The $\perp$-relation extended to sequents defines a tree with the hypotheses of the multi-cut rule, therefore there is a path from the sequent $S$ to the sequent $S' := \vdash !_{\sigma'} A', ?_{\tau'} \Delta'$, of sequents $\vdash !_{\sigma''} A''$, $?_{\tau''} \Delta''$. We prove by induction on this path, starting from $S$ and stopping one sequent before $S'$ that $\sigma \leq_f \tau''$:

- The initialisation comes from the condition of application of !_f on S.

- For the heredity, we have that the sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is cut-connected to a
$\vdash !_{\sigma(3)} A^{(3)}, ?_{\tau(3)} \Delta^{(3)}, ?_{\sigma''} (A''^{\perp})$ on $!_{\sigma''} A''$, therefore $\sigma \leq_f \sigma''$. We have two cases: either
this sequent is the conclusion of an ($!_u$)-rule and we apply axiom (axleqfu), either of
an ($!_f$)-rule and we apply axiom (axTrans). In each case, we have that $\sigma \leq_f \tau''$.

We conclude by induction and get a sequent $S'' := \vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ cut-connected to $S'$ on
the formula $!_{\sigma'} A'$ with $\sigma \leq_f \tau''$. From that we get that $\sigma \leq_f \sigma'$. Moreover, we have that
$\sigma' \leq_g \tau'$. As $\Delta'$ is non-empty, there is a signature $\rho' \in \tau'$ such that $\sigma' \leq_g \rho'$. We can
therefore apply axiom (axleqfg). We get that for each signatures $\sigma^{(3)}$ such that $\sigma \leq_f \sigma^{(3)}$,
$\sigma \leq_g \sigma^{(3)}$ and $\sigma^{(3)}(?_{m_1})$, which we can apply to $\sigma$ and $\vec{\tau}$ to get that $\sigma \leq_g \vec{\tau}$ and $\vec{\tau}(?_{m_1})$.

2. Then, we prove by induction on the tree defined with the $\perp$-relation and rooted by $S$
that for each sequents $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta'', \sigma \leq_g \tau''$:

- The initialisation is done with the first step.

- For heredity, we have that there is a sequent
$\vdash !_{\sigma(3)} A^{(3)}, ?_{\tau(3)} \Delta^{(3)}, ?_{\sigma''} (A''^{\perp})$ cut-connected to $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ on $!_{\sigma''} A''$, mean-
ing that $\sigma \leq_g \sigma''$, as the sequent is the conclusion of a promotion, we have that
$\sigma'' \leq_s \tau''$ for a $s \in \{g, f, u\}$, we conclude using axiom (axleqgs).

We conclude by induction and we use the inequalities from it to prove that $\sigma \leq_g \vec{\rho}$.

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

We then cover the cases where we commute an (!_u)-rule with the multi-cut. The first case is where there are only a list of (!_u)-rules in the hypotheses of the multi-cut:
► Lemma 20 (Justification for step (comm<sup>1</sup><sub>u</sub>)). If

$$ \frac{\pi \quad \sigma \leq_u \tau \quad !_u}{\vdash A, C \quad \vdash !_\sigma A, ?_\tau C \quad \vdash !_\sigma A, ?_\rho B} C^!_u \quad \text{mcut}(\iota, \perp) $$

is a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof, then

$$ \frac{\pi \quad C \quad \sigma \leq_u \rho \quad !_u}{\vdash A, B \quad \vdash !_\sigma A, ?_\rho B} C^!_u \quad \text{mcut}(\iota, \perp) $$

is a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof.

**Proof.** We prove that for each sequent $\vdash !_\sigma A', ?_\tau B'$ of $C' := C^!_u \cup \{\vdash !_\sigma A, ?_\tau B\}$, we have that $\sigma \leq_u \tau'$.

The $\perp$-relation extended to sequent defines a tree on $C'$. Taking $\vdash !_\sigma A, ?_\tau B$ as the root, the ancestor relation of this tree is a well-founded relation. We can therefore do an induction proof:

■ The base case is given by the condition of application of $(!_u)$ in the proof.

■ For heredity, we have that there is a sequent $\vdash !_{\sigma''} A'', ?_{\tau''} B'', ?_{\sigma'} (A'^{\perp})$ of $C'$, connected on $!_{\sigma'} A'$ to our sequent. By induction hypothesis, we have that $\sigma \leq_u \sigma'$. The rule on top of $\vdash !_{\sigma'} A', ?_{\tau'} B'$ is an $(!_u)$-promotion, we can use axiom (axTrans) and with the application condition of the promotion, we get that $\sigma \leq_u f'$.

We conclude by induction and get that $\sigma \leq_u \rho$.

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

The second case of $(!_u)$-commutation is where we have an $(!_f)$-rule and where the hypotheses concluded by an $(!_g)$-rule have empty contexts.

► Lemma 21 (Justification for step (comm<sup>2</sup><sub>u</sub>)). Let

$$ \frac{\pi \quad \sigma \leq_u \tau \quad !_u}{\vdash A, B \quad \vdash !_\sigma A, ?_\tau B \quad \vdash !_\sigma A, ?_\rho \Gamma} C^!_u \quad \text{mcut}(\iota, \perp) $$

be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof with $C$ containing at least one proof concluded by an $(!_f)$-promotion; and such that for each sequent conclusion of an $(!_g)$-promotion has empty context. We have that

$$ \frac{\pi \quad C \quad \sigma \leq_f \vec{\rho} \quad !_f}{\vdash A, B \quad \vdash A, \Gamma} \quad \text{mcut}(\iota, \perp) $$

is also a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof.

**Proof.** If one $(!_f)$-rule has empty contexts, there is only one $(!_f), ?_\rho \Gamma$ is empty and therefore $\sigma \leq_f \vec{\rho}$ is easily satisfied. If not, we do our proof in two steps:
1. As always, we notice that the $\perp$-relation extended to sequent defines a tree on $C'$, meaning that there is a path in this tree, from $S := \vdash !_\sigma A, ?_\tau B$ to a sequent $S' := \vdash !_{\sigma'} A', ?_{\tau'} \Delta$ being the conclusion of an !f-rule and with $\Delta$ being non-empty. Without loss of generality, we ask for $S'$ to be the closest such sequent (with respect to the $\perp$-relation). We prove by induction on this path, starting from $S$ and stopping one sequent before $S'$, that for each sequent $\vdash !_{\sigma''} A'', ?_{\tau''} B''$, that $\sigma \le_u \tau''$:

- The initialization comes from the condition of application of (!_u) on S.

- The heredity comes from the condition of application of !_u on the sequent $\vdash !_{\sigma''} A'', ?_{\tau''} B''$ and from lemma (axTrans).

Finally, as $S'$ is linked by the cut-formula $!_{\sigma'} A'$ to one of these sequents, we get that $\sigma \le_u \sigma'$. By the condition of application of (!_f) on $S'$, we get that $\sigma' \le_f \tau''$, and from lemma (axlequs), we have that $\sigma \le_f \tau''$.

2. We prove, for the remaining tree (which is rooted in $S'$), that for each sequents $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$, that $\sigma \le_f \tau''$. We prove it by induction.

- Initialization was done at last point.

- For heredity, if the sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is the conclusion of an (!_u)-rule, by induction hypothesis, we get that $\sigma \le_f \sigma''$, and by (!_u) application condition we get that $\sigma'' \le_u \tau''$, we get $\sigma \le_f \tau''$ with axiom (axleqfu).

- For heredity, if the sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is the conclusion of an (!_f)-rule, by induction hypothesis, we get that $\sigma \le_f \sigma''$, and by (!_f) application condition we get that $\sigma'' \le_f \tau''$, we get $\sigma \le_f \tau''$ with axiom (axTrans).

- For heredity, if the sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is the conclusion of an (!_g)-rule, then $\Delta''$ is empty and the proposition is easily satisfied.

We conclude by induction and we use the inequalities from it to prove that $\sigma \le_f \vec{\rho}$.

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

The following lemma deals with the case where there are sequents concluded by an (!_g)-rule with non-empty context and where the first rule encountered is an !f-rule.

**Lemma 22 (Justification for step (comm$^3_u$)).** Let

$$ \frac{\begin{array}{c} \pi_1 \\ \vdash A, B \\ \vdash !_{\sigma} A, ?_{\tau} B \end{array} \qquad \begin{array}{c} \sigma \le_u \tau \\ !_u \\ C_1^! \end{array} \qquad \frac{\begin{array}{c} \pi_2 \\ \vdash C, \Delta \\ \vdash !_{\sigma'} C, ?_{\tau'} \Delta \end{array} \qquad \begin{array}{c} \sigma' \le_f \tau' \\ !_f \\ C_2^! \end{array} \qquad \begin{array}{c} \text{mcut}(\iota, \perp) \\ \vdash !_{\sigma} A, ?_{\rho} \Gamma \end{array} $$

be a $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-proof, such that $C_2^!$ contains a sequent conclusion of an (!_g) rule with non-empty context; $C := \{\vdash !_\sigma A, ?_\tau B\} \cup C_1^! \cup \{\vdash !_{\sigma'} C, ?_{\tau'} \Delta\}$ are a cut-connected subset of sequents; and $C' := \{\vdash !_{\sigma'} C, ?_{\tau'} \Delta\} \cup C_2^!$ another one. We have that

$$ \frac{\begin{array}{c} \pi_1 \\ \vdash A, B \\ C_1 \end{array} \qquad \frac{\begin{array}{c} \pi_2 \\ \vdash C, \Delta \\ \vdash C, ?_{\tau'} \Delta \\ \vdash A, ?_{\rho} \Gamma \end{array} \qquad \begin{array}{c} \tau'(?_{m_1}) \\ ?_{m_1} \\ \text{mcut}(\iota, \perp) \\ \vdash !_{\sigma} A, ?_{\tau'} \Delta \end{array} \qquad \begin{array}{c} C_2^! \\ C_2^! \\ \text{mcut}(\iota, \perp) \\ \vdash !_{\sigma} A, ?_{\rho} \Gamma \end{array} $$

is also a $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-proof.

**Proof.** We do our proof in three steps:

1. There is a sequent $S'' := \vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$, with $\Delta''$ being non-empty, which is conclusion of an (!_g)-rule. The $\perp$-relation extended to sequents defines a tree on $C'$, therefore there is a path from the sequent $S' := \vdash !_{\sigma'} C, ?_{\tau'} \Delta$ to the sequent $S''$, of sequents $\vdash !_{\sigma'} A^{(3)}, ?_{\tau'} \Delta^{(3)}$. Let's suppose without loss of generality, that this sequent is the closest such sequent to $S'$. We prove by induction on this path, starting from $S'$ and stopping one sequent before $S''$ that $\sigma' \le_f \tau^{(3)}$:
- The initialisation comes from the condition of application of !_f on S'.

- For the heredity, we have that the sequent $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} \Delta^{(3)}$ is cut-connected to a $\vdash !_{\sigma^{(4)}} A^{(4)}, ?_{\tau^{(4)}} \Delta^{(4)}, ?_{\sigma^{(3)}} (A^{(3)\perp})$ on $!_{\sigma^{(3)}} A^{(3)}$, therefore $\sigma' \leq_f \sigma^{(3)}$. We have two cases: either this sequent is the conclusion of an (!_u)-rule and we apply axiom (axleqfu), either of an (!_f)-rule and we apply axiom (axTrans). In each case, we have that $\sigma' \leq_f \tau^{(3)}$. We conclude by induction and get a sequent $S^{(3)} := \vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} \Delta^{(3)}$ cut-connected to $S''$ on the formula $!_{\sigma''} A''$ with $\sigma' \leq_f \tau^{(3)}$. From that we get that $\sigma' \leq_f \sigma''$. Moreover, we have that $\sigma'' \leq_g \tau''$. As $\Delta''$ is non-empty, there is a signature $\rho'' \in \tau''$ such that $\sigma'' \leq_g \rho''$. We can therefore apply axiom (axleqfg). We get that for each signatures $\sigma^{(4)}$ such that $\sigma' \leq_f \sigma^{(4)}, \sigma' \leq_g \sigma^{(4)}$ and $\sigma^{(4)}(?_{m_1})$, which we can apply to $\sigma'$ and $\tau'$ to get that $\sigma' \leq_g \tau'$ and $\tau'(?_{m_1})$.

2. Again, we notice that the $\perp$-relation extended to sequent defines a tree on $C$, meaning that there is a path in this tree, from $S := \vdash !_\sigma A, ?_\tau B$ to $S'$. We prove by induction on this path, starting from $S$ and stopping one sequent before $S'$, that for each sequent $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} B^{(3)}$, that $\sigma \leq_u \tau^{(3)}$:

- The initialization comes from the condition of application of (!_u) on S.

- The heredity comes from the condition of application of !_u on the sequent $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} B^{(3)}$ and from lemma (axTrans).

Finally, as $S'$ is linked by the cut-formula $!_\sigma A'$ to one of these sequents, we get that $\sigma \leq_u \sigma'$.

3. Finally, we prove that for each sequents $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} \Delta^{(3)}$ of $C'$, $\sigma \leq_g \tau^{(3)}$. We prove it by induction as $C'$ is a tree with the $\perp$-relation.

- Initialization comes from the face that $\sigma \leq_u \sigma'$, $\sigma' \leq_g \tau'$ and axiom (axlequs).

- For heredity, we have that there is a sequent $\vdash !_{\sigma^{(4)}} A^{(4)}, ?_{\tau^{(4)}} \Delta^{(4)}, ?_{\sigma^{(3)}} (A^{(3)})^\perp$ of $C'$, connected on $!_{\sigma^{(3)}} A^{(3)}$ to our sequent. By induction hypothesis, we have that $\sigma \leq_g \sigma^{(3)}$. The rule on top of $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} \Delta^{(3)}$ is a promotion. We have two cases:

- If it's a (!_g)-promotion, we can use axiom (axTrans) and with the application condition of the promotion, we get that $\sigma \leq_g \tau^{(3)}$.

- If it's an (!_f)-promotion or an (!_u)-promotion, we can use axiom (axleqgs) and with the application condition of the promotion, we get that $\sigma \leq_g \tau^{(3)}$.

We conclude by induction.

We got two important properties:

1. For each sequent $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} \Delta^{(3)}$ of $C'$, we have that $\sigma \leq_g \tau^{(3)}$.

2. We have $\tau'(?_{m_1})$.

We conclude using inequalities of the first property to find that $\sigma \leq_g \vec{\rho}$. And we use the second property for the (?_{m_1})-rule. ◀

The last lemma of promotion commutation is about the case where we commute an (!_u)-promotion but when first meeting an (!_g)-promotion.

► Lemma 23 (Justification for step (comm$^4_u$)). Let

$$ \frac{\begin{array}{c} \pi_1 \\ \vdash A, B \qquad \sigma \leq_u \tau \\ \vdash !_\sigma A, ?_\tau B \end{array}}{!_u} \quad C_1^{!_u} \quad \frac{\begin{array}{c} \pi_2 \\ \vdash C, ?_{\tau'} \Delta \qquad \sigma' \leq_g \tau' \\ \vdash !_{\sigma'} C, ?_{\tau'} \Delta \end{array}}{!_g} \quad C_2^{!_2} \quad \frac{\begin{array}{c} \text{mcut}(\iota, \perp) \\ \vdash !_\sigma A, ?_{\vec{\rho}} \Gamma \end{array}}{!_u} $$
be a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$-proof such that $\mathcal{C} := \{\vdash !_\sigma A, ?_\tau B\} \cup C_1^! \cup \{\vdash !'_\sigma C, ?'_\tau \Delta\}$ are a cut-connected subset of sequents; and $\mathcal{C}' := \{\vdash !'_\sigma C, ?'_\tau \Delta\} \cup C_2^!$ another one. Then,

$$ \frac{\begin{array}{c} \pi_1 \\ \vdash A, B \end{array} \quad \begin{array}{c} \pi_2 \\ C_1 \quad \vdash C, ?_{\vec{\tau}} \Delta \quad C_2^! \end{array} \quad \frac{\begin{array}{c} \text{mcut}(\iota, \perp) \\ \vdash A, ?_{\vec{\rho}} \Gamma \end{array}}{\begin{array}{c} \sigma \le_g \vec{\rho} \\ \vdash !'_\sigma A, ?_{\vec{\rho}} \Gamma \end{array}} !_g $$

is also a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$-proof.

**Proof.** We do our proof in two steps:

1. First, we prove that for each sequents $\vdash !_{\sigma''} A, ?_{\tau''} B$ of $\mathcal{C} \setminus \{\vdash !_\sigma C, ?_{\tau'} \Delta\}$ that $\sigma \le_u \tau''$. We prove it by induction on this list starting with the sequent $S := \vdash !_\sigma A, ?_{\tau'} B$ (it is a list with the $\perp$-relation):

- Initialization comes from the condition of application of $(!_u)$ on $S$.

- Heredity comes from the condition of application of $(!_u)$ on the concerned sequent, from induction hypothesis and from axiom (axTrans).

We conclude by induction and deduce from the obtained property that $\sigma \le_u \sigma'$.

2. We then prove that for each sequents $\vdash !_{\sigma''} A, ?_{\tau''} \Delta$ of $\mathcal{C}'$, $\sigma \le_g \tau''$. We prove it by induction on $\mathcal{C}'$ as the $\perp$-relation defines a tree on it, for which we take $S' := !_{\sigma'} C, ?_{\tau'} \Delta$ as the root.

- The initialization comes from $\sigma \le_u \sigma'$ that we showed for first step, from $\sigma' \le_g \tau'$ which is the condition of application of $(!_g)$ on $S'$ and from axiom (axlequs).

- For heredity, we have that there is a sequent $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\tau^{(3)}} \Delta^{(3)}, ?_{\sigma''} (A''^\perp)$ of $\mathcal{C}'$, connected on $!_{\sigma''} A''$ to our sequent. By induction hypothesis, we have that $\sigma \le_g \sigma''$. The rule on top of $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is a promotion. We have two cases:

- If it's a $(!_g)$-promotion, we can use axiom (axTrans) and with the application condition of the promotion, we get that $\sigma \le_g \tau''$.

- If it's an $(!_f)$-promotion or an $(!_u)$-promotion, we can use axiom (axleqgs) and with the application condition of the promotion, we get that $\sigma \le_g \tau''$.

We conclude by induction

From the inequalities that we get from induction, we can easily prove that $\sigma \le_g \vec{\rho}$. $\quad$

Then we have the principal cases, starting with the contraction:

**► Lemma 24 (Justification for step (principal$_{?_c}$)).** If

$$ \frac{\begin{array}{c} \pi \\ \begin{array}{c} \underbrace{\vdash ?_\sigma A, \dots, ?_\sigma A}_{i} \Delta \\ C_\Delta \end{array} \quad \begin{array}{c} \sigma(\underline{?_{c_i}}) \\ ?_{c_i} \end{array} \quad \begin{array}{c} C_{?_\sigma A}^! \end{array} \end{array}}{\begin{array}{c} \vdash ?_\sigma A, \Delta \\ \Gamma, ?_{\vec{\rho}} \Gamma' \end{array}} \text{mcut}(\iota, \perp) $$

is a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$-proof, then

$$ \frac{\begin{array}{c} \pi \\ \begin{array}{c} \underbrace{\vdash ?_\sigma A, \dots, ?_\sigma A}_{i} \Delta \\ C_\Delta \end{array} \quad \begin{array}{c} C_{?_\sigma A}^! \quad \dots \quad C_{?_\sigma A}^! \end{array} \quad \begin{array}{c} \text{mcut}(\iota', \perp') \\ \Gamma, ?_{\vec{\rho}} \Gamma', \dots, ?_{\vec{\rho}} \Gamma' \end{array} \end{array}}{\begin{array}{c} \vdash \Gamma, ?_{\vec{\rho}} \Gamma' \end{array}} \quad \begin{array}{c} ?_{c_i} \vec{\rho} \\ ?_{c_i} \vec{\rho} \end{array} $$

is also a $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$-proof.
**Proof.** We prove for each sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta'' \in C_{\tau, \sigma A}^!$, we have that $\sigma \le_s \tau''$ (for one $s \in \{g, f, u\}$). As the relation $\perp$ defines a tree on $C' : C_{\tau, \sigma A}^!$ (rooted on the sequent $S := \vdash !_{\sigma} A, ?_{\tau'} \Delta'$ which is the sequent connected to $\vdash ?_{\sigma} A, \Delta$ on $?_{\sigma} A$), we do a proof by induction on this tree:

- Initialization comes from the application condition of the promotion.

- For heredity, we get from induction hypothesis that $\sigma \le_s \sigma''$ for a $s \in \{g, f, u\}$, from the condition of application of the promotion, we get that $\sigma'' \le_{s'} \tau''$ (again for a $s' \in \{g, f, u\}$), depending on the cases, from axioms (axTrans), (axleqgs), (axleqfu), (axleqfg), (axlequs), we get that $\sigma \le_{s''} \tau''$ for a $s'' \in \{g, f, u\}$.

We conclude by induction, we get using the obtained property, the fact that $\sigma(?_{c_i})$ and from axiom (axcontr), that for each sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta'' \in C_{\tau, \sigma A}^!$, $\bar{\tau}''(?_{c_i})$. We use property 1 to get that $\bar{\rho}(?_{c_i})$ is true, making the derivation valid in the proof of the statement. ◀

**► Definition 14.** Let $S^!$ be a sequent of a $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-context $C^!$, such that $C^!$ is a tree with respect to a cut-relation $\perp$. We define a $\mu$superLL$^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-context $\mathcal{O}_{mpx_S^!}(C^!)$ by induction on this relation taking $S^!$ as the root. We take advantage of this induction definition to define two sets of sequent $S_{C_1^!, S^!}^{2m}$ and $S_{C_1^!, S^!}^{2c}$. Let $C_1^!, \dots, C_n^!$ be the sons of $S^!$, such that $C^! = (S^! , (C_1^! , \dots , C_n^!))$, we have two cases:

- $S^! = S^!_g$, then we define $\mathcal{O}_{mpx_S}(C^!) := (S, (C_1^! , \dots , C_n^!))$; $S_{C_1^!, S^!}^{2m} = \emptyset$; $S_{C_1^!, S^!}^{2c} := C^!$.

- $S^! = S^!_f$ ou $S^! = S^!_u$, then let the root of $C_i^!$ be $S_i^!$, we define $\mathcal{O}_{mpx_S}(C^!):= (S, \mathcal{O}_{mpx_S^!_1}(C_1^!), \dots, \mathcal{O}_{mpx_S^!_n}(C_n^!))$; $S_{C_1^!, S^!}^{2m} := \{S^!\} \cup \bigcup_{i=1}^m S_{C_i^!, S_i^!}^{2m}$; $S_{C_1^!, S^!}^{2c} := \bigcup_{i=1}^c S_{C_i^!, S_i^!}^{2c}$.

<figure><img src="image_19.png" /></figure>
Finally, we have the multiplexing principal case:

► Lemma 25 (Justification for step (comm?_m)). Let

$$
\frac{C_{\Delta} \quad \overbrace{\vdash A, \dots, A, \Delta}^{i} \quad \overbrace{\sigma(\mu_{m_i})}^{?m_i} \quad ?_{\mu_i} C_{?\sigma A}^{!} \quad \text{mcut}(\iota, \perp)}{\vdash \Gamma, ?_{\rho'} \Gamma', ?_{\rho''} \Gamma''} \quad \text{mcut}(\iota, \perp)
$$

be a µsuperLL$^{∞}$(E, ≤$_{g}$, ≤$_{f}$, ≤$_{u}$)-proof with Γ being sent on C$_{Δ}$ ∪ Δ by ι ; ?$_{ρ}$ ′ $_{Γ}$′′ being sent on sequent of S ? c C ′ $_{1}$,S $_{1}$; and ?$_{ρ}$ ′ Γ ′ being sent on S ? c C ′ $_{1}$,S $_{1}$, where S $^{1}$:= !$_{σ}$A, ?$_{τ}$ ′ Δ ′ is the sequent cut-connected to ⊢ ?$_{σ}$A, Δ on the formula ?$_{σ}$A. We have that

$$
\frac{c_{\Delta} \quad \overbrace{A, \dots, A, \Delta}^{i} \quad \overbrace{\sigma_{mpx_S!}(C_{\sigma A}^{!}) \dots C_{\sigma p x_S!(C_{\sigma A}^{!})}^{i}} \quad \text{mcut}(\iota', \perp') \quad \overbrace{\rho'(?_{m_i})}^{?\bar{\rho}_{m_i}} \quad \overbrace{\Gamma', \dots, \Gamma', ?_{\bar{\rho}'\Gamma''}, \dots, ?_{\bar{\rho}'\Gamma''}}^{i}}{\overbrace{\Gamma, ?_{\bar{\rho}'\Gamma''}, \dots, ?_{\bar{\rho}'\Gamma''}}^{i}} \quad \overbrace{\rho'(?_{c_i})}^{?\bar{\rho}_{c_i}} \quad \overbrace{\Gamma, ?_{\bar{\rho}'\Gamma''}, ?_{\bar{\rho}'\Gamma''}}^{i} \quad \text{mcut}(\iota, \perp)
$$

is also a µsuperLL$^{∞}$(E, ≤$_{g}$, ≤$_{f}$, ≤$_{u}$)-proof.

**Proof.** We prove that for each sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ of $S_{C'!,S'!}^{?c}$, $\sigma \le_g \tau''$ and that for each sequent $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ of $S_{C'!,S'!}^{?m}$, $\sigma \le_f \tau''$ or $\sigma \le_u \tau''$. The $\perp$-relation defines a tree rooted on $\S!^!$, we do a proof by induction:

■ If $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is in $S_{C'!,S'!}^{?m}$, then its antecedent is also in $S_{C'!,S'!}^{?m}$, by induction, we have the $\sigma \le_f \sigma''$ or $\sigma \le_u \sigma''$. Moreover, the promotion applied on $\vdash !_{\sigma''} A'', ?_{f''} \Delta''$ is an $!_f$ or an $!_u$ promotion. We therefore have either by axiom (axlequs), either by axiom (axTrans), either by axiom (axleqfu), that $\sigma \le_f \tau''$ or $\sigma \le_u \tau''$.

■ If $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is in $S_{C'!,S'!}^{?c}$, and that its antecedent is in $S_{C'!,S'!}^{?m}$, then by induction, we have that $\sigma \le_f \sigma''$ or $\sigma \le_u \sigma''$. Moreover, the promotion applied on $\vdash !_{\sigma''} A'', ?_{f''} \Delta''$ is an $!_g$ promotion. Therefore, we have by axiom (axlequs) or (axleqfg) that $\sigma \le_g \tau''$.

■ If $\vdash !_{\sigma''} A'', ?_{\tau''} \Delta''$ is in $S_{C'!,S'!}^{?c}$, and that its antecedent is in $S_{C'!,S'!}^{?c}$, then by induction, we have that $\sigma \le_g \sigma''$. Therefore, by axiom (axleqgs), $\sigma \le_g \tau''$.

Finally we get that for all sequents $\vdash !_{\sigma''} A_i, ?_{\tau''} \Delta''$ of $S_{C'!,S'!}^{?m}$, $\tau''(?_{m_i})$ are true, as $\sigma \le_s \tau''$, $?_{m_i}(\sigma)$ ($s \in \{f, u\}$) and by lemma (axfumpx). We also get that for all sequents $\vdash !_{\sigma''} A, ?_{\tau''} \Delta$ of $S_{C'!,S'!}^{?c}$, $\bar{\tau}''(?_{c_i})$ are true as $\sigma \le_g \bar{\tau}''$, $?_{c_i}(\sigma)$ and by lemma (axgmpx).

From the condition on the proof of the statement and from property 1, we get that $\bar{g}'(?_{m_i})$ and $\bar{g}''(?_{c_i})$ are true and so that the right proof is correct. ◀

C.2 Rule permutations

► **Definition 15** (Permutation of rules). *We define one-step rule permutation on (pre-)proofs of µLL∞ with rules of figure 11.*

Given a µLL∞ (pre-)proof π and p ∈ {l, r, i}* a path in the proof, we define perm(π, p)
by induction on p:
<figure><img src="image_20.png" /><figcaption>Figure 11 One-step rule permutation</figcaption></figure>

- the proof $\text{perm}(\pi, \epsilon)$ is the proof obtained by applying the one-step rule permutation at the root of $\pi$ if it is possible, either it is not defined;

- we define $\text{perm}(q(\pi'), i \cdot p') := r(\text{perm}(\pi', q'))$ if $\text{perm}(\pi', q')$ is defined, otherwise it is not defined;

- we define $\text{perm}(q(\pi_l, \pi_r), l \cdot q') := q(\text{perm}(\pi_l, q'), \pi_r)$ if $\text{perm}(\pi_l, q')$ is defined, otherwise it is not defined;

- we define $\text{perm}(q(\pi_l, \pi_r), r \cdot q') := q(\text{perm}(\pi_l, q'), \pi_r)$ if $\text{perm}(\pi_l, q')$ is defined, otherwise it is not defined;

- for each other cases, $\text{perm}(\pi, p)$ is not defined.

A sequence of rule permutation starting from a $\mu LL^\infty$ pre-proof $\pi$ is a (possibly empty) sequence $(p_i)_{i \in \lambda}$ ($\lambda \in \omega$), where $p_i \in \{l, r, i\}$ such that if we set $\pi_0 := \pi$, then the sequence $(\pi_i)_{i \in 1+\lambda}$ defined by induction by $\pi_{i+1} := \text{perm}(\pi_i, p_i)$ are all defined. We say that the sequence $(\pi_i)_{i \in 1+\lambda}$ is the sequence of proofs associated to the sequence of rule permutation. We say that the sequence ends on $\pi_\lambda$ if $\lambda$ is finite, we also write it $\text{perm}(\pi, (p_i)_{i \in \lambda})$.

**Lemma 26 (Robustness of the proof structure to rule permutation).** *One-step rule permutation does not modify the structure of the proof.*

*Proof.* This lemma is immediate as the substitutions are defined between unary rule.

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

**Definition 16 (Finiteness of permutation of rules).** Let $\pi$ be a $\mu LL^\infty$ (pre-)proof, and let $(p_i)_{i \in \lambda}$ be a sequence of rule permutation starting from $\pi$ and let $(\pi_i)_{i \in 1+\lambda}$ be the sequence of proofs associated to it, let $q \in \{l, r, i\}^*$ be a path to the conclusion sequent of a rule (r) of $\pi$, we define the sequence of residuals $(q_i)_{i \in 1+\lambda}$ of (r) in $\pi_i$ to be a sequence of path defined by induction on i:

- if $i=0$, $q_0=q$;

- if $p_i = q_i$, then $q_{i+1} := q_i \cdot i$.

- if $q_i = p_i \cdot i$ then $q_{i+1} := p_i$.

- else $q_{i+1} := q_i$.

We say that a rule (r) in $\pi$ is finitely permuted if its sequence of residuals is ultimately constant. We say that $(p_i)_{i \in \lambda}$ is a rule permutation sequence with finite permutation of rules if each rule of $\pi_0$ is finitely permuted.
**Proposition 3** (Convergence of permutation with finite permutation of rules). Let $\pi$ be a $\mu LL^\infty$ pre-proof and let $(p_i)_{i \in \omega}$ be a permutation sequence with finite permutation of rules starting from $\pi$, then the sequence is converging.

**Proof.** Let $(\pi_i)_{i \in \omega}$ be the sequence of proofs associated to the sequence. Let's suppose for the sake of contradiction that the sequence is not converging. It implies, using lemma 26, that there is an infinite sequence of strictly increasing indexes $\varphi(i)$ such that the $(r_{\varphi(i)})$ are all at the same position. This implies by finiteness of permutation of one rules, than there are an infinite number of rules of $\pi_0$ which have $(r_{\varphi(i)})$ in their residuals, implying that one of the rules below the position of $(r_{\varphi(i)})$ in $\pi_0$ has infinitely many residuals being equal to $(r_i)$ or below $(r_i)$ contradicting the finiteness of permutation of one rule hypothesis.

◀

**Proposition 4** (Preservation of validity for permutations with finite permutation of rules). Let $\pi$ be a $\mu LL^\infty$ pre-proof and let $(p_i)_{i \in \omega}$ be a permutation sequence with finite permutation of rules starting from $\pi$ and converging (thanks to lemma 3 to a pre-proof $\pi'$. Then $\pi$ is valid if and only if $\pi'$ is.

**Proof.** From lemma 26, we have that the structure of the trees of the sequence stays the same, therefore the structure of $\pi$ is the same than the structure of $\pi'$, moreover the threads of $\pi$ and $\pi'$ are the same if we remove indexes where the thread is not active. Therefore validity is easily preserved both ways.

◀

### C.3 Details on Lemma 11

**Lemma 27.** Let $\pi_0$ be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ proof and let $\pi_0 \rightsquigarrow \pi_1$ be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ step of reduction. There exist a finite number of $\mu LL^\infty$ proofs $\theta_0, \dots, \theta_n$ such that $\theta_0 \to \dots \to \theta_n$, $\pi_0^\circ = \theta_0$ and $\theta_n = \pi_1^\circ$ up to a finite number of rule permutations, done only on rules that just permuted down the (mcut).

To prove this lemma, we need the following one. This lemma prove that when starting from the translation of a proof containing derelictions promotions and functorial promotions, there exist an order of execution of cut-elimination step that will make them disappear or commute under the cut. This order depends on how the proof is translated, for instance the following (opened) proof:

$$ \frac{\frac{\vdash A, B, C}{\vdash !A, ?B, ?C} !_f \quad \frac{\vdash C^\perp}{\vdash C} !_f}{\vdash !A, ?B} \text{mcut}(\iota, \perp) $$

has two translations:

$$ \frac{\frac{\vdash A, B, C}{\vdash A, B, ?C} ?_d \quad \frac{\vdash A, ?B, ?C}{\vdash A, ?B, ?C} !_p \quad \frac{\vdash C^\perp}{\vdash C} !_p}{\vdash !A, ?B} \text{mcut}(\iota, \perp) $$

$$ \frac{\frac{\vdash A, B, C}{\vdash A, ?B, C} ?_d \quad \frac{\vdash A, ?B, ?C}{\vdash A, ?B, ?C} !_p \quad \frac{\vdash C^\perp}{\vdash C} !_p}{\vdash !A, ?B} \text{mcut}(\iota, \perp) $$

To eliminate cuts, we apply in both the same cut-elimination steps but in a different order. We apply in both an $(!_p)$ commutative step, then apply in the first one a dereliction commutative step and a $(!_p)/(?_d)$ principal case; whereas in the second one we first apply the $(!_p)/(?_d)$ principal case then the dereliction commutative step.

**Lemma 28.** Let $n \in \mathbb{N}$, let $d_1, \dots, d_n \in \mathbb{N}$ and let $p_1, \dots, p_n \in \{0, 1\}$. Let $\pi$ be a $\mu LL^\infty$-proof concluded by an (mcut)-rule, on top of which there is a list of $n$ proofs $\pi_1, \dots, \pi_n$. We ask for each $\pi_i$ to be of one of the following forms depending on $p_i$:
- If $p_i = 1$, the $d_i + 1$ last rules of $\pi_i$ are $d_i$ derelictions and then a promotion rule. We ask for the principal formula of this promotion to be either a formula of the conclusion, or to be cut with a formula being principal in a proof $\pi_j$ on one of the last $d_j + p_j$ rules.

- If $p_i = 0$, the $d_i$ last rules of $\pi_i$ are $d_i$ derelictions.

In each of these two cases, we ask for $\pi_i$ that each principal formulas of the $d_i$ derelictions to be either a formula of the conclusion of the multicut, either a cut-formula being cut with a formula appearing in $\pi_j$ such that $p_j = 1$. We prove that $\pi$ reduces through a finite number of mcut-reductions to a proof where each of the last $d_i + p_i$ rules either were eliminated by a ($!_p/?!_d$)-principal case, or were commuted below the cut.

**Proof.** We prove the property by induction on the sum of all the $d_i$ and of all the $p_i$:

- (Initialization). As the sum of the $d_i$ and $p_i$ is 0, all $d_i$ and $p_i$ are equal to 0, meaning that our statement is vacuously true.

- (Heredity). We have several cases:

- If the last rule of a proof $\pi_i$ is a promotion or a dereliction for which the principal formula is in the conclusion of the (mcut), we do a commutation step on this rule obtaining $\pi'$. We apply our induction hypothesis on the proof ending with the (mcut); and with parameters $d'_1, \dots, d'_n$ as well as $p'_1, \dots, p'_n$ and proofs $\pi'_1, \dots, \pi'_n$. To describe these parameters we have two cases:

* If the rule is a promotion. We take for each $j \in [1, n]$, $d'_j = d_j$; $p'_j = p_j$ if $j \neq i$, $p'_i = 0$; $\pi'_j = \pi_j$ if $j \neq i$.

* If the rule is a dereliction. We take for each $j \in [1, n]$, $d'_j = d_j$ if $j \neq i$, $d'_i = d_i - 1$; $p'_j = p_j$.

The $\pi'_j$ will be the hypotheses of the (mcut) of $\pi''$. Note that $\sum d'_j + \sum p'_j = \sum d_j + \sum p_j - 1$ meaning that we can apply our induction hypothesis. Combining our reduction step with the reduction steps of the induction hypothesis, we obtain the desired result.

- If there are no rules from the conclusion but that one $\pi_i$ ends with $d_i > 0$ and $p_i = 0$, meaning that the proof ends by a dereliction on a formula $?F$. This means that there is proof $\pi_j$ such that $p_j = 1$ and such that $?F$ is cut with one of the formula of $\pi_j$, namely $!F^\perp$. As there are only one $!$-formula, and as $p_j = 1$, $!F^\perp$ is the principal rule of the last rule applied on $\pi_j$. We therefore can perform an ($!_p/?!_d$) principal case on the last rules from $\pi_i$ and $\pi_j$, leaving us with a proof $\pi'$ with an (mcut) as conclusion. We apply the induction hypothesis on this proof with parameters $d'_1 = d_1, \dots, d'_i = d'_i - 1, \dots, d'_n = d'_n$, $p'_1 = p_1, \dots, p'_j = p'_j - 1, \dots, p'_n = p_n$ and with the proofs being the hypotheses of the multicut. Combining our steps with the steps from the induction hypotheses, we obtain the desired result.

- We will show that the case where there are no rules from the conclusion and that no $\pi_i$ are such that $d_i > 0$ and $p_i = 0$, is impossible. Supposing, for the sake of contradiction, that this case is possible. We will construct an infinite sequence of proofs $(\theta_i)_{i \in \mathbb{N}}$ all different and all being hypotheses of the multi-cut, which is impossible. We know that there exist a proof $\theta_0 := \pi_j$ ending with a promotion on a formula $!A$ and that this formula is not a formula from the conclusion. This proof is in relation by the $\perp$-relation to another proof $\theta_1 := \pi_{j'}$. We know that this proof cannot be $\pi_j$ because the $\perp$-relation extended to sequents is acyclic. This proof also ends with a promotion on a principal formula which is not from the conclusion. By repeating this process, we obtain the desired sequence $(\theta_i)_{i \in \mathbb{N}}$, giving us a contradiction.

The statement is therefore true by induction

<figure><img src="image_22.png" /></figure>
**Proof of lemma 11.** Reductions from the non-exponential part of $\mu\text{superLL}^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ translates easily to one step of reduction in $\mu\text{LL}^\infty$. To prove the result on exponential part, we will describe each translation of the reductions of figure 5 and 6. For the commutative steps no commutation of rules are necessary.

- Step (comm$_{!g}$). This step translates to the commutation of one (!)-rule in $\mu\text{LL}^\infty$, which is one step of reduction.

- Step (comm$_{!f}$). We prove that lemma 28 applies to step (comm$_{!f}$). Taking the left proof from step (comm$_{!f}$) and translating it in $\mu\text{LL}^\infty$, we obtain a proof:

$$ \frac{\begin{array}{c} \pi_1^\circ \\ \begin{array}{c} \vdash A_1^\circ, \Delta_1^\circ \\ \vdash A_1^\circ, ?\Delta_1^\circ \\ \vdash !A_1^\circ, ?\Delta_1^\circ \end{array} \end{array} ?_d !_p \quad \dots \quad \begin{array}{c} \pi_n^\circ \\ \begin{array}{c} \vdash A_n^\circ, \Delta_n^\circ \\ \vdash A_n^\circ, ?\Delta_n^\circ \\ \vdash !A_n^\circ, ?\Delta_n^\circ \end{array} \end{array} ?_d !_p \quad \text{mcut}(\iota, \perp) \\ \vdash !A^\circ, ?\Gamma^\circ \end{array} $$

with $\iota(1) = (i, 1)$ for some $i$ and $n = 1 + \#(\mathcal{C})$. We apply our result on this proof with all the $p_i$ being equal to 1 and with $d_i = \#(\Delta_i)$. Moreover, we notice that there will be only one promotion rule commuting under the cut and that it commutes before any dereliction, giving us the translation of the functorial promotion under the multicut.

- Step (comm$_{!f}^2$). As for (comm$_{!g}$), this step only translates to the commutation of one (!)-rule in $\mu\text{LL}^\infty$, which is one step of reduction.

- Step (comm$_{!u}^1$). This step translates to the commutation of one (!$_p$)-rule, followed by $\#(\mathcal{C}^1_u) (!/?_d)$ principal steps and finally one (?$_d$) commutation giving us the translation of a unary promotion under the multicut.

- Step (comm$_{!u}^2$). We prove this step using lemma 28 as for step (comm$_{!f}^1$).

- Step (comm$_{!u}^3$) and (comm$_{!u}^4$). Both of these steps translate to the commutation of one (!$_p$), followed by $\#(\mathcal{C}^1_u) + 1 (!/?_d)$ principal steps.

- Step (comm$_{?m}$). We must distinguish three cases based on $i$:

- $i = 0$. This step translates to one (?$_w$)-commutative step.

- $i = 1$. This step translates to one (?$_d$)-commutative step.

- $i > 1$. This step translates to $i - 1$ commutation of (?$_c$) and $i$ commutation of (?$_d$).

- Step (comm$_{?c}$). This step translates to $i - 1$ commutation of (?$_c$).

- Step (principal$_{?c}$). This step translates to $i - 1$ contraction principal cases. At the end we obtain the following derivation under the multi-cut:

$$ \begin{array}{c} \overbrace{\begin{array}{c} \vdash \Gamma^\circ, ?\Gamma'^\circ, \dots, ?\Gamma'^\circ \end{array}}^{i} ?_c \\ \begin{array}{c} \vdash \Gamma^\circ, ?\Gamma'^\circ, \dots, ?\Gamma'^\circ \\ \vdots \\ \vdash \Gamma^\circ, ?\Gamma'^\circ, ?\Gamma'^\circ \end{array} \end{array} $$

which we can re-arrange to get the translation of $\#\Gamma' ?\bar{\rho}_{c_i}$ rules on each formulas of $?\Gamma'^\circ$. Note that for $i = 2$ no rule permutation are needed.

- Step (principal$_{?m}$). If $i \ge 1$, this step translates in two phases:

1. First $i - 1$ contraction principal cases;

2. followed by $\#(\mathcal{S}_{C',S'}^m) (?_d/!)$-principal cases, and $\#(\Gamma'')$ dereliction commutative cases.
To prove the second phase we re-use lemma 28 as for steps (comm<sub>f<sub>u</sub></sub><sup>2</sup>) and (comm<sub>f<sub>f</sub></sub><sup>1</sup>).
Finally, the obtained proof under the multi-cut look like this:

$$
\frac{\overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, \dots, ?\Gamma''^\circ, \Gamma'^\circ, \dots, \Gamma'^\circ}^{i} \overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, \dots, ?\Gamma''^\circ, \Gamma'^\circ, \dots, \Gamma'^\circ}^{i-1} ?_d}{\vdots}
$$

$$
\frac{\overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, \dots, ?\Gamma''^\circ, \Gamma'^\circ, \dots, ?\Gamma'^\circ}^{i} \overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, \dots, ?\Gamma''^\circ, ?\Gamma'^\circ, \dots, ?\Gamma'^\circ}^{i-1} ?_d}{\overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, \dots, ?\Gamma''^\circ, ?\Gamma'^\circ, \dots, ?\Gamma'^\circ}^{i-1} ?_c}
$$

$$
\frac{\vdots \quad \overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, ?\Gamma''^\circ, ?\Gamma'^\circ, ?\Gamma'^\circ}^{i} ?_c}{\vdots \quad \overbrace{\vdash \Gamma^\circ, ?\Gamma''^\circ, ?\Gamma'^\circ}^{i}}
$$

which we can re-arrange to get the translation of #Γ' ?ρ̄<sub>m<sub>i</sub></sub>, followed by the translation of
#Γ'' ?ρ̄<sub>c<sub>i</sub></sub>.

If $i = 0$, this step translates to a weakening principal case, giving us the translation of #Γ'
?ρ̄<sub>m<sub>0</sub></sub> and #Γ'' ?ρ̄<sub>c<sub>0</sub></sub> with no commutation of rules necessary. ◀

C.4 Details on Lemma 12

**► Lemma 29 (Completeness of the (mcut)-reduction system).** If there is a $\mu LL^\infty$-redex $\mathcal{R}$ sending $\pi^\circ$ to $\pi'^\circ$ then there exists a $\mu superLL^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$-redex $\mathcal{R}'$ sending $\pi$ to a proof $\pi''$, such that in the translation of $\mathcal{R}'$, $\mathcal{R}$ is applied.

**Proof.** We only prove the exponential cases, the non-exponential cases being immediate. We have several cases:

- If the case is the commutative step of a contraction or a dereliction or weakening (r), as it is on top of a (mcut), it necessarily means that (r) comes from the translation of a multiplexing or a contraction rule (r') which is also on top of an (mcut) in π, we can take R' as the step commutating (r') under the cut.

- If it is a principal case again, we have that there is a contraction or a dereliction or weakening rule (r) on top of a (mcut) on a formula ?A. It also means that each proofs cut-connected to ?A ends with a promotion. As π° is the translation of a μsuperLL∞(E, ≤<sub>g</sub>, ≤<sub>f</sub>, ≤<sub>u</sub>)-proof, it means that (r) is contained in the translation of a multiplexing or contraction rule (r') on a formula ?<sub>σ</sub>A on top of a (mcut). It also means that all the proofs cut-connected for this (mcut) to ?<sub>σ</sub>A are translations of promotions (no other rules than a promotion in μsuperLL∞(E, ≤<sub>g</sub>, ≤<sub>f</sub>, ≤<sub>u</sub>) translates to a derivation ending with a promotion). Therefore the principal case on (r') is possible, we can take R' as it.

- If it is the commutative step of a promotion (r), it means that all the proofs of the contexts of the (mcut) are promotions. Meaning that (r) is contained in the translation
of a promotion ($r'$) on top of (mcut). We also have that the context of this (mcut) are
only proof ending with a promotion for the same reasons that last point. We therefore
need to make sure that each (mcut) with a context full of promotions are covered by the
$\rightsquigarrow$-relation. Looking back at figure 5 together with conditions given by each corresponding
lemmas, we have that:

- Each (!_g)-commutation is covered by the first case.

- Each (!_f)-commutation is covered by the two cases that follows: the second of the two covers the case where there is an (!_g)-promotion in hypotheses of the multicut with non-empty context, whereas the first one covers the case where there are no such (!_g)-promotions in the hypotheses.

- The (!_u)-commutation is covered by all the remaining cases:

* The first one covers (!_u)-commutation when the hypotheses are all concluded by an
  (!_u)-rule.

* (!_u)-commutation with (!_f)-rules and (possibly) (!_g)-rule with empty context are covered by the second case.

* (!_u)-commutation with (!_f)-rules and (!_g)-rule with non-empty contexts is covered by the third and the fourth cases: the third case covering all the cases where the chain of (!_u) encounters a (!_f) first, the fourth one when it encounter a (!_g) first.

* (!_u)-commutation without (!_f) rules but with (!_g) with or without empty contexts is covered by last case.

◄

C.5 Details on the translation of fair reduction sequences

**Corollary 3.** For every fair $\mu$superLL$^{\infty}(\mathcal{E}, \le_g, \le_f, \le_u)$ reduction sequences $(\pi_i)_{i \in \omega}$, there exists:

- a fair $\mu$LL$^{\infty}$ reduction sequence $(\theta_i)_{i \in \omega}$;

- a sequence of strictly increasing $(\varphi(i))_{i \in \omega}$ natural numbers;

- for each $i$, an integer $k_i$ and a finite sequence of rule permutations $(p_i^k)_{k \in [0, k_i - 1]}$ starting from $\pi_i^\circ$ and ending $\theta_{\varphi(i)}$. For convenience in the proof, let's denote by $(\pi_i^k)_{k \in [0, k_i]}$ be the sequence of proofs associated to the permutation;

- for all $i > i'$, $p_i^k > p_{i'}^{k'}$ if $k' \in [0, k_i - 1)$ and $k \ge k_i$;

- for all $i, k$, $p_i^k$ are positions lower than the multicuts in $\pi_i^\circ$.

- for each $i' \ge i$ and for each $k \in [0, k_i - 1]$, $p_{i'}^k = p_i^k$

**Proof.** We construct the sequence by induction on the steps of reductions of $(\pi_i)_{i \in \omega}$.

- For $i=0$: we take $\theta_0 = \pi_0^0$, $\varphi(0) = 0$ and $k_0 = 0$.

- For $i+1$, suppose we constructed everything up to rank $i$. We use lemma 11 on the step $\pi_i \to \pi_{i+1}$ and get a finite sequence of reduction $\theta'_0 \to \dots \to \theta'_n$, such that there is a permutation of rules $(p_1, \dots, p_m)$ ($m \in \mathbb{N}$) starting on $\pi_{i+1}^0$ and ending on $\theta'_n$ such that $p_1, \dots, p_m$ are at the depths of rules that just commuted down the multicut during the sequence $\theta'_0 \to \dots \to \theta'_n$. We have that $\theta'_0 = \pi_i^0$, therefore $(p_i^0, \dots, p_i^{k_i-1})$ is a sequence of reduction starting from $\theta'_0$ and ending on $\theta_{\varphi(i)}$. As $\theta'_0$ and $\theta'_j$ are equal under the multicut rules of $\theta'_0$ (for each $j \in [0, n]$) and that depths $p_i^j, j \in [0, k_i - 1]$ are under the multicuts of $\pi_i$, we have that $(p_i^0, \dots, p_i^{k_i-1})$ is a sequence of rule permutation starting on proof $\theta'_j$. Let's denote by $\theta'_j^0, \dots, \theta'_j^{k_i}$ the sequence of proof associated to it. We have that for the same reason, $\theta'_j$ is equal to $\theta'_j^{k_i}$ on top of the depths of multicuts of $\theta'_j$. We therefore have that $\theta'_0^{k_i}, \dots, \theta'_n^{k_i}$ is an (mcut) reduction sequence of $\mu$LL$^{\infty}$ starting from $\theta_{\varphi(i)}$. As the two sequences of reductions $p_1, \dots, p_m$ and $p_i^0, \dots, p_i^{k_i-1}$ have disjoint sets of rules with
non-empty traces, we have that $p_i^0, \dots, p_i^{k_i-1}, p_1, \dots, p_m$ is a sequence of rule permutation starting from $\pi_{i+1}'$ and ending on the same proof than the proof ending the sequence $p_1, \dots, p_m, p_i^0, \dots, p_i^{k_i-1}$, namely $\theta_n'^{k_i}$. By setting $\varphi(i+1) := \varphi(i) + n$, $\theta_{\varphi(i)+j} := \theta_j'^{k_i}$ (for $j \in [0, n]$), $p_{i+1}^j = p_i^j$ for $j \le k_i-1$ and $p_{i+1}^{k_i-1+j} = p_j$ for $j \in [1, m]$, we have our property.

Here is a summary of the objects used in the inductive step:

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

We get fairness of $(\theta_i)_{i \in \omega}$ from lemma 12 and from the fact that after the translation of an (mcut)-step, $\pi^\circ \rightsquigarrow \pi'^\circ$, each residual of a redex $\mathcal{R}$ of $\pi^\circ$, is contained in the translations of residuals of the associated redex $\mathcal{R}'$ of lemma 12. ◀

## C.6 Details on the main theorem

**▶ Theorem 6.** Every fair (mcut)-reduction sequence of $\mu\text{superLL}^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ converges to a $\mu\text{superLL}^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ cut-free proof.

**Proof.** Consider a $\mu\text{superLL}^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ fair reduction sequence $(\pi_i)_{i \in 1+\lambda}$ ($\lambda \in \omega + 1$). If the sequence is finite, we use lemma 11 and we are done. If the sequence is infinite, using corollary 1 we get a fair infinite $\mu\text{LL}^\infty$ reduction sequence $(\theta_i)_{i \in \omega}$ and a sequence $(\varphi(i))_{i \in \omega}$ of natural numbers. By theorem 2, we know that $(\theta_i)_{i \in \omega}$ converges to a cut-free proof $\theta$ of $\mu\text{LL}^\infty$. We now prove that the sequence $(\pi_i)_{i \in \omega}$ converges to a $\mu\text{superLL}^\infty(\mathcal{E}, \le_g, \le_f, \le_u)$ pre-proof $\pi$ such that $\pi^\circ = \theta$ up to a permutation of rules (the permutations of one particular rule being finite).

First, we prove that for each depth $d$, there is an $i$ such that there are no (mcut)-rules under depth $d$ in $\pi_i$. Suppose for the sake of contradiction that there exist a depth $d$ such that there always exist a (mcut) at depth $d$. There is a rank $i'$ and an (mcut) rule in $\pi_{i'}$ such that for each $i \ge i'$, $\pi_i$ will always contain this (mcut) and (therefore) the branch $b$ to it never changes. The translations $\pi_i^{\circ'}$ contains the translation of the branch $b$ which also ends with an mcut. Since $\pi_{i'}^{\circ'}$ is equal to $\theta_{\varphi(i')}$ up to the permutations of rules under the multicut and that these permutations do not change the depths of the (mcut) rules, we have that the $\theta_{\varphi(i)}$ all contains a (mcut) at a depth equal to the depth of the translation of $b$.
This contradicts the productivity of this sequence of reduction, we therefore have that $(\pi_i)$ converges to a pre-proof $\pi$.

Second, we prove that $\pi^\circ$ is equal to $\theta$ up to a permutation of rules (the permutations of one particular rule being finite). The condition on the sequence given by corollary 1 defines a sequence of rule permutation starting from $\pi^\circ$:

$$p_0^0, \dots, p_0^{k_0-1}, p_1^{k_0}, \dots, p_1^{k_1-1}, \dots, p_n^{k_n-1}, \dots, p_{n+1}^{k_n}, \dots,$$

moreover we have that this is a permutation of rules with finite permutation, therefore this sequence of rule permutation converges to a $\mu LL^\infty$ pre-proof $\pi'$. We have for each $i$, that the end of the sequence of rule permutation

$$p_0^0, \dots, p_0^{k_0-1}, p_1^{k_0}, \dots, p_1^{k_1-1}, \dots, p_i^{k_i-1}, \dots, p_i^{k_i-1}$$

starting from $\pi^\circ$ is equal to $\pi_i^{k_i}$ under the multicuts. Therefore we have that the sequence $(\pi_i^{k_i})_{i \in \omega} = (\theta_{\varphi(i)})_{i \in \omega}$ converges to $\pi'$ and therefore that $\pi' = \theta$. As rule permutation with finite permutation and $(-)^\circ$ translation are robust to validity (both ways), we have that $\pi$ is valid. $\blacksquare$

### C.7 Details on corollary 2

**Corollary 4 (Cut Elimination for superLL).** *Cut elimination holds for superLL($\mathcal{E}$, $\le_g, \le_f, \le_u$) as soon as the 8 cut-elimination axioms of definition 1 are satisfied.*

**Proof.** Any superLL($\mathcal{E}$, $\le_g, \le_f, \le_u$)-proof is also $\mu$superLL$^\infty(\mathcal{E}$, $\le_g, \le_f, \le_u$)-proof therefore any sequence of (mcut)-reductions converges to a cut-free proof. A cut-free proof of sequents containing only superLL($\mathcal{E}$, $\le_g, \le_f, \le_u$)-formulas and valid rules from $\mu$superLL$^\infty(\mathcal{E}$, $\le_g, \le_f, \le_u$) is necessarily a superLL($\mathcal{E}$, $\le_g, \le_f, \le_u$) (cut-free) proof. $\blacksquare$
# Contents

<table><tbody><tr><td>1 Introduction</td><td>1</td></tr><tr><td>2 Background</td><td>2</td></tr><tr><td>2.1 Linear logic and non-wellfounded proofs</td><td>2</td></tr><tr><td>2.1.1 Formulas</td><td>2</td></tr><tr><td>2.1.2 Sequent calculi</td><td>3</td></tr><tr><td>2.1.3 Cut-elimination for linear logic with fixed-point</td><td>4</td></tr><tr><td>2.2 Super exponentials</td><td>5</td></tr><tr><td>3 Super exponentials with fixed-points</td><td>7</td></tr><tr><td>3.1 Definition of μsuperLL<sup>∞</sup></td><td>7</td></tr><tr><td>3.1.1 Formulas</td><td>7</td></tr><tr><td>3.1.2 Rules and proofs</td><td>7</td></tr><tr><td>3.2 Some instances of μsuperLL<sup>∞</sup></td><td>7</td></tr><tr><td>3.2.1 A linear modal μ-calculus</td><td>7</td></tr><tr><td>3.2.2 ELL with fixed point</td><td>8</td></tr><tr><td>4 Cut-elimination</td><td>8</td></tr><tr><td>4.1 (mcut)-elimination steps</td><td>8</td></tr><tr><td>4.2 Translating μsuperLL<sup>∞</sup> into μLL<sup>∞</sup></td><td>11</td></tr><tr><td>5 Conclusion</td><td>15</td></tr><tr><td>A Details on Section 2</td><td>17</td></tr><tr><td>A.1 Details on the multicut rule (Definition 6)</td><td>17</td></tr><tr><td>A.2 Details on the restriction of a multicut context (Definition 7)</td><td>17</td></tr><tr><td>A.3 One-step multicut-elimination for μMALL<sup>∞</sup></td><td>17</td></tr><tr><td>A.4 One-step multicut-elimination for μLL<sup>∞</sup></td><td>17</td></tr><tr><td>A.5 Proof of Axiom Expansion property</td><td>17</td></tr><tr><td>A.6 Proof of cut-elimination of superLL (Theorem 3)</td><td>21</td></tr><tr><td>A.7 Details on ELL as instance of superLL</td><td>25</td></tr><tr><td>B Details on Section 3</td><td>26</td></tr><tr><td>B.1 Details on μLL<sup>∞</sup> as an instance of μsuperLL<sup>∞</sup></td><td>26</td></tr><tr><td>C Details on Section 4</td><td>26</td></tr><tr><td>C.1 Details on the justification of (mcut)-steps</td><td>26</td></tr><tr><td>C.2 Rule permutations</td><td>34</td></tr><tr><td>C.3 Details on Lemma 11</td><td>36</td></tr><tr><td>C.4 Details on Lemma 12</td><td>39</td></tr><tr><td>C.5 Details on the translation of fair reduction sequences</td><td>40</td></tr><tr><td>C.6 Details on the main theorem</td><td>41</td></tr><tr><td>C.7 Details on corollary 2</td><td>42</td></tr></tbody></table>