# On the cut-elimination of the modal mu-calculus: Linear Logic to the rescue

Esaïe Bauer, Alexis Saurin

► To cite this version:

Esaïe Bauer, Alexis Saurin. On the cut-elimination of the modal mu-calculus: Linear Logic to the rescue. FoSSaCS 2025 - 28th International Conference on Foundations of Software Science and Computation Structures, Abdulla; Kesner, May 2025, Hamilton, Canada. pp.133-154, 10.1007/978-3-031-90897-2_7. hal-05409189

HAL Id: hal-05409189

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

Submitted on 10 Dec 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# On the cut-elimination of the modal µ-calculus: Linear Logic to the rescue

Esaïe Bauer(✉) and Alexis Saurin(✉)

Université Paris Cité & CNRS & INRIA, Pl. Aurélie Nemours, 75013 Paris, France
{esaie.bauer, alexis.saurin}@irif.fr

**Abstract.** This paper presents a proof-theoretic analysis of the modal µ-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal µ-calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, $\mu LL_\square^\infty$, which is a linear version of the modal µ-calculus, intertwining the modalities from the modal µ-calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for $\mu LL_\square^\infty$ and (ii) translating proofs of the modal mu-calculus into this new system via a “linear translation”, allowing us to extract the cut-elimination result.

# 1 Introduction

*Eliminability of cuts and the modal µ-calculus.* Since Kozen’s seminal work on the modal µ-calculus [17], this logic extending basic modal logic with least and greatest fixed-points has been extremely fruitful for the study of computational systems, especially reactive systems. In addition to its wide expressive power, its deep roots in logic also allow for a number of fruitful approaches, be they model-theoretic, proof-theoretic or automata-theoretic. Still, *cut-elimination* – a cornerstone of modern proof-theory – has only received partial solutions [1,6,21,22,24]:

- Either as cut-admissibility statements which are noneffective possibly using infinitary proof-systems such as (i) infinitely branching proof systems, allowing the $\omega$-rule [16] or (ii) non-wellfounded or circular proof systems [1,24], allowing proof-trees with infinitely long branches;

- Or as syntactic cut-elimination results capturing only a *fragment* of the calculus in systems with the $\omega$-rule [21,22]. A challenge in describing a *syntactic cut-elimination* for such systems is that the number of applications of a $\mu$-rule must sometimes be determined before knowing how many are needed to match each premises of a $\nu$-rule. In [6], the authors discuss a specific example where syntactic cut-elimination fails. While there are syntactic cut-elimination results in systems based on the $\omega$-rule [6,21,22], they capture only strict fragments of the modal $\mu$-calculus.

In fact, there is no syntactic cut-elimination theorem for the full modal μ-calculus. The present work establishes such a syntactic cut-elimination theorem for the modal μ-calculus in the setting of non-wellfounded sequent calculus.
*On unity and diversity in computational logic.* Logic presents at the same time a deep unity and a wide diversity. Miller [20] argues that the "universal character [of logic] has been badly fractured in the past few decades", due to the wide range of its applications, the various families of logics that have emerged and the different computational tools that are in use, often with little relationship. Miller thus proposes the following questions as the first of a list of "challenges":

**Challenge 1: Unify a wide range of logical features into a single framework.**

*How best can we explain the many enhancements that have been designed for logic: for example, classical / intuitionistic / linear, fixed points, first-order / higher-order quantification, modalities, and temporal operators? (...)*

In the present paper, we partially address Miller’s first challenge, providing a common framework for two of the main logics that emerged in the 1980s, Kozen’s modal μ-calculus [17] and Girard’s linear logic (LL) [14]. Working in the setting of circular and non-wellfounded proof systems for the above logics, we propose a so-called *linear decomposition* of the modal μ-calculus in linear logic with fixed-points. This proof-theoretic analysis of the modal μ-calculus allows us to do a finer-grained treatment of syntactic cut-elimination.

*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 and establish that the cut inference is *admissible* (according to this tradition, the cut-inference essentially lives at the metalevel, ensuring compositionality of the logic) or (ii) one can consider that the cut inference lives at the object-level and is a fundamental piece of proofs: one thus establishes that the cut inference is *eliminable*, ensuring the sub-formula property (and its numerous important consequences, ranging from consistency to interpolation properties).

This second tradition may use similar techniques as the first tradition, but it also permits the investigation of a syntactic, or effective, approach to cut-elimination, consisting of a cut-reduction relation on proofs, shown to be (at least) weakly normalizing, with the normal forms being cut-free proofs. An advantage of such syntactic cut-elimination results is that, in many settings (most notably LJ and LL [14]), such cut-reductions induce an interesting relation on proofs and have a computational interpretation that is the starting point of the Curry-Howard correspondence built upon sequent calculus [9].

*Linear Logic.* Linear logic (LL) is often described as a resource-sensitive logic. It is more accurate, though, to view it as a logic designed for analyzing cut-elimination itself. Indeed, LL comes from an analysis of structural rules, aiming at controlling them rather than weakening them as in substructural logics. This solves some fundamental drawbacks of cut-elimination in classical logic, such as its non-termination or non-confluence. For instance, LL permits the decomposition of both intuitionistic and classical logic, in a structured and fine-grained manner allowing the refinement of the cut-elimination of those logics as well as
their notion of model (allowing the building of a non-trivial denotational model of classical proofs); the prototypical example of such a linear decomposition consists in decomposing the usual intuitionistic arrow (i.e., the function type of the λ-calculus), $A \Rightarrow B$, into a replication operator and a linear implication: $!A \dashv B$ [10,14]. Further analyses on these exponential modalities led to the discovery of light logics, where the complexity of cut-elimination is tamed in a flexible way, usually by considering alternative, weaker exponential modalities.

The proof theory of LL was extended to $\mu LL^\infty$, that is LL with fixed-points in the finitary and non-wellfounded setting [2,12,26,27,28] and $\mu LL^\infty$ allowed for the same kind of linear decomposition for (the non-wellfounded version of) $\mu LJ$ and $\muLK$. A natural question is whether the extensions of LL with fixed-points can also help us achieve syntactic cut-elimination for the modal $\mu$-calculus.

*Contributions.* The discussion of the above paragraph suggests a first question: what would be a linear decomposition of the modal $\mu$-calculus? The first contribution of this paper is to provide such a linear decomposition of the modal $\mu$-calculus which is compatible with circular and non-wellfounded proof theory, $\mu LL^\infty$. This linear-logical modal $\mu$-calculus will allow us to complete the analysis of cut-elimination for the modal $\mu$-calculus, proving the first syntactic cut-elimination theorem for the full modal $\mu$-calculus (in the non-wellfounded setting). We therefore adopt the following roadmap in the body of the paper.

In Section 2, we recall the necessary technical background about $\mu LL^\infty$ and $\muLK^\infty$ proof theory. In Section 3, we motivate and introduce $\mu LL^\infty$ and prove its cut-elimination in Section 4. We then define the linear decomposition of $\muLK^\infty$ into $\mu LL^\infty$ from which we conclude to $\muLK^\infty$ cut-elimination theorem in Section 5 in the form of an infinitary weak-normalizing cut-reduction system.

# 2 Circular and (non-)wellfounded proof systems

We recall here some basic definitions of both wellfounded & non-wellfounded systems. Some standard definitions of proof theory such as *derivation rules*, *active formula* or *principal formula* are not recalled and can be found in [7].

## 2.1 The Modal μ-calculus

**Formulas** Let $\mathcal{V}$ and $\mathcal{A}$ be two disjoint sets of *fixed-point variables* and of *atoms* respectively. We define the pre-formulas of the modal $\mu$-calculus, $\muLK^\infty$, as: $F,G ::= a | X \mid \mu X.F \mid \nu X.F \mid \Box F \mid \Diamond F \mid F^\perp \mid F \to G \mid F \lor G \mid F \land G \mid F \mid T$ ($a \in \mathcal{A}, X \in \mathcal{V}$). Knaster-Tarski's theorem guarantees the existence of extremal fixed-points of monotonic functions on complete lattices; monotonicity is reflected syntactically as a *positivity condition* on variables, defined as:

**Definition 1 (Positive & negative occurrence of fixed-point variables)**

Let $X \in \mathcal{V}$ be a *fixed-point variable*, one defines the *fact*, for $X$, to occur positively (resp. negatively) in a *pre-formula* by induction on the *structure of pre-formulas*:
- $X$ occurs positively in $X$.

- $X$ occurs positively (resp. negatively) in $c(F_1, \dots, F_n)$, if there is some $1 \le i \le n$ such that $X$ occurs positively (resp. negatively) in $F_i$ for $c \in \{\Box, \Diamond, \vee, \wedge\}$.

- $X$ occurs positively (resp. negatively) in $F^{\perp}$ if it occurs negatively (resp. positively) in $F$.

- $X$ occurs positively (resp. negatively) in $F \to G$ if $X$ occurs either positively (resp. negatively) in $G$ or negatively (resp. positively) in $F$.

- $X$ occurs positively (resp. negatively) in $\delta Y.G$ (with $Y \neq X$) if it occurs positively (resp. negatively) in $G$ (for $\delta \in \{\mu, \nu\}$).

We can now define the formulas of $\mu LK_{\Box}^{\infty}$:

**Definition 2 (Formulas)** A $\mu LK_{\Box}^{\infty}$ formula $F$ is a closed pre-formula such that for any sub-pre-formula of $F$ of the form $\delta X.G$ (with $\delta \in \{\mu, \nu\}$), $X$ does not occur negatively in $G$.

By considering the $\{\mu, \nu, X\}$-free formulas of this system, we get $LK_{\Box}$. By considering the $\{\Box, \Diamond\}$-free formulas of $\mu LK_{\Box}^{\infty}$, we get the $\mu$-calculus. Finally, the intersection of these two systems, is propositional classical logic.

**Sequent calculus** We define, here, the sequents, rules and proofs for $\mu LK_{\Box}^{\infty}$.

**Definition 3 (Sequent)** A sequent is an ordered pair of two lists of formulas $\Gamma$, the antecedent, and $\Delta$, the succedent, that we write $\Gamma \vdash \Delta$.

**Remark 1 (Derivation rules & ancestor relation)** In the structural proof theory literature, inference rules are defined together with an ancestor relation (or sub-occurrence relation) between formulas of the conclusion and formulas of the premises of the rule. While this relation is often overlooked we provide some details here. Sequent being lists, we define the ancestor relation, to be a relation from the positions of the formula in the conclusion, to the positions of the formula in the premises. Those ancestor relations will be dealt graphically as in Figures 1 and 2, by drawing the ancestor relation on sequents when needed and leaving it implicit when unambiguous.

We define the inference rules for $LK_{\Box}$ in Figure 1. Rules for $LK$ will be the $\{\Box, \Diamond\}$-free rules of $LK_{\Box}$. We add rules of Figure 2 to $LK$, (resp. $LK_{\Box}$) to get the fixed-point version $\mu LK^{\infty}$ (resp. $\mu LK_{\Box}^{\infty}$) of this system. The two ex-change rules ($\text{ex}_l$) and ($\text{ex}_r$) from Figures 1 and 4 allows one to derive the rule $\frac{\sigma'(\Gamma) \vdash \sigma(\Delta)}{\Gamma \vdash \Delta} \quad \text{ex}(\sigma', \sigma)$ for any permutations $\sigma$ and $\sigma'$ of $\{1, \dots, \#(\Delta)\}$ and $\{1, \dots, \#(\Gamma)\}$ respectively, where $\sigma(\Delta)$ designates the action of $\sigma$ on the list $\Delta$, with the induced ancestor relation. In the rest of the article, we will intentionally treat the exchange rule implicitly: the reader can consider that each of our rules are preceded and followed by a finite number of rule (ex).

Proofs of non fixed-point systems, $LK$, $LK_{\Box}$ are the trees inductively generated by the corresponding set of rules of each of these systems. We can define a first notion of infinite derivations, pre-proofs, that will soon be refined:
<figure><img src="image_2.png" /><figcaption>Fig. 1: Rules of LK$_{□}$</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2: Rules for the fixed-point fragment</figcaption></figure>

**Definition 4 (Pre-proofs)** *Given a set of derivation rules, a pre-proof is a tree co-inductively generated using the rules of the system.*

**Example 1 (Regular pre-proof)** *Regular pre-proofs are those pre-proofs having a finite number of distinct sub-proofs. We represent them with back-edges.*

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

**Remark 2** *The pre-proofs define an inconsistent system. In fact, any sequent is provable:*

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

Proofs are defined as those pre-proofs satisfying a correctness condition:

**Definition 5 (Validity and proofs)** *Let $b = (s_i)_{i \in \omega}$ be a consecutive 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 \ge n}$, for some $n \in \omega$, of occurrences such that for each $j$, $F_j$ and $F_{j+1}$ satisfy the ancestor relation. We say that a thread of $b$ is valid if the minimal recurring formula of this sequence, for the sub-formula ordering, exists and is (i) either a $\nu$-formula appearing infinitely often on the succedent of its sequent or a $\mu$-formula appearing infinitely often in the antecedent of its sequent and (ii) the thread is infinitely often principal (there are an infinite number of principal formulas in it). 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.*

The least ($\mu$) and greatest ($\nu$) fixed-point constructors have the same (local) derivation rules: they are distinguished by the (global) validity condition, which is a parity condition akin to parity games for the $\mu$-calculus.
<figure><img src="image_6.png" /><figcaption>Fig. 3: Valid and invalid pre-proofs</figcaption></figure>

**Example 2 (Valid and invalid pre-proofs)** Here, we give some examples of infinite proofs. The pre-proof of Example 1 is valid, that of Remark 2 is invalid.

We use the notation Nat := µX.T ∨ X, representing the type of natural numbers. We can represent any natural number n by a finite valid proof π_n defined in Figure 3a. The infinite pre-proof π_∞, defined in Figure 3a, of ⊢ Nat is not valid: the infinite branch in π_∞ is supported by only one thread, which is not valid as the minimal formula is a µ-formula appearing only on the right of the proof. This is coherent with the interpretation that µ is a least fixed-point: the system would reject the infinite proof of Nat. Note that the same kind of proof with coNat := νX.T ∨ X would have given a valid proof.

The pre-proof of Figure 3b (representing the double function) is valid: The only infinite branch in it is the one going infinitely to the right at the application of the (∨₁)-rule. This branch is supported by the infinite thread in the antecedent of each sequent which has a µ-formula as its minimal formula.

## 2.2 Linear Logic with fixed-points

The main difference between LK (or LJ) and LL lies in the fact that formulas are not always erasable nor duplicable. Hence, the sequent A, B ⊢ A is not always provable, neither is A ⊢ A ⊗ A (a sequent similar to A ⊢ A ∧ A in LK). This restriction allows LL to interpret programs with finer resource control than LK (or LJ). Here we recall the usual definitions of both the wellfounded and non-wellfounded systems of LL, following the definitions of the previous section.

**Formulas** As for µLK<sub>⊤</sub><sup>∞</sup>, let us set V and A as two disjoint sets. The pre-formulas of the non-well-founded linear logic, µLL<sup>∞</sup> are: F, G ::= a | X | µX.F | νX.F | F<sup>⊥</sup> | F ↸<sub>0</sub> G | F ≀≀ G | F ⊗ G | ⊥ | 1 | F ⊕ G | F & G | 0 | ⊤ | ?F | !F, with a ∈ A, X ∈ V. Positivity of pre-formulas and µLL<sup>∞</sup> formulas are defined in the same way as for µLK<sub>⊤</sub><sup>∞</sup>. The {!, ?}-free formulas of µLL<sup>∞</sup> are the formulas of µMALL<sup>∞</sup>. The {µ, ν, X}-free fragment of formulas of µLL<sup>∞</sup> are the formulas of linear logic LL. The intersection of these two fragments is MALL.

**Sequent calculus** The definition of sequent is the same as for µLK<sub>⊤</sub><sup>∞</sup>. The rules of MALL are given by Figure 4, the rules of LL are the rules of MALL together with the rules of Figure 5. We add the rules of Figure 2 to MALL (resp. LL) to obtain the rules of µMALL<sup>∞</sup> (resp. µLL<sup>∞</sup>). Pre-proofs as well as validity are
<figure><img src="image_7.png" /><figcaption>Fig. 4: Rules of multiplicative and additive linear logic</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Fig. 5: Exponential fragment of LL</figcaption></figure>

defined as in the previous section.

In linear logic, duplicability and erasability are controlled by ? (why not) and ! (of course) modalities. The (!_c), (!_w), and (!_d) rules allow duplication, erasure, and use of !-prefixed antecedents, respectively. The (!_p) rule enables using an !-prefixed succedent when all antecedents are !-prefixed. This controlled approach to contraction and weakening sequentializes certain reductions in cut-elimination, leading to strong normalization for LL [25]. However, the good normalization properties of LL can be recovered by using a linear translation from LK to LL, similar to the double negation translations from LK to LJ. Indeed, every formula, every sequent, and every proof of LK can be translated into a proof in LL by adding ? and ! modalities. For instance in Figure 6 we show an example where each connective $c(A_1, \dots, A_n)$ can be translated as $!(c(?A_1, \dots, ?A_n))$ adding a ? on the formula from the succedent, the additional rules being shown in blue. By taking any maximal sequence of cut reduction on such proofs in LL and using the strong normalization property, we find a cut-free proof of the same sequent in LL. This projects to an LK proof of the original sequent, by simply *forgetting* superfluous modalities. In Section 5, we will use this technique to prove the cut elimination of the modal µ-calculus.

**Cut-elimination for µLL<sup>∞</sup>** We postpone to Section 4 the discussion of cut-elimination reductions (Definition 8, 10 and 11) and theorems (Theorem 2): they are directly introduced for µLL<sup>∞</sup> that we shall consider in the next section.
<figure><img src="image_9.png" /><figcaption>Fig. 6: Example of a linear translation</figcaption></figure>

### 3 A linear-logical modal $\mu$-calculus: $\mu LL_{\square}^{\infty}$

We now introduce $\mu LL_{\square}^{\infty}$, which can be viewed from two perspectives:

- as an extension of $\mu LL^{\infty}$ with modalities akin to the modal $\mu$-calculus;

- as a linearization of the modal $\mu$-calculus (where linear refers to linear logic – by default, any assumption must be used exactly once in a proof – and not to the structures of its models, as in LTL or linear-time $\mu$-calculus [30]).

In designing the $\mu LL_{\square}^{\infty}$ sequent calculus, the primary challenge lies in understanding the interaction between the $\square$ and $\diamond$ modalities and LL exponentials, while being compatible with the fixed-point inferences. A natural requirement for such a sequent calculus is to allow us to extend the linear decomposition of $\mu KL^{\infty}$ [28] to $\mu KL_{\square}^{\infty}$. The constraints imposed by such a linear decomposition will therefore guide us in defining the exponential and modal rules of $\mu LL_{\square}^{\infty}$. The following discussion illustrates these requirements through examples and will lead us to the desired sequent calculus defined in Definition 6 below.

A first approach would be to simply extend $\mu LL^{\infty}$ with the usual inferences for $\square$ and $\diamond$, extending the translation $(-)^{\bullet}$ from [28] on modalities as in Figure 6 setting $(\diamond A)^{\bullet} := !\diamond(A)^{\bullet}$ and $(\square A)^{\bullet} := !\square(A)^{\bullet}$. This approach is too simplistic, though, and fails. Consider indeed an instance of the modal rule $\square_p$ (defined in Figure 1) with $\Gamma = []$ and $\Delta = [B]: \vdash_A B \quad \vdash_{\square A, \diamond B} \square_p$. Following the standard sequent translation from LK to LL, we need to derive $\vdash ?\square A^\bullet, ?\diamond B^\bullet$ from the premise $\vdash ?A^\bullet, ?B^\bullet$. Reasoning bottom-up: to conclude $\vdash ?A^\bullet, ?B^\bullet$, we must remove both the $\diamond$ and the $\square$ with a modal rule. However, regardless of the sequence of rules used, we always end up with a sequent containing an ! together with either $\square$ or $\diamond$. An example of such a derivation is shown in Figure 7a. In our attempt to translate this rule, we are left with an unprovable sequent: indeed, the top sequent cannot be the conclusion of any rule in the system (except for cut and exchange, of course): $!\square A^\bullet$ cannot be principal since there is a $\diamond$-formula in the context, and $\diamond?B^\bullet$ cannot be principal since there is an !-formula.
<figure><img src="image_10.png" /><figcaption>Fig. 7: Translating the modal rule in a linear framework</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Fig. 8: Rules involving modalities for μLL<sub>□</sub><sup>∞</sup></figcaption></figure>

A natural solution is to allow !-promotion in contexts containing !, □-formulas on the left and ?, ◊-formulas on the right as in Figure 7c.<fnref n="1" /> The derivation of the translation of our (□<sub>p</sub>) instance can be completed as in Figure 7b.

Allowing □/◊-formulas in the context of a promotion rule has implications for the system's robustness to cut-elimination. For instance, taking the (?<sub>p</sub>/?<sub>w</sub>) principal case and adding modal formulas to the context naturally requires being able to weaken □ and ◊-formulas in the antecedent (resp. succedent):

$$ \frac{\frac{\Gamma \vdash \Sigma \quad ?_w \quad \frac{!\Delta, \Box A, C \vdash ?\Phi, \diamond \Psi}{\Gamma, !\Delta, \Box A \vdash \Sigma, ?\Phi, \diamond \Psi}}{\Gamma \vdash C, \Sigma} ?_p \quad \text{cut} \quad \sim \quad \frac{\Gamma \vdash \Sigma \quad \frac{\Gamma, !\Delta, \Box A \vdash \Sigma, ?\Phi, \diamond \Psi}{?_w, !_w, \Box w, \diamond w}}{\Gamma, !\Delta, \Box A \vdash \Sigma, ?\Phi, \diamond \Psi} $$

Similarly, the (?<sub>c</sub>/?<sub>p</sub>) key-case requires the ability to contract □/◊-formulas. We now give a formal definition of the linear-logical modal µ-calculus:

**Definition 6 (Linear-logical modal µ-calculus)** Pre-formulas of µLL<sub>□</sub><sup>∞</sup> are defined as: $F, G ::= a \in A | X \in V | \mu X.F | \nu X.F | F^{\perp} | F \neg G | F \neg G | F \otimes G | \perp | 1 | F \oplus G | F \& G | 0 | \top | ?F | !F | \diamond F | \Box F.$

We obtain positivity of an occurrence and the definition of formulas of µLL<sub>□</sub><sup>∞</sup> in the same way as for µLL<sub>□</sub><sup>∞</sup> and µLK<sub>□</sub><sup>∞</sup>. Rules for µLL<sub>□</sub><sup>∞</sup> are the rules for µLL<sup>∞</sup> together with those of Figure 8. Note that (!<sub>p</sub>) (resp. (?<sub>p</sub>)) is an instance of (!<sub>p</sub><sup>◇</sup>) (resp. (?<sub>p</sub><sup>□</sup>)). We define the sequents, pre-proofs, and proofs as in Section 2.

To justify the relevance of µLL<sub>□</sub><sup>∞</sup> we prove that there is a forgetful operation from µLL<sub>□</sub><sup>∞</sup> proofs to µLK<sub>□</sub><sup>∞</sup>, the skeleton. We define a translation SK(-) from µLL<sub>□</sub><sup>∞</sup> formulas, rules and pre-proofs to µLK<sub>□</sub><sup>∞</sup>:

<footnote n="1">¹ Note that allowing modal rules in contexts containing ? on the right and ! on the left would also solve our problem. However, forgetting the linear information of such a rule would not give us a rule derivable in µLK<sub>□</sub><sup>∞</sup>.</footnote>
**Definition 7 (μLK<sub>⊤</sub><sup>∞</sup>-Skeleton)** We define the skeleton of formulas inductively:

$$
\begin{align*}
\mathrm{SK}(1) &= \mathrm{T} & \mathrm{SK}(F \otimes G) &= \mathrm{SK}(F) \wedge \mathrm{SK}(G) & \mathrm{SK}(F^{\perp}) &= \mathrm{SK}(F)^{\perp} \\
\mathrm{SK}(\perp) &= \mathrm{F} & \mathrm{SK}(F \nparallel G) &= \mathrm{SK}(F) \vee \mathrm{SK}(G) & \mathrm{SK}(\diamond F) &= \diamond \mathrm{SK}(F) \\
\mathrm{SK}(\top) &= \mathrm{T} & \mathrm{SK}(F \& G) &= \mathrm{SK}(F) \wedge \mathrm{SK}(G) & \mathrm{SK}(\Box F) &= \Box \mathrm{SK}(F) \\
\mathrm{SK}(0) &= \mathrm{F} & \mathrm{SK}(F \oplus G) &= \mathrm{SK}(F) \vee \mathrm{SK}(G) & \mathrm{SK}(?F) &= \mathrm{SK}(F) \\
\mathrm{SK}(a) &= a & \mathrm{SK}(F \negmedspace \to \negmedspace G) &= \mathrm{SK}(F) \to \mathrm{SK}(G) & \mathrm{SK}(!F) &= \mathrm{SK}(F) \\
\mathrm{SK}(X) &= X & \mathrm{SK}(\mu X.F) &= \mu X.\mathrm{SK}(F) & \mathrm{SK}(\nu X.F) &= \nu X.\mathrm{SK}(F)
\end{align*}
$$

Sequents of μLK<sub>⊤</sub><sup>∞</sup> are translated to sequents of skeletons of these formulas.
Translation of rules are standard. Translations of pre-proofs are obtained co-
inductively by applying rule translations.

The following ensures that validity is preserved both ways by SK(-):

**Proposition 1 (Robustness of the skeleton to validity)** If $\pi$ is a valid pre-proof, then $\mathrm{SK}(\pi)$ is a $\mu\mathrm{LK}^\infty$ valid pre-proof, and vice versa.

4 Cut-elimination for μLK∞

To eliminate cuts in μLK<sub>⊤</sub><sup>∞</sup>, we employ a generalization of the cut inference called multicuts, as done in previous works on similar non-wellfounded proof systems [3,4,12,28].

**Definition 8 (Multicut rule)** The multicut rule is the following rule:

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

It can have any number of premises. The ancestor relation $\iota$ maps one formula
of the conclusion to exactly one formula of the premises, while the $\perp$-relation
links cut-formulas together, subject to acyclicity and connectedness conditions.

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

$$
\frac{\vdash A, B \quad B \vdash C \quad C \vdash D}{\vdash A, D} \mathrm{mcut}(\iota, \perp)
$$

The multicut rule should be seen as a tree of binary cuts, cf (cut/mcut)-case:

$$
\frac{C \quad \frac{\Gamma_1 \vdash F, \Delta_1 \quad \Gamma_2, F \vdash \Delta_2}{\Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2} \text{cut} \quad \frac{C}{\Gamma \vdash \Delta} \text{mcut}(\iota, \perp)}{\Gamma \vdash \Delta} \rightsquigarrow \frac{\Gamma_1 \vdash F, \Delta_1 \quad \Gamma_2, F \vdash \Delta_2}{\Gamma \vdash \Delta} \text{mcut}(\iota', \perp')
$$

Here, $\iota'(p) = \iota(p)$ for positions of formulas sent to $C$, and uses the ancestor relation of the cut-rule together with $\iota$ to determine the image of the other positions. The relation $\perp'$ is obtained from $\perp$ by adding $p \perp p'$, where $p$ and $p'$ are the positions of the two cut-formulas $F$.
$$
\begin{align*}
& \frac{\overline{\Gamma' \vdash \top, \Delta'} \top_r}{\Gamma \vdash \top, \Delta} \quad \mathcal{C} \quad \text{mcut}(\iota, \bot) \quad \rightsquigarrow \quad \overline{\Gamma \vdash \top, \Delta} \top_r \\
& \frac{\overline{\frac{\overline{\Gamma' \vdash \top, \Delta'} \top_r}{\Gamma \vdash \top, \Delta} \quad \mathcal{C}}}{\overline{\frac{\overline{\Gamma' \vdash \top, \Delta'} \top_r}{\Gamma \vdash \top, \Delta} \quad \mathcal{C}}} \quad \text{mcut}(\iota, \bot) \quad \rightsquigarrow \quad \overline{\frac{\overline{\Gamma' \vdash \top, \Delta'} \top_r}{\Gamma \vdash \top, \Delta} \quad \mathcal{C}} \quad \text{mcut}(\iota, \bot) \\
& \frac{\overline{\Gamma_1, F[X := \nu X.F] \vdash \Delta_1}}{\Gamma_1, \nu X.F \vdash \Delta_1} \quad \nu_l \quad \frac{\overline{\Gamma_2 \vdash F[X := \nu X.F], \Delta_2}}{\Gamma_2 \vdash \nu X.F, \Delta_2} \quad \nu_r \quad \mathcal{C} \quad \text{mcut}(\iota, \bot) \\
& \quad \rightsquigarrow \quad \frac{\overline{\Gamma_1, F[X := \nu X.F] \vdash \Delta_1}}{\Gamma \vdash \Delta} \quad \frac{\overline{\Gamma_2 \vdash F[X := \nu X.F], \Delta_2}}{\Gamma \vdash \Delta} \quad \mathcal{C} \quad \text{mcut}(\iota, \bot) \\
& \frac{\overline{\frac{\Gamma_1 \vdash A_1, \Delta_1}{\Gamma_1, \Gamma_2 \vdash A_1 \otimes A_2, \Delta_1, \Delta_2}}}{\Gamma \vdash \Delta} \quad \otimes_r \quad \frac{\overline{\Gamma_3, A_1, A_2 \vdash \Delta_3}}{\Gamma_3, A_1 \otimes A_2 \vdash \Delta_3} \quad \otimes_l \quad \mathcal{C} \quad \text{mcut}(\iota, \bot) \\
& \quad \rightsquigarrow \quad \frac{\overline{\Gamma_1 \vdash A_1, \Delta_1}}{\Gamma \vdash \Delta} \quad \frac{\Gamma_2 \vdash A_2, \Delta_2}{\Gamma \vdash \Delta} \quad \frac{\Gamma_3, A_1, A_2 \vdash \Delta_3}{\Gamma \vdash \Delta} \quad \mathcal{C} \quad \text{mcut}(\iota', \bot') \\
& \frac{\overline{\frac{\Gamma' \vdash A_1, \Delta'}{\Gamma' \vdash A_1 \& A_2, \Delta'}} \quad \mathcal{C}}{\overline{\frac{\Gamma' \vdash A_1, \Delta'}{\Gamma \vdash A_1 \& A_2, \Delta}}} \quad \&_r \quad \text{mcut}(\iota, \bot) \\
& \quad \rightsquigarrow \quad \frac{\overline{\frac{\Gamma' \vdash A_1, \Delta'}{\Gamma \vdash A_1, \Delta}} \quad \mathcal{C} \quad \text{mcut}(\iota, \bot)}{\overline{\frac{\Gamma' \vdash A_2, \Delta'}{\Gamma \vdash A_2, \Delta}}} \quad \&_r \quad \text{mcut}(\iota, \bot)
\end{align*}
$$

<caption>Fig. 9: Examples of (mcut)-step of µMALL$^{∞}$</caption>

## 4.1 The (mcut) reduction steps

As we use a multicut reduction strategy, we first describe the steps of reduction. To describe these mcut-steps of reduction, we will use a notation and a definition:

**Notation 1** (($\perp$)-contexts) If $\mathcal{C}$ is a list of $\mu LL_{\Box}^{\infty}$-proofs, we denote by $\mathcal{C}^{1/\Box}$ the list of proofs obtained by applying one of ($\top^{\diamond}_p$), ($\bot^{\diamond}_p$), ($\Box_p$) or ($\diamond_p$) rules to each proof of $\mathcal{C}$. If $\mathcal{C}$ is a list of $\mu LL_{\Box}^{\infty}$-proofs, we denote by $\mathcal{C}^{\Box}$ the list of proofs obtained by applying one of ($\Box_p$) or ($\diamond_p$) rules to each proof of $\mathcal{C}$.

**Definition 9 (Restriction of a mcut context)** Let $\frac{\mathcal{C}}{s}$ mcut($\iota, \bot$) be a multicut occurrence such that $\mathcal{C} = s_1 \dots s_n$ with $s_i := F_1, \dots, F_{k_i} \vdash G_1, \dots, G_{r_i}$. We define $C_{F_j}$ (resp. $C_{G_j}$) to be the sequents $\bot$-connected to the formula $F_j$ (resp. $G_j$). This is extended to contexts of formulas with $C_{\Gamma} := \cup_{F \in \Gamma} C_F$.

The mcut-reduction steps of $\mu MALL^{\infty}$ can be found in [4,28]; we provide examples of these steps in Figure 9. The reduction steps for the exponential and modal fragment of $\mu LL_{\Box}^{\infty}$ are presented in Figures 10 and 11, which include the exponential steps of $\mu LL^{\infty}$. For commutative steps, we present only the
$$
\begin{align*}
& \frac{\pi}{\substack{!\Gamma_1, \Box\Gamma_2 \vdash A, ?\Delta_1, \diamond\Delta_2 \\ !\Gamma', \Box\Gamma \vdash !A, ?\Delta, \diamond\Delta'}} \stackrel{!\Box}{\smile}_p \frac{C^{!/\Box}}{!\Gamma', \Box\Gamma \vdash !A, ?\Delta, \diamond\Delta'} \mathrm{mcut}(\iota, \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{!\Gamma_1, \Box\Gamma_2 \vdash A, ?\Delta_1, \diamond\Delta_2 \\ !\Gamma', \Box\Gamma \vdash A, ?\Delta, \diamond\Delta'}}{\substack{!\Gamma', \Box\Gamma \vdash !A, ?\Delta, \diamond\Delta' \\ !\Gamma', \Box\Gamma \vdash !A, ?\Delta, \diamond\Delta'}} \stackrel{!\Box}{\smile}_p \mathrm{mcut}(\iota, \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash A, \Delta \\ \Box\Gamma \vdash \Box A, \diamond\Delta \\ \Box\Gamma' \vdash \Box A, \diamond\Delta'}}{\Box_p} \stackrel{C^{\Box}}{\smile} \mathrm{mcut}(\iota, \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash A, \Delta \\ \Gamma \vdash \delta A, \Delta \\ \Gamma' \vdash \delta A, \Delta'}}{\Box\Gamma' \vdash \Box A, \diamond\Delta'} \stackrel{\delta_w}{C} \mathrm{mcut}(\iota, \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash \Delta \\ \Gamma \vdash \delta A, \Delta \\ \Gamma' \vdash \delta A, \Delta'}}{\Box\Gamma' \vdash \Box A, \diamond\Delta'} \stackrel{\delta_w}{C} \mathrm{mcut}(\iota', \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash \delta A, \delta A, \Delta \\ \Gamma \vdash \delta A, \Delta \\ \Gamma' \vdash \delta A, \Delta'}}{\Box\Gamma' \vdash \Box A, \diamond\Delta'} \stackrel{\delta_c}{C} \mathrm{mcut}(\iota, \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash \delta A, \delta A, \Delta \\ \Gamma' \vdash \delta A, \Delta \\ \Gamma' \vdash \delta A, \Delta'}}{\Box\Gamma' \vdash \Box A, \diamond\Delta'} \stackrel{\delta_c}{C} \mathrm{mcut}(\iota', \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash A, \Delta \\ \Gamma \vdash ?A, \Delta \\ \Gamma' \vdash ?A, \Delta'}}{\Box\Gamma' \vdash ?A, \diamond\Delta'} \stackrel{?_d}{C} \mathrm{mcut}(\iota, \perp) \\
& \stackrel{\pi}{\rightsquigarrow} \frac{\substack{\Gamma \vdash A, \Delta \\ \Gamma' \vdash A, \Delta \\ \Gamma' \vdash ?A, \Delta'}}{\Box\Gamma' \vdash A, \diamond\Delta'} \stackrel{?_d}{C} \mathrm{mcut}(\iota', \perp)
\end{align*}
$$

<caption>Fig. 10: $\mu LL_{\Box}^{\infty}$ exponential & modal commutative cut-elimination steps (commutation with right rules) – $\delta \in \{?, \diamond\}$</caption>

cases where the principal formula of the rule being commuted appears in the succedent of the sequent. For principal steps, we present only the cases where the cut-formula is a ?- or $\diamond$-formula. All other cases can be derived by duality.

**Definition 10 (Reduction sequence)** A reduction sequence $(\pi_i)_{i \in 1+\lambda}$ ($\lambda \in \omega + 1$) is a $\rightsquigarrow$ sequence s.t. $\pi_0$ contains at most one (mcut) rule per branch.

We aim to prove that each reduction sequence converges to a cut-free proof. However, this theorem is not true as stated, even for infinite reduction sequences: one could apply infinitely many reductions only on some part of the proof, without reducing cuts in another part of the proof. Therefore, we need to be more precise, which motivates the following definition, directly borrowed from [3,4] (the notion of residual is the usual one from rewriting):

**Definition 11 (Fair reduction sequences [3,4])** A mcut-reduction sequence $(\pi_i)_{i \in \omega}$ is fair if, for each $\pi_i$ such that there is a reduction $R$ to a proof $\pi'$, there exists a $j > i$ such that $\pi_j$ does not contain any residual of $R$.
<figure><img src="image_12.png" /><figcaption>Fig. 11: One side of the $\mu LL_\square^\infty$ exponential & modal principal cut-elimination steps – in all these proofs, $\delta \in \{?, \diamond\}$</figcaption></figure>

We can now state our cut-elimination theorem:

**Theorem 1 (Cut-elimination for $\mu LL_\square^\infty$)** Each fair (mcut)-reduction sequence of $\mu LL_\square^\infty$ valid proofs converges to a cut-free valid proof.

To prove it, we will translate formulas, proofs, and (mcut)-steps of $\mu LL_\square^\infty$ into $\mu LL^\infty$ and use the following cut-elimination result from [28]:

**Theorem 2 (Cut-elimination for $\mu LL^\infty$ [28])** Every fair (mcut)-reduction sequence of $\mu LL^\infty$ valid proofs converges to a cut-free valid proof.

**Remark 4** In [28], exponential formulas, proofs, and cut-steps are encoded into $\mu MALL^\infty$. We could have encoded $\mu LL_\square^\infty$ modalities into $\mu MALL^\infty$, replaying the proof of [28] for cut-elimination. However, using the $\mu LL^\infty$ cut-elimination theorem makes the result more modular and adaptable to future extensions of $\mu LL^\infty$ validity conditions or cut-elimination variants.

## 4.2 Translation of $\mu LL_\square^\infty$ into $\mu LL^\infty$

We provide a translation of $\mu LL_\square^\infty$ into $\mu LL^\infty$:

**Definition 12 (Translation of $\mu LL_\square^\infty$ into $\mu LL^\infty$)** The translation of formulas is defined inductively:
- *Translations of ♦ and □-formulas:* ($\diamond A)^{\circ} := ?A^{\circ}$ and ($\Box A)^{\circ} := !A^{\circ}$.

- *Translations of atomic and unit formulas and variables f:* $f^{\circ} := f$.

- *Translations of fixed-point:* $(\delta X.F)^{\circ} := \delta X.F^{\circ}$ (with $\delta \in \{\mu, \nu\}$).

- *Translations of other connectives:* $c(A_1, \dots, A_n)^{\circ} := c(A_1^{\circ}, \dots, A_n^{\circ})$.

Translations of structural rules for modalities, ($\diamond c$), ($\diamond w$), ($\Box c$) and ($\Box w$) are respectively ($?c$), ($?w$), ($!c$) and ($!w$). Translations for the promotions ($!^{\diamond p}$) and ($?^{\Box p}$) are respectively ($!_p$) and ($?_p$). Translations of the modal rules are given by:

$$ \frac{\Gamma \vdash A, \Delta \qquad \frac{\Gamma^{\circ} \vdash A^{\circ}, \Delta^{\circ}}{!^{\Gamma^{\circ}} \vdash !^{\Delta^{\circ}}} !_{d}^{\#(\Gamma)}, !_{d}^{\#(\Delta)}} \Box_{p} \rightsquigarrow \frac{\Gamma^{\circ} \vdash A^{\circ}, ?^{\Delta^{\circ}}}{!^{\Gamma^{\circ}} \vdash !^{A^{\circ}}, ?^{\Delta^{\circ}}} !_{p}^{\#} \\ \frac{\Gamma, A \vdash \Delta \qquad \frac{\Gamma^{\circ}, A^{\circ} \vdash \Delta^{\circ}}{!^{\Gamma^{\circ}}, A^{\circ} \vdash ?^{\Delta^{\circ}}} !_{d}, ?_{d}} \Box_{\Gamma} \diamond A \vdash \diamond \Delta \quad \rightsquigarrow \frac{\Gamma^{\circ}, A^{\circ} \vdash \Delta^{\circ}}{!^{\Gamma^{\circ}}, ?^{\Delta^{\circ}}, ?^{\Delta^{\circ}}} !_{p}^{\#} $$

Translations of other inference rules (r) are (r) themselves. Translations of pre-proofs are defined co-inductively using translations of rules.

The translation preserves the validity of pre-proof in both directions:

**Lemma 1 (Validity robustness to $(-)^{\circ}$ translation)** Let $\pi$ be a $\mu LL_{\Box}^{\infty}$ pre-proof. The proof $\pi$ is valid if and only if the proof $\pi^{\circ}$ is valid.

*Proof.* Let $B$ be a branch of $\pi$. We have that $B$ is validated by a thread $(A_i)$ if and only if $B^{\circ}$ is validated by $(A_i^{\circ})$, as the minimal recurring fixed point formula is a $\nu$ on the right (resp. $\mu$ on the left) in $(A_i)$ if and only if it is in $(A_i^{\circ})$.

Finally, we need to ensure that (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 2** Consider a $\mu LL_{\Box}^{\infty}$ reduction step $\pi_0 \rightsquigarrow \pi_1$. There exist a finite number of $\mu LL^{\infty}$ proofs $\theta_0, \dots, \theta_n$ such that: $\pi_0^{\circ} = \theta_0 \to \theta_1 \to \dots \to \theta_{n-1} \to \theta_n = \pi_1^{\circ}$.

*Proof (Proof sketch).* Reductions from the non-exponential part of $\mu LL_{\Box}^{\infty}$ translate easily to one step of reduction in $\mu LL^{\infty}$. The same is true for the exponential part, except for the commutation of the modal rule. The translation of the left proof of this step is of the form (we only consider the case of $\diamond_p$; $\Box_p$ is similar):

$$ \frac{\pi_i^{\circ} \qquad \pi_j^{\circ} \qquad \frac{!\Gamma_i^{\circ} \vdash A_i^{\circ}, \Delta_i^{\circ}}{!\Gamma_j^{\circ} \vdash A_j^{\circ}, ?\Delta_j^{\circ}} !_d, ?_d \qquad \frac{!\Gamma_j^{\circ} \vdash A_j^{\circ} \vdash ?\Delta_j^{\circ}}{!\Gamma_j^{\circ}, ?A_j^{\circ} \vdash ?\Delta_j^{\circ}} ?_p \qquad \text{with } 1 \le i \le n \text{ & } n+1 \le j \le n+m}{\vdash !A_i^{\circ}, ?\Gamma_i^{\circ}} \text{ mcut}(i, \perp) $$

Here, we notice that for each dereliction on a cut-formula, there exists a corresponding promotion that will be erased by a dereliction/promotion key-case. The first promotion will therefore commute under the cut, and then each dereliction on formulas of the conclusion will commute as well. Each dereliction and each promotion on cut-formulas will be erased, giving us the correct translation.
Now that we know that a step of (mcut)-reduction in $\mu LL_{\Box}^{\infty}$ translates to one or more $\mu LL^{\infty}$ (mcut)-reduction steps, it is easy to translate each reduction sequence of $\mu LL_{\Box}^{\infty}$ into a reduction sequence of $\mu LL^{\infty}$. However, to use the cut-elimination theorem of $\mu LL^{\infty}$, we need the reduction sequence to be fair. The purpose of the following lemma is to control the fairness of the translated reduction sequence:

**Lemma 3 (Completeness of the (mcut)-reduction system)** Let $\pi$ and $\pi'$ be two $\mu LL_{\Box}^{\infty}$ proofs. If there is a $\mu LL^{\infty}$-redex $\mathcal{R}$ sending $\pi^{\circ}$ to $\pi'$, then there is also a $\mu LL_{\Box}^{\infty}$-redex $\mathcal{R}'$ sending $\pi$ to a proof $\pi''$, such that in the translation of $\mathcal{R}'$, $\mathcal{R}$ is reduced.

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

- If the case is the commutative step of a weakening (resp. contraction, resp. dereliction) ($r$), it necessarily means that ($r$) is the translation of a rule ($r'$) being a contraction (resp. weakening, resp. dereliction) which is also on top of a (mcut) in $\pi$. We can take $\mathcal{R}'$ as the step commuting ($r'$) under the cut.

- If it is a principal case on a contraction or a weakening ($r$) on a formula $?A$ (resp. $!A$), it means that each proof cut-connected to $?A$ (resp. $!A$) ends with a promotion. As $\pi^{\circ}$ is the translation of a $\mu LL_{\Box}^{\infty}$-proof, it means that ($r$) is the translation of a weakening or contraction rule ($r'$) on a formula $?A'$ (resp. $!A'$) or $\diamond A'$ (resp. $\Box A'$) on top of a (mcut). It also means that all the proofs cut-connected to these formulas are promotions or modal rules (no other rules than a modal rule or a promotion in $\mu LL_{\Box}^{\infty}$ translates to a derivation ending with a promotion). Therefore, $\mathcal{R}'$ is the principal case on ($r'$).

- If it is a dereliction/promotion key case, the dereliction (resp. promotion) is the translation of a dereliction (resp. promotion). We take $\mathcal{R}'$ to be the redex formed by these two rules.

- If it is the commutative step of a promotion ($r$), it means that all the proofs of the contexts of the (mcut) are promotion rules. This means that all these rules come from the translation of promotion or modal rules. We need to ensure that each (mcut) with a context full of promotions or modal rules is covered by the (mcut)-reductions of $\mu LL_{\Box}^{\infty}$:

* The commutation of $(!_{\Box}^{\diamond})$ (or $(?_{\Box}^{\Box})$) is covered by the first commutative case in Figure 10.

* If it is a modal rule that is ready to be commuted, then other rules are necessarily modal rules and therefore is covered by the second commutative case in Figure 10.

We use the two previous lemmas, to prove the following:

**Corollary 1** If $\lambda \in \omega + 1 \ \& \ (\pi_i)_{i \in 1+\lambda}$ is a fair $\mu LL_{\Box}^{\infty}$ reduction sequence, then:

- there exists a fair $\mu LL^{\infty}$ reduction sequence $(\theta_i)_{i \in 1+\lambda'}$ with $\lambda' \in \omega + 1$;

- there exists a sequence of strictly increasing $(\varphi(i))_{i \in 1+\lambda'}$ of elements of $1+\lambda'$;
<figure><img src="image_13.png" /><figcaption>Fig. 12: Translating the Modal Rule with Non-Empty Antecedent</figcaption></figure>

— such that for each $i$, $\theta_{\varphi(i)} = \pi_i^o$.

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

— For $i = 0$: $\theta_0 = \pi_0^o$ and $\varphi(0) = 0$:

— For $i + 1$, suppose we have defined both sequences up to rank $i$. We use Lemma 2 on the step $\pi_i \rightsquigarrow \pi_{i+1}$ to get a finite sequence of reduction $\pi_i = \theta_0' \rightsquigarrow \dots \rightsquigarrow \theta_n' = \pi_{i+1}$. We then construct both sequences by setting $\varphi(i + 1) := \varphi(i) + n$, $\theta_{\varphi(i)+j} := \theta'_j$ (for $j \in [0, n]$).

Fairness of $(\theta_i)_{i \in 1+\lambda'}$ follows from Lemma 3 and from the fact that after the translation of an (mcut)-step, $\pi^o \rightsquigarrow \pi'^o$, each residual of a redex $\mathcal{R}$ of $\pi^o$, is contained in the translations of residuals of the associated redex $\mathcal{R}'$ of Lemma 3.

## 4.3 Cut-elimination for $\mu LL^\infty$

Finally, we can prove the main theorem of the section:

*Proof (of Theorem 1).* Let $(\pi_i)_{i \in 1+\lambda}$ be a fair $\mu LL^\infty$ reduction sequence. We use Corollary 1 and get a fair $\mu LL^\infty$ reduction sequence $(\theta_i)_{i \in 1+\lambda'}$ and a sequence $(\varphi(i))_{i \in 1+\lambda}$ of natural numbers. By Theorem 2, we know that $(\theta_i)_{i \in \omega}$ converges to a cut-free proof $\theta$ of $\mu LL^\infty$. Now suppose for the sake of contradiction that $(\pi_i)_{i \in 1+\lambda}$ does not converge to an (mcut)-free pre-proof. There is a $j$ and a path $p$ such that for each proof $\pi_{j'}$, with $j' \ge j$, there is an (mcut)-rule at the end of path $p$. This means that the translation of $p$ leads to an (mcut) for each proof $\theta_{j'}$ with $j' \ge \varphi(j)$, contradicting the convergence of $(\theta_j)$ to a cut-free proof. Moreover $(\pi_i)$ converges to a pre-proof $\pi$ such that $\pi^o = \theta$, since $\theta_{\varphi(j)}$ equals $\pi_j^o$ under multicuts. Since $\theta$ is cut-free, $\pi$ is both valid and cut-free by Lemma 1.

## 5 Cut-elimination of $\mu LK^\infty$

We extend the linear translation of $\mu LK^\infty$ from [28] to a translation from $\mu LK^\infty$ into $\mu LL^\infty$. The tentative translation of the modal formulas studied at the beginning of Section 3 actually only works with an empty antecedent. Adapting our
<figure><img src="image_14.png" /><figcaption>Fig. 13: Linear translation of the modal rules</figcaption></figure>

example by adding an antecedent to it: $\Gamma \vdash F, \Delta \quad \Box \Gamma \vdash \Box F, \Diamond \Delta \quad \Box p$ results in a derivation

attempt as shown in Figure 12a. If $\Gamma$ contains more than two formulas, $(?_p)$ can-
not be applied. However, adding an !-connective in the translation of $\Box$-formulas
as $\Box A^* := !\Box !A^*$, allows us to complete the derivation (see Figure 12b).

Based on this, we define a translation from $\mu LK_{\Box}^{\infty}$ into $\mu LL_{\Box}^{\infty}$:

**Definition 13 (Linear translation of $\mu LK_{\Box}^{\infty}$)** The translation $(-)^{\bullet}$ from $\mu LK_{\Box}^{\infty}$ formulas to $\mu LL_{\Box}^{\infty}$ formulas is defined by induction on formulas:

$$ (A_1 \to A_2)^* := !(?A_1 \to ?A_2^*) \qquad X^* := !X \qquad (\mu X.A)^* := !\mu X.?A^* $$

$$ (A_1 \wedge A_2)^* := !(?A_1^* \& ?A_2^*) \qquad T^* := !\top \qquad (\nu X.A)^* := !\nu X.?A^* $$

$$ (A_1 \vee A_2)^* := !(?A_1^* \oplus ?A_2^*) \qquad F^* := !0 \qquad (\Diamond A)^* := !\Diamond A^* $$

$$ (A^{\perp})^* := !(?A^*)^{\perp} \qquad a^* := !a \qquad (\Box A)^* := !\Box !A^* $$

Sequents are translated as $(\Gamma \vdash \Delta)^* := \Gamma^* \vdash ?\Delta^*$.

The following property must be kept in mind when defining rule translations
and is proved by an induction the formulas of $\mu LK_{\Box}^{\infty}$:

**Proposition 2** For any $\mu LK_{\Box}^{\infty}$ formula $A$, $A^*$ is an !-formula.

We provide the translation of modal rules in Figure 13. We define translations of proofs coinductively using rule translations. As the smallest formula of a totally ordered set of translations is the translation of the smallest formula, and branches of $\pi^*$ contain translations of threads from $\pi$ and vice-versa, we have:

**Lemma 4 (Robustness of $(-)^*$ to validity)** A pre-proof $\pi$ is valid if and only if $\pi^*$ is valid.

**Lemma 5 (Composition of SK(-) and of $(-)^*$)** For any $\mu LK_{\Box}^{\infty}$ pre-proof $\pi$, SK($\pi^*$) is equal to $\pi$.

We define our rewriting system using the SK(-) translation:

**Definition 14 ((mcut)-rewriting system of $\mu LK_{\Box}^{\infty}$)** The (mcut)-rewriting system of $\mu LK_{\Box}^{\infty}$ is defined as the (mcut)-system obtained from the $\mu LL_{\Box}^{\infty}$ (mcut)-system by discarding the linear information of proofs in this system.
Finally, we have the following theorem:

**Theorem 3** The reduction system of $\muLK_{\square}^{\infty}$ is infinitary weakly-normalizing.

*Proof.* Consider a $\muLK_{\square}^{\infty}$ proof $\pi$ and a fair reduction sequence $\sigma_{\mathrm{L}}$ from $\pi^{\bullet}$. By Theorem 1, $\sigma_{\mathrm{L}}$ converges to a cut-free $\mu LL_{\square}^{\infty}$ proof. By applying $\mathrm{SK}(-)$ to each proof in the sequence, we obtain a sequence of valid $\muLK_{\square}^{\infty}$ proofs such that either $\mathrm{SK}(\pi_i) = \mathrm{SK}(\pi_{i+1})$ or $\mathrm{SK}(\pi_i)$ reduces to $\mathrm{SK}(\pi_{i+1})$ with one step of $\muLK_{\square}^{\infty}$ mcut-reduction. We obtain a $\muLK_{\square}^{\infty}$ cut-reduction sequence $\sigma_{\mathrm{K}}$ that is infinite and converges to a valid, cut-free $\muLK_{\square}^{\infty}$ proof.

# 6 Conclusion

We have introduced $\mu LL_{\square}^{\infty}$, a linear version of the modal $\mu$-calculus, along with its circular and non-wellfounded proof systems. We have proved a cut-elimination theorem for fair cut-elimination reduction sequences, generalizing previous results on the non-wellfounded proof theory of linear logic. Through a linear translation of the circular and non-wellfounded proof systems for the modal $\mu$-calculus ($\muLK_{\square}^{\infty}$) to $\mu LL_{\square}^{\infty}$, we have obtained a cut-elimination theorem for the non-wellfounded sequent calculus of the modal $\mu$-calculus.

In our opinion, this work presents a new and interesting application of linear logic to the modal $\mu$-calculus, developing proof theories in both domains and highlighting the potential for cross-fertilization for the two communities. Indeed, this constitutes the first full syntactic cut-elimination theorem for a proof system modeling the full modal $\mu$-calculus.

Furthermore, the fine-grained cut-elimination inherited from linear logic opens up the possibility of developing a non-trivial cut-elimination equivalence on $\muLK_{\square}^{\infty}$ proofs. This, in turn, could lead to the design of a denotational semantics for proofs of modal $\mu$-calculus, a question that was previously out of reach due to both the lack of a syntactic cut-elimination theorem and the absence of structure in proofs of the modal $\mu$-calculus.

However, this is not the first work studying both linear logic and modal logic. Notably, studies on modal logic S4 through linear logic have addressed both its intuitionistic fragment, proving cut-admissibility [13], and its classical version [19,29]. Our work differs from these studies in two key aspects: (i) We employ a non-wellfounded setting. (ii) The logic S4 treats modalities as linear logic exponentials with a standard promotion and dereliction, making it a sub-system of the subexponentials [23]. Our work is different because we use a functorial promotion for modal rules, which requires us to examine the interaction between functorial and non-functorial promotion.

An important direction for future work is to explore whether our linear-logical modal mu-calculus can be adapted to wellfounded proof-systems of linear logic with fixed-points in a $\mu LL_{\square}$ sequent calculus. We aim to investigate if our methodology can be extended to obtain a cut-elimination theorem for the
finitary modal µ-sequent calculus via a linear translation from $\mu LL_\square$ to $\mu LL_\square$, building upon Baelde's results [2]. This question presents significant challenges due to the complex structure of fixed-point rules in finitary $\mu LL$. While omitting linear information from $\mu LL_\square$ proofs should yield $\mu LL_\square$ proofs that simulate cut-elimination, designing a linear translation from $\mu LL_\square$ to $\mu LL_\square$ that commutes with cut-elimination, as shown in this paper, remains a non-trivial task.

From the linear logic-theoretic point of view, our system $\mu LL_\infty$ can be viewed as a linear logic with two sets of exponential modalities satisfying different structural rules and exponentials. This is akin to so-called *light logics* [15,18], that are variants of linear logics developed by taming the power of exponential modalities in order to control the complexity of cut-elimination (for instance constraining the ?-context of a promotion to be immediately derelicted after a promotion ensures that typable programs have at most elementary complexity [15]).

Building on these ideas, we propose to develop a uniform framework for proving cut elimination in wellfounded proof systems of linear logic fragments that encompass both light logics and modal logics. This framework could be inspired by the subexponential system of Nigam & Miller [23] and the first author with Laurent [5], but extended to include functorial promotion. Such a system would allow us to treat light logics and our linear-logical modal mu-calculus as instances of a more general linear logic system.

In a similar direction, we shall investigate whether our approach of reducing cut-elimination to that of simpler systems can be useful for the circular approaches to session types [11,31] as well as to the study of productivity and normalization properties in functional reactive programming [8].

**Funding.** This work was partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.

**Acknowledgments.** The authors would like to thank the anonymous reviewers for their constructive and valuable comments, as well as Anupam Das, Abhishek De, Farzad Jafarrahmani, Johannes Kloibhofer, Paul-André Melliès and Bahareh Afshari for fruitful discussions on this work.

## References

1. Afshari, B., Leigh, G.E.: Cut-free completeness for modal mu-calculus. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–12 (2017). https://doi.org/10.1109/LICS.2017.8005088

2. Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Log. 13(1), 2:1–2:44 (2012). https://doi.org/10.1145/2071368.2071370. URL https://doi.org/10.1145/2071368.2071370

3. Baelde, D., Doumane, A., Kuperberg, D., Saurin, A.: 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. Association for Computing Machinery, New York, NY, USA
(2022). https://doi.org/10.1145/3531130.3533375. URL https://doi.org/10.1145/3531130.3533375

4. Baelde, D., Doumane, A., Saurin, A.: Infinitary Proof Theory: the Multiplicative Additive Case. In: CSL 2016, LIPIcs, vol. 62, pp. 42:1–42:17 (2016). https://doi.org/10.4230/LIPIcs.CSL.2016.42. URL http://drops.dagstuhl.de/opus/volltexte/2016/6582

5. Bauer, E., Laurent, O.: Super exponentials in linear logic. Electronic Proceedings in Theoretical Computer Science 353, 50–73 (2021). https://doi.org/10.4204/epcs.353.3. URL http://dx.doi.org/10.4204/EPTCS.353.3

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

7. Buss, S.R. (ed.): Handbook of Proof Theory. Elsevier, New York (1998)

8. Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair reactive programming. In: S. Jagannathan, P. Sewell (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pp. 361–372. ACM (2014). https://doi.org/10.1145/2535838.2535881. URL https://doi.org/10.1145/2535838.2535881

9. Curien, P., Herbelin, H.: The duality of computation. In: ICFP 2000, pp. 233–243. ACM (2000). https://doi.org/10.1145/351240.351262. URL https://doi.org/10.1145/351240.351262

10. Danos, V., Joinet, J., Schellinx, H.: A new deconstructive logic: Linear logic. J. Symb. Log. 62(3), 755–807 (1997). https://doi.org/10.2307/2275572. URL https://doi.org/10.2307/2275572

11. Derakhshan, F., Pfenning, F.: Circular proofs as session-typed processes: A local validity condition. Logical Methods in Computer Science Volume 18, Issue 2, 8 (2022). https://doi.org/10.46298/lmcs-18(2:8)2022. URL https://lmcs.episciences.org/5675

12. Doumane, A.: On the infinitary proof theory of logics with fixed points. Phd thesis, Paris Diderot University (2017)

13. Fukuda, Y., Yoshimizu, A.: A linear-logical reconstruction of intuitionistic modal logic S4. CoRR abs/1904.10605 (2019). URL http://arxiv.org/abs/1904.10605

14. Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987). https://doi.org/10.1016/0304-3975(87)90045-4. URL https://doi.org/10.1016/0304-3975(87)90045-4

15. Girard, J.Y.: Light linear logic 143(2), 175–204 (1998). https://doi.org/10.1006/inco.1998.2700

16. Jäger, G., Kretz, M., Studer, T.: Canonical completeness of infinitary $\mu$. The Journal of Logic and Algebraic Programming 76(2), 270–292 (2008). https://doi.org/https://doi.org/10.1016/j.jlap.2008.02.005. URL https://www.sciencedirect.com/science/article/pii/S1567832608000209. Logic and Information: From Logic to Constructive Reasoning

17. Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983). https://doi.org/10.1016/0304-3975(82)90125-6. URL https://doi.org/10.1016/0304-3975(82)90125-6

18. Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1–2), 163–180 (2004). https://doi.org/10.1016/j.tcs.2003.10.018

19. Martini, S., Masini, A.: A modal view of linear logic. Journal of Symbolic Logic 59(3), 888–899 (1994). https://doi.org/10.2307/2275915
20. Miller, D.: Finding unity in computational logic. In: Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS ’10. BCS Learning & Development Ltd., Swindon, GBR (2010)

21. Mints, G.: Effective cut-elimination for a fragment of modal mu-calculus. Studia Logica: An International Journal for Symbolic Logic **100**(1/2), 279–287 (2012). URL http://www.jstor.org/stable/41475226

22. Mints, G., Studer, T.: Cut-elimination for the mu-calculus with one variable. Electronic Proceedings in Theoretical Computer Science **77**, 47–54 (2012). https://doi.org/10.4204/eptcs.77.7. URL http://dx.doi.org/10.4204/EPTCS.77.7

23. Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: PPDP 2009, p. 129–140. ACM, New York, NY, USA (2009). https://doi.org/10.1145/1599410.1599427. URL https://doi.org/10.1145/1599410.1599427

24. Niwiński, D., Walukiewicz, I.: Games for the μ-calculus. Theoretical Computer Science **163**(1), 99–116 (1996). https://doi.org/10.1016/0304-3975(95)00136-0. URL https://www.sciencedirect.com/science/article/pii/0304397595001360

25. Pagani, M., Tortora de Falco, L.: Strong normalization property for second order linear logic. Theoretical Computer Science **411**(2), 410–444 (2010)

26. Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: M. Nielsen, U. Engberg (eds.) Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2303, pp. 357–371. Springer (2002). https://doi.org/10.1007/3-540-45931-6_25. URL https://doi.org/10.1007/3-540-45931-6_25

27. Santocanale, L.H.M.l., Fortier, J.: Cuts for circular proofs: semantics and cut-elimination. In: Computer Science Logic 2013, LIPIcs, vol. 23, pp. 248–262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Torino, Italy (2013). https://doi.org/10.4230/LIPIcs.CSL.2013.248. URL https://hal.science/hal-01260986

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

29. Schellinx, H.: A Linear Approach to Modal Proof Theory, pp. 33–43. Springer Netherlands, Dordrecht (1996). https://doi.org/10.1007/978-94-017-2798-3_3. URL https://doi.org/10.1007/978-94-017-2798-3_3

30. Stirling, C.: Modal and Temporal Logics. In: Handbook of Logic in Computer Science. Oxford University Press (1992). https://doi.org/10.1093/oso/9780198537618.003.0005. URL https://doi.org/10.1093/oso/9780198537618.003.0005

31. Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: M. Maffei, E. Tuosto (eds.) Trustworthy Global Computing, pp. 159–175. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
**Open Access.** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution, and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

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