# Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue

Esaïe Bauer

esaie.bauer@irif.fr

Université Paris Cité

Paris, France

Alexis Saurin

Université Paris Cité & CNRS & INRIA

Paris, France

## ABSTRACT

The aim of this paper is twofold: contributing to the non-wellfounded and circular proof-theory of the modal mu-calculus and to that of extensions of linear logic with fixed points. Contrarily to Girard's linear logic which is equipped with a rich proof theory, Kozen's modal mu-calculus has an underdeveloped one: for instance the modal mu-calculus is lacking a proper syntactic cut-elimination theorem.

A strategy to prove the cut-elimination theorem for the modal mu-calculus is to prove cut-elimination for a "linear translation" of the modal mu-calculus (that is define a translation of the statements and proofs of the modal mu-calculus into a linear sequent calculus) and to deduce the desired cut-elimination results as corollaries. While designing this linear translation, we come up with a sequent calculus exhibiting several modalities (or exponentials). It happens that the literature of linear logic offers tools to manage such calculi, for instance subexponentials by Nigam and Miller and super exponentials by the first author and Laurent.

We actually extend super exponentials with fixed-points and non-wellfounded proofs (of which the linear decomposition of the modal mu-calculus is an instance) and prove a syntactic cut-elimination theorem for these sequent calculi in the framework of non-wellfounded proof theory. Back to the classical modal mu-calculus, we deduce its cut-elimination theorem from the above results, investigating both non-wellfounded and regular proofs.

## KEYWORDS

circular and non-wellfounded proofs, cut elimination, exponential modalities, fixed-points, linear logic, modal μ-calculus, proof theory

## 1 INTRODUCTION

On unity and diversity in logic. It is striking how logic can show at the same time deep unity and diversity, maybe even more when considering computer science logic. On the one hand, this unity is embodied by the fundamental objects and questions of logic which could be broadly summarised as (i) how to design and use logical languages and logical consequences, from a model-theoretic or a proof-theoretic perspective, (ii) how to understand the logical invariants emerging from models or proofs and – in the CS-oriented part of logic – (iii) how to provide algorithms and softwares to mechanize these models and proofs with a specific focus on (iv) how intrinsically expressive and complex are those formalisms and problems? On the other hand, the vast diversity of logical languages and the broad nature of reasoning – and sometimes even the linguistic aspects of logical design – that one tries to capture logically is a source of multiplicity of formalisms which, sometimes, turn out to become incompatible: the ultimate aim of logic to universality can soon be

lost in the technicalities required to achieve the precise and efficient modelling of a specific phenomenon.

This diversity is of course source of very rich theories and allows us to regularly revisit the fundamental concepts themselves, which is highly valuable. For instance, depending on the adopted point of view (be it classical, intuitionistic or linear), one will be driven to various perspectives on what a model should be, from models of truth and provability (expressing invariants on logical statements) to models of proofs (expressing invariants on reasonings... and computation). Indeed, as soon as one is adopting the Curry-Howard perspective – viewing formulas as data types, proofs as programs and proof simplification as evaluation – it becomes natural to wonder not only when two formulas are equivalent and could be interchanged, but also when two proofs are equivalent and when one can be used to optimize another one.

This choice of point of view will also lead to various structures for mathematically representing proofs, whether one is primarily interested in *what* can be deduced (in which case one often chooses some optimal representation for deductions minimizing the size of proofs or the non-determinism in proof objects), or whether one is primarily interested in *how* logical statements can be deduced (in which case one often chooses more structured representations, allowing for non-trivial proof invariants and proof-equivalences). Both approaches induce fundamentally different choices in the structure of the representation of logical judgments themselves (by nature hypothetical): the various flavours of sequents found in the literature (as sets, multisets or lists as well as labelled or nested sequents, etc.) illustrate this variety.

When turning to the structure of proofs, one can approach proof-invariants either with semantical methods (from denotational semantics) or with syntactical methods (inference permutations, canonical representations of proofs, cut-elimination) but in both cases a fine-grained analysis of the process and requirements of cut-elimination is crucial.

When coming back to the expressiveness of the logical language under study (be it propositional, predicative of higher-order, whether it allows to model time or other modal aspects or whether it expresses (co)inductive statements), this choice has of course a direct and essential impact on the structure of models and proofs. For instance, when manipulating a logical language encompassing some form of inductive statements, one shall have some sort of inductive form of reasoning at hand, be it in the form of an induction axiom, in the form of Parks's inference rules, which reflect Knaster-Tarski's theorem, in the form of an infinitely branching $\omega$-rule, or in the form of non-wellfounded proofs, which correspond to a form of infinite descent reasoning. On view of the applications of induction
and coinduction in CS, it is natural to investigate the relationships between such representations of (co)inductive reasoning.

Indeed, studies on the *modal μ-calculus* have been extremely fruitful since Kozen's seminal paper [Koz83], investigating its properties by employing a number of approaches (model-theoretic, proof-theoretic, automata-theoretic, complexity-theoretic, etc). Still, *cut-elimination*, despite being a crucial property from a proof-theoretic perspective, only received partial solutions, either in the form of statements of cut-admissibility (usually deduced from a completeness theorem and therefore non effective) or syntactic cut-elimination results capturing only a fragment of the calculus [NW96, BS12, Min12, MS12, AL17]. The present work aims at contributing to syntactic cut-elimination theorems for the modal μ-calculus.

**Cut-admissibility vs cut-elimination.** The treatment of the cut-inference in sequent-based proof-systems follows two main traditions: (i) one can consider cut-free proofs as the primitive proof-objects, establishing that the cut-inference is admissible (according to that tradition, the cut-inference essentially lives at the meta level) or alternatively, (ii) one can consider that the cut inference lives at the object-level and is a fundamental piece of proofs, establishing that it is *eliminable* thus ensuring the sub-formula property (and its numerous important consequences, ranging from consistency to interpolation properties). This second tradition often comes with the investigation of a syntactic, or effective, approach to cut-elimination, consisting in a cut-reduction relation on proofs, shown to be (at least) weakly normalizing, the normal forms being cut-free proofs. In several settings (most notably LJ and LL [Gir87]), such cut-reductions may have a computational interpretation which was the starting point of Curry-Howard correspondence built upon sequent-calculus [CH00].

When considering cuts in the modal μ-calculus, one finds a lot of works which tried to address cut-elimination in some form. Some of them are admissibility results [NW96, AL17], possibly using non-wellfounded or circular systems. Systems with ω-rule also enjoy cut-admissibility (see [JKS08] for instance), however a problem that arises when trying to describe a *syntactic cut-elimination* is the fact that a choice on the number of time a μ-rule must be made sometimes before knowing how many times it should be to fit each hypotheses of a v-rule. In [BS12], the authors discuss a specific example where syntactic cut-elimination fails. Syntactic results of cut-elimination can still be found in ω-rule systems [MS12, BS12, Min12], however these systems are strict fragments of the modal μ-calculus. In fact, there is no syntactic cut-elimination theorem for the modal μ-calculus.

Linear logic is often described as a resource-sensitive logic but it is probably more correct to describe linear logic as a logic designed for analyzing cut-elimination itself. Indeed, linear logic comes from an analysis of structural rules, not to weaken them but to control them and offer a more constructive management of contraction and weakening, notably by offering means to cancel some fundamental drawbacks of classical proofs. For instance, linear logic allowed for decomposing, thanks to the controlled treatment of the structural rules of weakening and contraction by the exponential modalities,

both intuitionistic and classical logic, in a structured and fine-grained enough way so that it was possible to refine both the cut-elimination of those logics as well as their notion of model (allowing to build a non-trivial denotational model of proofs for classical logic) [Gir87, DJS97]. Further analyses on these exponential modalities led to find alternative presentations offering the possibility to tame their complexity in quite a flexible way, introducing *light logics*.

Those results were extended to logics with fixed-points in the finitary and non-wellfounded setting [Dou17, Sau23] and μLL<sup>∞</sup> allowed for the same kind of linear decomposition for (the non-wellfounded version of) μLJ and μLK. A natural question is therefore whether linear logic and its extensions with fixed-points can help us in achieving syntactic cut-elimination for the modal mu-calculus. This suggests a first question: what would be a linear decomposition of the modal μ-calculus? Let us forget for a moment about the fixed-point connective since to motivate the system μLL<sup>∞</sup>, we need to understand what problem will be encountered by the translation of μLK<sup>∞</sup> in it. Let us consider an example:

$$ \frac{\vdash A, B \qquad \Box p \rightsquigarrow \frac{\vdash !\Box A^*, \delta B^*}{\vdash ?!\Box A^*, \delta B^*} \quad ?d}{\vdash \Box A, \delta B} \quad ?d, !p $$

In this example, it would be convenient to have contexts prefixed with ◊, as applying the rules in this order would leave us with an unprovable sequent. From cut-elimination steps of exponentials, we have that adding ◊-formulas in the context of a promotion imposes to propagate all the structural rules of ? to ◊. This results in a system that extends μLL<sup>∞</sup> with structural rules on ◊ (◊<sub>c</sub> and ◊<sub>w</sub>), as well as the usual modal rule from modal μ-calculus (□<sub>p</sub>) and a relaxed constraint on the context of the promotion rule (!<sup>◊</sup><sub>p</sub>):

$$ \frac{\vdash A, \Gamma \qquad \Box p, \qquad \frac{\vdash \Diamond A, \Diamond A, \Gamma}{\vdash \Diamond A, \Gamma} \qquad \frac{\vdash \Gamma}{\vdash \Diamond A, \Gamma} \qquad \Diamond w}{\vdash A, ?\Gamma, \Diamond \Delta \qquad \frac{\vdash A, ?\Gamma, \Diamond \Delta}{\vdash !A, ?\Gamma, \Diamond \Delta} \qquad \Diamond p} $$

Do we break anything by doing so? In fact no, because we can rely on a theory for treating altogether various exponential modalities, known as subexponentials [NM09] or super exponentials [BL21]. It happens that the latter framework contains as an instance the sequent calculus LL<sub>□</sub> that we just outlined.

**Contributions.** This therefore suggests the following roadmap that we adopt in this paper: in Section 2, we recall the necessary technical background about μLL<sup>∞</sup>, superLL, and introduce μsuperLL<sup>∞</sup> and μLK<sup>∞</sup> (with list and sequence-based sequents). In Section 3, prove the cut-elimination for μsuperLL<sup>∞</sup> so that, in Section 4, we deduce various results on the cut-elimination of the modal mu-calculus in the circular and non-wellfounded setting.

More precisely, we first prove the infinitary weak normalization of a cut-elimination procedure for the non-wellfounded system μLK<sup>∞</sup> Then, while the normalization process is infinitary, adapting our μLK<sup>∞</sup> proofs to a system where sequents are sets of formulas, we can simultaneously use a regularisation procedure on them to get a circular and finitary weak-normalization reduction.

# 2 BACKGROUND

## 2.1 Formulas

Throughout this paper, we will work with various logics and will therefore consider different sets of formulas and sequent calculi
(namely LK, LK<sub>⊤</sub>, MALL, LL, superLL, µLL<sup>∞</sup>, µLK<sup>∞</sup>, µLL<sup>∞</sup>, µMALL<sup>∞</sup>, µsuperLL<sup>∞</sup>). We therefore give an uniform way of defining the formulas of such logics, to make the presentation generic, precise and concise, taking inspiration from [Sau23]:

DEFINITION 1 (μ-SIGNATURE). A μ-signature is a set of pairs (c, p) of a connective symbol c and a p ∈ {−, +}ⁿ with an n arity n ∈ N.

EXAMPLE 1 (μ-SIGNATURE ASSOCIATED TO OUR SYSTEMS). Here we define some μ-signature for our systems:

* µMALL<sup>∞</sup>: C<sub>MALL</sub> := {⊗, 𝒰, &, ⊕} × {(+, +)} ∪ {1, ⊥, τ, 0} × {()}.

* one-sided µLL<sup>∞</sup>: C<sub>LL₁</sub> := C<sub>MALL</sub> ∪ {!, ?} × {(+)}.

* two-sided µLL<sup>∞</sup>: C<sub>LL₂</sub> := C<sub>LL₁</sub> ∪ {(-∞, (-, +)), ((·)⊥, (-))}.

* one-sided µLK<sup>∞</sup>: C<sub>LK₁</sub> := {∧, ∨} × {(+, +)} ∪ {τ, F} × {}.

* two-sided µLK<sup>∞</sup>: C<sub>LK₂</sub> := C<sub>LK₁</sub> ∪ {(-, +)}, ((·)⊥, (-)).

* one-sided µLK<sup>∞</sup><sub>⊤</sub>: C<sub>LK<sub>⊤</sub>₁</sub> := C<sub>LK₁</sub> ∪ {◊, □} × {(+)}.

* two-sided µLK<sup>∞</sup><sub>⊤</sub>: C<sub>LK<sub>⊤</sub>₂</sub> := C<sub>LK<sub>⊤</sub>₁</sub> ∪ {(-, +)}, ((·)⊥, (-)).

Note that the definition of the μ-signature for superLL-systems is postponed to the next section as it requires some preliminary definitions.

DEFINITION 2 (PRE-FORMULAS). Let S be a triplet (C, V, A), with C a μ-signature, V a set of variables and A a set of atomic formulas, we define the set of pre-formulas FS over S to be the set defined by induction ((c, p) ∈ C, X ∈ V, a ∈ A):

$$
\mathcal{F}_S ::= X \mid a \mid c(\mathcal{F}_S, \dots, \mathcal{F}_S) \mid \mu X \cdot \mathcal{F}_S \mid v X \cdot \mathcal{F}_S
$$

DEFINITION 3 (POSITIVE AND NEGATIVE OCCURRENCE OF A FIXED-POINT VARIABLE). Let C be a μ-signature and a fixed-point variable X ∈ V, one defines the fact, for X, to occur positively (resp. negatively) in a pre-formula by induction on the structure of pre-formulas:

* The variable X occurs positively in X.

* X occurs positively (resp. negatively) in c(F₁, ..., Fₙ), for (c, p) ∈ C, if there is some 1 ≤ i ≤ n such that X occurs positively (resp. negatively) in Fᵢ and pᵢ = + or there is some 1 ≤ i ≤ n such that X occurs negatively (resp. positively) in Fᵢ and pᵢ = -.

* X occurs positively (resp. negatively) in δX.G if it occurs positively (resp. negatively) in G (for δ ∈ {μ, v}).

DEFINITION 4 (FORMULAS). Let S be a triplet (C, V, A), with C a μ-signature, V a set of variables and A a set of atomic formulas, a formula F over S is a closed pre-formula such that for any sub-pre-formula of F of the form δX.G (with δ ∈ {μ, v}), X does not occur negatively in G.

From this definition and definition 1 we get different sets of formulas, namely one-sided and two-sided versions of µMALL<sup>∞</sup>, µLL<sup>∞</sup>, µLK<sup>∞</sup> and µLK<sup>∞</sup><sub>⊤</sub>. By considering the µ, v, X-free formulas of these systems we get the fixed-point free versions of these systems: MALL, LL, LK, LK<sub>⊤</sub>.

DEFINITION 5 (NEGATION). Given a μ-signature C containing only connectives with positive polarity. Let t be an involution on C such that if t(c, p) = (c', p') then p = p'. Let A be a set of atoms with another involution κ on it and let V be a set of variables. We define (−)⊥(t,κ) to be the involution on formulas satisfying:

$$
X^{\perp(t, \kappa)} = X \qquad c(F_1, \dots, F_n)^{\perp(t, \kappa)} = t(c)(F_1^{\perp(t, \kappa)}, \dots, F_n^{\perp(t, \kappa)})
$$

$$
a^{\perp(t, \kappa)} = \kappa(a) \qquad (\mu X.F)^{\perp(t, \kappa)} = vX.F^{\perp(t, \kappa)}
$$

We then define an involution on the union of all positives connectives of example 1:

EXAMPLE 2 (DUAL CONNECTIVES ASSOCIATED TO OUR SYSTEMS). We define the involution t<sub>useful</sub> on positive connectives of example 1 to be the only involution satisfying:

$$
t_{\text{useful}}(\otimes, (+, +)) := (\mathfrak{A}, (+, +)) \qquad t_{\text{useful}}(\& , (+, +)) := (\oplus, (+, +))
$$

$$
t_{\text{useful}}(1, (\)) := (\perp, (\)) \qquad t_{\text{useful}}(\tau, (\)) := (0, (\))
$$

$$
t_{\text{useful}}(\wedge, (+, +)) := (\vee, (+, +)) \qquad t_{\text{useful}}(\tau, (\)) := (F, (\))
$$

$$
t_{\text{useful}}(\uparrow, +) := (\diamond, +) \qquad t_{\text{useful}}(\Box, +) := (\diamond, +)
$$

NOTATION 1. For the rest of the article, and for all our systems, we fix a set of countable variables V; a set A := A' ⊎ {a⊥ | a ∈ A'}, with an involution κ on it such that κ(a) = a⊥. For each particular systems containing only connectives with positive polarities, we take t to be the restriction of t<sub>useful</sub> on its μ-signature and use the notation A⊥ for A⊥(κ,t).

2.2 Sequent calculi

In this section, we define rules and proofs for both infinitary and finitary systems considered in example 1. Before defining inference rules, we need the definition of a sequent:

DEFINITION 6 (SEQUENT). A sequent is a pair of two lists of formulas Γ, Δ, that we usually write Γ ⊢ Δ. We call Γ the antecedent of the sequent and Δ the succedent of it. We also refer to the formulas of Γ (resp. Δ) as the hypotheses (resp. conclusions) of the sequent.

In one-sided systems we still use this definition, however the set of rules will only allow us to derive sequents with empty antecedent.

REMARK 1 (DERIVATION RULES & ANCESTOR RELATION). Usually, in the literature, derivation rules are defined as a scheme of one conclusion sequent and a list of hypotheses sequents. In our system, the derivation rules come with an ancestor relation linking one formula of the conclusion to zero, one or several formulas of the hypotheses. As we are working with sequent as lists, we define an ancestor relation, to be a relation from the positions of the formula in the conclusion, to a couple (i, j) with i the position of the hypothesis and j the position of the formula in the given hypothesis. For two-sided sequent, we would begin at 1 for the left-most formula of the antecedent.

When defining our rules, we draw the ancestor relation. For instance in the following example:

$$
\vdash F, \Delta_1 \quad \vdash G, \Delta_2 \quad \vdash F \otimes G, \Delta_1, \Delta_2 \quad \otimes
$$

the first formula of the conclusion (F₁ ⊗ F₂) is related to the first one of the first hypothesis (F₁) and also to the first one of the second hypothesis (F₂). Then for a formula in position i ∈ [2, #(Δ₁) + 1] will be related to the formula in position i of the first hypothesis. Whereas a formula in position i ∈ [#(Δ₁) + 2, #(Δ₁) + #(Δ₂) + 1] will be related to the formula in position i - #(Δ₁) of the second hypothesis. The red line keeping the order of formulas in a context.
<figure><img src="image_1.png" /><figcaption>Figure 1: one-sided LK$_{□}$ rules</figcaption></figure>

<figure><img src="image_2.png" /><figcaption>Figure 2: one sided MALL rules</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Figure 3: one sided exponential fragment of LL</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 4: Rules for the fixed-point fragment</figcaption></figure>

We then consider several sets of rules on the set of formulas over signatures defined in 1. We define rules for one-sided LK$_{□}$ in figure 1. Rules for LK will be the □, ◦-free rules of LK$_{□}$. Rules for MALL are defined in figure 2. We add rules of figure 3 to those of MALL to get the rules of LL. We add rules of figure 4 to LK, LK$_{□}$, MALL and LL to get the fixed-point versions of these systems: µLK$^{∞}$, µLK$_{□}^{∞}$, µMALL$^{∞}$ and µLL$^{∞}$. The exchange rule (ex) from figures 1 and 2 allows one to derive the rule $\frac{\vdash \sigma(\Gamma)}{\vdash \Gamma} \text{ex}(\sigma)$ for any permutation $\sigma$ of $\llbracket 1, \#(\Gamma) \rrbracket$, where $\sigma(\Gamma)$ designate the action of $\sigma$ on the list $\Gamma$. In the rest of the article, we will intentionally forget to write the exchange rule explicitely, the reader can consider that each of our rules are preceded and followed by a finite number of rule (ex).

The two-sided versions of LK, MALL and LL are defined as usual and not recalled here, however we define two-sided rules for modality in appendix A.2. Proofs of non fixed-point systems, LK, LK$_{□}$, MALL, LL, are the trees inductively generated by the corresponding set of rules of each of these systems. To define non-wellfounded proofs for fixed-point logics, we first need a definition:

**DEFINITION 7 (PRE-PROOFS).** Given a set of derivation rules, we define pre-proofs to be the trees co-inductively generated by rules of each of these systems.

**EXAMPLE 3 (CIRCULAR PROOF).** Circular pre-proofs are those pre-proofs having a finite number of sub-proofs. We represent them with

back-edges. Taking $F := vX.\diamond X$, we give an example of circular proof:

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

We consider definitions from Fischer-Ladner sub-formula set FL(F) of a formula F in appendix A.1.2. We don't give the proof of the following property here, but it can be found in [Dou17]:

**PROPOSITION 1 (FISCHER-LADNER SET FINITENESS).** Let F be a fischer-Ladner sub-formula, then FL(F) is a finite set.

**REMARK 2.** Notice that rules create only Fischer-Ladner sub-formulas from the conclusion sequent to the hypotheses. Therefore by property 1 one can only derive a finite number of formulas from a finite number of formulas. Meaning that if we represent sequents as sets, starting with one initial sequent one could derive only a finite number of new sequents from it.

**DEFINITION 8 (ACTIVE & PRINCIPAL OCCURRENCE OF A RULE).** We define active occurrences (resp. principal formula) of the rules of figures 1, 2, 3 and 4 to be the first occurrence (resp. formula) of each conclusion sequent of that rule except for:

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

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

* the modal rule (□) where all the occurrences are active and where □F is the principal formula.

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

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

## 2.3 Super exponential systems

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

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

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

From a signature $\mathcal{E}$, we can define two new sets of formulas:

**DEFINITION 11 (μ-SIGNATURE SPECIFIC TO superLL SYSTEMS).**
Signature for one-sided μsuperLL$^{∞}$: $C_{superLL}(\mathcal{E})_1 := C_{MALL} \cup \{(?_{\sigma}, +) | \sigma \in \mathcal{E}\} \cup \{(!_{\sigma}, +) | \sigma \in \mathcal{E}\}$ for $\mathcal{E}$ a set of exponential signatures.
Signature for two-sided μsuperLL$^{∞}$: $C_{superLL}(\mathcal{E})_2 := C_{superLL}(\mathcal{E})_1 \cup \{(-\sigma, (-, +)), ((-)^{\perp}, -)\}$ for $\mathcal{E}$ a set of exponential signatures.

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

For one set of signatures $\mathcal{E}$, we define many systems, parametrized by three relations on $\mathcal{E}$: $\leq_g$, $\leq_f$ and $\leq_u$. First we define the formulas of superLL($\mathcal{E}$) to be the $\mu$, $v$, X-free formulas of μsuperLL$^{∞}$(E). Formulas for one-sided superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) are the formulas generated from the μ-signature $C_{superLL}(\mathcal{E})_1$. Rules for this system are the rules of MALL from Figure 2 in combination with rules of Figure 5. Note that the multiplexing rule, $?_{m_i}$, is $(?_w)$ for $i=0$ and $(?_d)$ for $i=1$. Proofs from superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) are those trees inductively generated by the rules of this system. For its fixed-point version, μsuperLL$^{∞}$(E, $\leq_g$, $\leq_f$, $\leq_u$), we add the fixed-point rules of Figure 4. Rules for the two-sided versions of superLL(E, $\leq_g$, $\leq_f$, $\leq_u$) (resp. μsuperLL$^{∞}$(E, $\leq_g$, $\leq_f$, $\leq_u$)) will be rules of the two-sided versions of MALL (resp. μMALL$^{∞}$) as well as rule defined in Appendix A.3.1. We get μsuperLL$^{∞}$(E, $\leq_g$, $\leq_f$, $\leq_u$) pre-proofs, proofs, validity, as in the previous section. For the one-sided version, we extend $t_{useful}$ of Example 2 with every $?_{\sigma}$ and $!_{\sigma}$ where $\sigma$ is an exponential signature, $t_{useful}$ being an involution satisfying $t_{useful}(?_{\sigma}) := !_{\sigma}$. One can then define the negation from Definition 5 for one-sided μsuperLL$^{∞}$(E) keeping the same set of variables, atoms and involution $\kappa$ than in Notation 1 and taking $\iota$ to be the restriction of $t_{useful}$ to the μ-signature $C_{superLL}(\mathcal{E})$. We also use the notation $A^{\perp}$ for $A^{\perp(\iota, \kappa)}$.

In the remaining of this section, we will focus on fragment without fixed-points of super exponentials: superLL.

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

**DEFINITION 12 (DERIVABILITY CLOSURE).** Given a signature $\sigma$, we define the derivability closure $\bar{\sigma}$ to be the signature inductively

defined by:

$$ 
\begin{align*}
\sigma(r) &\Rightarrow \bar{\sigma}(r) \\
\bar{\sigma}(?_{c_i}) &\Rightarrow \bar{\sigma}(?_{c_j}) \Rightarrow \bar{\sigma}(?_{c_{i+j-1}}) \\
\sigma(?_{c_2}) &\Rightarrow \bar{\sigma}(?_{m_i}) \Rightarrow \bar{\sigma}(?_{m_j}) \Rightarrow \bar{\sigma}(?_{m_{i+j}}) \quad i, j \neq 0 \\
\sigma(?_{m_i}) &\Rightarrow \bar{\sigma}(?_{c_i}) \Rightarrow \bar{\sigma}(?_{m_i})
\end{align*}
$$

Derivability closure comes with the property that for each rule (r) such that $\bar{\sigma}(r)$ is true, the rule (r) is derivable for $?_{\sigma}$. In that flavour, we define sets of all possible derivations, which will be used to define the cut-elimination procedure. We define a notion of coherent sets of derivations which are sets of derivation having the same conclusion and open hypotheses. In combination with that, we use derivability closure to define coherent sets of derivations $?_{\sigma}^{\vec{c}_i}$ (resp. $?_{\vec{m}_i}$), for $i \in \mathbb{N}$, that have the same conclusion and hypothesis than $?_{c_i}$ (resp. $?_{m_i}$).

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

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

**THEOREM 1 (CUT ELIMINATION).** As soon as the 8 cut-elimination axioms of Table 1 are satisfied, cut elimination holds for superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$).

Many existing linear logic systems are instances of superLL. Here we give the example of Elementary Linear Logic.

**Elementary Linear Logic.** Elementary Linear Logic (ELL) [Gir98, DJ03] is a variant of LL where we remove $(?_d)$ and $(!_g)$ and add the functorial promotion:

$$ \vdash A, \Gamma \quad \vdash !A, ?\Gamma \quad !_f $$

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

As argued in [BL21], The superLL-systems subsume many more existing linear logic systems such as SLL [Laf04], LLL [Gir98], seLL [NM09]. The last two are particularly interesting as they require more than one exponential signature to be formalized. We do not discuss them here however, since we will have such an example with the linear version of the modal μ-calculus in Section 4.

Bauer and Laurent's aim [BL21] was primarily to formally prove many cut-elimination theorems in a uniform way. However the conditions for the cut-elimination to work can be used independently and that is what we aim to do for the modal μ-calculus.

## 2.4 Cut-elimination for fixed-point logics

To prove cut-elimination theorems in fixed-point logics, we use an intermediary rule called the multicut. The multicut is extensively defined in [Sau23].

See
details in
App. A.3.2

See
details in
App. A.3.3

See
details
in
App. A.3.5

See details
in App.
A.3.6
<figure><img src="image_6.png" /><figcaption>Figure 5: Exponential fragment of $\mu$superLL$^\infty$</figcaption></figure>

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

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

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

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

**DEFINITION 13 (MULTICUT RULE).** The multicut rule is a rule with an arbitrary number of hypotheses:

$$ \vdash \Gamma_1 \quad \dots \quad \vdash \Gamma_n \quad \text{mcut}(i, \perp) $$

The ancestor relation $i$ sends one formula of the conclusion to exactly one formula of the hypotheses; whereas the $\perp$-relation links cut-formulas together.

See
App. A.4.1

**REMARK 3.** The idea of the multicut is to abstract a finite tree of binary cuts quotiented by cut-commutation rule. We give an example of a multicut rule and represent graphically $i$ in red and $\perp$ in blue.

$$ \vdash A, B \quad \vdash B^{\perp}, C \quad \vdash C^{\perp}, D \quad \text{mcut}(i, \perp) $$

We can understand the multicut rule as a tree of binary cuts through the (cut/mcut)-principal case:

$$ \begin{gathered} \frac{C \quad \vdash F, \Gamma' \quad \vdash F^{\perp}, \Delta}{\vdash \Gamma} \quad \text{cut} \\ \leadsto \quad \frac{C \quad \vdash F, \Gamma' \quad \vdash F^{\perp}, \Delta}{\vdash \Gamma} \quad \text{mcut}(i', \perp') \end{gathered} $$

Here, $i'$ sends on $C$ formulas that were sent on $C$ by $i$, either it uses the ancestor relation of the cut-rule that has been merged. The relation $\perp'$ is obtained from $\perp$ by adding $F \perp' F^{\perp}$.

To make the multicut reduction rules more readable, we use the following definition:

See detail in
App. A.4.2.

**DEFINITION 14 (RESTRICTION OF A MULTICUT CONTEXT).** Let $\frac{C}{s}$ mcut($i, \perp$) be a multicut-occurrence such that $C = s_1 \dots s_n$ and let $s_i := \vdash F_1, \dots, F_{k_i}$, we define $C_{F_j}$ to be the sequents linked to the formula $F_j$ with the $\perp$-relation.

We extend this definition to contexts of formulas.

Multicut reduction rules for $\mu$MALL$^\infty$ are given in Appendix A.4.3. Reduction rules for exponential rules of $\mu$LL$^\infty$ can be found in [Sau23] as well as more details on $\mu$MALL$^\infty$ reduction rules.

The systems $\mu$MALL$^\infty$, $\mu$LL$^\infty$ and $\mu$LK$^\infty$ enjoy cut-elimination theorems, proofs can be found in [Sau23]. They are almost strong normalisation theorems, however because of the infinite nature of proofs, strong-normalisation cannot readily be true. This is why a smaller class of reduction sequence is considered: fair reductions.

**DEFINITION 15 (FAIR REDUCTION SEQUENCES).** A reduction sequence $(\pi_i)_{i \in \omega}$ is fair, if for each $\pi_i$ such that there is a reduction $\mathcal{R}$ to a proof $\pi'$, there exist a $j > i$ such that $\pi_j$ does not contain any residual of $\mathcal{R}$.

From [BDKS22] and [Sau23] we obtain the following results:

**THEOREM 2 ($\mu$MALL$^\infty$CUT-ELIMINATION [BDKS22]).** Any fair reduction sequence of $\mu$MALL$^\infty$ proofs converges to a cut-free $\mu$MALL$^\infty$-proof.

Note that a result about (ax)-free version of $\mu$MALL$^\infty$ was proved in [BDS16].

**THEOREM 3 ($\mu$LL$^\infty$CUT-ELIMINATION [SAU23]).** Any fair reduction sequence of $\mu$LL$^\infty$ proofs converges to a cut-free proof of $\mu$LL$^\infty$.

**THEOREM 4 ($\mu$LK$^\infty$ WEAK-NORMALIZATION [SAU23]).** For any proof $\pi$ of $\mu$LK$^\infty$, there exists a reduction sequence $(\pi_i)_{i \in 1+\lambda}$ ($\lambda \in \omega$) such that $\pi_0 = \pi$, which converges to a cut-free proof of $\mu$LK$^\infty$.

### 3 CUT-ELIMINATION FOR $\mu$superLL$^\infty$

We now are interested about proving cut-elimination theorems for $\mu$superLL$^\infty$ instances that satisfy axioms of Table 1. We start by defining all the (mcut) reduction rules of the exponential fragment of $\mu$superLL$^\infty$, the (mcut) reduction rules for the non-exponential fragment are those of $\mu$MALL$^\infty$.

In this section, we fix a set of signatures $\mathcal{E}$ and three relations $\leq_g, \leq_f$ and $\leq_u$ such that each $\sigma \in \mathcal{E}$ satisfies the axioms of Table 1.
## 3.1 (mcut)-elimination steps

In this section, we define the subset of (mcut)-elimination steps of $\mu$superLL$^\infty$ that will be necessary for the linear version of modal $\mu$-calculus, the remaining rules can be found in the long version of the paper.

For the missing steps, see App. B.1

**REMARK 4.** To define (mcut)-elimination steps we will need to use the derivability closure of the signatures, we will also use the definition of $?_{m_i}^{\vec{\sigma}}$ and $?_{c_i}^{\vec{\sigma}}$ (defined in Definition 25 as well as coherent sets of derivations). The rewriting relation $\rightsquigarrow$ will be described as $\pi \rightsquigarrow \Pi'$, where $\Pi'$ is a set of derivations. For that purpose, we will say that a set of derivations is valid if and only if it is non-empty.

To define (mcut)-elimination steps, it is suitable to have a specific notation for the contexts containing only proofs concluded by a promotion. We use notations similar to the notations used in $\mu$LL$^\infty$ cut-elimination proof [Sau23]:

**NOTATION 3** ($!$-CONTEXTS). $C^!$ denotes a list of $\mu$superLL$^\infty$ $(\mathcal{E}, \le_g, \le_f, \le_u)$-proofs which are all concluded by some promotion rule ($!_g, !_f$ or $!_u$).

Given $s \in \{g, f, u\}$, $C^!_s$ denotes a list of $\mu$superLL$^\infty$ $(\mathcal{E}, \le_g, \le_f, \le_u)$-proofs which are all concluded by an an ($!_s$)-rule.

In both cases, $C$ denotes the list of $\mu$superLL$^\infty$ $(\mathcal{E}, \le_g, \le_f, \le_u)$-proofs formed by gathering the immediate subproofs of the last promotion (being either $C^!$, or $C^!_s$).

We now give a series of lemmas that will be used to justify the (mcut)-reduction steps to be defined in the end of the section.

**LEMMA 1 (JUSTIFICATION FOR STEP (COMM!_g)).** If

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

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

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

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

**PROOF SKETCH.** We run through the $C^!$ context and use axioms (axTrans) and (axleqgs) to get that $\sigma \le_g \tau'$ for each signatures $\tau'$ appearing in $C^!$.

As signatures of $\vec{\rho}$ are all appearing in $C^!$, we get that $\sigma \le_g \tau'$. $\square$

See details
in App. B.1

**LEMMA 2 (JUSTIFICATION FOR STEP (COMM!_f)).** If

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

is a $\mu$superLL$^\infty$ $(\mathcal{E}, \le_g, \le_f, \le_u)$-proof with $C^!$ such that all sequents which are concluded with an ($!_g$) have an empty context (ie. no ?-formula), then

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

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

**PROOF SKETCH.** As for Lemma 1, we run through the $C^!$ context and use axiom (axTrans) and (axleqfu) to get that $\sigma \le_f \tau'$ for each signatures $\tau'$ appearing in $C^!$.

As signatures of $\vec{\rho}$ are all appearing in $C^!$, we get that $\sigma \le_f \vec{g}$.

For Lemma 2, the emptyness constraint on the $!_g$ rules ensures that the resulting proof is indeed a $\mu$superLL$^\infty$-proof. $\square$

See details
in App. B.1

The commutative steps of $(?_{m_i})$ and $(?_{c_i})$ are very straightforward, we do not provide any lemma of justification for steps (comm?_m) and (comm?_c).

**LEMMA 3 (JUSTIFICATION FOR STEP (PRINCIPAL?_c)).** If

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

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

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

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

Now, we shall state the lemma for the correctness of the principal reduction for multiplexing, but we need a definition first:

See proof in
App. B.1

**DEFINITION 16.** Let $S^!$ be a sequent of a $\mu$superLL$^\infty$ $(\mathcal{E}, \le_g, \le_f, \le_u)$-context $C^!$, such that $C^!$ is a tree with respect to a cut-relation $\perp$. We define a $\mu$superLL$^\infty$ $(\mathcal{E}, \le_g, \le_f, \le_u)$-context $O_{mpx_S!}(C^!)$ by induction on this relation taking $S^!$ as the root.

We take advantage of this inductive definition to define two sets of sequent $S^?_{C^!,S^!}$ and $S^?_{C^!,S^!}$. Let $C_1^!, \dots, C_n^!$ be the sons of $S^!$, such that $C^! = (S^!_1, (C_1^!, \dots, C_n^!))$, we have two cases:

* $S^! = S^!_g$, then we define $O_{mpx_S}(C^!) := (S, (C_1^!, \dots, C_n^!))$; $S^?_{C^!,S^!} = \emptyset$; $S^?_{C^!,S^!} := C^!$;

* $S^! = S^!_f$ ou $S^! = S^!_u$, then let the root of $C_i^!$ be $S_i^!$, we define $O_{mpx_S}(C^!) := (S, O_{mpx_S^!_1}(C_1^!), \dots, O_{mpx_S^!_n}(C_n^!))$; $S^?_{C^!,S^!} := \{S^!\} \cup \bigcup_{C_i^!,S_i^!} S^?_{C_i^!,S_i^!}$; $S^?_{C^!,S^!} := \bigcup_{C_i^!,S_i^!} S^?_{C_i^!,S_i^!}$.
LEMMA 4 (JUSTIFICATION FOR STEP (COMM$_{?M}$)). Let

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

be a $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$)-proof with $\Gamma$ being sent on $C_{\Delta}$ by $i$; $?\rho'\Gamma'$ being sent on sequents of $S_{C',S'}^{?m}$; and $?\rho''\Gamma''$ being sent on $S_{C',S'}^{?c}$, where $S^j := !\sigma A^\perp, ?\bar{\rho}'\Gamma'$) is the sequent cut-connected to $?\sigma A, \Delta$ on the formula $?\sigma A$. We have that

$$ \frac{C_{\Delta} \quad \overbrace{\vdash A, \dots, A, \Delta}^{i} \quad \overbrace{\underbrace{o_{mpx_S}(C_{?\sigma A})}_{i} \quad \dots \quad o_{mpx_S}(C_{?\sigma A})}^{i}}{\vdash \Gamma, ?\Gamma', \dots, ?\Gamma', ?\rho', ?\Gamma'', \dots, ?\rho'', \Gamma'' \quad \overbrace{\rho''(?m_i)}^{?\bar{\rho}'}} \quad \text{mcut}(i', \perp') \\ \qquad \quad \overbrace{\underbrace{\vdash \Gamma, ?\Gamma', ?\rho', ?\Gamma'', \dots, ?\rho'', \Gamma''}_{i} \quad \overbrace{\rho''(?c_i)}^{?\bar{\rho}''}}^{?\rho'} \quad \text{mcut}(i, \perp) \\ \qquad \quad \overbrace{\underbrace{\vdash \Gamma, ?\rho', ?\Gamma', ?\rho'', \dots, ?\rho'', \Gamma''}_{i} \quad \overbrace{\rho''(?c_i)}^{?\bar{\rho}''}}^{?\rho'} \quad \text{mcut}(i, \perp) $$

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

See proof in App. B.1

REMARK 5. The previous lemma deserves some comments and explanations. Notably, the lemma capture the cases of usual dereliction and weakening. Taking the following example with dereliction instead of $?m_1$:

$$ \frac{\begin{array}{c} \vdash A, \Delta \\ \vdash ?A, \Delta \end{array} \quad ?d \quad \begin{array}{c} \vdash A^\perp, B, C \\ \vdash !A^\perp, ?B, ?C \end{array} \quad !f \quad \begin{array}{c} \vdash B^\perp, ?D, ?E \\ \vdash !B^\perp, ?D, ?E \end{array} \quad !g \quad \begin{array}{c} \vdash D^\perp, F \\ \vdash !D^\perp, ?F \end{array} \quad !f \quad \text{mcut}(i, \perp) \\ \qquad \quad \vdash ?C, ?E, ?F, \Delta \end{array} $$

$$ \leadsto \frac{\begin{array}{c} \vdash A, \Delta \\ \vdash ?A, \Delta \end{array} \quad ?d \quad \begin{array}{c} \vdash A^\perp, B, C \\ \vdash B^\perp, ?D, ?E \end{array} \quad \frac{\begin{array}{c} \vdash D^\perp, F \\ \vdash !D^\perp, ?F \end{array}}{\text{mcut}(i, \perp)} \quad !f \\ \qquad \quad \frac{\begin{array}{c} \vdash C, ?E, ?F, \Delta \\ \vdash ?C, ?E, ?F, \Delta \end{array}}{?d} \end{array} $$

Note that $?c_i$ is the empty derivation. We can understand here the definitions of $O_{mpx_S}(C')$, $S_{C',S'}^{?c}$ and $S_{C',S'}^{?m}$. All the ($!f$) or ($!u$) preceding an ($!g$) are removed during the cut-elimination step, but promotions that comes after and ($!g$) still have to be applied as the $!$-connective is still there.

Occurrences that are in the context of an ($!f$) or an ($!u$) coming before an ($!g$) are derilicted and thus in $S_{C',S'}^{?m}$. They need to be as this type of promotions removes the exponential connective from the context.

Occurrences that are in the context of an ($!g$) are not derilicted as their exponential connectives is not removed through an ($!g$) promotion. Neither are occurrences of an ($!f$) or ($!u$) that follows an ($!g$) as their promotions are still to be applied. These occurrences are therefore all in $S_{C',S'}^{?c}$.

The following lemma is stated only for the case of steps defined in figure 6 and 7. See App.B.1 for more details.

LEMMA 5 (CORRECTNESS OF THE (MCUT)-REDUCTION SYSTEM). The left proofs and right set of proofs (we identify single proof derivation to the singleton containing it) of the rules of figures 6 and 7 are valid.

PROOF. We use lemmas 1, 2, 4, 3, commutative steps for contraction and multiplexing are obvious. □

## 3.2 Translating $\mu$superLL$^{\infty}$into $\mu$LL$^{\infty}$

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

DEFINITION 17 (TRANSLATION OF FORMULAS). The translation $(-)^{\circ}$ is defined by induction on formula by:

$$ c(F_1, \dots, F_n)^{\circ} := c(F_1^{\circ}, \dots, F_n^{\circ}) \qquad X^{\circ} := X $$

$$ \forall \sigma, (?\sigma A)^{\circ} := ?A^{\circ} \qquad a^{\circ} := a $$

$$ (!\sigma A)^{\circ} := !A^{\circ}. $$

for c any non-exponential connectives.

We then define proof translations:

DEFINITION 18 (PROOF TRANSLATIONS). We define the translations for exponential rules of $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$) into $\mu$LL$^{\infty}$ as sets of derivations. The set of the translations of another rule (r) is just the singleton $\{r\}$.

The set of translations of each rules will be given by all the derivations obtained from Figure 8 by commuting the ($?d$) and ($?c$) rules.

Proof translations $\pi^{\circ}$ of $\pi$ is the set of proofs coinductively defined on $\pi$ from rule translations.

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

LEMMA 6 (ROBUSTNESS OF THE $(-)^{\circ}$ TRANSLATION TO VALIDITY). Valid pre-proofs $\pi$ translates to valid pre-proofs $\pi^{\circ}$. Conversely, if $\pi^{\circ}$ is a valid pre-proof, then $\pi$ is also a valid pre-proof.

As one-step mcut-reductions of $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$) are defined from proofs to set of proofs, we define a sequence of mcut-reduction ($\pi_i$)$_{i \in 1+\lambda}$ ($\lambda \in \omega$) to be a sequence of proofs such that for each $i \in 1+\lambda$, there is a $\Pi_{i+1}$ such that $\pi_i \rightsquigarrow \Pi_{i+1}$ and $\pi_{i+1} \in \Pi_{i+1}$. The goal of this section is to prove that each such fair reductions sequences converges to a cut-free proof. We have to make sure (mcut)-reduction sequences are robust under this translation. In our proof of the final theorem, we also need one-step reduction-rules to be simulated by a finite number of reduction steps in the translation.

LEMMA 7. Let $\pi_0$ be a $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$) proof and let $\pi_0 \rightsquigarrow \Pi_1$ be a $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$) step of reduction. For each $\pi_1 \in \Pi_1$ and for each $\pi'_0 \in \pi_0^0$, there exist a finite number of $\mu$LL$^{\infty}$ proofs $\theta_0, \dots, \theta_n$ such that $\theta_0 \to \dots \to \theta_n$, $\pi'_0 = \theta_0$ and $\theta_n \in \pi_1^0$ up to a finite number of rule permutations, done only on rules that just permuted down the (mcut).

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

See detail in App.B.1
Cut-elimination for the circular modal mu-calculus:
linear logic and super exponentials to the rescue

<figure><img src="image_7.png" /><figcaption>Figure 6: Commutative cut-elimination steps of the exponential fragment of μsuperLL$^{∞}$ (cases specific to μLL$^{∞}$□)</figcaption></figure>

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

with S being the sequent cut-connected to ?$_{σ}$A, Δ on the formula ?$_{σ}$A.

<caption>Figure 7: Principal cut-elimination steps of the exponential fragment of μsuperLL$^{∞}$ (cases specific to μLL$^{∞}$□)</caption>

the proof is translated, for instance the following (opened) proof:

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

has two translations:

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

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

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

LEMMA 8. Let $n \in \mathbb{N}$, let $d_1, \dots, d_n \in \mathbb{N}$ and let $p_1, \dots, p_n \in \{0, 1\}$. Let $\pi$ be a $\mu LL^\infty$-proof concluded by an (mcut)-rule, on top of which there is a list of $n$ proofs $\pi_1, \dots, \pi_n$. We ask for each $\pi_i$ to be of one of the following forms depending on $p_i$:

* If $p_i = 1$, the $d_i + 1$ last rules of $\pi_i$ are $d_i$ derelictions and then a promotion rule. We ask for the principal formula of
<figure><img src="image_9.png" /><figcaption>Figure 8: Exponential rule translations from $\mu$superLL$^{\infty}(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ into $\mu$LL$^{\infty}$</figcaption></figure>

this promotion to be either a formula of the conclusion, or to be cut with a formula being principal in a proof $\pi_j$ on one of the last $d_j + p_j$ rules.

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

In each of these two cases, we ask for $\pi_i$ that each principal formulas of the $d_i$ derelictions to be either a formula of the conclusion of the multicut, either a cut-formula being cut with a formula appearing in $\pi_j$ such that $p_j = 1$.

$\pi$ reduces through a finite number of mcut-reductions to a proof where each of the last $d_i + p_i$ rules either were eliminated by a ($!p_i/?!d_i$)-principal case, or were commuted below the cut.

See proof in
App. 26

**PROOF OF LEMMA 7.** Reductions from the non-exponential part of $\mu$superLL$^{\infty}(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ translate easily to one step of reduction in $\mu$LL$^{\infty}$. To prove the result on exponential part, we will describe each translation of the reductions of Figures 6 and 7 and make sure that they are finite. The other cases, as well as more details on this proof are given in Appendix B.2.3. Note that for the commutative steps no commutation of rules is necessary.

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

* Step (comm$^1_f$). We use lemma 8, which applies to our step by first taking all $p_i = 1$ and $d_i$ to be the number of formulas in the context of each promotion.

* Step (comm$_2$). We must distinguish the cases based on i:

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

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

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

* Step (comm$_2$). This step translates to $i - 1$ commutations of (?_c).

* Step (principal$_2$). This step translates to $i - 1$ contraction principal cases, creating $i - 1$ contractions on each formula of the context that can be permuted together to get the translation of any of the derivations of $?_{\bar{c}_i}$. Note that for $i = 2$ no rule permutation are needed. (That is the case of the usual binary contraction.)

* Step (principal$_2$). This step translates in two phases:

(1) First $i - 1$ contraction principal cases;

(2) followed by #($S^2_{C',S'}$) (?_d/!)-principal cases, and #($\Gamma''$) dereliction commutative cases.

To prove the second phase we re-use lemma 8 as for steps (comm$^2_{-u}$) and (comm$^1_{u}$). We obtain a proof containing contractions and derelictions on formulas of the conclusions that can be permuted to obtain the desired property. Note that if $i = 0$, no rule permutations are needed. (That is the case of usual weakening.)

□

Now that we know that a step of (mcut)-reduction in $\mu$superLL$^{\infty}$ translates to some steps of (mcut)-reduction $\mu$LL$^{\infty}$, we have to control the fairness, which is the purpose of the following lemma:

**LEMMA 9 (COMPLETENESS OF THE (MCUT)-REDUCTION SYSTEM).**
If there is a $\mu$LL$^{\infty}$-redex $\mathcal{R}$ sending $\pi^\circ$ to $\pi^{\circ'}$ then there is also a $\mu$superLL$^{\infty}(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-redex $\mathcal{R}'$ sending $\pi$ to a proof $\pi''$, such that in the translation of $\mathcal{R}'$, $\mathcal{R}$ is reduced.

**PROOF.** The proof of this lemma is made in appendix B.2.4 as we need the full cut-steps of $\mu$superLL$^{\infty}$ to show that they are complete. □

**COROLLARY 1.** For every fair $\mu$superLL$^{\infty}(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ reduction sequences $(\pi_i)_{i \in \omega}$, there exists:

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

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

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

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

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

* For $i = 0$: we take any $\theta_0(= \pi'_0)$ in $\pi_0^\circ$, $\varphi(0) = 0$ and $k_0 = 0$:

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

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

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

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

Finally, we have:

**THEOREM 5.** Every fair (mcut)-reduction sequence of $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ converges to a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ cut-free proof.

**PROOF.** Consider a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ fair reduction sequence $(\pi_i)_{i \in 1+\lambda}$ ($\lambda \in \omega + 1$). If the sequence is finite, we use lemma 7 and we are done. If the sequence is infinite, using corollary 1 we get a fair infinite $\mu$LL$^\infty$ reduction sequence $(\theta_i)_{i \in \omega}$ and a sequence $(\varphi(i))_{i \in \omega}$ of natural numbers. By theorem 3, we know that $(\theta_i)_{i \in \omega}$ converges to a cut-free proof $\theta$ of $\mu$LL$^\infty$.

We now prove that the sequence $(\pi_i)_{i \in \omega}$ converges to a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ pre-proof $\pi$ such that $\pi^\circ = \theta$ up to a permutation of rules (the permutations of one particular rule being finite).

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

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

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

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

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

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

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

**COROLLARY 2 (CUT ELIMINATION FOR superLL).** *Cut elimination holds for superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) as soon as the 8 cut-elimination axioms of definition 1 are satisfied.*

**PROOF.** Any superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$)-proof is also $\mu$superLL$^\infty(\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$)-proof therefore any sequence of (mcut)-reductions converges to a cut-free proof. A cut-free proof of sequents containing only superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$)-formulas and valid rules from $\mu$superLL$^\infty(\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) is necessarily a superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) (cut-free) proof. $\square$

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

# 4 ON THE CUT-ELIMINATION OF THE MODAL μ-CALCULUS

As discussed in the introduction, to prove the cut-elimination of μLK<sub>⊤</sub><sup>∞</sup>, our approach will consist in encoding μLK<sub>⊤</sub><sup>∞</sup> into a new, more structured system: μLL<sub>⊤</sub><sup>∞</sup>. The system μLL<sub>⊤</sub><sup>∞</sup> is an instance of μsuperLL<sup>∞</sup>, therefore we get cut-elimination directly as a corollary of Theorem 5. However, by looking in the details of the proof, we can state some results in a slightly more general way.

## 4.1 A linear-logical modal μ-calculus

We start by giving a formal definition of the linear-logical modal μ-calculus: μLL<sub>⊤</sub><sup>∞</sup>. The term logical makes emphasis on the fact that the logic is linear in the use of resources, not in the structures of its models as in LTL or linear-time μ-calculus [Sti92].

DEFINITION 19 (μ-SIGNATURE FOR μLL<sub>⊤</sub><sup>∞</sup>). We define two μ-signatures for our systems:

* one-sided $\mu LL_{\square}^{\infty}: C_{LL_{\square 1}} := C_{LL_1} \cup \{(\square, +), (\diamond, +)\}$;

* two-sided $\mu LL_{\square}^{\infty}: C_{LL_{\square 2}} := C_{LL_2} \cup \{(\square, +), (\diamond, +)\}$.

From this μ-signature and definition 4, we get the formulas of μLL<sub>⊤</sub><sup>∞</sup>. Rules for our system will be rules of μLL<sup>∞</sup> together with:

$$ \frac{\vdash A, \Gamma \quad \Box p,}{\vdash \Box A, \diamond \Gamma} \qquad \frac{\vdash \diamond A, \diamond A, \Gamma \quad \diamond c,}{\vdash \diamond A, \Gamma} \qquad \frac{\vdash \Gamma \quad \diamond A, \Gamma \quad \diamond w,}{\vdash ! A, ? \Gamma, \diamond \Delta} \qquad \frac{\vdash A, ? \Gamma, \diamond \Delta \quad !^{\diamond} p}{\vdash ! A, ? \Gamma, \diamond \Delta} $$

From these rules, we define the sequents, pre-proofs and proofs in the same way as for systems of Section 2.1. Negation is already defined for a larger set of formulas.

PROPOSITION 2. The system $\mu LL_{\square}^{\infty}$ is the system $\mu superLL^{\infty}(\mathcal{E}, \leq_g)$, $\leq_f \leq u)$ such that:

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

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

* $\bullet \leq_g \bullet; \bullet \leq_g \star, \star \leq_f \star$, and all couples for the three relations $\leq_g, \leq_f$ and $\leq_u$ being false.

This system is $\mu LL_{\square}^{\infty}$ when taking:

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

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

## 4.2 Cut-elimination for μLL<sub>⊤</sub><sup>∞</sup>

To prove cut-elimination for μLL<sub>⊤</sub><sup>∞</sup>, we will translate formulas and proofs and (mcut)-steps of μLL<sub>⊤</sub><sup>∞</sup> into μLL<sup>∞</sup> and use the cut-elimination results from [Sau23] (as we did for μsuperLL<sup>∞</sup>). In [Sau23], exponential formulas, proofs and cut-steps are encoded into μMALL<sup>∞</sup>, following

$$ (\neg A)^{\bullet} = \mu X.(A^{\bullet} \oplus (\bot \oplus (X \otimes X))) \quad (!A)^{\bullet} = \nu X.(A^{\bullet} \& (1 \& (X \otimes X))) $$

Contrary to μsuperLL<sup>∞</sup> which deals with many exponentials, μLL<sub>⊤</sub><sup>∞</sup> only has two. Therefore we could have made the choice to encode the modalities of μLL<sub>⊤</sub><sup>∞</sup> directly into μMALL<sup>∞</sup>, replaying the proof of [Sau23] to get cut-elimination. However using the μLL<sup>∞</sup> cut-elimination theorem as such, makes our approach more modular

and more easy to adapt to future extensions of μLL<sup>∞</sup> validity condition or variants of its cut-elimination proof.

The translation of μLL<sub>⊤</sub><sup>∞</sup> into μLL<sup>∞</sup> is done using the translation from μsuperLL<sup>∞</sup> into μLL<sup>∞</sup> in section 3.2. We recall the translations of $\diamond, \Box$-formulas: $(\diamond A)^{\circ} := ?A^{\circ}$ and $(\Box A)^{\circ} := !A^{\circ}$.

Translation of structural rules for $\diamond, (\diamond c)$ and $(\diamond w)$, are the contraction and the weakening of $?$. Translations of the modal rule are given by (where the derelictions can permute with each other):

$$ \frac{\vdash A, \Gamma \quad \Box}{\vdash \Box A, \diamond \Gamma} \rightsquigarrow \frac{\vdash A^{\circ}, \Gamma^{\circ} \quad (\neg d)^{\star}}{\vdash ! A^{\circ}, ? \Gamma^{\circ} \quad !^{\diamond} p} $$

From lemma 6, this translation preserves validity both ways. Finally we have to make sure (mcut)-reduction sequences are robust under this translation. In our proof of the final theorem, we also need one-step reduction-rules to be simulated by a finite number of reduction steps in the translation:

LEMMA 10. Consider a $\mu LL_{\square}^{\infty}$ reduction step $\pi_0 \rightsquigarrow \Pi_1$. For each $\pi_1 \in \Pi_1$ and each $\pi_0^\circ \in \pi_0^\circ$, there exist a finite number of $\mu LL^{\infty}$ proofs $\theta_0, \dots, \theta_n$ such that:

$$ \pi_0^\circ \ni \pi_0' = \theta_0, \quad \theta_n \in \pi_1^\circ, \quad \text{and} \quad \theta_0 \to \dots \to \theta_n. $$

PROOF. To prove this lemma, we replay the proof of lemma 8. Noticing that the two cases where we need to perform rule permutation are the principal cases of the multiplexing and of the contraction. However we do not need to do rule permutation for the $(?_{c_i})$ principal case for $i = 2$. Neither, do we for $(?_{m_0})$. For $(?_{m_1})$ things are bit more tricky, we notice that in this particular instance of μsuperLL<sup>∞</sup> ($\mathcal{E}, \leq_g, \leq_f, \leq_u$) (taking notations from proposition 2, we only perform $?_{m_1}$ on $?_{\bullet}$-formulas. Moreover, we never have $\bullet \leq_f \sigma$ for any $\sigma \in \{\bullet, \star\}$, therefore in the left proof of the $?_{m_1}$ principal case, $O_{mpx_S}(C_{?_{\sigma}A}^!)$ is $C_{?_{\sigma}A}^!$ and $\Gamma''$ is empty. We therefore have only $?_{?_{c_1}^\sigma}^-$-rules that appears under the cut, which is the derivation containing 0 rules. $\square$

We use the previous lemma, as well as Lemma 9 to prove the following:

COROLLARY 3. For every fair $\mu LL_{\square}^{\infty}$ reduction sequence $(\pi_i)_{i \in \mathbb{N}}$, we have:

* a fair μLL<sup>∞</sup> reduction sequence $(\theta_i)_{i \in \omega}$;

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

* for each $i$, $\theta_{\varphi(i)} \in \pi_i^\circ$.

PROOF. The proof is done the same way than Corollary 1 but using Lemma 10 to avoid weakening the statement by authorizing permutation hypothesis. $\square$

Finally, we have:

THEOREM 6. Every fair reduction sequence of $\mu LL_{\square}^{\infty}$ converges to a $\mu LL_{\square}^{\infty}$ proof.

PROOF. To prove it, we can replay the proof from Theorem 5, using the, specific to μLL<sub>⊤</sub><sup>∞</sup>, Corollary 3, but we do not need to. We apply Theorem 5 for the instance of μsuperLL<sup>∞</sup> of Proposition 2. $\square$

See detail in
app. C.1.2
## 4.3 Cut-elimination of $\mu LK_{\square}^{\infty}$

We extend the translation from [Sau23] of $\mu LK^{\infty}$ to $\mu LK_{\square}^{\infty}$ to obtain a translation into $\mu LL_{\square}^{\infty}$. We define out translation for the two-sided version of both systems:

**DEFINITION 20 (LINEAR TRANSLATION OF $\mu LK_{\square}^{\infty}$).** We define the translation $(-)^{\bullet}$ from formulas of $\mu LK_{\square}^{\infty}$ to formulas of $\mu LL_{\square}^{\infty}$ by induction on these formulas in the following way:

$$ (A_1 \to A_2)^{\bullet} := !(?A_1^{\bullet} \dashv ?A_2^{\bullet}) \quad X^{\bullet} := !X \quad (\mu X.A)^{\bullet} := !\mu X.?A^{\bullet} $$

$$ (A_1 \wedge A_2)^{\bullet} := !(?A_1^{\bullet} \wedge ?A_2^{\bullet}) \quad T^{\bullet} := !T \quad (vX.A)^{\bullet} := !vX.?A^{\bullet} $$

$$ (A_1 \vee A_2)^{\bullet} := !(?A_1^{\bullet} \oplus ?A_2^{\bullet}) \quad F^{\bullet} := !0 \quad (\diamond A)^{\bullet} := !\diamond?A^{\bullet} $$

$$ (A^{\perp})^{\bullet} := !(?A^{\bullet})^{\perp} \quad a^{\bullet} := !a \quad (\Box A)^{\bullet} := !\Box?!A^{\bullet} $$

We also have a translation for sequents: $(\Gamma \vdash \Delta)^{\bullet} := \Gamma^{\bullet} \vdash ?\Delta^{\bullet}$.

See App. C.1.1 for more details

We give the translations of modal rules in Figure 9. We then define translations of proofs coinductively on the proofs using the translation of each rules. As the smallest formula (for inclusion ordering) of a totally ordered set of translations is the translation of the smallest formula, and that a branch of $\pi^{\bullet}$ contains all the translations of threads from $\pi$ and vice-versa, we have the following:

**LEMMA 11 (ROBUSTNESS OF $(-)^{\bullet}$ TO VALIDITY).** If $\pi$ is a valid pre-proof, then $\pi^{\bullet}$ also and vice versa.

We define a translation $SK(-)$ going from $\mu LL_{\square}^{\infty}$ formulas and pre-proofs to $\mu LK_{\square}^{\infty}$ formulas and pre-proofs, by forgetting linear information from formulas and pre-proofs (ie erasing exponential modalities, as well as dereliction and promotion, and projecting other connectives or inferences to the corresponding $\mu LK_{\square}^{\infty}$ connectives and inferences). This straightforwardly extends the $\mu LK^{\infty}$ case [Sau23] with the modal cases. $SK(-)$ preserves validity and it is compatible with $(-)^{\bullet}$: for each proof $\pi$ of $\mu LK_{\square}^{\infty}$, we have that $SK(\pi^{\bullet}) = \pi$.

See details in C.2.1

**DEFINITION 21 ((MCUT)-REWRITING SYSTEM OF $\mu LK_{\square}^{\infty}$).** We define (mcut)-rewriting system of $\mu LK_{\square}^{\infty}$ to be the (mcut)-system obtained from $\mu LL_{\square}^{\infty}$ (mcut)-system by forgetting the linear information of proofs of this system.

Finally, we have the following theorem:

**THEOREM 7.** *The (mcut)-reduction system of $\mu LK_{\square}^{\infty}$ is an infinitary weak-normalizing reduction relation.*

**PROOF.** Consider a $\mu LK_{\square}^{\infty}$ proof $\pi$ and a fair reduction sequence $\sigma_{\text{L}}$ from $\pi^{\bullet}$. By theorem 6, $\sigma_{\text{L}}$ converges to a cut-free $\mu LL_{\square}^{\infty}$ proof.

By applying $SK(-)$ to each proof in the sequence, we obtain a sequence of $\mu LK_{\square}^{\infty}$ valid proofs which are all valid and such that either $SK(\pi_i) = SK(\pi_{i+1})$ or $SK(\pi_i)$ reduces to $SK(\pi_{i+1})$ with one step of $\mu LK_{\square}^{\infty}$ mcut-reduction. By dropping the equality cases, we obtain a $\mu LK_{\square}^{\infty}$ cut-reduction sequence $\sigma_K$ that is infinite and converges to a valid, cut-free $\mu LK_{\square}^{\infty}$ proof. $\square$

## 4.4 Finitary circular cut-elimination for $\mu LK_{\square}^{\infty}$

The infinitary cut-elimination theorem for non-wellfounded $\mu LK_{\square}^{\infty}$ proofs, established in the previous section, can be extended to circular $\mu LK_{\square}^{\infty}$ proofs, achieving a true weak-normalization (that is, finitary) result by allowing both cut-reduction and back-edge introduction rules. Let us explain how we proceed.

First let us notice that, while we established in the previous sections the cut-elimination for the non-wellfounded $\mu$-calculus (in the form of an infinitary weak-normalization result) in proof systems where sequents are (possibly pairs of) lists of formulas, it is straightforward to derive from this a similar infinitary weak-normalization result for $\mu LK_{\square}^{\infty}$ presented with sequents as sets of formulas. For this, one can simply project the cut-reduction relation for sequents-as-lists to a relation between $\mu LK_{\square}^{\infty}$ non-wellfounded proofs for sequents-as-sets by using the forgetful map from lists to sets and notice that any valid proof in set-based $\mu LK_{\square}^{\infty}$ is the erasure of a valid proof in list-based $\mu LK_{\square}^{\infty}$ from which the infinitary weak normalization results follows.

Second, let us just recall that it is well-known that non-wellfounded cut-free proofs for $\mu LK_{\square}^{\infty}$ with sequents-as-sets can be regularized, by using an operation that discards a (potentially infinite) subtree and replaces it with a back-edge to a lower sequent, while preserving validity. This is due to the fact that only finitely many distinct sequents can occur in such a cut-free set-based derivation.

From the above two points one can obviously regularize the (non-wellfounded) cut-free proof obtained thanks to the infinitary weak-normalization mentioned above. In fact, one can do better and obtain a purely finitary cut-elimination for the circular modal-mu-calculus. Indeed, while the regularization process sketched above assumes proofs to be cut-free, it is possible to inline it in the cut-reduction process and apply it eagerly. We outline this now.

Let us consider finite representations of circular proofs (ie finite trees with back-edges) endowed with the following reduction $\mapsto$ rule which is structured in three types of rules:

**cut-reduction steps** the usual cut-elimination reduction for $\mu LK_{\square}^{\infty}$ set-based proofs;

**back-edge unfolding** a rule that unfolds a finite representation when the premise of a cut is the target of a back-edge;

**back-edge creation** a back-edge creation rule that replaces a bottom-most cut with a back-edge to a lower sequent as soon as it can be done according to the regularization process for cut-free non-wellfounded proofs described above.

Finally, we have the following, purely finitary weak-normalization theorem:

**THEOREM 4.1.** $\mapsto$ is a weakly normalizing reduction relation on circular $\mu LK_{\square}^{\infty}$ derivations the normal form of which are cut-free circular proofs.

## 5 CONCLUSION

We have introduced a family of logical systems, $\mu$superLL$^{\infty}$, and proved a syntactic cut-elimination theorem for them. Considering $\mu LL_{\square}^{\infty}$, one instance of $\mu$superLL$^{\infty}$, and a linear translation of $\mu LK_{\square}^{\infty}$ in this calculus, we established a cut-elimination theorem the non-wellfounded sequent calculus for the modal $\mu$-calculus, $\mu LK_{\square}^{\infty}$. From this result, a finitary weak normalization theorem for the circular fragment of $\mu LK_{\square}^{\infty}$ is finally provided.

From the linear logic-theoretic point of view, our system $\mu$superLL$^{\infty}$ subsumes various fixed-point versions of existing linear logic systems (extended most known light logics with least and greatest fixed-points and a non-wellfounded proof system) and we have a relatively simple and uniform proof of cut-elimination for each of them.
<figure><img src="image_11.png" /><figcaption>Figure 9: Translation of the modal rule into μLL<sup>∞</sup></figcaption></figure>

From the modal μ-calculus-theoretic point of view, this is the first result of a full syntactic cut-elimination for a proof system for the whole modal μ-calculus. We provide this result in the non-wellfounded system with sequents as lists of formulas as well as in the circular fragment, where sequents are sets of formulas. As Linear Logic has a particularly fine-grained proof theory, we conjecture that one can construct a non-trivial denotational semantics for the proofs of μLK<sup>∞</sup> from the linear translation. However, one cannot hope the same for the circular version as, for instance, sequents are translated into sets of formulas.

In our opinion, this work presents a new and non-trivial application of linear logic to modal μ-calculus, developing proof theories in both domains and highlighting the potential for cross-fertilization for the two communities.

The μsuperLL<sup>∞</sup> system as defined in this paper does not cover the digging rule as is done in [BL21]. Asking for the digging rule on modal formulas is equivalent to axiom 4 of modal logic. Other axioms of modal logic could be seen as rules from Linear Logic, such as axiom T in modal logic, and co-dereliction rules from Differential Linear Logic.

Another natural future work will be to fully cover super exponentials from [BL21], and even bigger systems, capturing more rules from Linear Logic and transferring its proof-theoretic properties to other logical systems.

REFERENCES

[AL17] Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In *2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science* (LICS), pages 1–12, 2017.

[BDKS22] David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22*, New York, NY, USA, 2022. Association for Computing Machinery.

[BDS16] David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In *CSL 2016*, volume 62 of LIPICS, pages 42:1–42:17, 2016.

[BL21] Esaie Bauer and Olivier Laurent. Super exponentials in linear logic. *Electronic Proceedings in Theoretical Computer Science*, 353:50–73, December 2021.

[BS12] 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.

[CH00] Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In *ICFP 2000*, pages 233–243. ACM, 2000.

[D]03 Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. 183(1):123–137, May 2003.

[D]S97 Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: Linear logic. *J. Symb. Log.*, 62(3):755–807, 1997.

[Dou17] Amina Doumane. *On the infinitary proof theory of logics with fixed points*. Phd thesis, Paris Diderot University, 2017.

[Gir87] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1–102, 1987.

[Gir98] Jean-Yves Girard. Light linear logic. 143(2):175–204, June 1998.

[JKS08] Gerhard Jäger, Mathis Kretz, and Thomas Studer. Canonical completeness of infinitary μ. *The Journal of Logic and Algebraic Programming*, 76(2):270–292, 2008. Logic and Information: From Logic to Constructive Reasoning.

[Koz83] Dexter Kozen. Results on the propositional mu-calculus. *Theor. Comput. Sci.*, 27:333–354, 1983.

[Laf04] Yves Lafont. Soft linear logic and polynomial time. *Theoretical Computer Science*, 318(1–2):163–180, June 2004.

[Min12] Grigori Mints. Effective cut-elimination for a fragment of modal mu-calculus. *Studia Logica: An International Journal for Symbolic Logic*, 100(1/2):279–287, 2012.

[MS12] Grigori Mints and Thomas Studer. Cut-elimination for the mu-calculus with one variable. *Electronic Proceedings in Theoretical Computer Science*, 77:47–54, February 2012.

[NM09] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In *PPDP 2009*, page 129–140, New York, NY, USA, 2009. ACM.

[NW96] Damian Niwiński and Igor Walukiewicz. Games for the μ-calculus. *Theoretical Computer Science*, 163(1):99–116, 1996.

[Sau23] Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points. TABLEAUX '23. Springer, 2023.

[Sti92] Colin Stirling. Modal and Temporal Logics. In *Handbook of Logic in Computer Science*. Oxford University Press, 12 1992.
# A APPENDIX ON THE BACKGROUND SECTION

## A.1 Details on the section 2.1

### A.1.1 Involutivity of the negation, definition 5.
We recall the definition of the involutive negation:

**DEFINITION 22 (NEGATION).** Given a $\mu$-signature C containing only connectives with positive polarity. Let $\iota$ be an involution on C such that if $\iota(c, p) = (c', p')$ then $p = p'$. Let $\mathcal{A}$ be a set of atoms with another involution $\kappa$ on it and let $\mathcal{V}$ be a set of variables. We define $(-)^{\perp(\iota, \kappa)}$ to be the involution on formulas satisfying:

$$X^{\perp(\iota, \kappa)} = X \qquad c(F_1, \dots, F_n)^{\perp(\iota, \kappa)} = \iota(c)(F_1^{\perp(\iota, \kappa)}, \dots, F_n^{\perp(\iota, \kappa)})$$

$$a^{\perp(\iota, \kappa)} = \kappa(a) \qquad (\mu X.F)^{\perp(\iota, \kappa)} = \nu X.F^{\perp(\iota, \kappa)}$$

**INVOLUTIVITY OF THE NEGATION.** We prove that this involution exists, we define it by induction on formulas. All cases are given by the definition above, except for $\nu X.F$ which will be:

$$(\nu X.F)^{\perp(\iota, \kappa)} = \mu X.F^{\perp(\iota, \kappa)}.$$

We prove by induction on formulas that it is indeed an involution:

* $(X \in \mathcal{V})$. If our formula is a variable $X$, then $X^{\perp(\iota, \kappa)} = X$ and so $(X^{\perp(\iota, \kappa)})^{\perp(\iota, \kappa)} = X$.

* $(a \in \mathcal{A})$. If our formula is an atom, we use involutivity of $\kappa$.

* $(c(F_1, \dots, F_n))$. For the connective case, involutivity of $\iota$ give us $\iota(\iota(c)) = c$ and induction hypothesis on $F_1, \dots, F_n$ to get:

$$\begin{align*}
& (c(F_1, \dots, F_n)^{\perp(\iota, \kappa)})^{\perp(\iota, \kappa)} \\
&= (\iota(c)(F_1^{\perp(\iota, \kappa)}, \dots, F_n^{\perp(\iota, \kappa)}))^{\perp(\iota, \kappa)} \\
&= (\iota(c)(F_1^{\perp(\iota, \kappa)}, \dots, F_n^{\perp(\iota, \kappa)}))^{\perp(\iota, \kappa)} \\
&= \iota(\iota(c))((F_1^{\perp(\iota, \kappa)})^{\perp(\iota, \kappa)}, \dots, (F_n^{\perp(\iota, \kappa)})^{\perp(\iota, \kappa)}) \\
&= c(F_1, \dots, F_n).
\end{align*}$$

* $(\delta X.F) (\delta \in \{\mu, \nu\})$. We set $\iota(\mu) = \nu$ and $\iota(\nu) = \mu$ and we have:

$$\begin{align*}
& ((\delta X.F)^{\perp(\iota, \kappa)})^{\perp(\iota, \kappa)} \\
&= (\iota(\delta)X.F^{\perp(\iota, \kappa)})^{\perp(\iota, \kappa)} \\
&= \iota(\iota(\delta))X.(F^{\perp})^{\perp} \\
&= \delta X.F.
\end{align*}$$

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

### A.1.2 Fischer-Ladner sub-formula definition.

**DEFINITION 23 (FISCHER-LADNER SUB-FORMULA).** Let $F$ be a formula on a signature $C$, the set of Fischer-Ladner sub-occurrences of $F$ is the smallest set $FL(F)$ containing $F$ itself and such that:

(i) If $c(F_1, \dots, F_n) \in FL(F)$ then $F_1, \dots, F_n \in FL(F)$ with $(c, p) \in C$.

(ii) If $\delta X.G \in FL(F)$ then $G[X := \delta X.G] \in FL(F)$ with $\delta \in \{\mu, \nu\}$.

## A.2 Details on the sequent calculi section 2.2

### A.2.1 Two-sided modality rules.
Rules of two-sided $\mu$LK$^{\infty}$ are the rules of $\mu$LK$^{\infty}$ together with rules of figure 10.

## A.3 Details on super exponential systems

### A.3.1 Two-sided Exponential rules for superLL.
Exponential rules of two-sided superLL($\mathcal{E}$, $\leq_g$, $\leq_f$, $\leq_u$) and $\mu$superLL$^{\infty}$(\mathcal{E}, $\leq_g$, $\leq_f$, $\leq_u$) are the same and are defined in figure 11.

### A.3.2 Details on the notion of coherent set of derivations.

**DEFINITION 24 (COHERENT SET OF DERIVATIONS).** A coherent set of derivations $S$ is a set of finite (possibly open) derivations, such that all the derivations have the same root sequents and the same list of open sequents. If $D_1, \dots, D_n$ (resp. $D_1, \dots, D_n, \dots$) are $n$ coherent sets (resp. an $\omega$-sequence of sets) of derivations such that each elements of $D_i$ has one open sequent equal to $O_i$ and a root equal to $R_i$, and such that for each $i \in [1, n-1]$ (resp. each $i \ge 1$), $O_i = R_{i+1}$, then we denote by:

$$\begin{array}{ccc}
\frac{O_n}{O_{n-1}} & D_n & \\
\vdots & & \\
\frac{O_1}{R_1} & D_1 & \\
\vdots & & \\
\frac{O_1}{R_1} & D_1 & \\
\end{array}
\quad \text{resp.} \quad
\begin{array}{ccc}
\vdots & \\
\frac{O_n}{O_{n-1}} & D_n \\
\vdots & \\
\frac{O_1}{R_1} & D_1 \\
\vdots & \\
\frac{O_1}{R_1} & D_1
\end{array}$$

the (coherent) set of derivations containing each

$$\begin{array}{ccc}
\frac{O_n}{O_{n-1}} & d_n & \\
\vdots & & \\
\frac{O_1}{R_1} & d_1 & \\
\vdots & & \\
\frac{O_1}{R_1} & d_1 & \\
\end{array}
\quad \text{resp.} \quad
\begin{array}{ccc}
\vdots & \\
\frac{O_n}{O_{n-1}} & d_n \\
\vdots & \\
\frac{O_1}{R_1} & d_1 \\
\vdots & \\
\frac{O_1}{R_1} & d_1
\end{array}$$

with $d_i \in D_i$.

We identify the singleton $\{d_i\}$ with the derivation $d_i$.

### A.3.3 Details on the derivability closure.

**DEFINITION 25.** Let $\sigma$ be a signature. For each $i \in \mathbb{N}$, we define two sets of derivations $\sigma_{c_i}^\bar{\sigma}$ and $\sigma_{m_i}^\bar{\sigma}$ by induction on $i$. We define $\sigma_{c_i}^\bar{\sigma}$ as the smallest (coherent) set of derivations containing:

* if $\sigma(?_{c_i})$, the derivation $?_{c_i}$ (it is a one-rule derivation).

* For each $j, j'$ such that $\bar{\sigma}(?_{c_j})$ and $\bar{\sigma}(?_{c_{j'}})$ and $j + j' - 1 = i$, the derivations of $(?_{c_{j+j'-1}})$ from figure 12.

We then define $\sigma_{m_i}^\bar{\sigma}$ by induction on $i$ as the smallest set containing:

* If $\sigma(?_{m_i})$, the derivation $?_{m_i}$ (it's a derivation formed of one rule).

* If $\sigma(?_{c_2})$, For each $j, j'$ such that $\bar{\sigma}(?_{c_j})$ and $\bar{\sigma}(?_{c_{j'}})$, such that $j + j' = i$, the derivations of $(?_{c_2} \Rightarrow ?_{m_{j+j'}})$ of figure 12.

* If $\bar{\sigma}(?_{m_1})$ and $\bar{\sigma}(?_{c_i})$, the derivations of $(?_{c_i} \Rightarrow ?_{m_i})$ of figure 12.

Finally we set $\sigma_{c_0}^\bar{\sigma} := \sigma_{m_0}^\bar{\sigma}$ and $\sigma_{c_1}^\bar{\sigma}$ being the singleton containing the 0-rule derivation.

**PROPOSITION 3.** Taking the convention $\bar{\sigma}(?_{c_0}) := \bar{\sigma}(?_{m_0})$ and $\bar{\sigma}(?_{c_1}) = \text{true}$, we have that $r^\bar{\sigma}$ is non-empty if and only if $\bar{e}(r) = \text{true}$.

**PROOF.** For $\Rightarrow$-direction, we do an induction on the derivability closure of $\sigma$. For $\Leftarrow$-direction, taking $\sigma_{c_i}^\bar{\sigma}$ and $\sigma_{m_i}^\bar{\sigma}$ we do an induction on $i$ using the inductive definition of the derivability closure. $\square$
<figure><img src="image_13.png" /><figcaption>Figure 10: Two-sided modality rules</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>Figure 11: Two-sided exponential rules for superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) and $\mu$superLL$^\infty(\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$)</figcaption></figure>

### A.3.4 Proof of Axiom Expansion property.

**LEMMA 12 (AXIOM EXPANSION).** One-step axiom expansion holds for formulas $?\sigma A$ and $!_\sigma A$ in superLL($\mathcal{E}$, $\le_g$, $\le_f$, $\le_u$) if $\sigma$ satisfies the following expansion axiom:

$$ \sigma \le_u \sigma \lor \sigma \le_f \sigma \lor (\sigma \le_g \sigma \land \sigma(\?\sigma_m)). $$

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

**PROOF.** We start by proving the first part of the theorem. We distinguish three cases depending on which branch of the disjunction holds for $\sigma$:

* If $\sigma \le_u \sigma$ is true, then we have:

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

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

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

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

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

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

### A.3.5 Proof of cut-elimination of superLL (Theorem 1). We first need three lemmas called the substitution lemmas:

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

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

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

$$ \frac{\vdash A, \dots, A, \Gamma}{\vdash ?_{\vec{\sigma}_2} \Delta, \dots, ?_{\vec{\sigma}_2} \Delta, \Gamma} S_g $$

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

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

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

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

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

$$ \frac{\pi \qquad \begin{array}{l} \vdash B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_1} A, \dots, ?_{\sigma_1} A \qquad \sigma_0 \leq_g \vec{\sigma}_3 \qquad \sigma_0 \leq_g \sigma_1 \\ \qquad \vdash !_{\sigma_0} B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_1} A, \dots, ?_{\sigma_1} A \end{array} !_g \qquad \rightsquigarrow \\ \\ \frac{\begin{array}{l} IH(\pi) \\ \vdash B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta \qquad \sigma_0 \leq_g \vec{\sigma}_3 \qquad \frac{\sigma_0 \leq_g \sigma_1}{\sigma_1 \leq_g \vec{\sigma}_2} \qquad \text{(axTrans)} \\ \qquad \vdash !_{\sigma_0} B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta \end{array}} !_g}{\vdash !_{\sigma_0} B, ?_{\vec{\sigma}_3} \Gamma', ?_{\sigma_2} \Delta, \dots, ?_{\sigma_2} \Delta} $$
• If it is a unary promotion, we use axiom (axlequis):

$$ \frac{\pi}{\vdash B, A \quad \sigma_0 \leq_u \sigma_1 \quad !_u} $$

$$ \frac{\pi}{\vdash \overline{B, A} \quad Sf \quad \frac{\sigma_0 \leq_u \sigma_1 \quad \overline{\sigma_1 \leq_f \vec{\sigma}_2}}{\sigma_0 \leq_f \vec{\sigma}_2} \quad !_f} $$

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

$$ \frac{\pi}{\vdash B, \Gamma', A, \dots, A \quad \sigma_0 \leq_f \vec{e}_3 \quad \sigma_0 \leq_f \sigma_1 \quad !_f} $$

• If it is a contraction (?$_{c_i}$) on ?$_{σ_1}$A, we use axiom (axfumpx):

$$ \frac{\pi}{\vdash \overbrace{\sigma_1 A, \dots, ?_{\sigma_1} A, \Gamma}^{n+i-1} (\sigma_1)(?_{c_i}) ?_{c_i}} $$

• If it is a multiplexing (?$_{m_i}$) on ?$_{σ_1}$A, we use axiom (axfumpx):

$$ \frac{\pi}{\vdash ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, A, \dots, A, ?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma \quad (\sigma_1)(?_{m_i})} $$

• If it is an (ax) rule on ?$_{σ_1}$A. Then Γ = !$_{σ_1}$A$^{⊥}$ and we have:

$$ \frac{\overbrace{\frac{\vdash A^{\perp}, A}{\vdash A^{\perp}, \Delta} Sf}^{\text{ax}} \overline{\sigma_1 \leq_f \vec{e}_2} !_f}{\vdash !_{\sigma_1} A^{\perp}, ?_{\sigma_2} \Delta} $$

□

**LEMMA 15 (UNARY FUNCTIONAL SUBSTITUTION LEMMA).** Let $\sigma_1$ and $\sigma_2$ be two exponential signatures such that $\sigma_1 \leq_u \sigma_2$. Let A and B be formulas, such that for all $\Gamma$, if $\vdash A, \Gamma$ is provable without using any cut then $\vdash B, \Gamma$ is provable without using any cut. Then we have

that for all $\Gamma$, if $\vdash \overbrace{?_{\sigma_1} A, \dots, ?_{\sigma_1} A, \Gamma}$ is provable without using any cut then $\vdash \overbrace{?_{\sigma_2} B, \dots, ?_{\sigma_2} B, \Gamma}$ as well, with $k_i$ positive integers.

**PROOF.** This lemma is proven the same way as Lemma 14. □

Finally we prove cut-elimination theorem 1:

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

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

• If one of the premises does not end with a rule acting on the cut formula, we apply the induction hypothesis with the premise(s) of this rule.

• If both last rules act on the cut formula which does not start with an exponential connective, we apply the standard reduction steps for non-exponential cuts leading to cuts involving strictly smaller cut formulas. We conclude by applying the induction hypothesis.

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

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

$$ \frac{\vdash A^{\perp}, ?_{\sigma_2} \Delta \quad \sigma_1 \leq_g \vec{\sigma}_2 \quad !_g}{\vdash !_{\sigma_1} A^{\perp}, ?_{\sigma_2} \Delta \quad \vdash ?_{\sigma_1} A, \Gamma} \text{ cut} $$

$$ \rightsquigarrow \frac{\vdash ?_{\sigma_1} A, \Gamma}{\vdash ?_{\sigma_2} A, \Gamma} \quad \overbrace{\sigma_1 \leq_g \vec{\sigma}_2}^{\text{Lem. 13}} $$

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

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

$$ \frac{\vdash A^{\perp}, \Delta \quad \sigma_1 \leq_f \vec{\sigma}_2 \quad !_f}{\vdash !_{\sigma_1} A^{\perp}, ?_{\sigma_2} \Delta \quad \vdash ?_{\sigma_1} A, \Gamma} \text{ cut} $$

$$ \rightsquigarrow \frac{\vdash ?_{\sigma_1} A, \Gamma}{\vdash ?_{\sigma_2} A, \Gamma} \quad \overbrace{\sigma_1 \leq_f \vec{\sigma}_2}^{\text{Lem. 14}} $$

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

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

□

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

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

$$ \frac{\vdash A, \Gamma \qquad \vdash !A, ?\Gamma \qquad !f}{\vdash !A, ?\Gamma} $$

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

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

$$ \frac{\frac{\vdash A, \Gamma \qquad \overline{\bullet \leq_f \bullet}}{\vdash !A, ?\Gamma} !f}{\vdash !A, ?\Gamma} \leftrightarrow \frac{\vdash A, \Gamma \qquad \vdash !A, ?A}{} !f $$

We have that ($!g$) is a restriction of ($!f$) in ELL and ($!u$) is non-existent.

* Moreover the cut-elimination axioms are satisfied. As $\mathcal{E}$ is a singleton, axioms (axgmpx), (axfmpx), (axcontr), (axTrans), (axleqgs), (axleqfu), (axlequs) hold. Axiom (axleqfg) is vacuously satisfied.

* The expansion axiom is satisfied since $\leq_f$ is reflexive.

## A.4 Details on the background on cut-elimination for fixed-point logics of section 2.4

### A.4.1 Details on the multicut rule 13. The multi-cut rule is a rule with an arbitrary number of hypotheses:

$$ \frac{\vdash \Gamma_1 \quad \dots \quad \vdash \Gamma_n}{\Gamma} \qquad \text{mcut}(t, \perp) $$

The ancestor relation $t$ sends one formula of the conclusion to exactly one formula of the hypotheses. Let $C := \{(i, j) \mid i \in [1, n]\}, j \in [1, \#\Gamma_i]\}$, $t$ is a map from $[1, \#\Gamma]$ to $C$ and $\perp$ is a relation on couple $C$:

* The map $t$ is injective;

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

* The relation $\perp$ is symmetric;

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

* If $(i, j) \perp (i', j')$, then the $\Gamma_i[j] = (\Gamma_{i'}[j'])^\perp$;

* The projection of $\perp$ on the first element is acyclic and connected.

### A.4.2 Details on the restriction of a multicut context (Definition 14).

*DEFINITION 26 (RESTRICTION OF A MULTICUT CONTEXT).* Let $\frac{C}{s}$ mcut($t, \perp$) be a multicut-occurrence such that $C = s_1 \dots s_n$ and let $s_i := \vdash F_1, \dots, F_{k_i}$, we define $C_{F_j}$ with $F_j \in s_i$ to be the least sub-context of $C$ such that:

* The sequent $s_i$ is in $C_{F_j}$;

* If there exists $l$ such that $(i, j) \perp (k, l)$ then $s_k \in C_{F_j}$;

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

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

### A.4.3 One-step multicut elimination for $\mu$MALL$^\infty$. Commutative one-step reductions for $\mu$MALL$^\infty$ are given in Figure 13 whereas principal reductions in Figure 14.

# B APPENDIX ON THE CUT-ELIMINATION FOR $\mu$superLL$^\infty$ SECTION

## B.1 Details on the section 3.1

In this section, we define and give a detailed justification of all the case of cut-elimination for $\mu$superLL$^\infty$. The rules are given in figure 15. As in section B.1, we write some conditions on the proofs of this figure in the corresponding lemma.

We start by the commutation cases of the different promotions. Commutation cases for the multiplexing and the contraction rules were given in section 3.1.

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

LEMMA 16 (JUSTIFICATION FOR STEP (COMM$_{!g}$)). If

$$ \frac{\pi \qquad \frac{\frac{\vdash A, ?\vec{\tau}\Delta \qquad \sigma \leq_g \vec{\tau}}{\vdash !\sigma A, ?\vec{\tau}\Delta} !g}{\vdash !\sigma A, ?\vec{\rho}\Gamma} C^!} {\text{mcut}(t, \perp)} $$

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

$$ \frac{\pi \qquad \frac{\frac{\vdash A, ?\vec{\tau}\Delta \qquad C^!}{\vdash A, ?\vec{\rho}\Gamma} \text{mcut}(t, \perp)}{\vdash !\sigma A, ?\vec{\rho}\Gamma} !g}{\text{mcut}(t, \perp)} \qquad \sigma \leq_g \vec{\rho} $$

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

PROOF. We prove that for each sequent $\vdash !\sigma' A', ?\vec{\tau}'\Delta'$ of $C' := C^! \cup \{\vdash !\sigma A, ?\vec{\tau}'\Delta'\}$, we have that $\sigma \leq_g \vec{\tau}'$.

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

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

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

- If it's a ($!g$)-promotion, we can use axiom (axTrans) with the application condition of the promotion, to get $\sigma \leq_g \vec{\tau}'$.

- If it's an ($!f$)-promotion or an ($!u$)-promotion, we can use axiom (axleqgs) with the application condition of the promotion, to get $\sigma \leq_g \vec{\tau}'$.
<figure><img src="image_15.png" /><figcaption>Figure 13: Commutative one-step reduction rules for $\mu$MALL$^\infty$</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>Figure 14: Principal one-step reduction rules for $\mu$MALL$^\infty$</figcaption></figure>

We conclude by induction and use the inequalities to prove that
$\sigma \le g \vec{\rho}$. $\square$

LEMMA 17 (JUSTIFICATION FOR STEP (COMM<sub>i,g</sub><sup>1</sup>)). If

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

$$
\frac{\pi \quad \sigma \le f \vec{\tau} \quad !f \quad C!}{\vdash A, \Delta \quad \vdash !\sigma A, ?\vec{\tau}\Delta \quad \vdash !\sigma A, ?\vec{\rho}\Gamma} \text{mcut}(i, \perp)
$$
is a $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$)-proof with $C^!$ such that each sequents concluded by an (!g) have an empty context, then

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

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

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

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

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

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

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

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

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

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

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

LEMMA 18 (JUSTIFICATION FOR STEP (COMM$^{2}_{\tau_f}$)). If

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

is a $\mu$superLL$^{\infty}$(E, $\le_g$, $\le_f$, $\le_u$)-proof with $C^!g$ containing a sequent conclusion of an (!g)-rule with at least one formula in the context, then

$$ \frac{\pi \quad \sigma \le_f \vec{\tau} (\tau_f) \quad ?_f \quad C_1^!g \quad C_2^!f \quad C_3^!u}{\vdash A, \Delta \quad \vdash !_\sigma A, ?_\tau \Delta} \quad \frac{\sigma \le_g \vec{\rho}}{\vdash !_\sigma A, ?_\rho \Gamma} $$

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

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

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

* The initialisation comes from the condition of application of !f on S.

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

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

* The initialisation is done with the first step.

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

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

We then cover the cases where we commute an (!u)-rule with the multi-cut. The first case is where there are only a list of (!u)-rules in the hypotheses of the multi-cut:

LEMMA 19 (JUSTIFICATION FOR STEP (COMM$^{1}_{\tau_u}$)). If

$$ \frac{\pi \quad \sigma \le_u \vec{\tau}}{\vdash A, C \quad \vdash !_\sigma A, ?_\tau C} \quad \frac{!u \quad C^!u}{\vdash !_\sigma A, ?_\rho B} \quad \text{mcut}(i, \perp) $$

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

$$ \frac{\pi \quad \sigma \le_u \rho}{\vdash A, C \quad \vdash A, B} \quad \frac{\text{mcut}(i, \perp)}{\vdash !_\sigma A, ?_\rho B} $$

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

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

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

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

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

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

**LEMMA 20 (JUSTIFICATION FOR STEP (COMM<sup>3</sup><sub>!u</sub>))**. Let

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

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

$$ \frac{\pi \quad \frac{\vdash A, B \quad C}{\vdash A, \Gamma} \quad \text{mcut}(l, \perp)}{\vdash !_{\sigma} A, ?_{\rho} \Gamma} \quad \sigma \leq f \quad \rho \quad !_f $$

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

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

(1) As always, we notice that the $\perp$-relation extended to sequent defines a tree on $C'$, meaning that there is a path in this tree, from $S := \vdash !_{\sigma} A, ?_{\tau} B$ to a sequent $S' := \vdash !_{\sigma'} A'$, $?_{\tau'} \Delta$ being the conclusion of an !_f-rule and with $\Delta$ being non-empty. Without loss of generality, we ask for $S'$ to be the closest such sequent (with respect to the $\perp$-relation). We prove by induction on this path, starting from S and stopping one sequent before $S'$, that for each sequent $\vdash !_{\sigma''} A''$, $?_{\tau''} B''$, that $\sigma \le_u \tau''$:

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

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

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

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

* Initialization was done at last point.

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

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

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

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

**LEMMA 21 (JUSTIFICATION FOR STEP (COMM<sup>3</sup><sub>!u</sub>))**. Let

$$ \frac{\pi_1 \quad \frac{\pi_2}{\vdash A, B \quad \sigma \le_u \tau \quad !_u} \quad C_1^{!u}}{\vdash !_{\sigma} A, ?_{\tau} B \quad C_1^l} \quad \frac{\vdash C, \Delta \quad \sigma' \le_f \tau' \quad !_f}{\vdash !_{\sigma'} C, ?_{\tau'} \Delta \quad C_2^l}}{\vdash !_{\sigma} A, ?_{\rho} \Gamma} \quad \text{mcut}(l, \perp) $$

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

$$ \frac{\pi_1 \quad \frac{\pi_2}{\vdash A, B \quad C_1 \quad \frac{\vdash C, \Delta \quad \tau' (?_{m_1})}{\vdash C, ?_{\tau'} \Delta}}{\vdash A, ?_{\rho} \Gamma}}{\vdash !_{\sigma} A, ?_{\rho} \Gamma} \quad \text{mcut}(l, \perp) \quad \sigma \le_g \rho \quad !_g $$

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

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

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

* The initialisation comes from the condition of application of !_f on $S'$.

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

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

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

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

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

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

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

* Initialization comes from the face that $\sigma \leq_u \sigma'$, $\sigma' \leq_g \vec{\tau}'$ and axiom (axlequis).

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

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

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

We conclude by induction.

We got two important properties:

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

(2) We have $\vec{\tau}'(\tau_{m_1})$.

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

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

LEMMA 22 (JUSTIFICATION FOR STEP (COMM⁴_u)). Let

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

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

$$ C' := \{\vdash \ !\sigma' C, !\vec{\tau}' \Delta\} \cup C_2^{!1} \text{ another one. Then,} $$

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

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

PROOF. We do our proof in two steps:

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

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

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

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

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

* The initialization comes from $\sigma \leq_u \sigma'$ that we showed for first step, from $\sigma' \leq_g \vec{\tau}'$ which is the condition of application of (!_g) on $S'$ and from axiom (axlequis).

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

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

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

We conclude by induction

From the inequalities that we get from induction, we can easily prove that $\sigma \leq_g \rho$. $\square$

Now, we have the lemma for the principal reduction of the multiplexing: But we need a definition first:

DEFINITION 27. Let $S^1$ be a sequent of a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-context $C^1$, such that $C^1$ is a tree with respect to a cut-relation $\perp$. We define a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-context $O_{mpx_S^1}(C^1)$ by induction on this relation taking $S^1$ as the root. We take advantage of this induction definition to define two sets of sequent $S_{C^1,S^1}^{?m}$ and $S_{C^1,S^1}^{?c}$. Let $C_1^1, \dots, C_n^1$ be the sons of $S^1$, such that $C^1 = (S^1, (C_1^1, \dots, C_n^1))$, we have two cases:

* $S^1 = S^1_g$, then we define $O_{mpx_S^1}(C^1) := (S, (C_1^1, \dots, C_n^1))$; $S^1_{C^1,S^1} = \emptyset$; $S^1_{C^1,S^1} := C^1$.
• $S^! = S^!f$ ou $S^! = S^!u$, then let the root of $C_i^!$ be $S_i^!$, we define $O_{mpx_S}(C^!):= (S, O_{mpx_S}C_1^!(C_1^!), \dots, O_{mpx_S}C_n^!(C_n^!))$; $S_{C^!S^!}^m := \{S^!\} \cup \cup_{C_i^!, S_i^!} S_{C_i^!S_i^!}^m$; $S_{C^!S^!}^c := \cup_{C_i^!, S_i^!} S_{C_i^!S_i^!}^c$

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

**LEMMA 23 (JUSTIFICATION FOR STEP (PRINCIPAL?_C))**. If

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

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

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

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

**PROOF.** We prove for each sequent $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta'' \in C_{2,\sigma A}^!$, we have that $\sigma \leq_s \vec{\tau}''$ (for one $s \in \{g, f, u\}$). As the relation $\perp$ defines a tree on $C'$: $C_{i,\sigma A}^!$ (rooted on the sequent $S := \vdash !_{\sigma A}, ?_{\vec{\tau}'} \Delta'$ which is the sequent connected to $\vdash ?_{\sigma A}, \Delta$ on $?_{\sigma A}$), we do a proof by induction on this tree:

• Initialization comes from the application condition of the promotion.

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

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

Finally, we have the multiplexing principal case:

**LEMMA 24 (JUSTIFICATION FOR STEP (COMM?_M))**. Let

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

be a $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f \leq_u)$-proof with $\Gamma$ being sent on $C_\Delta$ by $i$; $?_{\rho'} A'$ being sent on sequents of $S_{C^!S^!}^m$; and $?_{\rho''} \Gamma''$ being sent on $S_{C^!S^!}^c$, where $S(:= !_{\sigma A}, ?_{\vec{\tau}'})$ is the sequent cut-connected to $?_{\sigma A}, \Delta$ on

the formula $?_{\sigma A}$. We have that

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

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

**PROOF.** We prove that for each sequents $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta''$ of $S_{C^!S^!}^c$, $\sigma \leq_g \vec{\tau}''$ and that for each sequents $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta''$ of $S_{C^!S^!}^m$, $\sigma \leq_f \vec{\tau}''$ or $\sigma \leq_u \vec{\tau}''$. We have two cases:

• Either $S$ is the conclusion of an $!f$ or $!u$-promotion. In this case, we prove by induction following the inductive definition of $O_{mpx_S}(C_{2,\sigma A}^!)$ supposing that for $S' := \vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta''$, $\sigma \leq_f \sigma''$ or $\sigma \leq_u \sigma''$. Which is true for $S' = S$:

– If $S^! = S^!f$ $\vdash = \vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta''$, by hypothesis we have that $\sigma \leq_s \sigma''$ for $s \in \{f, u\}$. We prove by induction on $C^!$ that each sequents $\vdash !_{\sigma^{(3)}} A^{(3)}, ?_{\vec{\tau}^{(3)}} \Delta^{(3)}$ of it are such that $\sigma \leq_g \vec{\tau}''$.

* For initialization, as $\sigma \leq_s \sigma''$, we have by the condition of application of ($!g$) that $\sigma'' \leq_g \vec{\tau}''$, therefore by axiom (axleqfg) and (axlequs), that $\sigma \leq_g \vec{\tau}''$.

* For heredity, we get for induction hypothesis that $\sigma \leq_g \sigma^{(3)}$, from application condition of the promotion of the sequent in question, we get $\sigma^{(3)} \leq_s \vec{\tau}^{(3)}$ for $s \in \{g, f, u\}$, using axioms (axleqgs) we get $\sigma \leq_g \vec{\tau}^{(3)}$.

We conclude by induction and get the desired property. (As $S_{C^!S^!}^m$ is empty, sequents from it also satisfies the property.)

– $S^! = S^!f$ ou $S^! = S^!u$. Let $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta''$ be this sequent, then by hypothesis we have that $\sigma \leq_s \sigma''$ for $s \in \{f, u\}$. From condition of application of the promotion, we get that $\sigma'' \leq_s \vec{\tau}''$ ($s \in \{f, u\}$), therefore by lemma (axleqfu), and (axlequs), we get that $\sigma \leq_s \vec{\tau}''$ for $s'' \in \{f, u\}$, we can therefore apply induction hypothesis $i$ times on each $O_{mpx_S}C_i^!(C_i^!)$.$^*$ The inequality $\sigma \leq_s \vec{\tau}''$ gets us also that the sequent $S^!$ satisfies the desired property and we can conclude for both $S_{C^!S^!}^m$ and $S_{C^!S^!}^c$.

• Either $S$ is the conclusion of an $!g$-promotion. In that case, we prove by induction $C_{2,\sigma A}^!$ that for each sequents $\vdash !_{\sigma''} A'', ?_{\vec{\tau}''} \Delta''$ are such that $\sigma \leq_g \vec{\tau}''$. We prove it by induction on the tree defined by the $\perp$-relation:

– The initialization comes from the condition of application of ($!g$) on $S$.
- For heredity, we get that $\sigma'' \leq_s \vec{\tau}''$ for $s \in \{g, f, u\}$,
$\sigma \leq_g \sigma''$ from induction hypothesis and we conclude
using axiom (axleqgs).

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

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

## B.2 Details on the section 3.2

### B.2.1 Rule permutations.

DEFINITION 28 (PERMUTATION OF RULES). We define one-step
rule permutation on (pre-)proofs of $\mu LL^\infty$ with rules of figure 17.

Given a $\mu LL^\infty$ (pre-)proof $\pi$ and $p \in \{l, r, i\}^*$ a path in the proof,
we define $\text{perm}(\pi, p)$ by induction on $p$:

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

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

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

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

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

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

LEMMA 25 (ROBUSTNESS OF THE PROOF STRUCTURE TO RULE PERMUTATION). One-step rule permutation does not modify the structure of the proof.

PROOF. This lemma is immediate as the substitutions are defined
between unary rule.
$\square$

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

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

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

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

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

We say that a rule (r) in $\pi$ is finitely permuted if its sequence of residuals is ultimately constant. We say that $(p_i)_{i \in \lambda}$ is a rule permutation sequence with finite permutation of rules if each rule of $\pi_0$ is finitely permuted.

PROPOSITION 4 (CONVERGENCE OF PERMUTATION WITH FINITE PERMUTATION OF RULES). Let $\pi$ be a $\mu LL^\infty$ pre-proof and let $(p_i)_{i \in \omega}$ be a permutation sequence with finite permutation of rules starting from $\pi$, then the sequence is converging.

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

PROPOSITION 5 (PRESERVATION OF VALIDITY FOR PERMUTATIONS WITH FINITE PERMUTATION OF RULES). Let $\pi$ be a $\mu LL^\infty$ pre-proof and let $(p_i)_{i \in \omega}$ be a permutation sequence with finite permutation of rules starting from $\pi$ and converging (thanks to lemma 4 to a pre-proof $\pi'$. Then $\pi$ is valid if and only if $\pi'$ is.

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

### B.2.2 Proof of lemma 8.

LEMMA 26. Let $n \in \mathbb{N}$, let $d_1, \dots, d_n \in \mathbb{N}$ and let $p_1, \dots, p_n \in \{0, 1\}$. Let $\pi$ be a $\mu LL^\infty$-proof concluded by an (mcut)-rule, on top of which there is a list of $n$ proofs $\pi_1, \dots, \pi_n$. We ask for each $\pi_i$ to be of one of the following forms depending on $p_i$:

* If $p_i = 1$, the $d_i + 1$ last rules of $\pi_i$ are $d_i$ derelictions and then a promotion rule. We ask for the principal formula of this promotion to be either a formula of the conclusion, either to be cut with a formula being principal in a proof $\pi_j$ on one of the last $d_j + p_j$ rules.

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

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

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

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

* (Heredity). We have several cases:
<figure><img src="image_21.png" /><figcaption>Figure 15: Commutative cut-elimination steps of the exponential fragment of $\mu$superLL$^\infty$(remaining cases)</figcaption></figure>

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

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

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

The $\pi'_j$ will be the hypotheses of the (mcut) of $\pi''$.
Note that $\sum d'_j + \sum p'_j = \sum d_j + \sum p_j - 1$ meaning that
Cut-elimination for the circular modal mu-calculus:
linear logic and super exponentials to the rescue

<figure><img src="image_22.png" /><figcaption>**Figure 16:** Principal cut-elimination steps of the exponential fragment of μsuperLL$^{∞}$ (cases specific to μLL$^{□}$∞)</figcaption></figure>

<figure><img src="image_23.png" /><figcaption>**Figure 17:** One-step rule permutation</figcaption></figure>

we can apply our induction hypothesis. Combining
our reduction step with the reduction steps of the
induction hypothesis, we obtain the desired result.
- If there are no rules from the conclusion but that one
  $\pi_i$ ends with $d_i > 0$ and $p_i = 0$, meaning that the proof
  ends by a dereliction on a formula $?F$. This means

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

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

The statement is therefore true by induction □

### B.2.3 Details on proof of lemma 7.

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

**PROOF.** Here we give some details on the proof of lemma 7 as well as cases that were not covered it. Reductions from the non-exponential part of $\mu$superLL$^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ translates easily to one step of reduction in $\mu$LL$^\infty$. To prove the result on exponential part, we will describe each translation of the reductions of figure 6, 7,15 and ?? . For the commutative steps no commutation of rules are necessary.

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

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

$$ \begin{array}{ccc} \pi_1^\circ & & \pi_n^\circ \\ \begin{array}{c} \vdash A_1^\circ, \Delta_1^\circ \\ \vdash A_1^\circ, ?\Delta_1^\circ \\ \vdash !A_1^\circ, ?\Delta_1^\circ \end{array} & ?_d & \dots \\ \begin{array}{c} \vdash !A^\circ, ?\Gamma^\circ \end{array} & !_p & \dots \\ & \multicolumn{2}{c}{\text{mcut}(i, \perp)} \end{array} $$

with one of the $i(1) = (i, 1)$ for some $i$ and $n = 1 + \#(C)$. We apply our result on this proof with all the $p_i$ being equal to 1 and with $d_i = \#(\Delta_i)$. Moreover, we notice that there will be only one promotion rule commuting under the cut

and that it commutes before any dereliction, giving us one translation of the functorial promotion.

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

- Step (comm$^1_{\mathfrak{I}_u}$). This step translates to the commutation of one (!)-rule, followed by $\#(C^1_{\mathfrak{I}_u}) (!/?_d)$ principal steps and finally one (?_d) commutation.

- Step (comm$^2_{\mathfrak{I}_u}$). We prove this step using lemma 26 as for step (comm$^1_{\mathfrak{I}_f}$).

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

- Step (comm$_{\mathfrak{I}_m}$). We must distinguish three cases based on $i$:

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

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

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

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

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

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

which we can re-arrange to get the translation of any of the derivations of $?\tilde{\rho}_{c_i}$. Note that for $i = 2$ no rule permutation are needed.

- Step (principal$_{\mathfrak{I}_m}$). This step translates in two phases:

(1) First $i - 1$ contraction principal cases;

(2) followed by $\#(S^2_{C', S'_{\mathfrak{I}_f}}) (?_d/!)$-principal cases, and $\#(\Gamma'')$ dereliction commutative cases.

To prove the second phase we re-use lemma 26 as for steps (comm$^2_{\mathfrak{I}_u}$) and (comm$^1_{\mathfrak{I}_f}$).
Finally, the obtained proof under the multi-cut look like this:

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

which we can re-arrange these rules to get the translation of any of the derivations of $\bar{\sigma}'_{m_i}$, followed by any of the derivations of $\bar{\sigma}'_{c_i}$. Note that if $i = 0$, no re-arrangement is needed. □

### B.2.4 Proof of lemma 9.

**LEMMA 28 (COMPLETENESS OF THE (MCUT)-REDUCTION SYSTEM).**
If there is a $\mu LL^\infty$-redex $\mathcal{R}$ sending $\pi^\circ$ to $\pi'^\circ$ then there is also a $\mu superLL^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-redex $\mathcal{R}'$ sending $\pi$ to a proof $\pi''$, such that in the translation of $\mathcal{R}'$, $\mathcal{R}$ is applied.

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

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

* If it is a principal case again, we have that there is a contraction or a dereliction or weakening rule (r) on top of a (mcut) on a formula ?A. It also means that each proofs cut-connected to ?A ends with a promotion. As $\pi^\circ$ is the translation of a $\mu superLL^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$-proof, it means that (r) is contained in the translation of a multiplexing or contraction rule (r') on a formula $?_\sigma A$ on top of a (mcut). It also means that all the proofs cut-connected for this (mcut) to $?_\sigma A$ are translations of promotions (no other rules than a promotion in $\mu superLL^\infty(\mathcal{E}, \leq_g, \leq_f, \leq_u)$ translates to a derivation ending with a promotion). Therefore the principal case on (r') is possible, we can take $\mathcal{R}'$ as it.

* If it is the commutative step of a promotion (r), it means that all the proofs of the contexts of the (mcut) are promotions. Meaning that (r) is contained in the translation of a promotion (r') on top of (mcut). We also have that the context of this

(mcut) are only proof ending with a promotion for the same reasons that last point. We therefore need to make sure that each (mcut) with a context full of promotions are covered by the $\rightsquigarrow$-relation. Looking back at figure 15 together with conditions given by each corresponding lemmas, we have that:

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

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

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

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

* The second one covers the case where there are one proof ending with an (!_f)-rule and where all the proof ended by an (!_g)-promotions have a conclusion with empty context.

* The two last ones cover the cases where there is a proof ending by an (!_g)-promotion having conclusion with non-empty context. □

# C APPENDIX ON THE CUT-ELIMINATION OF MODAL $\mu$-CALCULUS SECTION

## C.1 Details on the linear-logical modal $\mu$-calculus of section 4.1

### C.1.1 Details on linear translation of $\mu KL^\infty$.

**DEFINITION 30 (LINEAR TRANSLATION OF $\mu KL^\infty$).** We consider the translation of the rules in figure 18 which complete the rules of figure 9.

We define translations of proofs coinductively on the proofs using the translation of each rules.

### C.1.2 Proofs that $\mu LL^\infty$-instance of superLL satisfy the cut-elimination axioms (property 2).

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

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

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

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

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

* Axiom (axTrans) is satisfied as $\leq_g$ and $\leq_f$ are transitive.

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

## C.2 Details on cut-elimination for $\muLK_{\square}^{\infty}$ of
section 4.3

### C.2.1 Definition of skeleton.

DEFINITION 31 ($\muLK_{\square}^{\infty}$-SKELETON). The $\muLK^{\infty}$-skeleton of a $\mu LL^{\infty}$ formula is defined inductively as follows ($\delta \in \{\mu, \nu\}$):

$$
\begin{align*}
SK(F \otimes G) &= SK(F) \wedge SK(G) & SK(F \otimes G) &= SK(F) \vee SK(G) \\
SK(!F) &= SK(F) & SK(F \& G) &= SK(F) \wedge SK(G) \\
SK(F \oplus G) &= SK(F) \vee SK(G) & SK(?F) &= SK(F) \\
SK(1) &= \top & SK(\bot) &= \top \\
SK(a) &= a & SK(\top) &= \top \\
SK(0) &= F & SK(a^{\perp}) &= \neg a \\
SK(F \to G) &= SK(F) \to SK(G) & SK(\delta X \cdot F) &= \delta X \cdot SK(F) \\
SK(X) &= X & SK(\Box F) &= \Box SK(F) \\
SK(\diamond F) &= \diamond SK(F)
\end{align*}
$$

Sequents of formulas of $\mu LL_{\square}^{\infty}$ are translated to sequent of skeletons of these formulas. Translations of pre-proofs are obtained co-inductively by translating the rules of each connectives independantly. Exponential rules are replaced by the derivation with no rules.

LEMMA 29 (ROBUSTNESS OF THE SKELETON TO VALIDITY). If $\pi$ is a $\mu LL_{\square}^{\infty}$ valid pre-proof, $SK(\pi)$ is a $\mu LK_{\square}^{\infty}$ valid pre-proof, and vice-versa.

PROOF. This comes from the fact that (i) minimal formula of a set of translated formulas is the translation of the minimal formula of the set of initial formulas; (ii) translations of branches contains all the translations of formulas of the initial branch and vice-versa. □

LEMMA 30 (COMPOSITION OF SK() AND OF (–)•). Let $\pi$ be a $\mu LK_{\square}^{\infty}$ pre-proof. We have that $SK(\pi^•)$ is equal to $\pi$.

PROOF. This comes from the fact that (–)•-translation translates each rules ($r$) of $\mu LK_{\square}^{\infty}$ to a derivation containing the pre-image of ($r$) by the translation $SK()$, adding only exponential rules. As exponential rules disappears from the proof by $SK()$, we get that $SK(r^•)$ is equal to ($r$). We coinductively apply this result on pre-proofs □
CONTENTS

<table><tr><td>Abstract</td><td>1</td></tr><tr><td>1 Introduction</td><td>1</td></tr><tr><td>2 Background</td><td>2</td></tr><tr><td>2.1 Formulas</td><td>2</td></tr><tr><td>2.2 Sequent calculi</td><td>3</td></tr><tr><td>2.3 Super exponential systems</td><td>4</td></tr><tr><td>2.4 Cut-elimination for fixed-point logics</td><td>5</td></tr><tr><td>3 Cut-elimination for μsuperLL<sup>∞</sup></td><td>6</td></tr><tr><td>3.1 (mcut)-elimination steps</td><td>7</td></tr><tr><td>3.2 Translating μsuperLL<sup>∞</sup> into μLL<sup>∞</sup></td><td>8</td></tr><tr><td>4 On the cut-elimination of the modal μ-calculus</td><td>12</td></tr><tr><td>4.1 A linear-logical modal μ-calculus</td><td>12</td></tr><tr><td>4.2 Cut-elimination for μLL<sup>∞</sup></td><td>12</td></tr><tr><td>4.3 Cut-elimination of μLK<sup>∞</sup></td><td>13</td></tr><tr><td>4.4 Finitary circular cut-elimination for μLK<sup>∞</sup></td><td>13</td></tr><tr><td>5 Conclusion</td><td>13</td></tr><tr><td>References</td><td>14</td></tr></table>

<table><tr><td>A</td><td>Appendix on the background section</td><td>15</td></tr><tr><td>A.1</td><td>Details on the section 2.1</td><td>15</td></tr><tr><td>A.2</td><td>Details on the sequent calculi section 2.2</td><td>15</td></tr><tr><td>A.3</td><td>Details on super exponential systems</td><td>15</td></tr><tr><td>A.4</td><td>Details on the background on cut-elimination for fixed-point logics of section 2.4</td><td>19</td></tr><tr><td>B</td><td>Appendix on the cut-elimination for μsuperLL<sup>∞</sup> section</td><td>19</td></tr><tr><td>B.1</td><td>Details on the section 3.1</td><td>19</td></tr><tr><td>B.2</td><td>Details on the section 3.2</td><td>25</td></tr><tr><td>C</td><td>Appendix on the cut-elimination of modal μ-calculus section</td><td>29</td></tr><tr><td>C.1</td><td>Details on the linear-logical modal μ-calculus of section 4.1</td><td>29</td></tr><tr><td>C.2</td><td>Details on cut-elimination for μLK<sup>∞</sup> of section 4.3</td><td>31</td></tr><tr><td>Contents</td><td></td><td>32</td></tr></table>