# A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points (extended version)

Alexis Saurin

► To cite this version:

Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points (extended version). 2023. hal-04169137

HAL Id: hal-04169137

https://hal.science/hal-04169137

Preprint submitted on 23 Jul 2023

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
A linear perspective on cut-elimination for
non-wellfounded sequent calculi with
least and greatest fixed points
(extended version)

Alexis Saurin*

IRIF, CNRS, Université de Paris Cité & INRIA
 alexis.saurin@irif.fr

**Abstract.** This paper establishes cut-elimination for $\mu LL^\infty$, $\mu LK^\infty$ and $\mu LJ^\infty$, that are non-wellfounded sequent calculi with least and greatest fixed-points, by expanding on prior works by Santocanale and Fortier [20] as well as Baelde et al [4,3]. The paper studies a fixed-point encoding of LL exponentials in order to deduce those cut-elimination results from that of $\mu MALL^\infty$. Cut-elimination for $\mu LK^\infty$ and $\mu LJ^\infty$ is obtained by developing appropriate linear decorations for those logics.

**Keywords:** LL, $\mu$-calculus, non-wellfounded proofs, cut elimination

# 1 Introduction

*On the non-wellfounded proof-theory of fixed-point logics.* In the context of logics with induction and coinduction (such as logics with inductive definitions à la Martin Löf [6,9,10,25], or variants of the $\mu$-calculus [22,23,11]), the need for a (co)inductive invariant (in the form of the Park's rule for induction) is replaced by the ability to pursue the proof infinitely, admitting non-wellfounded branches, when considering non-wellfounded and circular proofs (also called cyclic, or regular proofs, since the proof tree is a regular tree, with finitely many distinct subtrees). In such frameworks, sequent proofs may be finitely branching but non-wellfounded derivation trees and infinite branches shall satisfy some validity condition. (Otherwise one could derive any judgement, see Figure 1(a).) Various validity conditions have been considered in the literature [3].

The non-wellfounded and circular proof-theory of fixed-points attracted a growing attention first motivated by proof-search [18,17,1,16,29,7,8] and more recently by a Curry-Howard perspective, studying the dynamics of the cut-elimination in those logics [4,20,30] where formulas correspond to (co)inductive types. Notice also that when interested in the computational content of proofs, we will not focus solely on the regular fragment as we expect, for instance, that we can write a regular program that computes a non-ultimately periodic stream.

<footnote>* This work was partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. (a) Example of an invalid circular pre-proof. (b) Schema of the multicut rule.</figcaption></figure>

**Cut-elimination and LL.** When studying the structure of proofs and their cut-elimination properties, LL, Girard's Linear Logic [21], is a logic of choice: the careful treatment of structural rules gives access to a lot of information and a fine-grained control over cut-reduction. The constrained use of structural rules indeed renders the cut-elimination theorem more informative than in LJ and of course LK. Interestingly it provided a positive feedback on the understanding of LJ and LK: by decorating intuitionistic and classical proofs with enough exponential modalities (!, ?), they can become LL proofs and one can therefore refine the original cut-elimination relations [21,13]. This approach impacted the understanding of evaluation strategies of programming languages such as call-by-name and call-by-value notably. Another way to view this is by noting that in, say, LK the additive and multiplicative presentation of conjunction (resp. disjunction) can be shown to be interderivable thanks to structural rules. This fails in LL and it is the reason why LL has well-established additive – ⊕, &, ⊤, 0 – (resp. multiplicative ⊗, ⊗, ⊥, 1) fragments. It is the role of the exponential fragment to relate the additive and multiplicative worlds, by mean of the fundamental equivalence: !A ⊗!B ⊢! !(A&B) (and its dual, ?A⊗?B ⊢? !(A ⊕ B)). The exponential modalities are precisely introduced where structural rules are needed to restore the equivalence between the additive and multiplicative conjunctions; in categorical models of LL [27], this principle is referred to as Seely isomorphisms.

**Cut-elimination for non-wellfounded proofs.** Proving cut-elimination results for non-wellfounded proofs in the presence of least and greatest fixed-points requires to use reasoning techniques coping with the non-inductive structure of the considered formulas (fixed-points formulas regenerate) and proof objects (which are non-wellfounded). For instance, Santocanale and Fortier [20] proved cut-elimination for the regular fragment of non-wellfounded proofs of purely additive linear logic with fixed points, µALL while Baelde et al. [4] proved cut-elimination for non-wellfounded proofs with additive and multiplicative connectives, µMALL. In both cases, the proof relies on a generalization of the cut-rule (which abstracts a portion of a proof tree constituted only of cut inferences, the multicut rule, see Figure 1(b)) and on a reasoning by contradiction to prove that one can eliminate cuts at the limit of an infinite cut reduction sequence, while preserving the validity condition. Baelde et al. [4,3] use a so-called “locative” approach by modelling sequents as sets of formulas paired with addresses which determines uniquely the formula occurrence in a sequent and makes explicit the ancestor relation used to trace the progress along branches. Moreover, the cut-elimination
proof proceeds by a rather complex semantical, indirect, argument relying on a
soundness theorem.

In a slightly different direction, Das and Pous [15] proved a cut-elimination
result for Kleene algebras and their variants. This can be viewed as a non-
commutative version of intuitionistic MALL with a particular form of inductive
construction, Kleene's star. Kuperberg et al [24] and more specifically Pinault's
PhD thesis [28] as well as Das [14] examine non-wellfounded versions of System
T based on [15], exploring the computational content of non-wellfounded proofs.

Neither Santocanale and Fortier's [30,20], nor Baelde et al. [4,3] works captured full linear logic: the exponentials are missing and the proofs cannot deal with them in a simple way. Indeed, the proof for $\mu ALL$ strongly relies on the assumption the sequents are pairs of formulas $(A \vdash B)$ while in $\mu MALL$, the locative approach taken by Baelde et al. is not well-suited to work with structural rules: the extension of the proof would be possible though highly technical. In contrast, our motto in the present work is to work with traditional sequents as lists of formulas and to exploit the (co)inductive nature of LL exponentials.

*On the (co)inductive nature of exponential modalities in linear logic.* The original works by Baelde and Miller on fixed-points in linear logic [5,2] focus on $\mu MALL$ only and present an encoding of the exponential modalities of LL using least and greatest fixed points. Indeed, the ? and ! modalities have an infinitary character which is well-known from the early days of linear logic (see Section V.5 of Girard's seminal paper [21]) and which is in fact respectively inductive for ? and coinductive for !; let us discuss it briefly here.

One can decide to contract a ?-statement any *finite* number of times before it is ultimately weakened or derelicted. It is therefore natural to represent ?A with formula_0?A = $\mu X.A \oplus (\perp \oplus (X \oslash X))$: A allows for dereliction, $\perp$ for weakening and $X \oslash X$ will regenerate, by unfolding, two copies of _0?A, making the contraction derivable. The $\oplus$ and $\mu$ connectives respectively provide the ability to choose either of those three inferences and to repeat finitely this process.

On the other hand, a !-formula is a formula which, during cut-elimination, shall maintain a proper interaction with *any number* of contractions, weakenings or derelictions: a proof concluded with a promotion shall be able to react to any number of duplications or erasure before the promotion actually interact with a dereliction to open the *exponential box*: from that follows the coinductive character of !A modelled as !_0A = $\nu X.A \& (1 \& (X \otimes X))$.

As informally described above and formally established by Baelde and Miller [5], the exponential rules can be derived in the finitary sequent calculus $\mu MALL$: to any LL provable sequent can be associated a provable $\mu MALL$ sequent via the above translations of the exponentials. However, until now one can hardly say more about this embedding for two deep reasons: (i) the fundamental Seely isomorphisms which relate the additive and multiplicative versions of conjunction (resp. disjunction) are still derivable through this encoding but they are no more isomorphisms and (ii) it is unknown whether the converse of the above provability preservation result holds: whether the $\mu MALL$ provability of the translation of an LL sequent $s$ entails the LL provability of $s$ itself. A contribution of the
Several appendices are provided for the reviewers, at their discretion.

It details some definitions and provides proofs which, most often, could not be included in the body of the paper due to lack of space. A companion technical report is available online [31]. References to the Appendices are presented in such margin paragraphs.

present paper is to put to work Baelde and Miller's encoding, showing that, in the case of non-wellfounded proofs, its structure is faithful enough to extract information of the cut-reduction behaviour of the logic.

*Contributions and organization of the paper.* The main result of this paper is a cut-elimination theorem for $\mu LL^\infty$, the non-wellfounded sequent calculus for linear logic extended with least and greatest fixed points. Our proof proceeds by encoding LL exponentials in $\mu MALL^\infty$ and studying $\mu LL^\infty$ cut-reduction sequences through their simulation in $\mu MALL^\infty$ which may be a *transfinite* sequence. In Section 2, we introduce our logics, $\mu MALL^\infty$, $\mu LL^\infty$, $\mu LK^\infty$ and $\mu LJ^\infty$, altogether with their non-wellfounded proofs and validity conditions. We adapt $\mu MALL^\infty$ cut-elimination theorem [4] to our setting where sequents are lists and prove a compression lemma for $\mu MALL^\infty$ transfinite cut-reduction sequences. Section 3 constitutes the core of our paper: we define $\mu LL^\infty$ cut-reduction rules, study the encoding of exponentials in $\mu MALL^\infty$ and show that $\mu LL^\infty$ cut-reduction steps can be simulated in $\mu MALL^\infty$, before proving $\mu LL^\infty$ cut-elimination theorem. We prove in Section 4, as corollaries, cut-elimination for $\mu LK^\infty$ and $\mu LJ^\infty$, the non-wellfounded sequent-calculi for classical and intuitionistic logic. While our result for $\mu LL^\infty$ shows that any fair cut-reduction sequence produces a cut-free valid proof, our two other cut-elimination results are truly (infinitary) weak-normalization results. We finally conclude in Section 5 with perspectives. A major advantage of our approach is that $\mu MALL^\infty$ cut-elimination proof and, to some extent, the validity conditions, are regarded as black box, simplifying the presentation of the proof and making it reusable wrt. other validity condition or $\mu MALL^\infty$ proof techniques. An additional by-product of our approach, to the theory of linear logic, is to illustrate the fact that Seely isomorphisms are not needed to reach a cut-free proof.

# 2 Non-wellfounded proofs: $\mu MALL^\infty$, $\mu LL^\infty$, $\mu LK^\infty$, $\mu LJ^\infty$.

## 2.1 $\mu$-signatures and formulas.

**Definition 1 ($\mu$-signature).** A $\mu$-signature is a set $C$ of pairs $(c,p)$ of a connective symbol $c$ and a tuple $p$ of elements of $\{+, -\}$. The arity of $c$, $\mathrm{ar}(c)$, is the length of $p$, while the elements of $p$ indicate the mono/antitonicity of the connective in the given component. The empty tuple will be denoted as $()$.<fnref n="1" />

*Example 2 ($\mu$-signature associated with $\mu MALL$, $\mu LL$, $\mu LK$, $\mu LJ$).* The $\mu$-signature associated with $\mu MALL$, $\mu LL$, $\mu LK$, $\mu LJ$, considered in this paper are:

- $\mu MALL$ signature: $C_{\mu MALL} = \{\mathcal{O}, \otimes, \oplus, \&\} \times \{(+, +)\} \cup \{0, 1, \top, \bot\} \times \{()\}$;

- one-sided $\mu LL$ signature: $C_{\mu LL_1} = C_{\mu MALL} \cup \{\mathcal{O}, ?\} \times \{(+)\}$;

- two-sided $\mu LL$ signature: $C_{\mu LL_2} = C_{\mu LL_1} \cup \{(-\mathcal{O}, (-, +)), (\cdot \bot, (-))\}$;

<footnote n="1">¹ $\mu$-signature can be enriched to consider quantifiers but we restrict to the propositional case here.</footnote>
- $\mu$LK signature: $C_{\muLK} = \{\wedge, \vee\} \times \{(+, +)\} \cup \{(\Rightarrow, (-, +))\} \cup \{\vdash, F\} \times \{()\}$;

- $\mu$LJ signature: $C_{\muLJ} = C_{\muLK}$.

**Definition 3 (Pre-formulas).** Given a $\mu$-signature $C$, a countable set $\mathcal{V}$ of fixed-point variables and a set of atomic formulas $\mathcal{A}$, the set of **pre-formulas** over $\mathcal{S}$ is defined as the least set $\mathcal{F}_{\mathcal{S}}$ such that: (α) $\mathcal{A} \cup \mathcal{V} \subseteq \mathcal{F}_{\mathcal{S}}$; (β) for every $c$ of arity $n$ in $C$ and $F_1, \dots, F_n \in \mathcal{F}_{\mathcal{S}}$, $c(F_1, \dots, F_n) \in \mathcal{F}_{\mathcal{S}}$; (γ) for every $X \in \mathcal{V}$ and pre-formula $F \in \mathcal{F}_{\mathcal{S}}$, $\mu X.F \in \mathcal{F}_{\mathcal{S}}$ and $\nu X.F \in \mathcal{F}_{\mathcal{S}}$.

**Definition 4 (Positive and negative occurrences of a variable).** Given a $\mu$-signature $C$ and a fixed-point variable $X \in \mathcal{V}$, one defines by induction on pre-formulas the fact, for $X$, to occur positively (resp. negatively) in a pre-formula : (α) $X$ occurs positively in $X$; (β) $X$ occurs positively (resp. negatively) in $c(F_1, \dots, F_n)$, for $(c,p) \in C$, if there is some $1 \le i \le n$ such that $X$ occurs positively (resp. negatively) in $F_i$ and $p_i = +$ or there is some $1 \le i \le n$ such that $X$ occurs negatively (resp. positively) in $F_i$ and $p_i = -$; (γ) $X$ occurs positively (resp. negatively) in $\sigma Y.F$, for $\sigma \in \{\mu, \nu\}$, if $Y \ne X$ and $X$ occurs positively (resp. negatively) in $F$.

**Definition 5 ($\mu$-formula).** A $\mu$-formula $F$ over a signature $\mathcal{S}$ is a pre-formula containing no free fixed-point variable and such that for any sub-pre-formula of $F$ of the form $\sigma X.G$, all occurrences of $X$ in $G$ are positive.

**Definition 6.** One-sided $\mu LL$ formulas are those formulas defined over the signature $C_{\mu LL_1}$ together with a set of atomic formulas $\{a, a^{\perp} \mid a \in \mathcal{A}\}$ for a countable set $\mathcal{A}$. Negation $(\neg)^{\perp}$ is the involution on pre-formulas defined by:

$$ (a^{\perp})^{\perp} = a; \quad \perp^{\perp} = 1; \quad \top^{\perp} = 0; \quad (F \otimes G)^{\perp} = F^{\perp} \otimes G^{\perp}; \quad (F \oplus G)^{\perp} = F^{\perp} \& G^{\perp}; \\ (\neg F)^{\perp} = \neg F^{\perp}; \quad X^{\perp} = X; \quad (\nu X.F)^{\perp} = \mu X.F^{\perp}. $$

**Definition 7 ($\mu$-Fischer-Ladner subformulas).** Given a $\mu$-signature $C$ and a $\mu$-formula $F$, $FL(F)$ is the least set of formulas such that:

- $F \in FL(F)$;

- $c(F_1, \dots, F_n) \in FL(F) \Rightarrow F_1, \dots, F_n \in FL(F)$ for $c \in C$;

- $\sigma X.B \in FL(F) \Rightarrow B[\sigma X.B/X] \in FL(F)$ for $\sigma \in \{\mu, \nu\}$.

*Example 8.* Let us consider $F = \nu X.((a \otimes a^{\perp}) \otimes (!X \otimes \mu Y.X))$. $FL(F)$ is the set $\{F, (a \otimes a^{\perp}) \otimes (!F \otimes \mu Y.F), a \otimes a^{\perp}, a, a^{\perp}, !F \otimes \mu Y.F, !F, \mu Y.F\}$.

Appendix B.1 provides more details.

The finiteness of $FL(F)$ makes it an adequate notion of subformula:

**Proposition 9.** For any $\mu$-signature $\mathcal{S}$ and $\mu$-formula $F$, $FL(F)$ is finite.

See proof in Doumane's PhD thesis [18].

## 2.2 $\mu MALL^{\infty}$, $\mu LL^{\infty}$, $\mu LK^{\infty}$ & $\mu LJ^{\infty}$ inference rules.

Now, we define the inference rules associated with the above $\mu$-signatures.
<figure><img src="image_3.png" /><figcaption>Fig. 2. (a) $\mu$MALL$^{\infty}$ Inferences; (b) $\mu$LL$^{\infty}$ Exponential Inferences</figcaption></figure>

**Definition 10 (Sequents and inferences).** A sequent $s = \Gamma \vdash \Delta$ over a $\mu$-signature $S$ is a pair of finite lists $\Gamma, \Delta$ of $S$-formulas: $\Gamma$ is the antecedent and $\Delta$ the succedent. An inference rule $r$, usually presented by a schema, is the data of a conclusion sequent, premise sequents, together with an ancestor relation relating formulas of the conclusion with formulas of the premises. A rule has a subset of distinguished principal formulas of the conclusion.

Appendix B.2 provides more details.

**Convention 1** In the following, the ancestor relation will be depicted as colored lines joining related formulas. The **principal** formulas of an inference are the formulas which are explicitly spelled out in the conclusion sequent of an inference, not described via a context meta-variable. A formula occurrence of an inference is said to be **active** if it is principal or related to a principal formula by the ancestor relation. We will freely use the derived rules obtained by **pre-** and **post-composition with the exchange rule**, adapting the ancestry relation accordingly. Finally, for one-sided sequent calculi with an involutive negation $\vdash^{\perp}$, we may write $\Gamma \vdash \Delta$ for sequents $\vdash \Gamma^{\perp}, \Delta$ to clarify the computational behaviour of our examples (keeping the rule names unchanged).

**Definition 11** ($\mu$MALL$^{\infty}$, $\mu$LL$^{\infty}$, $\mu$LK$^{\infty}$, $\mu$LJ$^{\infty}$). $\mu$MALL$^{\infty}$ inferences are given in Figure 2. Those for one-sided $\mu$LL$^{\infty}$ in Fig. 2(a) and 2(b). Those for $\mu$LK$^{\infty}$ in Fig. 3. Those for $\mu$LJ$^{\infty}$ by considering only inference from Fig. 3 where the succedent of both premises and conclusion sequents are singletons.

Appendix B.3 provides more details on $\mu$LJ$^{\infty}$.

In the above sequent calculi, every inference but the cut satisfies the subformula property wrt. FL-subformulae. The 2-sided $\mu$LL$^{\infty}$ sequent calculus, over $C_{\mu LL_2}$, is defined as usual and not recalled here for space constraints.
<figure><img src="image_4.png" /><figcaption>Fig. 3. $\mu$LK$^\infty$ Two-sided Inferences</figcaption></figure>

## 2.3 Pre-proofs and validity conditions.

**Definition 12 (Pre-proofs).** The set $P_{S,I}$ of *I*-pre-proofs associated to some of the above $\mu$-signatures $S$ and sets of inferences $\mathcal{I}$ is the set of finite or infinite trees whose nodes are correctly labelled with inferences and sequents.

See details in appendix B.4.

Pre-proofs are equipped with a metric structure as follows: we define a *distance* $d: P_{S,I} \times P_{S,I} \to \mathbb{R}$ as: $d(\pi, \pi') = 0$ if $\pi = \pi'$ and $d(\pi, \pi') = 2^{-k}$ where $k$ is the length of the shortest position where $\pi$ and $\pi'$ differ otherwise.

*Example 13.* Consider $\mu$LJ formulas $N = \mu X.\top \lor X$ and $S = \nu X.N \land X$. They represent nats and streams of nats. The $\mu$LJ$^\infty$ derivations of Figure 4 respectively represent natural numbers, successor function, $n :: n + 1 :: n + 2 :: \dots$, the double functions and the function that builds a stream enumerating the natural numbers from its input: the cut-elimination process considered below will ensure that cutting $\pi_k$ with $\pi_{enum}$ will infinitely reduce to $\pi_{from}^k$. Figure 5 shows other examples of $\mu$LL$^\infty$ pre-proofs, discussed with the validity condition.

The back-edge arrow to a lower sequent is a fixed-point definition of the proof object: the subproof rooted in the source is equal to the proof rooted in the target. This fixed-point definition trivially has a unique solution.

In the following, we assume given a $\mu$-signature $S$ and a sequent calculus $S$ for this signature and we shall define the valid $S$-proofs as a subset of $S$-pre-proofs, by introduction a **thread-based validity condition**.

More details provided in appendix B.4.

**Definition 14 (Thread and validity).** Given a pre-proof $\pi$ and an infinite branch $\beta = (s_i)_{i \in \omega}$ in $\pi$, a **thread** for $\beta$ is an infinite sequence $\theta$ of formula occurrences such that $\forall i \in \omega$, $\theta_i$ is a formula occurrence of $s_i$ and $\theta_{i+1}$ are ancestor of each other. $\theta$ is said to **support** $\beta$.

A formula $F$ is **recurring** in a thread $\theta$ of $\beta$ if there are infinitely many $i$ such that $\theta_i$ is an occurrence of $F$.

A thread $\theta$ is **valid** if it contains infinitely often the principal formula (occurrence) of a $\nu$ or $\mu$ rule and if the set of recurring formulas of $\theta$ has a least element (for the usual subformula ordering) which is (i) a $\nu$ formula when the least element occurs in the succedents or (ii) a $\mu$ formula if it occurs in the antecedents. A pre-proof is **valid** if all its infinite branches have a suffix supported by a valid thread.
<figure><img src="image_5.png" /><figcaption>Fig. 4. Examples of $\mu LJ^\infty$ pre-proofs.</figcaption></figure>

Example 15 ((Non-)valid pre-proofs). Consider the pre-proof in Fig. 5(a), with $F = \nu X.((a\mathcal{F}a^\perp) \otimes (!X \otimes \mu Y.X))$ and $G = \mu Y.F$. The rightmost branch is supported by the green thread for which the least recurring formula is $F$, a $\nu$-formula. All other branches are valid: this pre-proof is valid. Consider now the same pre-proof but with $F = \nu X.((a\mathcal{F}a^\perp)\otimes(!X\otimes G))$ and $G = \mu Y.\nu X.((a\mathcal{F}a^\perp)\otimes (!X \otimes Y))$. $G$ is now a subformula of $F$ and $G$, a $\mu$-formula, and becomes the least recurring formula of all threads along the right-most infinite branch. This branch is invalid: the pre-proof is not a proof. Examples of $\mu LL^\infty$ invalid pre-proofs are given in Fig. 1(a), 5(b-c). In Fig. 4, $\pi_{\text{double}}$ has a left thread on $N$ while $\pi_{\text{from}}^n$, $\pi_{\text{enum}}$ have right threads on $S$: they are valid.

## 2.4 Non-locative $\mu$MALL$^\infty$ cut-elimination theorem

The validity condition defines a subset of pre-proofs, ensuring good properties for those non-wellfounded derivations that satisfy the validity condition. In this paper, we will mainly be interested in cut-elimination theorem, which was proved for $\mu$MALL$^\infty$ [4] and that we review in this subsection. In [4], a somehow stronger result than cut-elimination is proved: infinitary strong normalization with respect to the class of fair reduction sequences.

The only new result developed in this subsection is the lifting of the occurrence-based cut-elimination result of [4] to our setting system, for which we first introduce the multicut inference and review the main multicut-reduction steps for $\mu$MALL$^\infty$ before defining fair reductions. The cut-elimination results of [4,20] do not rewrite cuts, per se, but subtrees of cuts in the form of an abstraction called *multicut* which is a variable arity inference defined as follows:

See details in appendix B.5.

**Definition 16.** The *multicut inference* is given by the data of (i) a conclusion sequent $s$, (ii) a non-empty list of premises $(s_1, \dots, s_n)$, $n \ge 1$, (iii) an ancestor relation $\iota$ which is an injective map from the conclusion formulas to the premise formulas and relates identical formulas and additionally (iv) a *cut-connectedness relation* $\perp$ which is a total, symmetric, binary relation among the formula occurrences of the premises which are not ancestor of a conclusion
<figure><img src="image_6.png" /><figcaption>Fig. 5. Examples of valid and invalid pre-proofs.</figcaption></figure>

formula, which relates dual formulas<fnref n="2" /> and which satisfies a connectedness and acyclicity condition (see [3,4]). The multicut inference has no principal formula.

We write this multicut rule as:

$$ \frac{s_1 \dots s_n}{s} \text{ mcut}(\iota, \perp) $$

In the following, we only consider $\mu$MALL$^\infty$ pre-proofs with specific multicuts:

**Definition 17 (μMALL_m^∞).** $\mu$MALL_m^∞ (pre) proofs are those (pre) proofs built from $\mu$MALL^∞ inferences and the multicut, such that (i) any branch contains at most one multicut and (ii) any occurrence of a cut is above a multicut inference.

In the following, we shall always assume, even without mentioning it, that we consider proofs in $\mu$MALL_m^∞ (as well as $\mu$LL_m^∞, $\mu$LJ_m^∞, $\mu$LK_m^∞). We need the following definition (from [4]), identifying the premises of an mcut which are cut-connected to a given formula occurrence:

**Definition 18 (Restriction of a mcut-context).** Consider an occurrence of a mcut $\frac{s_1 \dots s_n}{s} \text{ mcut}(\iota, \perp)$ and assume $s_i$ to be $\vdash F_1, \dots, F_k$. We define $C_{F_j}, 1 \le j \le k$, to be the least set of sequent occurrences contained in $\{s_1, \dots, s_n\}$ such that:
(i) If $\exists k, l$ such that $(k, l) \perp (i, j)$, then $s_k \in C_{F_j}$;
(ii) for any $k, k' \ne i$, if $s_k \in C_{F_j}$ and $\exists l, l'$ such that $(k, l) \perp (k', l')$, then $s_{k'} \in C_{F_j}$. We define $C_\emptyset = \emptyset$ and $C_{F,\Gamma} = C_F \cup C_\Gamma$.

When relating $\mu$LL^∞ and $\mu$MALL^∞ mcut-sequences below, we shall consider not only finite sequence nor $\omega$-indexed sequences but also transfinite sequences. Those are sequences of triples of a proof, a redex and the position of the redex in the proof tree. A position $p$ has a **depth** $dph(p)$ which is its length.

**Definition 19 (mcut-reduction rules, transfinite sequences).** $\mu$MALL^∞ mcut-reduction sequences are directly adapted from [3,4]. Given an ordinal $\lambda$, a **transfinite reduction sequence** of length $\lambda$, or $\lambda$TRS, is a $\lambda$-indexed sequence $(\pi_i, r_i, p_i)_{i \in \lambda}$ such that $\pi_i \to^{p_i}_{r_i} \pi_{i+1}$, for any $i$ such that $i+1 \in \lambda$, where the reduction occurs at position $p_i$ reducing mcut-redex $r_i$.

See details in appendix B.6.

**Definition 20 (Weak and strong convergence).** A (transfinite) mcut reduction sequence $(\pi_i, r_i, p_i)_{i \in \alpha}$ is **weakly converging** if for any limit ordinal $\beta \in \alpha$, $\lim(\pi_i)_{i \in \beta} = \pi_\beta$. $(\pi_i, r_i, p_i)_{i \in \alpha}$ is **strongly converging** if it is weakly converging and moreover for any limit ordinal $\beta \in \alpha$, $\lim(dph(p_i))_{i \in \beta} = +\infty$.

See details in appendix A.

<footnote n="2">² When working with two-sided sequents, $\perp$ will relate identical formulas, one in a succedent, the other in an antecedent.</footnote>
*Remark 21.* The cut-reduction rules preserve the property that every branch of a proof has at most one multicut inference: $\mu\mathsf{MALL}^\infty_m$ is closed by cut-reduction.

A $\mu\mathsf{MALL}^\infty_m$ pre-proof $\pi$ may contain multiple cut-redexes: $\pi \rightarrow^{p_1}_{r_1} \pi_1$ and $\pi \rightarrow^{p_2}_{r_2} \pi_2$. As usual, a notion of residual associates to $(r_1, p_1)$, a set of redexes of $\pi_2$, $(r_1, p_1)/(r_2, p_2)$ which is generalized to reduction sequences: $(r_1, p_1)/\sigma$.

See details in appendix B.8.

**Definition 22 (Fair reduction sequences).** A reduction sequence $(\pi_i, r_i, p_i)_{i \in \omega}$ is fair if for all $i \in \omega$ and $r, p$ such that $\pi_i \rightarrow^{p_i} \pi'$ there is some $j \ge i$ such that $\pi_j$ does not contain a residual of $(r, p)$ anymore.

**Theorem 23.** Every fair mult-reduction sequence of $\mu\mathsf{MALL}^\infty$ valid proofs of $\vdash \Gamma$ (strongly) converges to a cut-free valid proof of $\vdash \Gamma$.

See proof in appendix B.7.

## 2.5 Compressing transfinite $\mu\mathsf{MALL}^\infty$ cut-reduction sequences

In the previous paragraph, we introduced not only $\omega$-indexed sequences, but transfinite $\mu\mathsf{MALL}^\infty$ cut-reduction sequences as we shall need reduction beyond $\omega$ when simulating $\mu\mathsf{LL}^\infty$ cut-elimination in $\mu\mathsf{MALL}^\infty$. We shall now prove that a class of transfinite $\mu\mathsf{MALL}^\infty$ mcut-reduction sequences can be compressed to $\omega$ TRS. This result can be viewed as adapting to our setting the compression lemma from infinitary rewriting [32], even though we require more on the structure of the compressed sequences as it will be useful to establish $\mu\mathsf{LL}^\infty$ cut-elimination.

**Definition 24 (Depth-increasing).** A $\mu\mathsf{MALL}^\infty$ cut reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ is depth-increasing if $(\mathrm{depth}(p_i))_{i \in \omega}$ is (weakly) increasing.

See details on infinitary rewriting in appendix A.

**Definition 25 (Reordering).** An mcut reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \alpha}$ is a reordering of $\sigma' = (\pi'_i, r'_i, p'_i)_{i \in \beta}$ if there is a bijection $o$ between $\alpha$ and $\beta$ such that for any $i \in \alpha$, $(r'_{o(i)}, p'_{o(i)}) = (r_i, p_i)$.

**Proposition 26 (Compression lemma).** Let $\sigma = (\pi_i, r_i, p_i)_{i \in \alpha}$ be a strongly converging $\mu\mathsf{MALL}^\infty$ transfinite cut-reduction sequence. There exists a $\mu\mathsf{MALL}^\infty$ cut-reduction sequence $\mathrm{Comp}(\sigma) = (\pi'_i, r'_i, p'_i)_{i \in \beta}$ which is a reordering of $\sigma$, depth-increasing, strongly converging with the same limit as $\sigma$ and such that $\beta = \alpha$ if $\alpha$ is finite and $\beta = \omega$ otherwise.

See proof in App B.9.

## 3 Cut-elimination theorem for $\mu\mathsf{LL}^\infty$

The aim of this section is to prove the following theorem:

**Theorem 27.** For any valid $\mu\mathsf{LL}^\infty$ proof $\pi$, fair $\mu\mathsf{LL}^\infty$ mcut-sequences from $\pi$ converge to cut-free $\mu\mathsf{LL}^\infty$ proofs.

The idea of the proof and outline of the present section are as follows:
1. We shall first define the cut-reduction rules for $\mu LL^\infty$ by extending $\mu MALL^\infty$ multicut-reduction with rules for reducing exponential cuts.

2. We then encode exponentials with fixed-points and translate $\mu LL^\infty$ sequents (resp. pre-proofs) into $\mu MALL^\infty$, preserving validity both ways.

3. We will then simulate $\mu LL^\infty$ reductions in $\mu MALL^\infty$: a single $\mu LL^\infty$ step may require an infinite, or even transfinite, $\mu MALL^\infty$ mcut-reduction sequence.

4. Finally, we will study the simulation of fair $\mu LL^\infty$ cut-reduction sequences. Even though the simulation of $\mu LL^\infty$ sequences builds transfinite sequences, we shall see that one can associate a(n almost) fair $\mu MALL^\infty$ mcut-reduction sequence to any fair $\mu LL^\infty$ mcut-reduction sequence, and conclude. The next four subsections will closely follow the above pathway.

## 3.1 Cut-elimination rules for $\mu LL^\infty$

$\mu LL^\infty$ mcut-reduction is defined by extending $\mu MALL^\infty$ multicut-reduction with the steps given in Figure 6. The reduction rules for the exponentials assume a condition on the premisses of the multi-cut rule: all the proofs (hereditarily) cut-connected to some distinguished formula must have promotions as last inferences.

**Definition 28** ($(!p)$-ready contexts). A subset of the subproofs of a multicut is said to be ($(!p)$-ready if all its elements are concluded with an ($!p$) rule. $C^1$ will denote a ($!p$)-ready context and $C^1_Γ$ a context restriction which is ($!p$)-ready.

*Remark 29.* The condition for triggering the exponential key reductions $(?w)/(!p)$ and $(?c)/(!p)$ as well as the ($!p$)-commutation rule is expressed in terms of ($!p$)-readiness: for every $?-formula$ $?G$ in the context of a promotion which shall either commute or cut-reduce with a $?-rule, we require that $C_{?G}$ is ($!p$)-ready.

More details can be found in appendix C.1.

## 3.2 Embedding $\mu LL^\infty$ in $\mu MALL^\infty$

To extend the cut-elimination result from $\mu MALL^\infty$ to $\mu LL^\infty$, we encode the exponential connectives using fixed points as follows, following Baelde [2]:

**Definition 30.** $?^•(F) = \mu X.F \oplus (\bot \oplus (X\ominus X)); ?^•(F) = \nu X.F \& (1\&(X \otimes X))$

This straightforwardly induces an embedding of $\mu LL^\infty$ into $\mu MALL^\infty$:

**Definition 31 (Embedding of $\mu LL^\infty$ sequents into $\mu MALL^\infty$).**

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
(a)^{\bullet} & = a & \text{if } a \text{ is an atom} \\
(u)^{\bullet} & = u & \text{if } u \in \{1, \bot, \top, 0\} \\
(A \star B)^{\bullet} & = (A)^{\bullet} \star (B)^{\bullet} & \text{if } \star \in \{\& , \oplus , \ominus , \otimes\}
\end{array}
\quad
\left|
\begin{array}{l}
(\sigma X.F)^{\bullet} = \sigma X.(F)^{\bullet} , \sigma \in \{\mu, \nu\} \\
(?F)^{\bullet} = ?^•(F^•) \\
(!F)^{\bullet} = !^•(F^•)
\end{array}
\right.
$$

**Definition 32** ($\mu MALL^\infty$ derivability of the exponentials). $\mu LL^\infty$ exponential rules can be encoded in $\mu MALL^\infty$ as shown in Figure 7. We denote the derivable rules by $?d^•$, $?c^•$, $?w^•$ and $!p^•$ respectively. ($!p^•$ uses a circular proof.)

**Proposition 33 (Preservation of validity).** $\pi$ is a valid $\mu LL^\infty$ proof of $\vdash \Gamma$ iff $\pi^•$ is a valid $\mu MALL^\infty$ proof of $\vdash \Gamma^•$.
<figure><img src="image_7.png" /></figure>

where $?F \perp!F^{\perp}$ and $\perp'$ coincides with $\perp$ except for $F \perp' F^{\perp}$.

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

where $C'_F \neq \emptyset$, $\perp'$ corresponds to $\perp$ on $C_\Gamma$ and is a "duplication" of $\perp$ on $C'_F$ and each copy of $?F$ is in $\perp'$-relation with the corresponding copy of $!F^{\perp}$ in $C'_F$.

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

where $C'_F \neq \emptyset$ and $\perp'$ corresponds to the restriction of $\perp$ on $C_\Gamma, \Gamma$.

<caption>Fig. 6. $\mu LL^\infty$ mcut-reduction rules.</caption>

*Proof (Proof sketch).* We simply relate the infinite branches in both pre-proofs. Assuming that $\pi$ is valid, consider the special case of an infinite branch $\beta$ of $\pi$• that, when entering the encoding of a promotion, follows the left-most premise of the ($\&$) rule. To such an infinite branch it is easy to associate an infinite branch $b$ of $\pi$. $b$ is valid and supported by a thread $t$ with least formula $\nu X \cdot F$. $(\nu X \cdot F)\bullet$ is the least recurring formula in the thread $\theta$ associated with $t$ in $\beta$: $\beta$ is valid.

The detailed proof can be found in Appendix C.2.

## 3.3 Simulation of $\mu LL^\infty$ cut-elimination steps

Now we have to show that $\mu LL^\infty$ cut-elimination steps can be simulated by the previous encoding. E.g., the commutation rule for dereliction is simulated by a
<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /><figcaption>Fig. 7. $\mu$MALL$^{\infty}$ encoding of the exponential inferences.</figcaption></figure>

($\mu$)/($\text{Cut}$) commutation followed by a ($\oplus$)/($\text{Cut}$) commutation as follows:

$$ \frac{\substack{\vdash F, G, \Gamma \\ \vdash^{?\bullet} F, G, \Gamma \quad (?d^\bullet)} \quad \substack{\vdash G^\perp, \Delta \\ \vdash^{?\bullet} F, \Gamma, \Delta}}{\substack{\text{(Cut)} \\ \text{($\oplus$)}}} \rightarrow^2 \frac{\substack{\vdash F, G, \Gamma \quad \vdash G^\perp, \Delta \\ \vdash F, \Gamma, \Delta \quad \vdash^{?\bullet} F, \Gamma, \Delta}}{\substack{\text{(Cut)} \\ (?d^\bullet)}} $$

The challenge is to show that the simulation of reductions also holds (i) for the reductions involving ($!p$) as well as (ii) for reductions occurring **above** a promotion rule (aka. in a box) since the encoding of [$!p$] uses an infinite, circular derivation. In the promotion commutation case for instance, we have:

$$ \frac{\substack{\vdash F, ?\bullet G, ?\bullet \Gamma \\ \vdash^{!\bullet} F, ?\bullet G, ?\bullet \Gamma}}{\substack{\text{($!p^\bullet$)} \\ \vdash^{!\bullet} F, ?\bullet \Gamma, ?\bullet \Delta}} \rightarrow_{\text{(Cut)}}^{\omega} \frac{\substack{\vdash F, ?\bullet G, ?\bullet \Gamma \\ \vdash^{!\bullet} G^\perp, ?\bullet \Delta}}{\substack{\text{($!p^\bullet$)} \\ \vdash^{!\bullet} F, ?\bullet \Gamma, ?\bullet \Delta}} \rightarrow_{\text{(Cut)}} \frac{\substack{\vdash G^\perp, ?\bullet \Delta \\ \vdash^{!\bullet} G^\perp, ?\bullet \Delta}}{\substack{\text{($!p^\bullet$)} \\ (?d^\bullet)}} $$

See proof in App C.3.

**Proposition 34.** Each $\mu LL^{\infty}$ mcut-reduction $r$ can be simulated in $\mu MALL^{\infty}$ by a (possibly infinite) sequence of mcut-reductions, denoted $r^\bullet$.

*Remark 35.* Conversely, one can wonder whether a possible reduction in $\pi^\bullet$ necessarily comes from the simulation of a reduction step in $\pi$. It is almost the case except when the reduction in $\pi^\bullet$ comes from exponential cuts requiring a ($!p$)-ready context (ie. ($!p$) commutation as well as $(?w)/(!p)$ and $(?c)/(!p)$ key cases, see above): in those cases indeed, if the context is “partially ready” – meaning that some, but not all, the required premises are promoted – a prefix of the sequence simulating the reduction step can indeed be performed, before being stuck. As consequence – and we shall exploit it in the next section when proving $\mu LL^{\infty}$ cut-elimination – the simulation of a fair reduction sequence is not necessarily fair, but only as long as the above cases are involved:

**Proposition 36.** There exists a fair reduction $\rho$ from some $\mu LL^{\infty}$ (pre-)proof $\pi$ such that $\rho^\bullet$ is an $\omega$-indexed unfair $\mu MALL^{\infty}$ cut-reduction sequence

See proof in App C.4.
### 3.4 Proof of $\mu LL^\infty$ cut-elimination theorem

$\mu LL^\infty$ cut-elimination theorem follows from the following two lemmas:

**Lemma 37.** Let $\pi$ be a $\mu LL^\infty$-proof of $\vdash \Gamma$ and $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ a fair $\mu LL^\infty$ cut-reduction sequence from $\pi$. $\sigma$ converges to a cut-free $\mu LL^\infty$-pre-proof of $\vdash \Gamma$.

See proof in App C.5.

**Lemma 38.** Let $\pi$ be a $\mu LL^\infty$ pre-proof of $\vdash \Gamma$ and let us consider a cut-reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ in $\mu LL^\infty$ from $\pi$ that converges to a cut-free $\mu LL^\infty$ pre-proof $\pi'$. $\sigma^\bullet$ is a strongly converging (possibly transfinite) sequence.

See proof in App C.5.

**Proof (Sketch for Thm. 27).** Let $\pi$ be a $\mu LL^\infty$-proof of $\vdash \Gamma$ and $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ be a fair $\mu LL^\infty$ mcut-reduction sequence from $\pi$. Consider the associated (transfinite) $\mu MALL^\infty$ mcut-reduction sequence $\sigma^\bullet$ from $\pi^\bullet$ obtained by simulation. By Lemma 37, $\sigma$ converges (strongly) to a cut-free $\mu LL^\infty$ pre-proof $\pi'$.

See details in App C.5.

Let us prove that $\pi'$ is valid. By Lemma 38, $\sigma^\bullet$ is a transfinite mcut-reduction sequence from $\pi^\bullet$ strongly converging to $\pi'^\bullet$. By Prop. 26, $\sigma^\bullet$ can be compressed into $\rho = (\pi'_i, r'_i, p'_i)_{i \in \omega}$ an $\omega$-indexed depth-increasing $\mu MALL^\infty$ mcut-reduction sequence which converges to $\pi'^\bullet$ and contains the same reductions as $\sigma^\bullet$. By Proposition 36, $\rho$ may not be fair: this prevents us from concluding directly by Proposition 33 but we can still conclude. Let us consider $\rho_f$ a fair reduction sequence obtained from $\rho$ by reducing those redexes which cause the lack of fairness of $\rho$ and let us consider the limit of $\rho_f$, $\pi_f$. To any infinite branch $\beta$ of $\pi'^\bullet$, one can associate a branch $\beta_f$ of $\pi_f$: it coincides with $\beta$ except when the next inference of $\beta_f$ is on a $(!F)^\bullet$ (in a sequent, say, $\vdash (!F)^\bullet$, $?^\bullet\Delta^\bullet$ which is not principal along $\beta$). In that case, we expand $\beta_f$ by following the unique premise of the ($\nu$) rule, the second premise of the first ($\&$) rule and the first premise of the second ($\&$) rule, reaching $\vdash 1$, $?^\bullet\Delta^\bullet$, in which case we know that the 1 is not principal (and never will be) and we follow back $\beta$. $\beta_f$ has exactly the same threads as $\beta$: finite threads may only be extended finitely on occurrences of $(!F)^\bullet$. Since $\rho_f$ is fair, $\beta_f$ is valid and so is $\beta$.

We can then conclude that $\pi'^\bullet$ is cut-free and valid and, using preservation of validity (Proposition 33), that $\pi'$ is a valid cut-free $\mu LL^\infty$-proof. $\square$

Infinitary cut-elimination for $\mu LL^\infty$ two-sided sequent calculus is an easy corollary of Theorem 27. Indeed, fair cut-reduction sequences in two-sided $\mu LL^\infty$ are mapped to fair reduction sequences in one-sided $\mu LL^\infty$ from which follows:

**Corollary 39.** Fair 2-sided $\mu LL^\infty$ valid mcut-reduction sequences eliminate cuts.

See proof in App C.5.

## 4 Cut-elimination theorem for $\mu LK^\infty$ and $\mu LJ^\infty$

Cut-elimination theorems for both $\mu LK^\infty$ and $\mu LJ^\infty$ can be established as corollaries of Theorem 27. For lack of space, we directly go to our results and postpone to future work a detailed study of the generalizations to non-wellfounded sequent calculi of the linear embeddings of LK and LJ into LL developed since Girard seminal paper. We shall comment on those translations in the conclusion.
## 4.1 $\mu$LK$^{\infty}$ cut-elimination: Skeletons and decorations

To any $\mu$LL$^{\infty}$ formulas and $\mu$LL$^{\infty}$ proofs, one can associate their skeletons, that is corresponding $\mu$LK$^{\infty}$ formulas and proofs, after erasing of the linear information:

**Definition 40 (Skeleton).** Sk(A) is defined by induction on A ∈ $\mu$LL$^{\infty}$:

$$ \begin{array}{rcl} \mathrm{Sk}(A \otimes B) & = & \mathrm{Sk}(A) \wedge \mathrm{Sk}(B) \\ \mathrm{Sk}(A \& B) & = & \mathrm{Sk}(A) \wedge \mathrm{Sk}(B) \\ \mathrm{Sk}(1) & = & \mathrm{Sk}(\top) = \top \\ \mathrm{Sk}(A \to B) & = & \mathrm{Sk}(A) \Rightarrow \mathrm{Sk}(B) \end{array} \quad \left| \begin{array}{rcl} \mathrm{Sk}(A \otimes B) & = & \mathrm{Sk}(A) \vee \mathrm{Sk}(B) \\ \mathrm{Sk}(A \oplus B) & = & \mathrm{Sk}(A) \vee \mathrm{Sk}(B) \\ \mathrm{Sk}(\bot) & = & \mathrm{Sk}(0) = \mathrm{F} \\ \mathrm{Sk}(\sigma X.A) & = & \sigma X.\mathrm{Sk}(A) \end{array} \right| \begin{array}{rcl} \mathrm{Sk}(!A) & = & \mathrm{Sk}(A) \\ \mathrm{Sk}(?A) & = & \mathrm{Sk}(A) \\ \mathrm{Sk}(a) & = & a \\ \mathrm{Sk}(X) & = & X \end{array} $$

with $\sigma \in \{\mu, \nu\}$.

Given a 2-sided $\mu$LL$^{\infty}$ pre-proof $\pi$ of $\Gamma \vdash \Delta$ with last rule r and premises $(\pi_i)_{1 \le i \le n}$, $\mathrm{Sk}(\pi)$ is the $\mu$LK$^{\infty}$ pre-proof of $\mathrm{Sk}(\Gamma) \vdash \mathrm{Sk}(\Delta)$ defined corecursively, by case on r: (i) if r ∈ {(!p), (?d)}, $\mathrm{Sk}(\pi) = \mathrm{Sk}(\pi_1)$; (ii) otherwise, apply the $\mu$LK$^{\infty}$ rule corresponding to r with premises $(\mathrm{Sk}(\pi_i))_{1 \le i \le n}$.

See details in App D.1.

See proof in App D.2.

**Proposition 41.** $\mathrm{Sk}(\cdot)$ transports valid $\mu$LL$^{\infty}$-proofs to valid $\mu$LK$^{\infty}$ proofs.

$\mu$LK$^{\infty}$ cut-elimination follows from the existence of $\mu$LK$^{\infty}$ linear decorations.

See details in App D.3.

**Proposition 42.** For any $\mu$LK$^{\infty}$ sequent s and any $\mu$LK$^{\infty}$ proof $\pi$ of s, there is a linear decoration of $\pi$, that is a $\mu$LL$^{\infty}$ proof $\pi^d$ such that $\mathrm{Sk}(\pi^d) = \pi$.

**Definition 43 ($\mu$LK$^{\infty}$ cut-reduction).** $\mu$LK$^{\infty}$ mcut-reduction relation is defined as follows: $\rightarrow_{\mu}$LK$^{\infty}$ = {($\mathrm{Sk}(\pi)$, $\mathrm{Sk}(\pi')$) | $\pi \rightarrow_{mcut} \pi'$ & $\pi \ne \pi'$}.

See proof in App D.4.

**Theorem 44.** $\mu$LK$^{\infty}$ enjoys cut-elimination.

## 4.2 $\mu$LJ$^{\infty}$ cut-elimination

The linear decoration for $\mu$LJ$^{\infty}$ is simply Girard's call-by-value translation [21] extended to fixed-points on formulas and proofs as follows:

$$ \begin{array}{l} [X]^j = !X; \\ [\mu X.F]^j = !\mu X.[F]^j; \\ [\nu X.F]^j = !\nu X.[F]^j. \\ \left[ \frac{\pi}{\Gamma \vdash F[\sigma X.F/X]} \quad (\sigma_i) \right]^j = \frac{[\Gamma]^j \vdash [F]^j[\sigma X.[F]^j/X]}{[\Gamma]^j \vdash \sigma X.[F]^j} \quad (\sigma_i) \\ \frac{[\Gamma]^j \vdash [\sigma X.F]^j}{[\Gamma]^j \vdash [\pi]^j} \\ \left[ \frac{\pi}{\Gamma, F[\sigma X.F/X] \vdash G} \quad (\sigma_i) \right]^j = \frac{[\Gamma]^j, [F]^j[\sigma X.[F]^j/X], \vdash [G]^j}{[\Gamma]^j, \sigma X.[F]^j \vdash [G]^j} \quad (\sigma_i) \end{array} $$

The translation is consistent with $\mu$LJ$^{\infty}$- and $\mu$LL$^{\infty}$-positivity conditions.

**Definition 45 ($\mu$LL$^{\infty}$).** $\mu$LL formulas are defined inductively as:

$$ I, J ::= a \mid !X \mid I \to J \mid I \& J \mid I \oplus J \mid \top \mid 0 \mid \mu X.I \mid \nu X.I \mid !I. $$

A $\mu$LL sequent is a sequent of $\mu$LL formulas with exactly one formula in the succedent. A $\mu$LL$^{\infty}$ proof is a $\mu$LL$^{\infty}$ proof containing only $\mu$LL sequents.
The translation preserves validity, following from $[X]^j = !X$, by induction.

**Lemma 46.** *The following hold:*

- For any $\mu LJ$ formulas $A, B$, $\sigma \in \{\mu, \nu\}$, $[A[\sigma X.B/X]]^j = [A]^j[\sigma X.[B]^j/X]$.

- For any $\mu LJ$ formula $A$, $[A]^j$ is a $\mu LL$ formula.

- If $\pi$ is a $\mu LJ^\infty$ proof of $\Gamma \vdash F$, then $[\pi]^j$ is a $\mu LL^\infty$ proof of $[\Gamma]^j \vdash [F]^j$.

On $\mu LL^\infty$ proofs, the skeletons of the previous section can be reused: $Sk(\cdot)$ transports valid $\mu LL^\infty$ proof to valid $\mu LJ^\infty$ proofs. Moreover $\mu LL^\infty$ proofs are closed by $\mu LL^\infty$ cut-reductions from which we deduce, as for $\mu LK^\infty$, that:

**Theorem 47.** *$\mu LJ^\infty$ enjoys cut-elimination.*

# 5 Conclusion

In the present paper, we established several cut-elimination results for non-wellfounded proof systems for logics with least and greatest fixed-points expanding on previous works [4,20]: (i) for $\mu MALL^\infty$ with sequents as lists in contrast sequents as sets of locative occurrences [4], (ii) for the 1-sided and 2-sided sequent calculi of $\mu LL^\infty$, (iii) for $\mu LK^\infty$ and (iv) for $\mu LJ^\infty$. We also established additional results from a compression lemma for $\mu MALL^\infty$ strongly converging cut-reduction sequences to linear embeddings of $\mu LK^\infty$ and $\mu LJ^\infty$ into $\mu LL^\infty$.

*On the meaning and expressiveness of tree-exponential modalities.* The proof of our main result proceeds by encoding LL exponentials in $\mu MALL^\infty$ following an encoding first considered by Baelde and Miller, and studying $\mu LL^\infty$ cut-reduction sequences through their simulation in $\mu MALL^\infty$, which was first conjectured in Doumane's thesis [18]. We think that the present paper does not only demonstrate the usefulness of the encoding but that it also suggests new questions. Indeed, this encoding has interesting features:

See discussion
& example in
appendix E.

- this “rigid” tree-like exponential does not exhibit the Seely isomorphism but, even though those isomorphisms are common in axiomatizations of categorical models of linear logic, it is not necessary to have them as isomorphisms to build a denotational model of linear logic (that is, which quotients proofs up to cut-equivalence): the present work is actually an example of this fact. (They are crucial, though, to encode the $\lambda$-calculus in linear logic, as additional equations are needed, which are realized by Seely isos.)

- These exponentials allow for a realization of a somehow non-uniform promotion: indeed, while a proof of $\vdash !^\bullet F, ?^\bullet \Gamma$ has to provide a proof of $\vdash F, ?^\bullet \Gamma$, the circular definition of the promotion is not the only possible definition: one can consider as well promotions that would provide a distinct value each time a box is opened (e.g. a proof of $\vdash !^\bullet \mu X.1 \oplus X$ may provide distinct integers depending on how structural rules managed the resource).

This tree-like exponential is being investigated with Ehrhard and Jafarrahmani.
*Benefiting from advances in infinitary rewriting.* Our cut-elimination proof by encoding $\mu LL^\infty$ into $\mu MALL^\infty$ relies on a simulation of reductions sequences which makes use of transfinite reductions sequences and compression results. Those techniques are inspired and adapted from the literature on infinitary rewriting. We plan to make clearer the connection between non-wellfounded proof theory and infinitary rewriting in the future, even though in the present state it was not possible to readily apply results from infinitary rewriting such as the compression lemma which we has to reprove in our setting [32]. Moreover, we did not make use of coinductive formulations of infinitary rewriting [19]. That is another direction for future work: currently, we do not know how to use those formulations of infinitary rewriting because the sequences we consider by simulation are not given as (strongly) converging sequences. We plan to reconsider this and benefit from the coinductive approach to infinite reduction sequences.

*On linear translations for fixed-point logics and non-wellfounded proofs.* We obtained a cut-elimination theorem for $\mu LK^\infty$ and $\mu LJ^\infty$ thanks to linear translations which deserve some comments. While the linear translation used for $\mu LJ^\infty$ is standard (it is a call-by-value translation dating back to Girard's seminal paper), the treatment of classical logic was more complex. Indeed, usual linear translation for classical logic introduce, at places, cuts. Due to the sensitivity of the straight-thread validity condition with respect to the presence of cuts in cycles, we could not use those translations. However, we plan to investigate whether a more standard translation can be used in the specific case of bouncing validity [3].

*A treatment of cut-elimination which is agnostic to validity conditions.* Last but not least, a major advantage of our approach is that $\mu MALL^\infty$ cut-elimination proof and, to some extent, the validity conditions, are regarded as black boxes, simplifying the presentation of the proof and making it reusable wrt. other validity condition or $\mu MALL^\infty$ proof techniques. The proof seems to be reusable easily with bouncing validity for instance (even though setting up an adequate definition of bouncing validity for $\mu LL^\infty$ is quite tricky). A fragment which seems promising and that we wish to investigate in the near future, is $\mu MELL^\infty$ equipped with bouncing validity [3].

*Acknowledgement* The author would like to thank first David Baelde and Amina Doumane for their extensive collaboration and brilliant ideas on the topic of $\mu MALL^\infty$; the idea of a cut-elimination proof exploiting the fixed-point encoding of the exponentials emerged in joint discussions with them. Many thanks to Esaïe Bauer, Anupam Das, Abhishek De, Claudia Faggian, Farzad Jafarrahmani, Paul-André Melliès and Luc Pellissier for helpful discussions and constructive feedback on earlier versions of this draft. Last, the author would like to thanks to the anonymous reviewers who brought very relevant suggestions for the present paper and future works.
References

1. Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In Simona Ronchi Della Rocca, editor, *Computer Science Logic 2013 (CSL 2013)*, volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30–44, Dagstuhl, Germany, 2013. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2013/4188, doi: 10.4230/LIPIcs.CSL.2013.30.

2. David Baelde. Least and greatest fixed points in linear logic. *ACM Trans. Comput. Logic*, 13(1), jan 2012. doi:10.1145/2071368.2071370.

3. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In *LICS*, pages 63:1–63:13. ACM, 2022.

4. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In *25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France*, volume 62 of LIPIcs, pages 42:1–42:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://www.dagstuhl.de/dagpub/978-3-95977-022-4.

5. David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In Nachum Dershowitz and Andrei Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning*, pages 92–106, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.

6. James Brotherston. *Sequent Calculus Proof Systems for Inductive Definitions*. PhD thesis, University of Edinburgh, November 2006.

7. James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, *Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings*, volume 6803 of Lecture Notes in Computer Science, pages 131–146. Springer, 2011. doi:10.1007/978-3-642-22438-6\_12.

8. James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. A generic cyclic theorem prover. In Ranjit Jhala and Atsushi Igarashi, editors, *Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings*, volume 7705 of Lecture Notes in Computer Science, pages 350–367. Springer, 2012. doi:10.1007/978-3-642-35182-2\_25.

9. James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In *22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)*, pages 51–62. IEEE, 2007.

10. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. *Journal of Logic and Computation*, 21(6):1177–1216, 2011.

11. Kai Brünnler and Thomas Studer. Syntactic cut-elimination for a fragment of the modal mu-calculus. *Annals of Pure and Applied Logic*, 163(12):1838–1853, 2012. URL: https://www.sciencedirect.com/science/article/pii/S0168007212000760, doi:https://doi.org/10.1016/j.apal.2012.04.006.

12. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. *Ann. Pure Appl. Log.*, 109(3):205–241, 2001. doi: 10.1016/S0168-0072(00)00056-7.

13. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: Linear logic. *J. Symb. Log.*, 62(3):755–807, 1997.
14. Anupam Das. A circular version of Gödel's T and its abstraction complexity. CoRR, abs/2012.14421, 2020.

15. Anupam Das and Damien Pous. Non-wellfounded proof theory for (kleene+action)(algebras+lattices). In CSL, volume 119 of LIPIcs, pages 19:1–19:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.

16. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time $\mu$-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273–284. Springer, 2006. doi:10.1007/11944836\_26.

17. Amina Doumane. Constructive completeness for the linear-time $\mu$-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005075.

18. Amina Doumane. On the infinitary proof theory of logics with fixed points. PhD thesis, Paris Diderot University, 2017.

19. Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. Coinductive foundations of infinitary rewriting and infinitary equational logic. Log. Methods Comput. Sci., 14(1), 2018. doi:10.23638/LMCS-14(1:3)2018.

20. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 248–262. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013.

21. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1–101, 1987. doi:10.1016/0304-3975(87)90045-4.

22. Dexter Kozen. Results on the propositional $\mu$-calculus. Theoretical Computer Science, 27(3):333–354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. URL: http://www.sciencedirect.com/science/article/pii/0304397582901256, doi:https://doi.org/10.1016/0304-3975(82)90125-6.

23. Dexter Kozen. A finite model theorem for the propositional $\mu$-calculus. Studia Logica, 47(3):233–241, Sep 1988. doi:10.1007/BF00370554.

24. Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic proofs, system t, and the power of contraction. Proc. ACM Program. Lang., 5(POPL):1–28, 2021.

25. Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179–216. Elsevier, 1971. URL: https://www.sciencedirect.com/science/article/pii/S0049237X08708474, doi:https://doi.org/10.1016/S0049-237X(08)70847-4.

26. Damiano Mazza and Kazushige Terui. Parsimonious types and non-uniform computation. In ICALP, volume 9135 of Lecture Notes in Computer Science, pages 350–361. Springer, 2015.

27. Paul-André Mellès. Categorical semantics of linear logic. In Interactive models of computation and program behavior, Panoramas et Synthèses, page 213 pages. Société Mathématique de France, 2009.

28. Laureline Pinault. From automata to cyclic proofs : equivalence algorithms and descriptive complexity. (Des automates aux preuves cycliques : algorithmes
d'équivalence et complexité descriptive). PhD thesis, University of Lyon, France,
2021.

29. Reuben N. S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In Yves Bertot and Viktor Vafeiadis, editors, *Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017*, pages 53–65. ACM, 2017. doi:10.1145/3018610.3018623.

30. Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, *Foundations of Software Science and Computation Structures*, volume 2303 of *Lecture Notes in Computer Science*, pages 357–371. Springer, 2002.

31. Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points (technical report). https://www.irif.fr/_media/users/saurin/pub/mull_cutElimination_long.pdf.

32. Terese. *Term Rewriting Systems*, volume 55 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press, 2003.
# A Appendix on infinitary rewriting

In the present section, we review some standard notions of infinitary rewriting which shall be useful in the remainder of the paper and are standard from the literature, see for instance TERERESE book [32] for a general reference for infinitary rewriting covering (more than) what we will need.

**Definition 48 (Non-wellfounded terms).** Given a signature $\Sigma$, that is a set of pairs $(f, a)$ of a function symbol $f$ and an arity $a \in \omega$, we write as usual Term($\Sigma$) for the set of finite terms over $\Sigma$. The set of **non-wellfounded terms**, or **infinite terms** over $\Sigma$, written Term$^\infty(\Sigma)$, is given as the set of $\Sigma$-labelled infinite trees given by a set $P$ of (finite) sequences of natural numbers, the **positions of the tree**, and a function $\ell: P \mapsto \Sigma$, the **labelling function** satisfying the following conditions:

- $P$ is prefix closed: if $p \cdot k \in P$, then $p \in P$;

- if $p \cdot k \in P$ and $k' \le k$, then $p \cdot k' \in P$;

- for any $p \in P$, if $a$ is the arity of $\ell(p)$, then $p \cdot k \in P$ if and only if $0 \le i < a$.

If $t \in \text{Term}^\infty(\Sigma)$, we denote by $\text{Pos}(t)$ the set of **positions of** $t$ and if $p \in \text{Pos}(t)$, the **subterm of** $t$ at $p$, written $t_{@p}$, is the subtree of $t$ rooted in $p$.

Two positions $p, p'$ of a term are **incomparable** if none is a prefix of the other. The length of a position is defined as usual

We define a **distance** between terms $d: \text{Term}^\infty(\Sigma) \times \text{Term}^\infty(\Sigma) \to \mathbb{R}$ as: $d(s, t) = 0$ if $s = t$ and $d(s, t) = 2^{-k}$ where $k$ is the length of the shortest position $p \in \text{Pos}(s) \cap \text{Pos}(t)$ where $s$ and $t$ differ otherwise.

**Definition 49 (Infinitary rewriting rules, infinitary rewriting step).** An **infinitary rewriting rule** $(\infty RR)$ if a pair $(t, s)$ with $t \in \text{Term}(\Sigma)$ and $s \in \text{Term}^\infty(\Sigma)$ such that $t$ is not reduced to a variable and $\text{Var}(s) \subseteq \text{Var}(t)$.

If $r$ is an $\infty RR$, $t, s \in \text{Term}^\infty(\Sigma)$ and $p \in \text{Pos}(t)$, we call an **infinitary rewriting step** $(\infty RS)$ from $t$ to $s$ along $r$ at $p$, and write $t \to_r^p s$, if $r = (t', s')$ and there exists a substitution $\sigma: \text{Var}(t') \mapsto \text{Term}^\infty(\Sigma)$ such that $t_{@p} = \sigma(t')$, $s_{@p} = \sigma(s')$.

If $p$ is a position and $R = t \to_r^p s$ is an $\infty RS$, the **depth** of $p$ (resp. $R$), written $\text{dph}(p)$, is the length of $p$.

**Definition 50 (Transfinite reduction sequence).** Given a signature $\Sigma$, a set of infinitary rewriting rules $\mathcal{R}$ and an ordinal $\lambda$, a **transfinite reduction sequence** of length $\lambda$, or $\lambda$TRS, is a $\lambda$-indexed sequence $(t_i, r_i, p_i)_{i \in \lambda}$ such that:

- $\forall i \in \lambda, t_i \in \text{Term}^\infty(\Sigma), r_i \in \mathcal{R}, p_i \in \text{Pos}(t_i)$;

- $t_i \to_{r_i}^{p_i} t_{i+1},$ for any $i$ such that $i+1 \in \lambda$.

**Definition 51 (Weak and strong convergence).** Let $\rho = (t_i, r_i, p_i)_{i \in \alpha}$ be a $\alpha$TRS. $\rho$ is **weakly converging** if for every limit ordinal $\lambda \le \alpha$, $(d(t_i, t_\lambda))_{i \in \lambda}$ tends to 0. $\rho$ is **strongly converging** if it is weakly converging and if for every limit ordinal $\lambda \le \alpha$, $(\text{dph}(p_i))_{i \in \lambda}$ tends to infinity.
Example 52. Let us consider $\pi = \frac{\frac{\vdots}{\vdash \Gamma, \mu X.X}^{(\mu)} \quad \frac{\vdots}{\vdash \nu X.X, \Delta}^{(\nu)} \quad \dots}{\vdash \Gamma, \Delta}^{(\nu)}$. With

the cut-reduction system to be considered in this paper, $\pi \to^{\epsilon}_{(princ, \{\mu X.X, \nu X.X\})} \pi$, therefore there is a weakly converging reduction sequence from $\pi$ but not strongly converging reduction.

Remark 53. It is easy to see that in a strongly converging reduction sequence, there can only be finitely many reduction steps occurring at each depth; therefore every strongly converging reduction sequence is indexed by a countable ordinal.

We end this section with a property that will be essential in our construction, the compression property:

**Definition 54 (Compression property).** A *infinitary term rewriting system is said to have the compression property (or is said to be CP) when for every transfinite strongly converging reduction sequence from *s* converging to *t*, there is a strongly converging reduction sequence indexed by *ω* or a finite ordinal from *s* converging to *t*.*

**Proposition 55 (Compression Lemma [32]).** Every left-linear infinitary term rewriting system is CP.
## B Appendix on the non-wellfounded proof systems:
$\mu MALL^\infty$, $\mu LL^\infty$, $\mu LK^\infty$, $\mu LJ^\infty$.

### B.1 $\mu$-Formulas and subformulas (details on Section 2.1)

One can represent the Fischer-Ladner closure as a graph, following Example 8.

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

### B.2 Inference rules

**Definition 56 (S-sequents and inferences).** A sequent $s = \Gamma \vdash \Delta$ over a $\mu$-signature $S$ is a pair of finite lists $\Gamma, \Delta$ of $S$-formulas. (As usual, $\Gamma$ is called the antecedent and $\Delta$ the succedent.)

An inference rule $r = (s, (s_1, \dots, s_n), \text{Princ}, \alpha, l)$ is the data of

- a conclusion $S$-sequent $s$, also noted $\text{Conc}(r)$;

- a tuple of premise $S$-sequents $s_1, \dots, s_n$, also noted $\text{Prem}(r)$;

- together with an ancestor relation $\alpha \subseteq [1, \text{Card}(s)] \times \{(i, j), 1 \le i \le n, 1 \le j \le \text{Card}(s_i)\}$;

- a subset $\text{Princ} \subseteq \{1, \dots, \text{Card}(s)\}$ of cardinality at most 2, identifying the so-called principal formulas of the (conclusion of the) inference, also noted $\text{Princ}(r)$;

- and a label $l$, the rule name, also noted $\text{RName}(r)$.

We set a number of conventions that will facilitate the description and manipulation of sequent derivations.

**Convention 2** In the following, inference rules will be described, as is usual, as inference schema thanks to both formula meta-variables (ranging over $F, G, \dots$) and context meta-variables (ranging over $\Gamma, \Delta, \dots$) while the ancestor relation will be depicted as colored lines joining related formulas. When identical context meta-variables are related, we mean that the part of the ancestor relation such described relates the ith formula of the bottom context with the ith formula of the topmost context: that will allow us to avoid the very explicit description of inference rules given above, while allowing to reconstruct it at will.

**Convention 3** In the sequent calculi defined in the following, we follow the usual convention that the principal formulas of an inference are all those formulas which are explicitly spelled out in the conclusion sequent and not described via a context meta-variable.

A formula occurrence of an inference is said to be active if it is principal or if its a related to a principal formula of the inference by the ancestor relation.
**Convention 4** In general, all the considered sequent calculi will have the ex-change rule and we shall make the assumption that the set of inference rules to be closed by pre-composition and post-composition of the exchange rule. By that, we mean that we will freely use the derived rules which are obtained by adding any number of exchange rule above and below each inference, adapting the ancestry relation of course.

**Convention 5** When considering a proof system with one-sided sequents and an involutive negation $\Gamma \perp \Delta$, we shall sometimes write $\Gamma \vdash \Delta$ for sequents $\Gamma \perp \Delta$ in order to make the computational behaviour of our examples clearer. The labelling of our inferences will be unchanged (note that the index associated to formulas in a sequent remain unchanged by this operation).

## B.3 $\mu LJ^\infty$ sequent calculus

We provide details on Definition 11:

**Definition 57 ($\mu LJ^\infty$ inferences).** The inference rules of $\mu LJ^\infty$ sequent calculus, defined with respect to the $\mu$-signature $C_{\mu LJ}$, is given in Figure 8.

<figure><img src="image_13.png" /><figcaption>Fig. 8. $\mu LJ^\infty$ Inferences</figcaption></figure>

## B.4 Pre-proofs and validity (Appendix for Section 2.3)

We provide some details on Definition 12:

**Definition 58 (Pre-proofs).** Given one of the above considered $\mu$-signatures and sets of inferences, the corresponding set of pre-proofs is the set of finite and infinite trees whose nodes are labelled with inference rules and which are locally correct in the following sense: for every node $n$ of a pre-proof, the arity $n$ coincides with the number of premises of the corresponding inference and the
ith premise of n matches the conclusion sequent of the root of the ith subtree of n. Such a tree is called a pre-proof of sequent s if s is the conclusion sequent of the root of the pre-proof.

We provide more details here about the precise treatment of infinite branches and threads given in Section 2.3.

**Definition 59 (Infinite branch).** Given a pre-proof $\pi$, the set of infinite branches of $\pi$, $\infty\text{Br}(\pi)$ is defined as $\infty\text{Br}(\pi) = \{(a_i)_{i \in \omega} / \pi = \frac{\pi_1 \cdots \pi_k}{r} \text{ & } 1 \le a_0 \le k \text{ & } (a_{i+1})_{i \in \omega} \in \infty\text{Br}(\pi_{a_0})\}$.

It is useful to consider also enriched branches: $\infty\text{EBr}(\pi) = \{(a_i, r_i)_{i \in \omega} / \pi = \frac{\pi_1 \cdots \pi_k}{r} \text{ & } 1 \le a_0 \le k \text{ & } (a_{i+1}, r_{i+1})_{i \in \omega} \in \infty\text{EBr}(\pi_{a_0})\}$.

Enriched branches are convenient to define threads:

**Definition 60 (Thread).** Let $\pi$ be a pre-proof and $\beta = (a_i, r_i)_{i \in \omega} \in \infty\text{EBr}(\pi)$. We define

$$ \begin{array}{l} \infty\text{Th}(\beta) = \{(t_i)_{i \in \omega}/r_0 = (s, (s_1, \dots, s_k), p, \alpha, l), 1 \le t_0 \le \text{Card}(s) \\ \qquad \& \alpha(t_0, (a_0, t_1)) \& (t_{i+1})_{i \in \omega} \in \infty\text{Th}((a_{i+1})_{i \in \omega})\}. \end{array} $$

It is useful to consider also enriched threads:

$$ \begin{array}{l} \infty\text{ETh}((a_i, r_i)_{i \in \omega}) = \{(a_i, r_i, t_i)_{i \in \omega}/r_0 = (s, (s_1, \dots, s_k), p, \alpha, l), 1 \le t_0 \le \text{Card}(s) \\ \qquad \& \alpha(t_0, (a_0, t_1)) \& (a_{i+1}, r_{i+1}, t_{i+1})_{i \in \omega} \in \infty\text{ETh}((a_{i+1}, r_{i+1})_{i \in \omega})\}. \end{array} $$

**Definition 61 (Recurring formula).** A formula $F$ is recurring in an enriched thread $(a_i, r_i, t_i)_{i \in \omega}$ if $\{i \in \omega / \text{Conc}(r_i)(t_i) = F\}$ is infinite.

**Definition 62 (Valid thread).** A thread $\tau = (a_i, r_i, t_i)_{i \in \omega} \in \infty\text{ETh}(\beta)$ is said to be a valid thread for $\beta$ if for any $i \in \mathbb{N}$, there exists $j \ge i$ such that $t_j$ is principal in $r_j$ (and $r_j$ is not an exchange rule) and the set of recurring formulas of $\tau$ has a least elements for the subformula ordering which is $\nu$ when it occurs in the succedents of sequents or a $\mu$ if it occurs in the antecedent of sequents.

**Definition 63 (Valid pre-proof).** A pre-proof is valid if all its infinite branches have suffixes which are supported by valid threads.

## B.5 Details on the multicut rule (Definition 16)

**Definition 64 (Multicut inference rule (Expanded definition)).** The multicut inference is given by the data of

- a conclusion sequent $s$;

- non-empty tuple $(s_1, \dots, s_n)$ of premises, $n \ge 1$;

- an ancestor relation $\iota$ which is an injective map from the conclusion formulas to the premise formulas, that is from $C = [1, \text{Card}(s)]$ to $\text{Pr} = \{(j, k), 1 \le j \le n, 1 \le k \le \text{Card}(s_j)\}$, that is, for any $1 \le i \le \text{Card}(s)$ there exists a unique $(j, k) \in \text{Pr}$ such that $\iota(i, (j, k))$ and a given pair $(j, k)$ is in relation with at most one conclusion formula.

Moreover, if $\iota(i, (j, k))$, then $s(i) = s_j(k)$: the ancestor relation relates identical formulas.
## B.7 Adapting Baelde et al. $\mu$MALL$^{∞}$ cut-elimination proof to sequents as lists (Proof of Theorem 23).

We here sketch how to transfer the cut-elimination result for $\mu$MALL$^{∞}$ formulated as in Baelde et al [4,3] where sequents are sets of occurrences (ie of pairs of a formula and of an address) and the system of the present paper where sequents are ordered lists of formulas, with the exchange rule.

Let us refer to proofs with sequents as sets of occurrences as $\mu$MALL$_o^∞$, proofs with sequents as ordered lists as $\mu$MALL$_l^∞$ for clarity.

- It is straightforward to lift the $\mu$MALL$_l^∞$ proof system considered in the present paper to a proof system in which sequents are *ordered lists* of *occurrences* (following the methodology described in [4] that we do not recall here.) Call this system $\mu$MALL$_o^∞$.

- One can define two forgetful maps:

• $(\cdot)^{\text{occ}} : \mu$MALL$_o^\infty \to \mu$MALL$_l^\infty$

• $(\cdot)^{\text{list}} : \mu$MALL$_o^\infty \to \mu$MALL$_o^\infty$

that respectively erase the addresses or the ordering of the formulas (together with the exchange rules, accordingly).

- Both of those maps are validity preserving and are onto.

- It is straightforward that:

If $\pi, \pi' \in \mu$MALL$_o^\infty$ such that $\pi \xrightarrow{\mu$MALL$_o^\infty} \pi'$, then $(\pi)^{\text{occ}} \xrightarrow{\mu$MALL$_o^\infty} (\pi')^{\text{occ}}$ and if $\pi, \pi' \in \mu$MALL$_o^\infty$ such that $\pi \xrightarrow{\mu$MALL$_l^\infty} \pi'$, then either $(\pi)^{\text{list}} = (\pi')^{\text{list}}$ or $(\pi)^{\text{list}} \xrightarrow{\mu$MALL$_o^\infty} (\pi')^{\text{list}}$. (Indeed, in the case of an exchange commutation for instance, the two proofs are translated to the same proof.)

- It is straightforward as well that there exists no infinite cut-reduction sequence made of only exchange commutations.

- Now, consider some proof $\pi$ in $\mu$MALL$_l^\infty$ and consider an antecedent of $\pi$ by $(\cdot)^{\text{occ}}$ and consider a fair cut-reduction sequence $\sigma$ from $\pi$. Clearly, $\sigma$ can be lifted to a sequence $\sigma_o$ in $\mu$MALL$_o^\infty$, preserving fairness as reduction steps exactly match.

- Finally, $(\sigma_o)^{\text{list}}$ is a fair reduction sequence in $\mu$MALL$_o^\infty$, which is therefore productive and has a valid cut-free proof as a limit, from which we conclude that $\sigma_o$ and finally $\sigma$ has a cut-free and valid limit.

## B.8 Residuals

**Definition 67 (Residual).** Let $\pi$ be a $\mu$MALL pre-proof such that $\pi \xrightarrow{p_1} \pi_1$ and $\pi \xrightarrow{p_2} \pi_2$. We define the notion of residual of $(r_1, p_1)$ after $(r_2, p_2)$, written $(r_1, p_1)/(r_2, p_2)$ as follows:

- if $p_1, p_2$ are incomparable, then $(r_1, p_1)/(r_2, p_2) = \{(r_1, p_1)\}$
- if $p_1 = p_2 = p$ then $(r_1, p_1)/(r_2, p_2) =$

$$
\left\{
\begin{array}{ll}
\emptyset & \text{if } r_1 \text{ and } r_2 \text{ are the same reduction step} \\
\emptyset & \text{if } r_1 \text{ and } r_2 \text{ are both (Cut)/(Ax) key cases involving two distinct axioms which are equivalent to } \\
& \text{the } \emptyset \text{ reduction step} \\
\{(r_1, p_1)\} & \text{if } r_2 \text{ is a principal reduction} \\
\{(r_1, p_1 \cdot 1), (r_1, p_1 \cdot 2)\} & \text{if } r_2 \text{ is a (\&) commutation} \\
\{(r_1, p_1 \cdot 0)\} & \text{if } r_2 \text{ is a } (\oplus), (\ominus) \text{ or } (\sigma) \text{ commutation} \\
\{(r_1, p_1 \cdot 1)\} & \text{if } r_2 = (\text{ext}, (\otimes)) \text{ and } r_1 \text{ is cut-connected to the } \otimes \text{ left context} \\
\{(r_1, p_1 \cdot 2)\} & \text{if } r_2 = (\text{ext}, (\otimes)) \text{ and } r_1 \text{ is cut-connected to the } \otimes \text{ right context}
\end{array}
\right.
$$

## B.9 Details on the compression of $\mu$MALL$^\infty$ cut-reduction sequence: Proof of Proposition 26

The following lemma is a trivial observation:

**Lemma 68 (Cut-reductions at incomparable positions commute).** Let $\pi$ a $\mu$MALL$^\infty$ pre-proof such that $\pi \to_{r_1}^{p_1} \pi_1$, $\pi \to_{r_2}^{p_2} \pi_2$ with $p_1, p_2$ incomparable. Then there exists $\pi_3$ such that $\pi_1 \to_{r_2}^{p_2} \pi_3$ and $\pi_2 \to_{r_1}^{p_1} \pi_3$.

**Lemma 69.** Let $\sigma = (\pi_i, r_i, p_i)_{i \in \omega+1}$ be a strongly converging $\mu$MALL$^\infty$ cut-reduction sequence, with $\pi_\omega \to_{r_\omega}^{p_\omega} \pi_{\omega+1}$. There exists a strongly converging $\mu$MALL$^\infty$ cut-reduction sequence $\text{Comp}(\sigma) = (\pi'_i, r'_i, p'_i)_{i \in \omega}$ which converges to $\pi_{\omega+1}$. More precisely, there exists some $j$ such that

- for any $i < j$, $(\pi'_i, r'_i, p'_i) = (\pi_i, r_i, p_i)$

- $r'_j = r_\omega, p'_j = p_\omega$

- and $r'_{i+1} = r_i, p'_{i+1} = p_i$ for any $i \ge j$ and

- $\text{Comp}(\sigma)$ strongly converges to $\pi_{\omega+1}$

*Proof.* The lemma is a direct consequence of Lemma 68 since, by strong convergence, there exists some $j$ such that for any $i \ge j$, $p_i$ is longer than $p_\omega$, therefore the reduction $r_\omega$ occurring at $p_\omega$ in $\pi_\omega$ can already be performed in $\pi_j$ since the root of the subproof at $p_\omega$ will never be modified in $(\pi_i, r_i, p_i)_{j \le i \in \omega}$, therefore there must be a multicut at $p_\omega$ in $\pi_i$ for every $j \le i \in \omega$ and since this is there is at most one multicut per branch, all $p_i$ for $j \le i \in \omega$ are incomparable with $p_\omega$.

We can now prove that $\mu$MALL$^\infty$ cut-reduction is CP:

**Proposition 70 (Compression lemma).** Let $\sigma = (\pi_i, r_i, p_i)_{i \in \alpha}$ be a strongly converging $\mu$MALL$^\infty$ transfinite cut-reduction sequence. There exists a $\mu$MALL$^\infty$ cut-reduction sequence $\text{Comp}(\sigma) = (\pi'_i, r'_i, p'_i)_{i \in \beta}$ which is a reordering of $\sigma$, depth-increasing, strongly converging with the same limit as $\sigma$ and such that if $\alpha$ is finite, then $\beta = \alpha$ and $\beta = \omega$ otherwise.

*Proof.* By transfinite induction on the length of the reduction $\sigma$ that we want to compress and make depth-increasing.
- If $\alpha$ is a successor ordinal $\alpha = \lambda+1$, the property follows directly from Lemma 68: applying induction hypothesis to the prefix of length $\lambda$ results in a reduction $\sigma' = (\pi'_i, r'_i, p'_i)_{i \in \beta'}$ which is depth-increasing and such that every redex fired in the prefix of $\sigma$ of length $\lambda$ is still present. In particular, $\sigma'$ strongly converges to $\pi_\alpha$.

$\sigma'$ being depth-increasing, there exists some $j$ such that for any $i < j$, $\mathrm{dpth}(p'_i) \le \mathrm{dpth}(p_\alpha)$ and for any $j \le i \in \beta'$, $\mathrm{dpth}(p'_i) > \mathrm{dpth}(p_\alpha)$, therefore the reduction $r_\alpha$ occurring at $p_\alpha$ in $\pi_\alpha$ can already be performed in $\pi'_j$ since the root of the subproof at $p_\alpha$ will never be modified in $(\pi'_i, r'_i, p'_i)_{j \le i \in \beta'}$, therefore there must be a multicut at $p_\alpha$ in $\pi'_i$ for every $j \le i \in \beta'$. Since there is at most one multicut per branch, all $p'_i$ for $j \le i \in \beta'$ are incomparable with $p_\alpha$. In particular, $\pi'_j \xrightarrow{r_\alpha} \pi''_j$ and for any $j \le i \in \beta' \pi''_i \xrightarrow{r'_i} \pi''_{i+1}$ by using the commutation property.

In particular $\sigma'' = (\pi''_i, r''_i, p''_i)_{j \le i \in \beta'}$ strongly converges to $\pi_{\alpha+1}$. Considering the reduction sequence $(\pi'_i, r'_i, p'_i)_{i<j} \cdot (\pi'_j, p_\alpha, r_\alpha) \cdot \sigma''$ one gets a depth-increasing reduction sequence indexed by $\beta = 1 + \beta'$ (due to the additional reduction step $(\pi'_j, p_\alpha, r_\alpha)$ inserted in the reduction sequence) with such that every redex of $\sigma$ is still present. Finally, notice that $\alpha$ was a finite ordinal, $\beta = 1 + \beta' = 1 + \lambda = \lambda + 1 = \alpha$ as expected and if $\alpha$ is infinite, $\beta' = \omega$ and $\beta = 1 + \omega = \omega$.

- If $\alpha$ is a limit ordinal.

Let us first observe the following fact: if $d$ is the minimal depth of a reduction step in $\sigma$, by strong convergence, there is a finite number $n_d$ of reduction steps of $\sigma$ at depth $d$ and there is an ordinal $\alpha' < \alpha$ such that for any $\alpha' \in i \in \alpha$, $\mathrm{dpth}(p_i) > d$. By applying the transfinite induction hypothesis to $\sigma_{\alpha'} = (\pi_j, r_j, p_j)_{j \in \alpha'}$, one gets a depth-increasing reduction sequence $\sigma'_{\beta'} = (\pi'_i, r'_i, p'_i)_{i \in \beta'}$ with the same limit and containing the same reduction steps as $\sigma_{\alpha'}$ and which is indexed by $\min(\alpha', \omega)$. In particular, $\sigma'_{\beta'} = \sigma'_d \cdot \sigma''_d$ with all reduction steps in $\sigma'_d$ being at depth $d$ and all reduction steps in $\sigma''_d$ being at depth at least $d+1$. Therefore $\sigma''_d \cdot (\pi_i, r_i, p_i)_{\alpha' \in i \in \alpha}$ is a strongly converging sequence of length at most $\alpha$ and having all its reduction steps at depth at least $d+1$. Then one builds by induction on $i \in \omega$, $(k_i, \sigma_i, \sigma'_i)_{i \in \omega}$ such that:

1. for any $i \in \omega$, $\sigma_i = (\pi_j^i, r_j^i, p_j^i)_{j \in \alpha_i}$ with $\alpha_i \le \alpha$ and for any $j \in \alpha_i$, $\mathrm{dpth}(p_j^i) \ge i$;

2. for any $i \in \omega$, $k_i \le k_{i+1}$, $\sigma'_i = (\pi'_j, r'_j, p'_j)_{k_i \le j < k_{i+1}}$ and if $k_i \le j < k_{i+1}$, $\mathrm{dpth}(p'_j) = i$;

3. for any $i \in \omega$, $(\pi'_j, r'_j, p'_j)_{j < k_i} \cdot \sigma_i$ is a strongly converging $\mu$MALL$^\infty$ cut reduction sequence that contains the same reduction steps as $\sigma$ up to reordering.

**Initialization.** We set $\sigma_0 = \sigma$ and $k_0 = 0$. By the above observation with $d=0$, we get an $\alpha'_0 \le \alpha$ we build $\sigma'_0$, we set $k_1 = k_0 + n_0$ and set $\sigma_1 = \sigma''_0 \cdot (\pi_j^0, r_j^0, p_j^0)_{\alpha'_0 \in j \in \alpha}$. Conditions 1–3 are satisfied for $i=0$.

**Heredity.** Assuming $(k_i)_{i \le l}$, $(\sigma_i)_{i \le l}$, $(\sigma'_i)_{i < l}$ are built, satisfying the conditions, one proceeds as above taking $\sigma_l$ for $\sigma$ and $l+1$ for $d$ and setting $k_{l+1} = k_l + n_l$ and $\sigma'_l$ being provided as before and $\sigma_{l+1}$ as the concatenation of $\sigma''_l$ and $(\pi'_j, r'_j, p'_j)_{\alpha'_i \in i \in \alpha_i}$, satisfying the required conditions.
Finally, we set $\sigma' = (\pi'_j, r'_j, p'_j)_{j \in \omega}$ which is trivially depth increasing, strongly converging, and which is a reordering of the reduction steps of $\sigma$: any reduction step of $\sigma'$ comes from a reduction in $\sigma$ and for any reduction step $(r_i, p_i)$ in $\sigma$, it occurs by construction in $\sigma'_{\text{depth}(p_i)}$ and therefore in $\sigma'$.
# C Appendix on Section 3

## C.1 Details on $\mu LL^\infty$ cut-reduction rules

We detail the rules of $\mu LL^\infty$ cut elimination.

**Definition 71.** *Cut commutations or External reductions are defined in fig. 11.*

**Definition 72.** *Key cut-reductions, or internal reductions, are the principal reductions given in fig. 12 together with the following two reductions:*

- the merge $(\text{mcut})/(\text{Cut})$ reduction

$$ \frac{\begin{array}{c} \vdash \Delta, F \quad \vdash \Gamma, F^{\perp} \\ \mathcal{C} \quad \begin{array}{c} \vdash \Delta, \Gamma \\ \vdash \Sigma \end{array} \end{array} \quad \begin{array}{c} \text{(Cut)} \\ \text{mcut}(\iota, \perp) \end{array} \quad \begin{array}{c} \longrightarrow \\ r \end{array} \quad \frac{\begin{array}{c} \mathcal{C} \quad \begin{array}{c} \vdash \Delta, F \\ \vdash \Sigma \end{array} \end{array} \quad \begin{array}{c} \text{mcut}(\iota, \perp') \end{array} $$

where $\perp'$ extends $\perp$ with $F \perp' F^{\perp}$ and $r = (\text{merge}, \{F, F^{\perp}\})$.

- the axiom reduction $(\text{mcut})/(\text{Ax})$ defined as follows, with $F, F'$ and $F''$ being three occurrences of the same formula, that we distinguish with primes instead of explicitly describing their positions in sequents.

$$ \frac{\begin{array}{c} \mathcal{C} \quad \begin{array}{c} \vdash F, F' \perp \\ \vdash \Sigma \end{array} \end{array} \quad \begin{array}{c} \text{(Ax)} \\ \text{mcut}(\iota, \perp) \end{array} \quad \begin{array}{c} \longrightarrow \\ r \end{array} \quad \frac{\begin{array}{c} \mathcal{C} \quad \begin{array}{c} \vdash F'', \Gamma \\ \vdash \Sigma \end{array} \end{array} \quad \begin{array}{c} \text{mcut}(\iota', \perp') \end{array} $$

where $r = (\text{CutAx}, \{F, F'^{\perp}\})$, $F'^{\perp} \perp F''$ and $\iota', \perp'$ are defined as follows:

* for all $G \in \Sigma$, if $\iota(G) = F$ then $\iota'(G) = F''$, otherwise $\iota'(G) = \iota(G)$;

* $\perp' = \perp \cup \{\{F'', G\} | \{F, G\} \in \perp\}$.

## C.2 Proof of Proposition 33

**Proposition 73 (Preservation of validity).** $\pi$ is a valid $\mu LL^\infty$ proof of $\vdash \Gamma$ iff $\pi^\bullet$ is a valid $\mu MALL^\infty$ proof of $\vdash \Gamma^\bullet$.

*Proof.* It is simply a matter of relating the infinite branches in both pre-proofs: Since every infinite branch in $\pi$ gives rise to at least an infinite branch of $\pi^\bullet$, validity of $\pi^\bullet$ entails that of $\pi$. Conversely, let us prove that all infinite branches of $\pi^\bullet$ are valid. Let us consider three types of infinite branches:

- Let us consider an infinite branch $\beta$ of $\pi^\bullet$ such that a suffix of $\beta$ loops around the backedges of the encoding of some promotion introducing $!F$ in $\pi$. In that case $\beta$ is valid as it is inhabited by a thread having as least recurring formula $(!F)^\bullet$ (indeed, in such a case, the only recurring formulas of the thread are $(!F)^\bullet, F^\bullet \&(1\&( (!F)^\bullet \otimes (!F)^\bullet)), 1\&( (!F)^\bullet \otimes (!F)^\bullet)$ and $(!F)^\bullet \otimes (!F)^\bullet$)
<figure><img src="image_14.png" /></figure>

In the promotion commutation case, all premises in $C^!$ are assumed to end with promotion rules.

In all the above rules, one requires that $\iota'$ and $\iota''$ are the ancestry relation induced by $\iota$ after the possible modification of the premises when taking restrictions of the premises as in the $\otimes$ commutation and relate the subformulas of the commuted formula occurrence that are not in the premise and conclusion of the multicut. (For instance, for the contraction commutation, each occurrence of $?F$ is related to the occurrence in the corresponding position in the premise.)

**Fig. 11.** External reduction rules, where $r = (\text{ext}, F)$ and $F$ is the principal occurrence.
$$ \frac{C \quad \frac{\vdash F, \Gamma}{\vdash?F, \Gamma} \quad \frac{\vdash F^{\perp}, ?\Delta}{\vdash!F^{\perp}, ?\Delta} \quad \frac{(\mathbf{!p})}{\mathrm{mcut}(\iota, \perp)} \quad \xrightarrow{r} \quad \frac{C \quad \vdash F, \Gamma \quad \vdash F^{\perp}, ?\Delta}{\vdash \Sigma} \quad \mathrm{mcut}(\iota, \perp') }{\vdash \Sigma} $$

where $?F \perp! F^{\perp}$ and $\perp'$ coincides with $\perp$ except for $F \perp' F^{\perp}$.

$$ \frac{C_{\Gamma} \quad \frac{\vdash?F, ?F, \Gamma}{\vdash?F, \Gamma} \quad \frac{(\mathbf{?c})}{\mathrm{mcut}(\iota, \perp)} \quad \xrightarrow{r} \quad \frac{C_{\Gamma} \quad C_{?F}^{\perp} \quad C_{?F}^{\perp} \quad \vdash?F, ?F, \Gamma}{\vdash \Gamma', ?\Sigma, ?\Sigma} \quad \mathrm{mcut}(\iota', \perp') }{\vdash \Gamma', ?\Sigma} $$

where $C_{?F}^{\perp} \neq \emptyset$, $\perp'$ corresponds to $\perp$ on $C_{\Gamma}$ and is a "duplication" of $\perp$ on $C_{?F}^{\perp}$ and each copy of $?F$ is in $\perp'$-relation with the corresponding copy of $!F^{\perp}$ in $C_{?F}^{\perp}$.

$$ \frac{C_{\Gamma} \quad \frac{\vdash \Gamma}{\vdash?F, \Gamma} \quad \frac{(\mathbf{?w})}{\mathrm{mcut}(\iota, \perp)} \quad \xrightarrow{r} \quad \frac{C_{\Gamma} \quad \vdash \Gamma}{\vdash \Gamma'} \quad \frac{\mathrm{mcut}(\iota', \perp')}{(\mathbf{?w})^{*}}}{\vdash \Gamma', ?\Sigma} $$

where $C_{?F}^{\perp} \neq \emptyset$ and $\perp'$ corresponds to the restriction of $\perp$ on $C_{\Gamma}, \Gamma$.

$$ \frac{C \quad \frac{\vdash \Delta, F \quad \vdash \Gamma, G}{\vdash \Delta, \Gamma, F \otimes G} \quad (\otimes) \quad \frac{\vdash \Theta, F^{\perp}, G^{\perp}}{\vdash \Theta, F^{\perp} \otimes G^{\perp}} \quad (\otimes) \quad \xrightarrow{r} \quad \frac{C \quad \vdash \Delta, F \quad \vdash \Gamma, G \quad \vdash \Theta, F^{\perp}, G^{\perp}}{\vdash \Sigma} \quad \mathrm{mcut}(\iota, \perp') }{\vdash \Sigma} $$

where $F \otimes G \perp F^{\perp} \otimes G^{\perp}$ and $\perp'$ coincides with $\perp$ except for $F \perp' F^{\perp}$ and $G \perp' G^{\perp}$.

$$ \frac{C \quad \frac{\vdash \Delta, F_1 \quad \vdash \Delta, F_2}{\vdash \Delta, F_1 \& F_2} \quad (\&) \quad \frac{\vdash \Gamma, F_i^{\perp}}{\vdash \Gamma, F_1^{\perp} \oplus F_2^{\perp}} \quad (\oplus) \quad \xrightarrow{r} \quad \frac{C \quad \vdash \Delta, F_i \quad \vdash \Gamma, F_i^{\perp}}{\vdash \Sigma} \quad \mathrm{mcut}(\iota, \perp') }{\vdash \Sigma} $$

If $\{F_1 \& F_2, F_1^{\perp} \oplus F_2^{\perp}\} \in \perp'$, where: $\perp' \triangleq \perp \cup \{\{F_i, F_i^{\perp}\}\}$.

$$ \frac{C \quad \frac{\vdash \Delta, F[\mu X.F/X]}{\vdash \Delta, \mu X.F} \quad (\mu) \quad \frac{\vdash \Gamma, F^{\perp}[\nu X.F^{\perp}/X]}{\vdash \Gamma, \nu X.F^{\perp}} \quad (\nu) \quad \xrightarrow{r} \quad \frac{C \quad \vdash \Delta, F[\mu X.F/X] \quad \vdash \Gamma, F^{\perp}[\nu X.F^{\perp}/X]}{\vdash \Sigma} \quad \mathrm{mcut}(\iota, \perp) }{\vdash \Sigma} $$

where $\mu X.F \perp \nu X.F^{\perp}$ and $\perp'$ coincides with $\perp$ except for $F[\mu X.F/X] \perp' F^{\perp}[\nu X.F^{\perp}/X]$.

$$ \frac{C \quad \frac{\vdash \Gamma}{\vdash \Gamma, \perp} \quad (\perp) \quad \xrightarrow{r} \quad \frac{(1)}{\mathrm{mcut}(\iota, \perp)} }{\Sigma} $$

**Fig. 12.** Principal reductions, where $r = (\mathrm{princ}, \{F, F'^{\perp}\})$ with $\{F, F'^{\perp}\}$ the principal occurrences that have been reduced for the $\mu$MALL rules and $r \in \{(\mathrm{princ}, \{F, F'^{\perp}\}, (\mathbf{?d})), (\mathrm{princ}, \{F, F'^{\perp}\}, (\mathbf{?c})), (\mathrm{princ}, \{F, F'^{\perp}\}, (\mathbf{?w}))\}$ for the exponential case.

In the principal reduction involving contraction and weakening, the restrictions $C_{?\Delta}$ are required to contain only proofs ending with a promotion rule.
- Otherwise, let us first consider the special case of an infinite branch that, each time it enters the encoding of a promotion, takes the left-most premise of the `&` rule. To such an infinite branch it is easy to associate an infinite branch `b` of $\pi$ which is valid, therefore supported by a thread the least formula of which is some $\nu X.F$. Then one observes that $(\nu X.F)^\bullet$ is recurring in $\beta$ as is the least such formula: $\beta$ is valid.

- In the last case, on each promotion, one shall first backedge a finite number of times on the backedges of the promotion before moving towards the encoding of the premise of the promotion. Note that during those loop phases, the subformulas of the context $(?\Delta)^\bullet$ are preserved as well as $F^\bullet$. This allows to find, as in the previous case, a $\nu$-formula that is the lest recurring formula along some thread.

### C.3 Simulation of $\mu LL^\infty$ cut-reduction: proof of Proposition 34

**Proposition 74 (Simulation of $\mu LL^\infty$ cut-elimination steps).** Each $\mu LL^\infty$ $mcut$-reduction $r$ can be simulated in $\mu MALL^\infty$ by a (possibly infinite) sequence of $mcut$-reductions, denoted $r^\bullet$.

*Proof.* We first assume that the position of the reduction is not above some `(!p)` rule. In that case, the simulation of $\mu MALL^\infty$ reduction rules is trivial.

The simulation of exponential cut-reductions are shown in Figures 13 & 14 in the simplified case of cuts. The simulation for the general $mcut$ case can easily be inferred: it does not modify the length of the simulated sequence for commutation rules nor in the `(?d)/(!p)` key reduction, while the simulation of contraction and weakening key reductions shall be adapted to take into account the length of the `(!p)-ready` context of the $mcut$ rule.

In the case the position of the reduction step is above a certain number of `(!p)`, the redex is in fact encoded as an infinity of redexes, which induce, in each case, a simulation of length $\omega$ done as a depth-increasing reduction, which is always possible.

### C.4 Proof of Proposition 36

**Proposition 75 (Non-preservation of fairness by simulation).** There exists a $\mu LL^\infty$ (pre-)proof $\pi$ and a fair reduction $\rho$ from $\pi$ such that $\rho^\bullet$ is an $\omega$-indexed $\mu MALL^\infty$ cut-reduction sequence from $\pi^\bullet$ which is not fair.

*Proof.* Consider pre-proofs $\pi_k, k \in \omega$:

$$ \pi_k = \frac{\frac{\vdots \quad (\nu) \quad \vdots}{\vdash \mu Y.Y \quad (\nu) \quad (\nu) \quad (\nu) \quad (\nu)} \quad (\nu) \quad (\nu) \quad (\nu) \quad (\nu)}{\frac{\vdots \quad (\nu) \quad (\nu) \quad (\nu)}{\vdash \mu X.X, \nu Y.Y \quad (\nu) \quad (\nu) \quad (\nu) \quad (\nu)} \quad (\nu) \quad (\nu) \quad (\nu) \quad (\nu)} \quad (\sigma) \quad \frac{\vdots \quad (\sigma)}{\vdash \mu B^\perp, \sigma Z.Z \quad (\sigma) \quad (\sigma)} \quad mcut(i, \perp) $$
<figure><img src="image_15.png" /><figcaption>Fig. 13. Simulation of $\mu LL^{\infty}$ (m)cut-commutation rules</figcaption></figure>

The mcut-reduction sequence $\rho = (\pi_i, r_i, p_i)_{i \in \omega}$ consisting in commuting $(\sigma)$ inferences below the multicut at each step is fair, since the $(?w)$ and $(!p)$ rules never constitute a reducible key-step as the context is not ready.

On the other hand, in the simulation $\pi_0^\bullet$ of $\pi_0$ there is a $(\mu)/(\nu)$ key-step that is reducible in each $\pi_i^\bullet$ but that is never performed: $\rho^\bullet$ is not fair.

Note that the proposition holds both for valid and invalid pre-proof as choosing $\sigma$ to be $\mu$ or $\nu$ in the above example covers both situations.

## C.5 Proofs of Section 3.4

### Proof of Lemma 37

**Lemma 76.** Let $\pi$ be a $\mu LL^{\infty}$-proof of $\vdash \Gamma$ and let us consider a fair cut-reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ in $\mu LL^{\infty}$ initiated with $\pi$. $\sigma$ converges to a cut-free $\mu LL^{\infty}$-preproof of $\vdash \Gamma$.

*Proof.* Let $\pi$ be a $\mu LL^{\infty}$-proof of $\vdash \Gamma$ and let us consider a fair cut-reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ in $\mu LL^{\infty}$ initiated with $\pi$. We want to prove that $\sigma$ has a limit, say $\pi'$, and that this limit is a cut-free $\mu LL^{\infty}$-preproof of $\vdash \Gamma$.

Consider the associated (potentially transfinite) $\mu MALL^{\infty}$ cut-reduction sequence $\sigma^\bullet$ initiated in $\pi^\bullet \vdash \Gamma^\bullet$ obtained by simulating each cut-reduction step of $\sigma$.

Reasoning by contradiction, assume that $\sigma$ does not converge to a cut-free pre-proof, that means that there exists a position $p$ and an integer $k$ such that for any $i$ larger than $k$, the subproof of $\pi_i$ rooted at $p$, denoted as $\pi_i@p$, is concluded with a cut inference.
<figure><img src="image_16.png" /><figcaption>Fig. 14. Simulation of $\mu LL^\infty$ key-(m)cut rules</figcaption></figure>

By the fairness assumption, that implies that there is a suffix $\tau$ of $\sigma$ (in fact $(\pi_i, r_i, p_i)_{i \ge k}$) containing infinitely many cut-reduction steps occurring at the root of the subproof of $\pi_i$ rooted in $p$ $(\pi_i @ p)$, for $i \ge k$. We want to view $\tau^p = (\pi_i @ p)_{i \ge k}$ as a reduction sequence. As such, this is not a $\mu LL^\infty$ cut-reduction sequence as there are steps of $\tau$ reducing outside of the $\pi_i @ p$: in that case, $\pi_i @ p = \pi_{i+1} @ p$.

Let $I = \{i \ge k \mid p_i = p\}$ and let $\kappa$ be an enumeration of the infinite set $I$. Since for any $j \ge k$ such that $j \notin I$, $\pi_j @ p = \pi_{j+1} @ p$, the sequence $\rho = (\pi_{\kappa(i)} @ p, r_{\kappa(i)}, \epsilon)_{i \in \omega}$ is a cut-reduction sequence which is a fair $\mu LL^\infty$ cut-reduction sequence and which consists only of key-cut-reduction such that the multicuts remain at the root.

Consider the $\mu MALL^\infty$ encoding of $\rho$, $\rho^\bullet$. One can first remark that it is an $\omega$-indexed sequence since no reduction occurs above a promotion in $\rho$ and since there is no commutation rule. $\rho^\bullet$ is therefore unproductive, from which we want to draw a contradiction with $\mu MALL^\infty$ cut-elimination theorem.

Is $\rho^\bullet$ a fair reduction sequence? Proposition 36 shows that it is not necessarily the case: there may be available reduction steps which are not fired along $\rho^\bullet$ (in fact they can only be $(\mu)/(\nu)$, $(\oplus)/(\&)$) key cases as they come only from the condition on the application of key cases for weakening and contraction) and which have residual along the whole sequence $\rho^\bullet$. Let $\sigma$ be a reduction obtained from $\rho^\bullet$ by firing those redexes causing the lack of fairness of $\rho^\bullet$: it is easy to notice that $\sigma$ is fair. But remark that $\sigma$ contains exactly the same commutation rules as $\rho^\bullet$, that is none, contradicting $\mu MALL^\infty$ cut-elimination theorem.

## Proof of Lemma 38
**Lemma 77.** Let $\pi$ be a $\mu LL^\infty$ pre-proof of $\vdash \Gamma$ and let us consider a cut-reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ in $\mu LL^\infty$ initiated with $\pi$ that converges to a cut-free $\mu LL^\infty$ pre-proof $\pi'$. $\sigma^\bullet$ is a strongly converging (possibly transfinite) sequence.

*Proof.* Let $\lambda$ be the indexing ordinal of $\sigma^\bullet$: $\sigma^\bullet = (\pi'_i)_{i \in \lambda}$. We want to prove that $\sigma^\bullet$ is strongly converging. This comes from two facts:

- first, because $\pi'^\bullet$ - the encoding of the limit of $\sigma$ - is cut-free, the depth of the redexes tend to infinity when tending to the limit ordinal $\lambda$ indexing $\sigma^\bullet$ as $\sigma$ is itself strongly converging.

- Second, because only !-commutations as well as reductions above a promotion can create infinite reduction sequence. Let $\lambda'$ be a limit ordinal strictly below $\lambda$: the depths of the cuts reduced in $\pi'_i$ tend to infinity as $i$ tends to $\lambda'$ as it corresponds either to the simulation of a ! commutation, which is strongly converging or to a reduction in an exponential box, which is also simulated by a strongly converging sequence.

**Details on the cut-elimination proof, page 14**

**Theorem 78.** Fair $\mu LL^\infty$ $mcut$-reduction sequences converge to cut-free $\mu LL^\infty$ proofs.

*Proof.* Let $\pi$ be a $\mu LL^\infty$-proof of $\vdash \Gamma$ and let us consider a fair cut-reduction sequence $\sigma = (\pi_i, r_i, p_i)_{i \in \omega}$ in $\mu LL^\infty$ initiated with $\pi$. We want to prove that $\sigma$ has a limit, say $\pi'$, which is a cut-free $\mu LL^\infty$-proof of $\vdash \Gamma$.

Consider the associated (potentially transfinite) $\mu MALL^\infty$ cut-reduction sequence $\sigma^\bullet$ initiated in $\pi^\bullet \vdash \Gamma^\bullet$ obtained by simulating each cut-reduction step of $\sigma$. By Lemma 37, we know that $\sigma$ converges to a cut-free $\mu LL^\infty$ pre-proof. From this, one can conclude that $\sigma$ is productive and therefore that $\sigma$ *strongly converges* to some $\mu LL^\infty$ cut-free pre-proof $\pi'$.

We are left with proving that the limit of $\sigma, \pi'$, is actually valid. By Lemma 38, $\sigma^\bullet$ is a *transfinite* cut-reduction sequence from $\pi^\bullet$ which *strongly converges* to $\pi'^\bullet$. Therefore, the Compression Lemma applies to $\pi'^\bullet$: there exists $\rho = (\pi'_i, r'_i, p'_i)_{i \in \omega}$ an $\omega$-indexed $\mu MALL^\infty$ cut-reduction sequence converging to $\pi'^\bullet$.

In order to apply $\mu MALL^\infty$ cut-elimination theorem, we would need to ensure that $\rho$ is fair, from which validity of $\pi'^\bullet$ would follow and that of $\pi'$ by Proposition 33. However, we know by Proposition 36 that it is not necessary the case. We can still conclude by considering what happens when $\rho$ is made fair (in a reduction sequence called $\rho_f$). By remark 35, we know that the loss of fairness of $\rho$ can only have one reason: the lack of (!p)-readiness, in a multicut $mcut(\iota, \perp)$, of the cut-context associated to the context of a (!p) rule the principal formula of which (i) either is $\iota$-related to a formula in the conclusion of the (mcut), therefore blocking a (!p) commutation rule, or (ii) is $\perp$-related with a ?F which is conclusion of a (?w) or of a (?c) rule, therefore blocking a key cut-reduction step of type (?w)/(!p) or (?c)/(!p). Indeed, in those two cases, the $\mu MALL^\infty$-encoding of the proof can perform partially the simulation of the reduction that is blocked.
We shall analyze more precisely what happen in this case to prove that to any infinite branch $\beta$ of $\pi'^{\bullet}$, one can associate an infinite branch $\beta_f$ of the limit, say $\pi_f$, of $\rho_f$ ($\rho_f$ being fair by assumption, it has a limit which is valid) containing the same infinite threads as $\beta$.

Before proceeding, let us notice that the content of remark 35 does not entail that the only reduction steps added to $\rho$ in order to obtain $\rho_f$ are the partial reduction of (the simulation of) the blocked reductions. Indeed, let us consider the case of a blocked (!p)-commutation:

$$ \frac{!(\pi)}{\vdash!F, ?\Gamma \quad (!p)} \quad C_{?\Gamma} \quad \text{with } !\!(\pi) = \frac{\pi}{\vdash!F, ?\Gamma} \quad (!p), \text{ assuming that } C_{?\Gamma} \text{ is not } (!p)-\text{ready.} $$

The $\mu$MALL$^\infty$ encoding of the above proof is: $\frac{!^{\bullet}(\pi^{\bullet})}{\vdash !^{\bullet}F^{\bullet}, ?^{\bullet}\Gamma^{\bullet}} \quad (C_{?\Gamma})^{\bullet}} \quad \text{mcut}(\iota, \perp)$

and since $!^{\bullet}(\pi^{\bullet})$ is concluded with ($\&$) and ($\nu$) rules on $!^{\bullet}F^{\bullet}$, the corresponding commutation step can be performed (and will be performed in a fair reduction) resulting in

$$ \frac{C_{?\Gamma}^{\bullet} \quad \pi^{\bullet}}{\vdash F^{\bullet}, \Sigma^{\bullet}} \quad \text{mcut}(\iota, \perp) \quad \frac{C_{?\Gamma}^{\bullet} \quad \overline{\vdash 1}^{(1)} \quad (!w)^{\bullet+}}{\vdash 1, \Sigma^{\bullet}} \quad \text{mcut}(\iota, \perp) \quad \frac{C_{?\Gamma}^{\bullet} \quad \frac{!^{\bullet}(\pi^{\bullet}) \quad !^{\bullet}(\pi^{\bullet})}{\vdash!F^{\bullet} \otimes!F^{\bullet}, ?\Gamma^{\bullet}, ?\Gamma^{\bullet}} \quad (!c)^{\bullet+}}{\vdash!F^{\bullet} \otimes!F^{\bullet}, ?\Gamma^{\bullet}} \quad \text{mcut}(\iota, \perp) \quad \frac{\vdash!F^{\bullet} \otimes!F^{\bullet}, \Sigma^{\bullet}}{\vdash!F^{\bullet}, \Sigma^{\bullet}} \quad (!) \quad (\&) \quad (\&)} $$

In the left-most premise, the subproof $\pi^{\bullet}$ is cut with $C_{?\Gamma}^{\bullet}$ which could unlock productive new reduction steps.

On the other hand, considering the middle premise, one notices that this cannot happen as the (1) inference is guarded by at least one (encoding of) weakening (since $\Gamma$ is non-empty, otherwise $C_{?\Gamma}$ is (!p)-ready) which will not interact with some premise of $C_{?\Gamma}^{\bullet}$ by non-readiness.

Similarly, analyzing the cases of blocked key cut-steps of type $(?w)/(!p)$ or $(?c)/(!p)$, one realizes that $\rho_f$ could contain some additional $(\mu)/(\nu)$, $(\oplus^2)/(\&)$, $(\oplus^1)/(\&)$ steps or some additional $(\mu)/(\nu)$, $(\oplus^2)/(\&)$, $(\oplus^2)/(\&)$ steps respectively. In particular, the (encoding of the) premise of the blocked structural rule cannot produce part of the cut-free proof $\pi_f$ as they are blocked respectively by $(?w)^{\bullet}$ and by $(?c)^{\bullet}$ respectively.

This remark is the key to conclude the proof: indeed, let $\beta$ be an infinite branch of $\pi'^{\bullet}$ and let us consider $\rho_f$ a fair reduction sequence obtained from $\rho$ by reducing those redexes which have residuals along the whole of $\rho$ causing the lack of fairness of $\rho$ (and doing that hereditarily) and let us consider the limit $\pi_f$ of this sequence.

The above analysis of the blocking situations allows us to define a branch $\beta_f$ of $\pi_f$ as follows: $\beta_f$ agrees with $\beta$ as long as possible. When the next inference in $\pi_f$ differ from that of $\beta$, that means that it comes from the commutations of inferences used in the simulation of a (!p) which is blocked.
In that case one requires $\beta_f$ to follow the unique premise of the ($\nu$) rule, the second premise of the ($\&$) rule and finally the first premise of the following ($\&$) rule, ending in sequent $\vdash 1, ?\Delta$ as described below:

$$ \frac{\frac{\frac{\frac{\vdash 1, ?\Delta\bullet}{\vdash F\bullet, ?\Delta\bullet} \quad \vdash (!F)^{\bullet} \otimes (!F)^{\bullet}, ?\Delta\bullet} {\vdash 1 \& ((!F)^{\bullet} \otimes (!F)^{\bullet}), ?\Delta\bullet} \quad (\&)} {\vdash F\bullet \& (1 \& ((!F)^{\bullet} \otimes (!F)^{\bullet})), ?\Delta\bullet} \quad (\&)} {\vdash (!F)^{\bullet}, ?\Delta\bullet} \quad (\nu) $$

and we follow back the branch according to $\beta$ as before.

It is easy to notice that in $\beta_f$ we have exactly the same (infinite) threads as in $\beta$ (some finite thread may possibly have been extended *finitely* on occurrences of $(!F)^{\bullet}$): indeed, the only inferences on which $\beta_f$ differs from $\beta$ are of the type pictured in green above and therefore end in a 1 formula. Therefore $\beta$ is valid if, and only if, $\beta_f$ is valid, which is the case since $\rho_f$ is fair.

We can then conclude that $\pi'^{\bullet}$ is cut-free and valid and, using preservation of validity, that $\pi'$ is a valid cut-free $\mu LL^{\infty}$-proof.

## Proof of Corollary 39

**Corollary 79.** Fair two-sided $\mu LL^{\infty}$ cut-reduction sequences converge to cut-free two-sided $\mu LL^{\infty}$ proofs.

*Proof.* A fair reduction sequence in two-sided $\mu LL^{\infty}$ can easily be seen to map to a fair reduction sequence in one-sided $\mu LL^{\infty}$ from which the result follows.

A two-sided sequent $\Gamma \vdash \Delta$ is mapped to $\vdash \Gamma^{\perp}, \Delta$ with $A \dashv B$ interpreted as $A^{\perp} \bowtie B$. Each right rule is mapped to the same rule and each left rule is mapped to the same rule for the de Morgan dual connective. In such a way, any two-sided $\mu LL^{\infty}$ pre-proof $\pi$ can be mapped to a one-sided $\mu LL^{\infty}$ pre-proof $\pi^{\text{mono}}$ preserving validity: $\pi$ is valid if, and only if, $\pi^{\text{mono}}$ is valid.

From the above remark, any fair reduction cut-reduction sequence $(\pi_i)_{i \in \omega}$ in two-sided $\mu LL^{\infty}$ can be mapped to a fair one-sided cut-reduction sequence $(\pi_i^{\text{mono}})_{i \in \omega}$ which has a limit $\Pi$ which is valid. It follows that $(\pi_i)_{i \in \omega}$ is productive and that its limit $\pi$ satisfies $\pi^{\text{mono}} = \Pi$ from which validity follows.
# D Appendix on Section 4

## D.1 Details on skeletons

To any $\mu LL^\infty$ formulas and $\mu LL^\infty$ proofs, one can associate their classical skeletons, that is corresponding $\mu LK^\infty$ formulas and proofs, after erasing of the linear information of the sequent and proof:

**Definition 80 (μLK$^\infty$-Skeleton).** The $\mu LK^\infty$-skeleton of a $\mu LL^\infty$ formula is defined inductively as follows ($\sigma \in \{\mu, \nu\}$):

$$ \begin{array}{c|c|c} \mathrm{Sk}(A \otimes B) = \mathrm{Sk}(A) \wedge \mathrm{Sk}(B) & \mathrm{Sk}(A \otimes B) = \mathrm{Sk}(A) \vee \mathrm{Sk}(B) & \mathrm{Sk}(!A) = \mathrm{Sk}(A) \\ \mathrm{Sk}(A \& B) = \mathrm{Sk}(A) \wedge \mathrm{Sk}(B) & \mathrm{Sk}(A \oplus B) = \mathrm{Sk}(A) \vee \mathrm{Sk}(B) & \mathrm{Sk}(?A) = \mathrm{Sk}(A) \\ \mathrm{Sk}(1) = \top & \mathrm{Sk}(\bot) = \mathrm{F} & \mathrm{Sk}(a) = a \\ \mathrm{Sk}(\top) = \top & \mathrm{Sk}(0) = \mathrm{F} & \mathrm{Sk}(a^\perp) = \neg a \\ \mathrm{Sk}(A \to B) = \mathrm{Sk}(A) \Rightarrow \mathrm{Sk}(B) & \mathrm{Sk}(\sigma X.A) = \sigma X.\mathrm{Sk}(A) & \mathrm{Sk}(X) = X \end{array} $$

Let $\pi$ be a two-sided $\mu LL^\infty$ pre-proof of $\Gamma \vdash \Delta$. $\mathrm{Sk}(\pi)$ is the $\mu LK^\infty$ pre-proof of $\mathrm{Sk}(\Gamma) \vdash \mathrm{Sk}(\Delta)$ obtained by the following corecursive process by case analysis on the last rule $r$ of $\pi$:

- if $r = (Ax)$, then $\mathrm{Sk}(\pi)$ is an axiom;

- if $r = (Cut)$, then $\mathrm{Sk}(\pi)$ ends with a cut of premises the skeletons of the premises of $\pi$;

- if $r$ is a fixed-point rules, then $\mathrm{Sk}(\pi)$ ends with the same rule of $\mu LK^\infty$ with, for premise, the skeleton of the premise of $\pi$;

- if $r$ is a multiplicative or additive rule, then $\mathrm{Sk}(\pi)$ ends with the corresponding rule for the associated connective with, for premises, the skeletons of the premises of $\pi$;

- if $r$ is a structural rules for an exponential formula or an exchange rule, then $\mathrm{Sk}(\pi)$ ends with the corresponding structural rules with, for premise, the skeleton of the premise of $\pi$;

- if $r$ is a promotion or dereliction, then $\mathrm{Sk}(\pi)$ is the skeleton of the premise of $\pi$ of $\mathrm{Sk}(\pi)$.

## D.2 Proof of Proposition 41

**Proposition 81.** For any valid $\mu LL^\infty$ proof $\pi$ of $s$, $\mathrm{Sk}(\pi)$ is a valid $\mu LK^\infty$ proof of $\mathrm{Sk}(s)$.

*Proof.* It is easy to check that $\mathrm{Sk}(\pi)$ is a $\mu LK^\infty$ pre-proof (as soon as one admit both additive and multiplicative inference for classical conjunction and disjunction):

- even though the corecursive call, in the promotion and dereliction cases are non-guarded, the procedure is productive as there can only be finitely many such inferences

- $\mathrm{Sk}(\pi)$ is trivially locally correct and of conclusion $\mathrm{Sk}(s)$.

Every infinite branch of $\mathrm{Sk}(\pi)$ is valid since all fixed-points unfoldings are preserved in the skeleton and therefore every infinite thread of a branch of $\pi$ with least recurring formula $F$ may be mapped to a thread of minimal formula $\mathrm{Sk}(F)$
### D.3 A linear decoration of $\muLK^\infty$ into $\muLL^\infty$

We consider the following embedding of $\muLK^\infty$ (and $\muLK^\infty$ sequents) into two-sided $\muLL^\infty$:

$$ 
\begin{align*}
[a]^k &= !a \\
[X]^k &= !X \\
[A \Rightarrow B]^k &= !((? [A]^k) \dashv (? [B]^k)) \\
[A \wedge B]^k &= !((? [A]^k) \& (? [B]^k)) \\
[A \vee B]^k &= !((? [A]^k) \oplus (? [B]^k)) \\
[\sigma X.A]^k &= ! \sigma X. ? [A]^k \quad \sigma \in \{\mu, \nu\} \\
[T]^k &= ! \top \\
[F]^k &= ! 0
\end{align*}
$$

One easily checks that the translation is consistent with positivity conditions of $\muLK$ and that:

**Lemma 82.** For any $\muLK$ formula $A$, $[A]^k$ is a $\muLL$ formula.

Moreover, setting $[X]^k = !X$ entails easily that:

**Lemma 83.** For any $\muLK$ formula $A, B$, $\sigma \in \{\mu, \nu\}$,

$$ [A[\sigma X.B/X]]^k = [A]^k[\sigma X. ?[B]^k/X]. $$

*Proof.* This simply follows from the fact that $[X]^k = !X$, by induction on $A$.

**Definition 84 (Translation of $\muLK^\infty$ proofs in $\muLL^\infty$ proofs).** In Figures 15 and 16, each $\muLK^\infty$ inference is translated in a $\muLL^\infty$ proof pattern relating the translation of the premises sequents to the translation of the conclusion sequent.

A non-wellfounded $\muLK^\infty$ pre-proof $\pi$ of $\Gamma \vdash \Delta$ can therefore be translated into a non-wellwounded pre-proof $[\pi]^k$ of $[\Gamma \vdash \Delta]^k$ of $\muLL^\infty$.

In the above definition and the corresponding figures, we do not make explicit the ancestor relations as it is unambiguous.

**Remark 85.** Notice that the translation preserve the ancestor relation in the following sense: for each inference $r$ of $\muLK^\infty$, if the $i$th formula of conclusion $s$ is in ancestor relation with the $j$th formula of the $k$th premise $s_k$, then in $[r]^k$, the $i$th formula of $[s]^k$ is in relation, for the transitive closure of $\muLL^\infty$ ancestor relation, with the $j$th formula of the $k$th open sequent $[s_k]^k$.

**Proposition 86.** Let be a non-wellfounded $\muLK^\infty$ pre-proof $\pi$ of $\Gamma$. $\pi$ is a valid $\muLK^\infty$ proof if, and only if, $[\pi]^k$ is a valid $\muLL^\infty$ proof.

*Proof.* Indeed, the infinite branches of $\pi$ are in one-to-one correspondence with the infinite branches of $[\pi]^k$, the thread are preserved thanks to the previous remark and the translation of formula ensures that a thread is valid in $\pi$ if, and only if, it is valid in $[\pi]^k$.
$$
\begin{align*}
\left[ \overline{\Gamma, F \vdash F, \Delta} \quad (\mathbf{Ax}) \right]^k &= \frac{\overline{[F]^k \vdash [F]^k} \quad (\mathbf{Ax})}{\overline{[F]^k \vdash ?[F]^k} \quad (\mathbf{d}_r)} \quad \overline{[\Gamma]^k, [F]^k \vdash ?[F]^k, ?[\Delta]^k} \quad (\mathbf{w}_l)^*, (\mathbf{w}_r)^* \\
\left[ \frac{\Gamma \vdash \Delta, F \quad \Gamma', F \vdash \Delta'}{\Gamma, \Gamma' \vdash \Delta, \Delta'} \quad (\text{Cut}) \right]^k &= \frac{\overline{[\Gamma']^k, [F]^k \vdash ?[\Delta']^k} \quad (\mathbf{p}_l)}{\overline{[\Gamma']^k, ?[F]^k \vdash ?[\Delta']^k} \quad (\text{Cut})} \quad \overline{[\Gamma, \Gamma']^k \vdash ?[\Delta, \Delta']^k} \\
\left[ \frac{\Gamma \vdash \Delta}{\Gamma \vdash F, \Delta} \quad (\mathbf{W}_r) \right]^k &= \frac{\overline{[\Gamma]^k \vdash ?[\Delta]^k} \quad (\mathbf{w}_r)}{\overline{[\Gamma]^k \vdash ?[F]^k, ?[\Delta]^k}} \\
\left[ \frac{\Gamma \vdash \Delta}{\Gamma, F \vdash \Delta} \quad (\mathbf{W}_l) \right]^k &= \frac{\overline{[\Gamma]^k \vdash ?[\Delta]^k} \quad (\mathbf{w}_l)}{\overline{[\Gamma]^k, [F]^k \vdash ?[\Delta]^k}} \quad (\text{Since } [F]^k \text{ is a !-formula.}) \\
\left[ \frac{\Gamma \vdash F, F, \Delta}{\Gamma \vdash F, \Delta} \quad (\mathbf{C}_r) \right]^k &= \frac{\overline{[\Gamma]^k \vdash ?[F, F, \Delta]^k}}{\overline{[\Gamma]^k \vdash ?[F, \Delta]^k}} \quad (\mathbf{c}_r) \\
\left[ \frac{\Gamma, F, F \vdash \Delta}{\Gamma, F \vdash \Delta} \quad (\mathbf{C}_l) \right]^k &= \frac{\overline{[\Gamma, F, F]^k \vdash ?[\Delta]^k}}{\overline{[\Gamma, F]^k \vdash ?[\Delta]^k}} \quad (\mathbf{c}_l) \\
&\qquad \text{(Since } [F]^k \text{ is a !-formula.)} \\
\left[ \frac{\Gamma \vdash \Delta, G, F, \Delta'}{\Gamma \vdash \Delta, F, G, \Delta'} \quad (\mathbf{X}_r) \right]^k &= \frac{\overline{[\Gamma]^k \vdash ?[\Delta, G, F, \Delta']^k}}{\overline{[\Gamma]^k \vdash ?[\Delta, F, G, \Delta']^k}} \quad (\mathbf{X}_r) \\
\left[ \frac{\Gamma, G, F, \Gamma' \vdash \Delta}{\Gamma, F, G, \Gamma' \vdash \Delta} \quad (\mathbf{X}_l) \right]^k &= \frac{\overline{[\Gamma, G, F, \Gamma']^k \vdash ?[\Delta]^k}}{\overline{[\Gamma, F, G, \Gamma']^k \vdash ?[\Delta]^k}} \quad (\mathbf{X}_l)
\end{align*}
$$

<caption>Fig. 15. Translation of $\mu$LK$^\infty$ inferences into $\mu$LL$^\infty$: identity and structural rules</caption>
$$ \left[ \frac{\Gamma \vdash F, \Delta \quad \Gamma \vdash G, \Delta}{\Gamma \vdash F \wedge G, \Delta} \quad (\wedge_r) \right]^k = \frac{[\Gamma]^k \vdash? [F]^k, ?[\Delta]^k \quad [\Gamma]^k \vdash? [G]^k, ?[\Delta]^k}{[\Gamma]^k \vdash?!([F]^k \&? [G]^k), ?[\Delta]^k} \quad (?_{\mathrm{d}_r}) \quad (!_{\mathrm{p}_r}) $$

$$ \left[ \frac{\Gamma, F_i \vdash \Delta}{\Gamma, F_1 \wedge F_2 \vdash \Delta} \quad (\wedge_i) \right]^k = \frac{\frac{[\Gamma]^k, [F_i]^k \vdash? [\Delta]^k}{[\Gamma]^k, ?[F_i]^k \vdash? [\Delta]^k} \quad (?_{\mathrm{p}_i})}{\frac{[\Gamma]^k, ?[F_1]^k \&? [F_2]^k \vdash? [\Delta]^k}{[\Gamma]^k, [F_1 \wedge F_2]^k \vdash? [\Delta]^k} \quad (!_{\mathrm{d}_i})} $$

$$ \left[ \frac{\Gamma \vdash F_i, \Delta}{\Gamma \vdash F_1 \lor F_2, \Delta} \quad (\lor_i) \right]^k = \frac{\frac{[\Gamma]^k \vdash? [F_i]^k, ?[\Delta]^k}{[\Gamma]^k \vdash?!([F_1]^k \oplus ?[F_2]^k), ?[\Delta]^k}}{[\Gamma]^k \vdash? [F_1 \lor F_2]^k, ?[\Delta]^k} \quad (\oplus_i), \quad (!_{\mathrm{p}_i}) \quad (?_{\mathrm{d}_i}) $$

$$ \left[ \frac{\Gamma, F \vdash \Delta \quad \Gamma, G \vdash \Delta}{\Gamma, F \lor G \vdash \Delta} \quad (\lor_i) \right]^k = \frac{\frac{[\Gamma]^k, [F]^k \vdash? [\Delta]^k}{[\Gamma]^k, ?[F]^k \vdash? [\Delta]^k} \quad (?_{\mathrm{p}_i})}{\frac{[\Gamma]^k, ?[F]^k \oplus ?[G]^k \vdash? [\Delta]^k}{[\Gamma]^k, [F \lor G]^k \vdash? [\Delta]^k} \quad (!_{\mathrm{d}_i})} \quad (\oplus_i) $$

$$ \left[ \overline{\Gamma \vdash \top, \Delta} \quad (\top_r) \right]^k = \frac{\overline{\frac{[\Gamma]^k \vdash \top, ?[\Delta]^k}{[\Gamma]^k \vdash?! \top, ?[\Delta]^k}} \quad (!_{\mathrm{p}_r})}{[\Gamma]^k \vdash? [\top]^k, ?[\Delta]^k} \quad (?_{\mathrm{d}_r}) $$

$$ \left[ \overline{\Gamma, F \vdash \Delta} \quad (\mathfrak{F}_i) \right]^k = \frac{\overline{[\Gamma]^k, 0 \vdash? [\Delta]^k}}{[\Gamma]^k, [F]^k \vdash? [\Delta]^k} \quad (!_{\mathrm{d}_i}) $$

$$ \left[ \frac{\Gamma, F \vdash G, \Delta}{\Gamma \vdash F \Rightarrow G, \Delta} \quad (\Rightarrow_r) \right]^k = \frac{\frac{[\Gamma]^k, [F]^k \vdash? [G]^k, ?[\Delta]^k}{[\Gamma]^k, ?[F]^k \vdash? [G]^k, ?[\Delta]^k} \quad (?_{\mathrm{p}_i})}{\frac{[\Gamma]^k \vdash?!([F]^k \to? [G]^k), ?[\Delta]^k}{[\Gamma]^k \vdash? [F \Rightarrow G]^k, ?[\Delta]^k} \quad (?_{\mathrm{d}_i})} \quad (-\circ_r), \quad (!_{\mathrm{p}_r}) $$
$$ \left[ \frac{\Gamma \vdash F, \Delta \quad \Gamma', G \vdash \Delta'}{\Gamma, \Gamma', F \Rightarrow G \vdash \Delta, \Delta'} \quad (\Rightarrow_l) \right]^k = \frac{\frac{[\Gamma']^k, [G]^k \vdash? [\Delta']^k}{[\Gamma']^k, ?[G]^k \vdash? [\Delta']^k} \quad (?_{\mathrm{p}_i})}{\frac{[\Gamma]^k \vdash? [F]^k, ?[\Delta]^k}{[\Gamma, \Gamma']^k, ?[F]^k \to? [G]^k \vdash? [\Delta]^k, ?[\Delta']^k} \quad (-\circ_l)} \quad (!_{\mathrm{d}_i}) $$

$$ \left[ \frac{\Gamma \vdash G[\sigma X.G/X], \Delta}{\Gamma \vdash \sigma X.G, \Delta} \quad (\sigma_r) \right]^k = \frac{\frac{[\Gamma]^k \vdash \sigma X. ?[G]^k, ?[\Delta]^k}{[\Gamma]^k \vdash?! \sigma X. ?[G]^k, ?[\Delta]^k}}{[\Gamma]^k \vdash? [\sigma X.G]^k, ?[\Delta]^k} \quad (!_{\mathrm{p}_r}) \quad (?_{\mathrm{d}_r}) \quad (\sigma_r) $$

$$ \left[ \frac{\Gamma, G[\sigma X.G/X] \vdash \Delta}{\Gamma, \sigma X.G \vdash \Delta} \quad (\sigma_l) \right]^k = \frac{\frac{[\Gamma]^k, [G[\sigma X.G/X]]^k \vdash? [\Delta]^k}{[\Gamma]^k, ?([G]^k[\sigma X. ?[G]^k/X]) \vdash? [\Delta]^k}}{\frac{[\Gamma]^k, \sigma X. ?[G]^k \vdash? [\Delta]^k}{[\Gamma]^k, [\sigma X.G]^k \vdash? [\Delta]^k}} \quad (!_{\mathrm{p}_i}) \quad (\sigma_l) \quad (!_{\mathrm{d}_i}) $$

<caption>Fig. 16. Translation of $\mu$LK$^\infty$ inferences into $\mu$LL$^\infty$: logical rules</caption>
## D.4 Proof of Theorem 44

**Theorem 87.** $\muLK^\infty$ eliminates cuts.

*Proof.* Let $\pi \in \muLK^\infty$ be a proof of $\Gamma \vdash \Delta$. $\pi^d$ is a valid proof of $(\Gamma \vdash \Delta)^d$ so that by cut-elimination, there is a fair reduction sequence $\sigma = (\Pi_i)_{i \in \omega}$ with $\Pi_0 = \pi^d$ which converges to a cut-free $\mu LL^\infty$ proof $\Pi'$. For any $i \in \omega$, one has either $\mathrm{Sk}(\Pi_i) = \mathrm{Sk}(\Pi_{i+1})$ or $\mathrm{Sk}(\Pi_i) \to_{\muLK^\infty} \mathrm{Sk}(\Pi_{i+1})$ so that one can extract from $\sigma$ a strongly converging $\to_{\muLK^\infty}$-reduction sequence which converges to $\mathrm{Sk}(\Pi')$, a cut-free valid $\muLK^\infty$ proof of $\Gamma \vdash \Delta$.
$$
\frac{\pi_S \quad \pi'_S}{!A \otimes! B \vdash! A \otimes! B} \quad \text{(Cut)} \quad \rightarrow_{\text{cut}}^{*} \quad \frac{\frac{\overline{A \vdash A} \quad (\text{Ax})}{!A \vdash A} \quad (\text{?d}) \qquad \overline{B \vdash B} \quad (\text{Ax})}{!B \vdash B} \quad (\text{?d})}{\frac{!A, !B \vdash A \quad (\text{?w})}{!A, !B \vdash! A} \quad (\text{!p}) \qquad \overline{!A, !B \vdash B} \quad (\text{!w})}{!A, !B \vdash! A} \quad (\text{!p})} \quad \frac{\overline{!A, !B, !A, !B \vdash! A \otimes! B} \quad (\text{?c})^2}{\overline{!A, !B \vdash! A \otimes! B}} \quad (\text{?c})^2}{\overline{!A \otimes! B \vdash! A \otimes! B}} \quad (\text{?c})^2
$$

E.3 What about the fixed-point encoding?

$$
\frac{(\pi_S)^{\bullet} \quad (\pi'_S)^{\bullet}}{!^{\bullet} A \otimes!^{\bullet} B \vdash!^{\bullet} A \otimes!^{\bullet} B} \quad \text{(Cut)} \quad \rightarrow_{\text{cut}}^{\omega} \quad \frac{\frac{\overline{A \vdash A} \quad (\text{Ax})}{!^{\bullet} A \vdash A} \quad (\text{?d}^{\bullet}) \qquad \overline{B \vdash B} \quad (\text{Ax})}{!^{\bullet} B \vdash B} \quad (\text{?d}^{\bullet})}{\frac{!^{\bullet} A, !^{\bullet} B \vdash A \quad (\text{?w}^{\bullet})}{!^{\bullet} A, !^{\bullet} B \vdash! A \quad (\text{!p}^{\bullet})} \qquad \overline{!^{\bullet} A, !^{\bullet} B \vdash! B} \quad (\text{!p}^{\bullet})} \quad \frac{!^{\bullet} A, !^{\bullet} B \vdash! A, !^{\bullet} B \vdash! A \otimes! B \quad (\text{?c}^{\bullet})^2}{!^{\bullet} A, !^{\bullet} B \vdash! A \otimes! B \quad (\text{?c}^{\bullet})}}}{\overline{!^{\bullet} A \otimes!^{\bullet} B \vdash!^{\bullet} A \otimes!^{\bullet} B}} \quad (\text{?c}^{\bullet})^2}
$$

The left occurrences of *A*, *B* require two unfoldings of the *v*-fixed-point, while
the right occurrences of *A*, *B* require only one unfolding of the *v*-fixed-point.

The fixed-point unfolding structure keeps track of the history of the structural
rules.

E.4 There is more than a promotion in !•

Remember the encoding of promotion in $\mu$MALL$^{∞}$:

$$
\[
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c}
\multirow{2}{*}{\begin{smallmatrix} !^{\bullet} & (\pi) \\ \vdash & F, ? \Delta \end{smallmatrix}} & \multirow{2}{*}{\begin{smallmatrix} (\!p) \end{smallmatrix}} & \multicolumn{4}{c}{=} \\
& & \multicolumn{4}{c}{\begin{smallmatrix} \vdash & (!F)^{\bullet}, (?\Delta)^{\bullet} \\ \vdash & (!F)^{\bullet} \otimes (!F)^{\bullet}, (?\Delta)^{\bullet}, (?\Delta)^{\bullet} \\ \vdash & (!F)^{\bullet} \otimes (!F)^{\bullet}, (?\Delta)^{\bullet} \end{smallmatrix}} \\
& & & \multicolumn{4}{c}{\begin{smallmatrix} (\text{?c}^{\bullet})^{*} \\ (\text{?c}^{\bullet})^{*} \\ (\text{?c}^{\bullet})^{*} \end{smallmatrix}} \\
& & & & \multicolumn{2}{c}{\begin{smallmatrix} (\nu), (&), (&) \end{smallmatrix}}
\end{array}
\]
$$

This is certainly not the only way to derive a sequent $\vdash$ (!F)•, (?Δ)•

Indeed, for any family $(\pi_i)_{i \in I}$ of proofs of $\vdash F, ? \Delta$ and any map $\varphi$ from $\{l, r\}^*$ to $I$, one gets a derivation shown in Figure 17.

Such a proof allows us to provide a different linear proofs in "each copy" of the
exponential box and therefore to have a sort of non-uniform promotion [12,26].
<figure><img src="image_17.png" /><figcaption>Fig. 17. A non-uniform promotion</figcaption></figure>