A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Saurin, Alexis; Bauer, Esaïe

doi:10.4230/LIPIcs.CSL.2026.17

A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Alexis Saurin

Université Paris Cité & CNRS & INRIA, Pl. Aurélie Nemours, 75013 Paris, France Esaïe Bauer

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

Abstract

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives.

Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination.

More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal $\mu$ -calculus.

Keywords and phrases:

cut elimination, exponential modalities, fixed-points, linear logic, light logics, mu-calculus, non-wellfounded proofs, proof theory, sequent calculus, subexponentials, super exponentials

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Linear logic ; Theory of computation

\rightarrow

Proof theory

Related Version:

Long version: https://arxiv.org/abs/2506.14327 [7]

Funding:

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

DOI:

10.4230/LIPIcs.CSL.2026.17

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

On the redundancy of cut-elimination proofs.

While cut-elimination is certainly a cornerstone of structural proof theory since Gentzen’s introduction of the sequent calculus, an annoying fact is that a slight change in a proof system induces the need to reprove globally the cut-elimination property. Such redundant new proofs are usually quite boring and fastidious, often lacking any new insight: cut-elimination results lack modularity.

This results in the need for re-establishing a theorem which differs only very marginally from a previously proven one, even though the details are very technical and the failure of cut-elimination may hide in those small variants. There are mainly two directions to try and make cut-elimination results more uniform, namely reduction and axiomatization:

Cut-elimination by reduction: The first option consists in proving a new cut-elimination result by means of translation between proof systems, allowing us to reduce the cut-elimination property of a given system to that of another one for which the property is already known. Very frequent in term-calculi such as the variants of the $\lambda$ -calculus, this approach is also applied in proof theory, for instance in translations between classical, intuitionistic and linear logics [14, 15] where linear translations come with such simulation results. A recent application of this approach is the second author’s proof of cut-elimination for $\mu\text{LL}^{\infty}$ , the infinitary proof system for linear logic extended with least and greatest fixed-points, which is proved [22] by a reduction to the cut-elimination property of the exponential-free fragment of the logic [2], while dealing with the infinitary features of such proof systems.
Axiomatizing systems eliminating cuts: The second option consists in abstracting properties ensuring that cut-elimination holds in a sequent calculus, and to provide sufficient conditions for cut-elimination to hold. For instance, after Nigam and Miller’s work on subexponentials [20] providing a family of logics extending LL with exponential admitting various structural rules, the first author and Laurent provided a systematic and generic setting that captures most of the light logics to be found in the literature [16, 18], superLL, for which they provided a uniform proof of cut-elimination based on an axiomatization stating a set of sufficient conditions for cut-elimination to hold [6]. Another line of work, more algebraic, establishing sufficient conditions for cut-elimination is that of Terui et al. [11, 24, 10, 25, 9] which established modular and systematic cut-elimination results by combining methods from proof theory and algebra.

Linear modal $\mu$ -calculus.

One of the motivations originated in our recent work [5] establishing a cut-elimination theorem for the classical modal $\mu$ -calculus with infinite proofs. A key step in our work consisted in proving cut-elimination of $\mu\text{LL}_{\Box}^{\infty}$ , a linear variant of the classical modal $\mu$ -calculus, to which cut-elimination of the classical modal $\mu$ -calculus could be reduced. Indeed, linear logic offers powerful tools for translating systems like $\mu\text{LK}^{\infty}$ [22] and $\mu\text{LK}_{\Box}^{\infty}$ [17] into linear systems making the transfer of properties of those systems to other logics efficient. The study of cut-elimination for $\mu\text{LL}_{\Box}^{\infty}$ naturally leads to considering a more systematic treatment of exponentials and modalities revisiting work by the first author and Laurent [6] and introducing $\mu\text{superLL}^{\infty}$ .

Light logics with least and greatest fixed points.

Taming the deductive power of linear logic’s exponential connectives allows one to get complexity bounds on the cut-elimination process [16, 18]. Adding fixed points in such logics enriches the study of complexity classes [3, 8, 21, 12], as well as the study of light $\lambda$ -calculi enriched with fixpoints as in [4].

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

The systems discussed in the previous paragraph differ from those defined in the present article: they are based on recursive types while we consider extremal fixed-points (i. e., inductive and coinductive types) and we base our study on potentially infinite and regular derivation trees, etc. However, both systems have strong similarities that we shall discuss in a later section, making a stronger link between our systems and light systems from the literature.

Organization and contributions of the paper.

The main contribution of this paper is a syntactic cut-elimination result for a large class of (parametrized) linear systems with least and greatest fixed-points coming with a notion of non-wellfounded and regular proofs. More precisely, we show that the two approaches described above can be mixed in order to provide a uniform cut-elimination proof for a large family of logics called $\mu\text{superLL}^{\infty}$ that extends both $\mu\text{LL}^{\infty}$ and super exponentials: (i) a single proof is obtained for a large class of proof systems and (ii) by relying on a proof translation method, no new termination measure needs to be designed, and the argument simply relies on simulation results from one logic to another. In Section 2, we recall some definitions and results about infinitary rewriting theory and linear logic. Section 3 introduces a variant of the first author and Laurent’s system of super exponentials [6] on which we set up, in Section 4, a parametrized system, $\mu\text{superLL}^{\infty}$ , which is superLL extended with fixed-points and non-wellfounded proofs. Finally, in Section 5, we define the cut reduction system that achieves syntactic cut-elimination and provide the proof of our main theorem, the cut-elimination of $\mu\text{superLL}^{\infty}$ , through an encoding into $\mu\text{LL}^{\infty}$ . As a corollary, we get cut-elimination theorems for the two proof systems considered above: $\mu\text{LL}_{\Box}^{\infty}$ and $\mu\text{ELL}^{\infty}$ . Further details, clarifications, examples, and detailed proofs are provided either in the appendices or in the long version of this paper [7].

2 Background on LL, fixed-points and non-wellfounded proofs

In this paper, we study the proof theory of different systems of linear logic (LL). It is much more convenient to work on one-sided sequent systems as proofs and descriptions of these systems are more compact than in the two-sided version. However, the results for the two-sided systems can be retrieved systematically from the one-sided systems with straightforward and well-known translations between them as in [22] for instance.

2.1 Formulas, sequent calculi and non-wellfounded proofs

Let $\mathcal{V}$ and $\mathcal{A}$ be two disjoint countable sets of fixed-point variables and atomic formulas respectively. The (pre-)formulas of $\mu\text{LL}$ are defined inductively as ( $a\in\mathcal{A},X\in\mathcal{V}$ ):
$F,G\hskip 5.0pt::=\hskip 5.0pta\nobreakspace\mid a^{\perp}\mid X\mid\mu X.F% \mid\nu X.F\nobreakspace\mid F\invamp G\mid F\otimes G\mid\bot\mid 1\mid F% \oplus G\mid F\with G\mid 0\mid\top\mid\wn F\mid\oc F.$
Formulas of $\mu\text{LL}^{\infty}$ are such closed pre-formulas ( $\mu$ and $\nu$ being binders for variables in $\mathcal{V}$ ). By considering the $\{\mu,\nu,X\}$ -free formulas of this system, we get LL, the usual formulas of linear logic [15]. By considering the $\{\oc,\wn\}$ -free formulas of it, we get the formulas of $\mu\text{MALL}^{\infty}$ , the multiplicative and additive linear logic with fixed points [2]. By considering the intersection of these two subsets of formulas, we get the formulas of MALL, the multiplicative and additive linear logic. The $\{\wn,\oc\}$ -fragment is called the exponential fragment of linear logic.

Definition 1 (Negation).

We define $(-)^{\perp}$ to be the involution on formulas satisfying:

\begin{array}[]{clclclcl}\bot^{\perp}&=1\nobreak\nobreak&X^{\perp}&=X\nobreak% \nobreak&(A_{1}\otimes A_{2})^{\perp}&=A_{1}^{\perp}\invamp A_{2}^{\perp}% \nobreak\nobreak&(A_{1}\with A_{2})^{\perp}&=A_{1}^{\perp}\oplus A_{2}^{\perp}% \\ \top^{\perp}&=0&{a^{\perp}}^{\perp}&=a&(\mu X.F)^{\perp}&=\nu X.F^{\perp}&% \nobreakspace(\wn F)^{\perp}&=\oc F^{\perp}\end{array}

The sequent calculi that we consider in this paper are built on one-sided sequents: a sequent is a list of formulas $\Gamma$ , that we usually write $\vdash\Gamma$ . Usually, in the literature, derivation rules are defined as a scheme of one conclusion sequent and a (possibly empty) list of hypotheses sequents. In our system, the derivation rules come equipped with an ancestor relation linking each formula in the conclusion to zero, one, or several formulas of the hypotheses. When defining our rules, we provide this link by drawing the ancestor relation with colors (see Figures 1, 2, and 3). As usual, some formulas may be distinguished as principal formulas: both formulas in the conclusion of an axiom rule are principal, no formula is principal in the conclusion of an $(\text{ex})$ or $(\text{cut})$ inference while in other rules of Figures 1, 2, and 3 the leftmost occurrence of each conclusion sequent is principal.

Definition 2 (MALL, LL and $\mu\text{LL}^{\infty}$ inference rules).

Figure 1 defines MALL inference rules.

Figure 1: one-sided MALL rules.

LL inferences are obtained by considering Figures 1 and 2.

Figure 2: one-sided exponential fragment of LL.

Finally, inference rules for $\mu\text{MALL}^{\infty}$ and $\mu\text{LL}^{\infty}$ are obtained by adding rules of Figure 3 to MALL and LL inferences.

Figure 3: Rules for the fixed-point fragment.

In the rest of the article, we will not write the exchange rules explicitly: one can assume that every rule is preceded and followed by a finite number of instances of $(\text{ex})$ . While proofs for MALL and LL are the usual trees inductively generated by the inference rules, defining non-wellfounded proofs for fixed-point logics requires some definitions:

Definition 3 (Pre-proofs).

Given a set of derivation rules, we define pre-proofs to be the trees co-inductively generated by rules of each of those systems. Regular (or circular) pre-proofs are those pre-proofs having a finite number of distinct sub-proofs.

We represent regular proofs with back-edges as in the following example:

Example 4 (Regular proof).

We give an example of circular proof:

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

Definition 5 (Validity and proofs).

Let $b=(s_{i})_{i\in\omega}$ be a sequence of sequents defining an infinite branch in a pre-proof $\pi$ . A thread of $b$ is a sequence $(F_{i}\in s_{i})_{i>n}$ of formula 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 sub-formula ordering, exists and is a $\nu$ -formula and that the formulas of this thread are infinitely often principal. A branch $b$ is valid if there exists a valid thread of $b$ . A pre-proof is valid and is a proof if each of its infinite branches is valid.

Example 6.

Given a formula $A$ , let us consider ${\wn}^{\bullet}A=\mu X.({A}\oplus(\bot\oplus(X\invamp X)))$ and ${\oc}^{\bullet}A=\nu X.({A}\with(1\with(X\otimes X)))$ . Assuming a context $\Gamma$ and a valid proof $\pi$ of $\vdash A,\wn\Gamma$ , the following is a valid proof of $\vdash{\oc}^{\bullet}A,\wn\Gamma$ :

(In every infinite branch along the 2 back-edges, ${\oc}^{\bullet}A$ is the minimal recurring formula.)

2.2 Cut-elimination for linear logic with fixed-point

Cut-elimination holds for $\mu\text{MALL}^{\infty}$ and $\mu\text{LL}^{\infty}$ in the form of the infinitary weak normalization of a multicut-reduction relation: a new rule, the multicut (mcut), is introduced, that corresponds to an abstraction of several cuts. This rule has an arbitrary number of premises:

and it is parameterized by two relations: (i) the ancestor relation $\iota$ which relates each formula of the conclusion to exactly one formula among the hypotheses and (ii) the multicut relation, $\perp\!\!\!\perp$ , which links cut-formulas together.

Example 7.

Representing $\iota$ and $\perp\!\!\!\perp$ in red and blue, the (cut/mcut) step is as follows:

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

Definition 8 (Restriction of a multicut context).

Let be a multicut occurrence with $\mathcal{C}=s_{1}\dots s_{n}$ and $s_{i}$ being $\vdash F_{1}\dots F_{k_{i}}$ . For $1\leq j\leq k_{i}$ , $\mathcal{C}_{F_{j}}$ is the restriction of $\mathcal{C}$ to the sequents hereditarily linked to $F_{j}$ with the $\perp\!\!\!\perp$ -relation.

The previous definition extends to contexts, writing $\mathcal{C}_{F_{1}\dots F_{n}}$ . For instance, writing $\mathcal{C}$ for the premises of the rightmost mcut in Example 7, $\mathcal{C}_{B^{\perp}}=\{\vdash A,B;\vdash C^{\perp},D\}$ while $\mathcal{C}_{A}=\emptyset$ .

Cut-elimination for $\mu\text{MALL}^{\infty}$ and $\mu\text{LL}^{\infty}$ is proved syntactically with a rewriting system on proofs with (mcut). As standard in sequent calculi, those (m)cut-reduction steps are divided in principal cases and (m)cut-commutation cases.

The cut elimination result is then stated as a strong normalization result for a class of infinitary reductions, initiated with proofs containing exactly one (mcut) at the root of the proof. Indeed, strong normalization is trivially lost in such infinitary settings as one can always build infinite sequences that never activate some (mcut), thus converging to a non-cut-free proof. Fair reductions precisely prevent this situation by asking that no (mcut) that can be activated remains forever inactive along the reduction sequence. The following definition is borrowed from [1, 2], residuals corresponding to the usual notion of TRS [23]:

Definition 9.

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^{\prime}$ , there exists a $j>i$ such that $\pi_{j}$ does not contain any residual of $\mathcal{R}$ .

This fairness condition allowed Baelde et al. [1, 2] to obtain a (multi)cut-elimination result for $\mu\text{MALL}^{\infty}$ which, combined with the following encoding of exponential formulas using notations from Example 6, ${(\wn A)}^{\bullet}={\wn}^{\bullet}{A}^{\bullet}$ and ${(\oc A)}^{\bullet}={\oc}^{\bullet}{A}^{\bullet}$ (extended to proof and cut-reduction steps), induces the following $\mu\text{LL}^{\infty}$ multicut-elimination result [22]:

Theorem 10.

Every fair $\mu\text{LL}^{\infty}$ (mcut)-reduction sequence converges to a cut-free proof.

3 Super exponentials

In this section, we define a family of parameterized logical systems, adapting the methodology of [6] and using the sequent formalism from the previous section. Consequently, the section lies in between background on earlier work by the first author with Laurent and new material, since we propose an alternative system, with an alternative choice of formalization. We discuss briefly some of these differences here and shall come back to this comparison in the discussion of related works. The super exponentials of the first author with Laurent [6] only include functorial promotion and rely on the so-called digging rule to recover the usual Girard’s promotion rule. On the other hand, we propose below another formalization of super exponentials, adapting the system to capture both functorial and Girard’s promotions primitively while we discard the digging which is not needed nor well-suited for the extension with fixed-points. The reader will find more details in the discussion of future work.

This means that the general philosophy of this section follows that of [6]. However, the uniform cut-elimination theorem that we prove for the super exponential systems below provides a new and quite different proof from the original argument of the first author and Laurent. The first parameters of these systems will allow us to define formulas:

Definition 11 (Superexponential formulas).

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

F,G\hskip 5.0pt::=\hskip 5.0pta\in\mathcal{A}\nobreakspace\mid a^{\perp}\mid F% \invamp G\mid F\otimes G\mid\bot\mid 1\mid F\oplus G\mid F\with G\mid 0\mid% \top\mid\wn_{\sigma}F\mid\oc_{\sigma}F.

Elements of $\mathcal{E}$ are called exponential signatures. The orthogonal $(-)^{\perp}$ is defined as the involution extending that of Definition 1 with: $(\oc_{\sigma}A)^{\perp}=\wn_{\sigma}A^{\perp}$ for any $\sigma\in\mathcal{E}$ .

Notation 12 (List of exponential signatures).

Let $\Delta=A_{1}\dots A_{n}$ be a list of $n$ formulas and $\vec{\sigma}=\sigma_{1}\dots\sigma_{n}$ a list of $n$ exponential signatures. The list of formulas $\wn_{\sigma_{1}}A_{1}\dots\wn_{\sigma_{n}}A_{n}$ is written $\wn_{\vec{\sigma}}\Delta$ . Moreover, given a binary relation $R$ on exponential signatures and two lists of exponential signatures $\vec{\sigma}=\sigma_{1},\dots,\sigma_{m}$ and $\vec{\sigma^{\prime}}=\sigma^{\prime}_{1},\dots,\sigma^{\prime}_{n}$ , we write $\vec{\sigma}\mathop{R}\vec{\sigma^{\prime}}$ for $\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq m\\ 1\leq j\leq n\end{subarray}}\sigma_{i}\mathop{R}\sigma^{\prime}_{j}$ .

While each element $\sigma\in\mathcal{E}$ induces two exponential modalities, $\wn_{\sigma},\oc_{\sigma}$ , the inference rules will be described in two phases: first, each $\sigma\in\mathcal{E}$ will be equipped with a set of rule names $\{\wn_{\text{m}_{i}}\mid i\in\mathbb{N}\}\cup\{\wn_{\text{c}_{i}}\mid i\geq 2\}$ which can be used to introduce the connective $\wn_{\sigma}$ . Second, some binary relations over $\mathcal{E}$ will govern the available promotion rules, introducing $\oc_{\sigma}$ .

Definition 13.

The set of exponential rule names is ${\mathcal{N}}=\{\wn_{\text{m}_{i}}\mid i\in\mathbb{N}\}\cup\{\wn_{\text{c}_{i}% }\mid i\geq 2\}$ .

To each exponential signature $\sigma\in\mathcal{E}$ , one associates a subset of $\mathcal{N}$ , $[\sigma]$ .

For the sake of clarity, given $\sigma\in\mathcal{E}$ we will write (when unambiguous) $\sigma$ instead of $[\sigma]$ , omitting $[\cdot]$ throughout the paper. We shall also switch freely from viewing $\sigma$ (more precisely, $[\sigma]$ ) as a subset of $\mathcal{N}$ or as its boolean characteristic function, write, for instance, $\wn_{\text{m}_{i}}\in\sigma$ (resp. $\wn_{\text{c}_{i}}\in\sigma$ ) when convenient, or considering $\sigma(\wn_{\text{m}_{i}})$ (resp. $\sigma(\wn_{\text{c}_{i}})$ ) as a truth value.

Definition 14.

For one set of signatures $\mathcal{E}$ , we define many systems, parameterized by three binary relations on $\mathcal{E}$ : $\leq_{\text{g}},\leq_{\text{f}}$ and $\leq_{\text{u}}$ . Rules for this system are the rules of MALL from Figure 1 in combination with the super exponential rules of Figure 4: multiplexing ( $\wn_{\text{m}_{i}}$ ), contraction ( $\wn_{\text{c}_{i}}$ ) as well as functorial ( ${\oc_{\text{f}}}$ ), Girard ( ${\oc_{\text{g}}}$ ) and unary ( ${\oc_{\text{u}}}$ ) promotions.

Each exponential rule comes with a side-condition written to the right of the premises.

Figure 4: Exponential fragment of

\mu\text{superLL}^{\infty}

.

Remark 15.

Below, the side-condition for an exponential rule may also be written next to the rule label or simply omitted when it has been checked elsewhere. Those side-conditions are not part of the proof-object itself: all exponential inferences are unary rules.

Note that the nullary multiplexing rule corresponds to usual weakening $(\wn_{\text{w}})$ and unary multiplexing corresponds to dereliction $(\wn_{\text{d}})$ .

Definition 16 ( $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ ).

The proofs of $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ are the trees inductively generated by those inferences, satisfying the above side-conditions.

There are instances of superLL where cut-elimination fails: some conditions are required, so that cut inferences can indeed be eliminated. The following two definitions aim at formulating these conditions in a suitable way:

Definition 17 (Derivability closure).

Given a signature $\sigma$ , we define the derivability closure $\bar{\sigma}$ to be the signature inductively defined by:

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

Proposition 18.

If $\bar{\sigma}(r)$ holds, then $(r)$ is derivable for connective $\wn_{\sigma}$ , using only inference rules $\wn_{\text{m}_{i}}$ and $\wn_{\text{c}_{i}}$ on this connective.

Notation 19.

We name $\wn_{\text{c}_{i}}^{\bar{\sigma}}$ (resp. $\wn_{\text{m}_{i}}^{\bar{\sigma}}$ ), for $i\in\mathbb{N}$ , any derivation using only $\wn_{\text{c}_{j}}$ and $\wn_{\text{m}_{j}}$ rules and having the same conclusion and hypothesis as $\wn_{\text{c}_{i}}$ (resp. $\wn_{\text{m}_{i}}$ ). We write $\bar{\sigma}(\wn_{\text{c}_{0}})$ for $\bar{\sigma}(\wn_{\text{m}_{0}})$ and set $\bar{\sigma}(\wn_{\text{c}_{1}})$ to true for all $\sigma$ and $\wn_{\text{c}_{1}}^{\bar{\sigma}}$ to be the empty derivation.

To define a cut-reduction system, we define a set of axioms on the exponential signatures of a superLL-system:

Definition 20 (Cut-elimination axioms).

The cut-elimination axioms for a superLL-system are the axioms defined in Table 1.

To clarify these axioms, let us recall the system of subexponentials [20], in which exponential signatures must satisfy certain conditions to guarantee cut-elimination. The axiom $(\mathsf{Ax_{trans})}$ expresses the transitivity of the relations $\leq_{s}$ , which is part of the conditions needed for a preorder, as in the system of Nigam and Miller. This transitivity is particularly useful in commutative cases involving interactions between promotion rules. The axioms $(\mathsf{Ax^{g}_{m})}$ , $(\mathsf{Ax^{fu}_{m})}$ , and $(\mathsf{Ax_{c})}$ capture the upward closure of the preorder relations with respect to the applicability predicates of the various $\wn$ -rules. These are used for handling principal cases involving $\wn$ -rules. Finally, the remaining axioms are specific to our system and are used for handling commutation cases where promotion interacts with other promotion rules.

In superLL-systems, each axiom corresponds to one cut-elimination step, modulo our notation $\leq_{s}$ with $s\in\{g,f,u\}$ which factors together similar cases that differ only in the type of promotion rule ( ${\oc_{\text{g}}}$ , ${\oc_{\text{f}}}$ or ${\oc_{\text{u}}}$ ). However, as our reduction system with fixed-points uses the (mcut)-rule which corresponds to the concatenation of many cuts, each reduction step may require several axioms.

Table 1: Cut-elimination axioms.

$\begin{array}[]{|clcll|c|}\hline\cr\sigma\leq_{\text{g}}\sigma^{\prime}&% \Rightarrow&\sigma(\wn_{\text{m}_{i}})&\Rightarrow&\bar{\sigma^{\prime}}(\wn_{% \text{c}_{i}})\hfill i\geq 0&(\mathsf{Ax^{g}_{m})}\\ \sigma\leq_{s}\sigma^{\prime}&\Rightarrow&\sigma(\wn_{\text{m}_{i}})&% \Rightarrow&\bar{\sigma^{\prime}}(\wn_{\text{m}_{i}})\hfill i\geq 0\text{ and % }s\neq g&(\mathsf{Ax^{fu}_{m})}\\ \sigma\leq_{s}\sigma^{\prime}&\Rightarrow&\sigma(\wn_{\text{c}_{i}})&% \Rightarrow&\bar{\sigma^{\prime}}(\wn_{\text{c}_{i}})\hfill i\geq 2&(\mathsf{% Ax_{c})}\\ \sigma\leq_{s}\sigma^{\prime}&\Rightarrow&\sigma^{\prime}\leq_{s}\sigma^{% \prime\prime}&\Rightarrow&\sigma\leq_{s}\sigma^{\prime\prime}&(\mathsf{Ax_{% trans})}\\ \sigma\leq_{\text{g}}\sigma^{\prime}&\Rightarrow&\sigma^{\prime}\leq_{s}\sigma% ^{\prime\prime}&\Rightarrow&\sigma\leq_{\text{g}}\sigma^{\prime\prime}&(% \mathsf{Ax_{\leq}^{gs})}\\ \sigma\leq_{\text{f}}\sigma^{\prime}&\Rightarrow&\sigma^{\prime}\leq_{\text{u}% }\sigma^{\prime\prime}&\Rightarrow&\sigma\leq_{\text{f}}\sigma^{\prime\prime}&% (\mathsf{Ax_{\leq}^{fu})}\\ \sigma\leq_{\text{f}}\sigma^{\prime}&\Rightarrow&\sigma^{\prime}\leq_{\text{g}% }\sigma^{\prime\prime}&\Rightarrow&\sigma\leq_{\text{g}}\sigma^{\prime\prime}% \land(\sigma\leq_{\text{f}}\sigma^{\prime\prime\prime}\Rightarrow(\sigma\leq_{% \text{g}}\sigma^{\prime\prime\prime}\land\sigma^{\prime\prime\prime}(\wn_{% \text{m}_{1}})))&(\mathsf{Ax_{\leq}^{fg})}\\ \sigma\leq_{\text{u}}\sigma^{\prime}&\Rightarrow&\sigma^{\prime}\leq_{s}\sigma% ^{\prime\prime}&\Rightarrow&\sigma\leq_{s}\sigma^{\prime\prime}&(\mathsf{Ax_{% \leq}^{us})}\\ \hline\cr\end{array}$
with $s\in\{g,f,u\}$ , all the axioms are universally quantified.
For convenience, we use the notation $\wn_{\text{c}_{0}}:=\wn_{\text{m}_{0}}$ and set $\bar{\sigma}(\wn_{\text{c}_{1}})=\text{true}$ for all $\sigma$ .

In the first author and Laurent’s system [6], properties of axiom expansion and cut-elimination hold. We defer the former to Section A.1 and state the latter:

Theorem 21 (Cut Elimination).

As soon as the 8 cut-elimination axioms of Table 1 are satisfied, cut elimination holds for $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ .

This theorem will be proved, in Section 5, as a corollary of $\mu\text{superLL}^{\infty}$ cut-elimination theorem. Many existing variants of LL are instances of superLL, e.g. let us consider ELL [16, 13]:

Example 22.

Elementary Linear Logic (ELL) is a variant of LL where ( $\wn_{\text{d}}$ ) and $(\oc_{\text{p}})$ are replaced by functorial promotion:

.

This system is captured as the instance of $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ system with $\mathcal{E}=\{\bullet\}$ , defined by $\bullet(\wn_{\text{c}_{2}})=\bullet(\wn_{\text{m}_{0}})=\text{true}$ (and $(\bullet)(r)=\text{false}$ otherwise), ${\leq_{\text{g}}}={\leq_{\text{u}}}=\emptyset$ and $\bullet\leq_{\text{f}}\bullet$ .

This $\textnormal{{$\text{superLL}$}}(\mathcal{E},{\leq_{\text{g}}},{\leq_{\text{f}}% },{\leq_{\text{u}}})$ instance is ELL and satisfies the axioms of cut-elimination.

As argued in [6], the superLL-systems subsume many other existing variants of LL such as SLL [18], LLL [16], seLL [20]. The last two are particularly interesting as they require more than one exponential signature to be formalized. In the following section, we will look at some examples for the fixed-point version of $\mu\text{superLL}^{\infty}$ .

4 Super exponentials with fixed-points

In this section, we define $\mu\text{superLL}^{\infty}$ and give some interesting instances of it.

4.1 Definition of $\mu$ superLL^∞

Let $\mathcal{E}$ be a set. The pre-formulas of $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E})$ are $\textnormal{{$\text{superLL}$}}{}(\mathcal{E})$ formulas extended with fixed-point variables and fixed-point constructs (with $a\in\mathcal{A}$ , $X\in\mathcal{V}$ , $\sigma\in\mathcal{E}$ ):

F,G\hskip 1.00006pt::=\hskip 1.00006pta\mid a^{\perp}\mid X\mid F\invamp G\mid F% \otimes G\mid\bot\mid 1\mid F\oplus G\mid F\with G\mid 0\mid\top\mid\wn_{% \sigma}F\mid\oc_{\sigma}F\mid\mu X.F\mid\nu X.F.

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

Again, for one set of signatures $\mathcal{E}$ we define many systems, each parametrized with $\leq_{\text{g}},\leq_{\text{f}}$ and $\leq_{\text{u}}$ . The inference rules for this system are the rules of $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ together with the fixed-point fragment of Figure 3. As before, pre-proofs of $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ are the trees coinductively generated by the rules of $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ and validity is defined in the same way as for $\mu\text{LL}^{\infty}$ .

4.2 Some instances of $\mu$ superLL^∞

4.2.1 A linear modal $\mu$ -calculus

An application of super exponentials can be found in modelling the linear modal $\mu$ -calculus introduced in [5] to prove a cut-elimination theorem for the modal $\mu$ -calculus. We show below how one can view the multi-modal $\mu$ -calculus $\mu\text{LL}_{\Box}^{\infty}$ as an instance of $\mu\text{superLL}^{\infty}$ (details in Section B.1).

Let us consider a set of actions $\mathsf{Act}$ . Formulas of $\mu\text{LL}_{\Box}^{\infty}$ are those of $\mu\text{LL}^{\infty}$ with the addition of a pair of modalities, $\lozenge_{\alpha}F$ and $\Box_{\alpha}F$ , for each $\alpha\in\mathsf{Act}$ . Rules of $\mu\text{LL}_{\Box}^{\infty}$ are the rules of $\mu\text{LL}^{\infty}$ where the promotion is extended with $\lozenge$ -contexts. Rules on modalities are a functorial promotion (called the modal rule) and a contraction and a weakening on $\lozenge$ -formulas:

(with $\alpha,\alpha_{1},\dots,\alpha_{n}\in\mathsf{Act}$ ) The system considered in [5] corresponds to the case where $\mathsf{Act}$ is a singleton, that is, a calculus with two exponential names, one of these names representing the $\mu$ -calculus modality rather than a linear exponential.

$\mu\text{LL}_{\Box}^{\infty}$ can be modelled as the super exponential system $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ with:

$\blacksquare$

$\mathcal{E}:=\{\bullet\}\cup\mathsf{Act}$ .
$\blacksquare$

$\bullet(\wn_{\text{c}_{2}})=\bullet(\wn_{\text{m}_{0}})=\bullet(\wn_{\text{m}_% {1}})=\text{true}$ , for any $\alpha\in\mathsf{Act},\alpha(\wn_{\text{c}_{2}})=\alpha(\wn_{\text{m}_{0}})=% \text{true}$ , and all the other elements have value false for both signatures.
$\blacksquare$

$\bullet\leq_{\text{g}}\bullet$ ; $\bullet\leq_{\text{g}}\alpha$ ; $\alpha\leq_{\text{f}}\alpha$ for any $\alpha\in\mathsf{Act}$ and all other couples for the three relations $\leq_{\text{g}},\leq_{\text{f}}$ and $\leq_{\text{u}}$ are false.

This system is $\mu\text{LL}_{\Box}^{\infty}$ when taking: $\wn_{\bullet}:=\wn,\quad\oc_{\bullet}:=\oc,\quad\wn_{\alpha}:=\lozenge_{\alpha% }\quad\text{and}\quad\oc_{\alpha}:=\Box_{\alpha}$ . Moreover, the system satisfies cut-elimination axioms of Table 1.

4.2.2 ELL with fixed points

In [3], an affine version of second-order ELL with recursive types, called $\text{EAL}_{\mu}$ , is introduced. This system allows only finite proofs. Affine means weakening applies to any formula. Fixed points are added to a two-sided system with $\multimap$ and $(-)^{\perp}$ , which are non-increasing predicates, unlike in our system. The paper proves $\text{EAL}_{\mu}$ cut-elimination and refines complexity bounds from ELL.

Considering $\mu\text{ELL}^{\infty}$ , an instance of Example 22 with fixed points, gives us a typing system which is close to $\text{EAL}_{\mu}$ . Namely, consider $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ with the same $\mathcal{E},\leq_{\text{g}},\leq_{\text{f}}$ , and $\leq_{\text{u}}$ as in Example 22. Since the axioms in Table 1 only concern $\mathcal{E},\leq_{\text{g}},\leq_{\text{f}}$ , and $\leq_{\text{u}}$ , they are also satisfied by this instance of $\mu\text{superLL}^{\infty}$ .

Our systems differ in two ways from that of Baillot: (i) the extremal fixed-points instead of generic fixed-points and the fact that our system contains only increasing predicates, and (ii) the infinite nature of our proofs. Thus, our cut-elimination theorem may not apply due to (i), and even if it did, it might not ensure finite proofs because of (ii). However, Baillot [3] uses only fixed-point variables in positive positions of its predicates when proving complexity bounds, which addresses (i). Additionally, using only $\mu$ -fixed-points to encode fixed points ensures that cut-free proofs remain finite, resolving the incompatibility induced by (ii) by preventing infinite branches. (Moreover, the impact of weakening can be tamed by designing a translation that also makes the system affine.)

Remark 23.

Note that there is no proof of the conclusion sequent of Example 4 in $\mu\text{ELL}^{\infty}$ .

4.2.3 $\mu$ superLL ${}^{\infty}_{\top}$

In the following, we want to consider the cut-reduction rules for a family of $\mu\text{superLL}^{\infty}$ systems under some conditions. We shall define the reduction rules for each system ensuring that they indeed define a relation over the proofs of a given system. In order to do so, it will be very convenient to consider the following subsidiary but technically significant case of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ , with a set of signature parameters $\mathcal{E}$ . This can be viewed as the maximal (or most permissive) $\mu\text{superLL}^{\infty}$ over signature $\mathcal{E}$ :

$\blacksquare$

We set $\sigma(r)=\text{true}$ for each $\sigma\in\mathcal{E}$ and rule name $(r)$ .
$\blacksquare$

We set $\sigma\leq_{\text{s}}\sigma^{\prime}$ for each $\text{s}\in{g,f,u}$ and all $\sigma,\sigma^{\prime}\in\mathcal{E}$ .

The defined system $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ is $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ .

This system is useful for the following reason: due to the very permissive use of exponentials in such a system, essentially any reduction rule will happen to be a reduction relation over $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ , allowing us to define the reduction rules for this system easily. We shall then check that the other systems of the family, satisfying the axioms, are closed by those relations. In order to achieve this result, the following lemma is useful. It is immediate as each $\wn$ -rule (resp. promotion) applicable to a sequent $S$ of $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}}^{% \prime},\leq_{\text{f}}^{\prime},\leq_{\text{u}}^{\prime})$ is also applicable in $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ , since $\sigma(r)=\text{true}$ for all rules $(r)$ and signatures $\sigma\in\mathcal{E}$ (resp. $\sigma\leq_{\text{s}}\sigma^{\prime}$ for each $\text{s}\in\{g,f,u\}$ and $\sigma,\sigma^{\prime}\in\mathcal{E}$ ).

Lemma 24.

Let $\pi$ be a $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}}^{% \prime},\leq_{\text{f}}^{\prime},\leq_{\text{u}}^{\prime})$ -proof. Then $\pi$ is a proof of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ .

5 Cut-elimination

Let us fix an instance, $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ , that we simply refer to as $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ in the following, keeping the relations $\leq_{\text{g}},\leq_{\text{f}}$ and $\leq_{\text{u}}$ implicit.

5.1 (mcut)-elimination steps

We define the (mcut)-elimination steps of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ by first presenting the steps $\pi\rightsquigarrow\pi^{\prime}$ in $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ . We show that if $\pi$ is a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proof, then so is $\pi^{\prime}$ . To define these steps, we introduce a specific notation for premises concluding with promotions, following the conventions of the $\mu\text{LL}^{\infty}$ cut-elimination proof [22]:

Notation 25 ( $(\oc)$ -contexts).

$\mathcal{C}^{\oc}$ denotes a list of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proofs which are all concluded by some promotion rule ( ${\oc_{\text{g}}},{\oc_{\text{f}}}$ or ${\oc_{\text{u}}}$ ). Given $s\in\{g,f,u\}$ , $\mathcal{C}^{\oc_{s}}$ denotes a list of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proofs which are all concluded by an $(\oc_{s})$ -rule. In both cases, $\mathcal{C}$ denotes the list of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proofs formed by gathering the immediate subproofs of the last promotion (being either $\mathcal{C}^{\oc}$ , or $\mathcal{C}^{\oc_{s}}$ ).

The principal case for the multiplexing rule needs the definition of ${{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S^{\oc}}(\mathcal{C}^{\oc})$ contexts. The intuition is that when a multiplexing rule reduces (i) with a Girard’s promotion, it simply cancels with it, while when it interacts (ii) with a $({\oc_{\text{f}}})$ or $({\oc_{\text{u}}})$ , not only do those two rules cancel, but also the other promotions hereditarily $\perp\!\!\!\perp$ -connected to the first $({\oc_{\text{f}}})$ or $({\oc_{\text{u}}})$ rule, until some Girard’s promotion is reached, in which case this propagation stops. A graphical representation of this definition is given in Section C.1.

Definition 26 ( ${{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S^{\oc}}(\mathcal{C}^{\oc})$ contexts).

Let $\pi$ be some $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proof concluded in a $\text{mcut}(\iota,\perp\!\!\!\perp)$ inference, $\mathcal{C}^{\oc}$ a context of the multicut which is a tree with respect to a cut-relation $\perp\!\!\!\perp$ and $S^{\oc}$ be a sequent of $\mathcal{C}^{\oc}$ that we shall consider as the root of the tree.

We define a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -context ${{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S^{\oc}}(\mathcal{C}^{\oc})$ altogether with two sets of sequents, $\mathcal{S}^{\wn_{\text{m}}}_{\mathcal{C}^{\oc},S^{\oc}}$ and $\mathcal{S}^{\wn_{\text{c}}}_{\mathcal{C}^{\oc},S^{\oc}}$ , by induction on the tree ordering on $\mathcal{C}^{\oc}$ :

Let $\mathcal{C}^{\oc}_{1},\dots,\mathcal{C}^{\oc}_{n}$ be the sons of $S^{\oc}$ , such that $\mathcal{C}^{\oc}=(S^{\oc},(\mathcal{C}^{\oc}_{1},\dots,\mathcal{C}^{\oc}_{n}))$ , we have two cases:

$\blacksquare$

$S^{\oc}=S^{\oc_{\text{g}}}$ , then we define ${{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S^{\oc}}(\mathcal{C}^{\oc}):=(S,(% \mathcal{C}^{\oc}_{1},\dots,\mathcal{C}^{\oc}_{n}))$ ; $\mathcal{S}^{\wn_{\text{m}}}_{\mathcal{C}^{\oc},S^{\oc}}:=\emptyset$ ; $\mathcal{S}^{\wn_{\text{c}}}_{\mathcal{C}^{\oc},S^{\oc}}:=\mathcal{C}^{\oc}$ .
$\blacksquare$

$S^{\oc}=S^{\oc_{\text{f}}}$ or $S^{\oc}=S^{\oc_{\text{u}}}$ , then let the root of $\mathcal{C}^{\oc}_{i}$ be $S_{i}^{\oc}$ , we define ${{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S^{\oc}}(\mathcal{C}^{\oc})$ as
$(S,{{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S_{1}^{\oc}}(\mathcal{C}^{\oc}_{1% }),\dots,{{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S_{n}^{\oc}}(\mathcal{C}^{% \oc}_{n}))$ ; $\mathcal{S}^{\wn_{\text{m}}}_{\mathcal{C}^{\oc},S^{\oc}}:=\{S^{\oc}\}\cup% \bigcup\mathcal{S}^{\wn_{\text{m}}}_{\mathcal{C}^{\oc}_{i},S_{i}^{\oc}}$ ; $\mathcal{S}^{\wn_{\text{c}}}_{\mathcal{C}^{\oc},S^{\oc}}:=\bigcup\mathcal{S}^{% \wn_{\text{c}}}_{\mathcal{C}^{\oc}_{i},S_{i}^{\oc}}$ .

Definition 27 ( $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ cut-relation).

The exponential steps of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ are defined in Figures 5, 6, and 7. The non-exponential steps of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ are the steps of $\mu\text{MALL}^{\infty}$ .

Conditions:

$\blacksquare$

$({\text{comm}}^{1}_{\oc_{\text{f}}})$ : each sequent concluded by $({\oc_{\text{g}}})$ in $\mathcal{C}^{\oc}$ has empty context;
$\blacksquare$

$({\text{comm}}^{2}_{\oc_{\text{f}}})$ : some $({\oc_{\text{g}}})$ -rule in $\mathcal{C}^{\oc}$ has a non-empty context;
$\blacksquare$

$({\text{comm}}^{2}_{\oc_{\text{u}}})$ : $\mathcal{C}^{\oc}$ contains at least one $({\oc_{\text{f}}})$ and each of its $({\oc_{\text{g}}})$ -rules has empty context;
$\blacksquare$

$({\text{comm}}^{3}_{\oc_{\text{u}}})$ : $\mathcal{C}^{\oc}_{2}$ contains a $({\oc_{\text{g}}})$ with non-empty context and $\mathcal{C}:=\{\vdash\oc_{\sigma}A,\wn_{\tau}B\}\cup\mathcal{C}^{{\oc_{\text{u% }}}}_{1}\cup\{\vdash\oc_{\sigma^{\prime}}C,\wn_{\vec{\tau^{\prime}}}\Delta\}$ is cut-connected and $\mathcal{C}^{\prime}:=\{\vdash\oc_{\sigma^{\prime}}C,\wn_{\vec{\tau^{\prime}}}% \Delta\}\cup\mathcal{C}^{\oc}_{2}$ as well;
$\blacksquare$

$({\text{comm}}^{4}_{\oc_{\text{u}}})$ : $\mathcal{C}:=\{\vdash\oc_{\sigma}A,\wn_{\tau}B\}\cup\mathcal{C}^{{\oc_{\text{u% }}}}_{1}\cup\{\vdash\oc_{\sigma^{\prime}}C,\wn_{\vec{\tau^{\prime}}}\Delta\}$ is cut-connected and $\mathcal{C}^{\prime}:=\{\vdash\oc_{\sigma^{\prime}}C,\wn_{\vec{\tau^{\prime}}}% \Delta\}\cup\mathcal{C}^{\oc}_{2}$ as well.

Figure 5: Commutative cut-reduction steps of the

\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})

promotion rules.

Figure 6: Commutative cut-reduction steps for

\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})

contraction and multiplexing rules.

with

\Gamma

sent on

\mathcal{C}_{\Delta}\cup{\Delta}

by

\iota

;

\wn_{\vec{\rho^{\prime\prime}}}\Gamma^{\prime\prime}

sent on sequents of

\mathcal{S}^{\wn_{\text{m}}}_{\mathcal{C}^{\oc},S^{\oc}}

; and

\wn_{\vec{\rho^{\prime}}}\Gamma^{\prime}

sent on

\mathcal{S}^{\wn_{\text{c}}}_{\mathcal{C}^{\oc},S^{\oc}}

, where

S^{\oc}:=\vdash\oc_{\sigma}A,\wn_{\vec{\tau^{\prime}}}\Delta^{\prime}

is the sequent cut-connected to

\vdash\wn_{\sigma}A,\Delta

on the formula

\wn_{\sigma}A

.

Figure 7: Principal cut-reduction steps of the exponential fragment of

\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})

.

We now prove that $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ is closed under the cut-reduction relation as soon as the cut-elimination axioms are satisfied, i.e., that a cut-reduction step from a proof in $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ produces a proof that is also in $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ . We thus obtain cut-reduction relation for each $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ well-behaved system.

Lemma 28 (Soundness of the mcut-steps).

Suppose $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ satisfies the 8 cut-elimination axioms and let $\pi\rightsquigarrow\pi^{\prime}$ be a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ step. If $\pi$ is a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proof, then so is $\pi^{\prime}$ .

Proof sketch.

Non-exponential cases are trivial as $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ and $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ share the same non-exponential rules. For the exponential cases, we proceed by case analysis on the steps. We make explicit which axioms are needed for each case and provide some details for the proof for case $({\text{comm}}^{2}_{\oc_{\text{f}}})$ .

$\blacksquare$

Case $({\text{comm}}_{\oc_{\text{g}}})$ uses $(\mathsf{Ax_{trans})}$ and $(\mathsf{Ax_{\leq}^{gs})}$ .
$\blacksquare$

Case $({\text{comm}}^{1}_{\oc_{\text{f}}})$ uses $(\mathsf{Ax_{trans})}$ and $(\mathsf{Ax_{\leq}^{fu})}$ .
$\blacksquare$
Case $({\text{comm}}^{2}_{\oc_{\text{f}}})$ . First notice that, by hypothesis, $\sigma\leq_{\text{f}}\vec{\tau}$ . The proof is done in two steps:
1. 1.
  
  From $\vdash\oc_{\sigma}A,\wn_{\vec{\tau}}\Delta$ we follow mcut-connected sequents until reaching one $\vdash\oc_{\sigma^{\prime}}A^{\prime},\wn_{\vec{\tau^{\prime}}}\Delta^{\prime}$ conclusion of an $({\oc_{\text{g}}})$ -rule with $\wn_{\vec{\tau^{\prime}}}\Delta^{\prime}$ non-empty, for each signature $\sigma^{\prime}$ in these sequents, we prove that $\sigma\leq_{\text{f}}\sigma^{\prime}$ using axiom $(\mathsf{Ax_{trans})}$ or $(\mathsf{Ax_{\leq}^{fu})}$ . Then we use axiom $(\mathsf{Ax_{\leq}^{fg})}$ to prove that $\vec{\tau}(\wn_{\text{m}_{1}})$ holds and $\sigma\leq_{\text{g}}\vec{\tau}$ . Since $\vec{\tau}(\wn_{\text{m}_{1}})$ holds, application of $(\wn_{\text{m}_{1}})$ is allowed.
2. 2.
  
  We run through all the sequents and using axiom $(\mathsf{Ax_{\leq}^{gs})}$ , we prove that $\sigma\leq_{\text{g}}\sigma^{\prime\prime}$ for each signature $\sigma^{\prime\prime}$ we encounter.
We therefore have $\sigma\leq_{\text{g}}\vec{\rho}$ as signatures from $\vec{\rho}$ are contained in hypotheses of the mcut: the application of $({\oc_{\text{g}}})$ is therefore legal.
$\blacksquare$

Case $({\text{comm}}^{1}_{\oc_{\text{u}}})$ uses $(\mathsf{Ax_{trans})}$ .
$\blacksquare$

Case $({\text{comm}}^{2}_{\oc_{\text{u}}})$ uses $(\mathsf{Ax_{trans})}$ , $(\mathsf{Ax_{\leq}^{us})}$ and $(\mathsf{Ax_{\leq}^{fu})}$ .
$\blacksquare$

Case $({\text{comm}}^{3}_{\oc_{\text{u}}})$ uses $(\mathsf{Ax_{trans})}$ , $(\mathsf{Ax_{\leq}^{fu})}$ , $(\mathsf{Ax_{\leq}^{fg})}$ , $(\mathsf{Ax_{\leq}^{us})}$ and $(\mathsf{Ax_{\leq}^{gs})}$ .
$\blacksquare$

Case $({\text{comm}}^{4}_{\oc_{\text{u}}})$ uses $(\mathsf{Ax_{trans})}$ , $(\mathsf{Ax_{\leq}^{us})}$ and $(\mathsf{Ax_{\leq}^{gs})}$ .
$\blacksquare$

Cases $(\text{comm}_{\wn_{\text{m}}})$ and $(\text{comm}_{\wn_{\text{c}}})$ are immediate, as the exponential rules involved in these cases apply to the same exponential connective in both the left and right proofs.
$\blacksquare$

Case $(\text{principal}_{\wn_{\text{c}}})$ uses $(\mathsf{Ax_{trans})}$ , $(\mathsf{Ax_{\leq}^{gs})}$ , $(\mathsf{Ax_{\leq}^{fu})}$ , $(\mathsf{Ax_{\leq}^{fg})}$ , $(\mathsf{Ax_{\leq}^{us})}$ and $(\mathsf{Ax_{c})}$ .
$\blacksquare$

Case $(\text{principal}_{\wn_{\text{m}}})$ uses $(\mathsf{Ax_{\leq}^{us})}$ , $(\mathsf{Ax_{trans})}$ , $(\mathsf{Ax_{\leq}^{fu})}$ , $(\mathsf{Ax_{\leq}^{fg})}$ , $(\mathsf{Ax_{\leq}^{gs})}$ , $(\mathsf{Ax^{fu}_{m})}$ and $(\mathsf{Ax^{g}_{m})}$ .

$\hfill\blacktriangleleft$

We now define the (mcut)-steps of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ :

Definition 29 ( $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ cut-reduction steps).

We define the cut-reduction steps of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ as the context-closure of the relation defined by the pairs $\pi\rightsquigarrow\pi^{\prime}$ of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ such that $\pi$ is in $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ .

5.2 Translating $\mu$ superLL^∞ into $\mu$ LL^∞

We now give a translation of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ into $\mu\text{LL}^{\infty}$ using directly the results of [22] to deduce $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ and then $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ cut-elimination in a modular way:

Definition 30 ( $(-)^{\circ}$ -translation).

We define $(-)^{\circ}$ by induction on formulas ( $c$ is any non-exponential connective): $c(F_{1},\dots,F_{n})^{\circ}:=c(F_{1}^{\circ},\dots,F_{n}^{\circ});\quad X^{% \circ}:=X;\quad\forall\sigma,(\wn_{\sigma}A)^{\circ}:=\wn A^{\circ};\quad a^{% \circ}:=a;\quad(\oc_{\sigma}A)^{\circ}:=\oc A^{\circ}.$ We define translations for exponential rules of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ in Figure 8. Other rules have their translations equal to themselves. Proof translation $\pi^{\circ}$ of $\pi$ is the proof coinductively defined on $\pi$ from rule translations.

Figure 8: Exponential rule translations from

\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})

into

\mu\text{LL}^{\infty}

.

Since fixed-points are not affected by the translation, we have the following lemma:

Lemma 31 ( $(-)^{\circ}$ preserves validity).

$\pi$ is a valid proof if and only if $\pi^{\circ}$ is a valid proof.

The goal of this section is to prove that each fair reduction sequence converges to a cut-free proof. We have to make sure $(\text{mcut})$ -reduction sequences are robust under this translation. In our proof of the final theorem, we also need one-step reduction-rules to be simulated by a finite number of reduction steps in the translation, which is the objective of the following lemma. For the following lemma, we will need rule permutations, whose detailed definition is given in Section C.2.

Lemma 32.

Let $\pi_{0}$ be a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ proof and let $\pi_{0}\rightsquigarrow\pi_{1}$ be a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ step of reduction. There exists a finite number of $\mu\text{LL}^{\infty}$ proofs $\theta_{0},\dots,\theta_{n}$ such that $\theta_{0}\rightarrow\dots\rightarrow\theta_{n},\quad\pi_{0}^{\circ}=\theta_{0}$ and $\theta_{n}=\pi_{1}^{\circ}$ up to a finite number of rule permutations, done only on rules that have just permuted below the $(\text{mcut})$ .

Proof sketch.

Non-exponential cases and commutations of multiplexing or contraction are immediate. Promotion commutations translate to commutation rules and promotion key-cases. We must ensure that there exists a sequence of reductions commuting the translation of each promotion. Key-cases are trickier as they do not send the rules in the correct order: we need rule permutations to recover the translation of the target proof of the step. $\hfill\blacktriangleleft$

Now that we know that a step of (mcut)-reduction in $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ translates to some steps of (mcut)-reduction in $\mu\text{LL}^{\infty}$ , the following lemma allows us to control the fairness:

Lemma 33 (Completeness of the (mcut)-reduction system).

If there is a $\mu\text{LL}^{\infty}$ -redex $\mathcal{R}$ sending $\pi^{\circ}$ to ${\pi^{\prime}}^{\circ}$ then there exists a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ -redex $\mathcal{R}^{\prime}$ sending $\pi$ to a proof $\pi^{\prime\prime}$ , such that in the translation of $\mathcal{R}^{\prime}$ , $\mathcal{R}$ is applied.

We have that validity is preserved if each rule is permuted a finite number of times:

Proposition 34.

If $\pi$ is a $\mu\text{LL}^{\infty}$ pre-proof sent to a pre-proof $\pi^{\prime}$ , via a permutation for which the permutation of one particular rule is finite, then $\pi$ is valid if and only if $\pi^{\prime}$ is.

We provide in Section C.3, an example illustrating how rule permutations behave in the context of the following corollary.

Corollary 35.

For every fair $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ reduction sequence $(\pi_{i})_{i\in\omega}$ , there exists:

$\blacksquare$

a fair $\mu\text{LL}^{\infty}$ reduction sequence $(\theta_{i})_{i\in\omega}$ ;
$\blacksquare$

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

for each $i$ , an integer $k_{i}$ and a finite sequence of rule permutations $(p_{i}^{k})_{k\in\{0,\dots,k_{i}-1\}}$ starting from $\pi_{i}^{\circ}$ and ending on $\theta_{\varphi(i)}$ . For convenience in the proof, let us denote by $(\pi_{i}^{k})_{k\in\{0,\dots,k_{i}\}}$ the sequence of proofs associated to the permutation;
$\blacksquare$

for all $i>i^{\prime}$ , $p_{i}^{k}>p_{i}^{k^{\prime}}$ if $k^{\prime}\in\{0,\dots,k_{i^{\prime}}-1\}$ and $k\geq k_{i^{\prime}}$ ;
$\blacksquare$

for all $i, k$ , $p_{i}^{k}$ is a position lower than the multicuts in $\pi_{i}^{\circ}$ .
$\blacksquare$

for each $i^{\prime}\geq i$ and for each $k\in\{0,\dots,k_{i}-1\},p^{k}_{i^{\prime}}=p^{k}_{i}$

Proof sketch.

We construct the sequence by induction on the steps of reductions of $(\pi_{i})_{i\in\omega}$ , starting with $\theta_{0}=\pi_{0}^{\circ}$ , $\varphi(0)=0$ and $k_{0}=0$ and then applying Lemma 32 for each of the following steps. We get fairness of $(\theta_{i})_{i\in\omega}$ from Lemma 33. $\hfill\blacktriangleleft$

We can now prove cut-elimination of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ :

Theorem 36.

Every fair (mcut)-reduction sequence of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ converges to a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ cut-free proof.

Proof sketch.

Consider $(\pi_{i})_{i\in 1+\lambda}$ , $\lambda\in\omega+1$ , a fair $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ cut-reduction sequence. If the sequence is finite, we use Lemma 32 and we are done. If the sequence is infinite, using Corollary 35 we get a fair infinite $\mu\text{LL}^{\infty}$ reduction sequence $(\theta_{i})_{i\in\omega}$ . By Theorem 10, we know that $(\theta_{i})_{i\in\omega}$ converges to a cut-free proof $\theta$ of $\mu\text{LL}^{\infty}$ . We prove that $(\pi_{i})_{i\in\omega}$ converges to a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ pre-proof using the fact that $(\theta_{i})_{i}$ is the translation of $(\pi_{i})_{i}$ and that it is productive.

Validity of the limit $\pi$ of $(\pi_{i})_{i}$ follows from the translation of $\pi$ being equal to $\theta$ up to rule-permutation (each particular rule permutes finitely). From Lemma 31 and Proposition 34, these two operations preserve validity, therefore $\pi$ is valid which concludes the proof. $\hfill\blacktriangleleft$

Finally, we have our main result, proving cut-elimination of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ :

Theorem 37.

If the axioms of Table 1 are satisfied, then every fair (mcut)-reduction sequence of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ converges to a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ cut-free proof.

Proof.

Let $(\pi_{i})_{i\in 1+\lambda}$ be a fair reduction sequence of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ . By Lemma 24, each $\pi_{i}$ is a valid proof of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ . Moreover, the sequence $(\pi_{i})_{i\in 1+\lambda}$ is fair for the reduction system of $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ : if a $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ -redex, $\theta\rightsquigarrow\theta^{\prime}$ appears in this sequence, then $\theta$ is a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proof and by Lemma 28, $\theta^{\prime}$ is also a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proof. This means that $\theta\rightsquigarrow\theta^{\prime}$ is a redex of $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ , and we conclude by fairness of $(\pi_{i})_{i}$ with respect to the $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -rewriting system. Therefore, we can apply Theorem 36 to obtain that $(\pi_{i})_{i\in 1+\lambda}$ converges to a cut-free $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ -proof $\pi$ . Since all rules in $\pi$ are $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -rules, $\pi$ is a $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ -proof. $\hfill\blacktriangleleft$

An important remark is that the above proof does not rely on Theorem 21 in any way. As a consequence, cut-elimination for superLL is in fact a direct corollary of Theorem 37:

Proof of Theorem 21.

Any $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ -proof is also a $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ -proof, so any sequence of (mcut)-reductions converges to a cut-free proof. A cut-free proof of sequents containing only $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ -formulas and valid rules from $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ is necessarily a $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ (cut-free) proof. $\hfill\blacktriangleleft$

Remark 38.

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

Since $\mu\text{LL}_{\Box}^{\infty}$ and $\mu\text{ELL}^{\infty}$ are instances of $\mu\text{superLL}^{\infty}$ satisfying the cut-elimination axioms, we have the following results as immediate corollaries of Theorem 37:

Corollary 39 (Cut Elimination for $\mu\text{LL}_{\Box}^{\infty}$ ).

Cut elimination holds for $\mu\text{LL}_{\Box}^{\infty}$ .

Corollary 40 (Cut Elimination for $\mu\text{ELL}^{\infty}$ ).

Cut elimination holds for $\mu\text{ELL}^{\infty}$ .

6 Conclusion

We introduced a family of logical systems, $\mu\text{superLL}^{\infty}$ , and proved a syntactic cut-elimination theorem for them. Our systems feature various exponential modalities with least and greatest fixed-points in the setting of circular and non-wellfounded proofs. Our aim in doing so is to develop a methodology to make cut-elimination proofs more uniform and reusable. A key feature of our development is to combine proof-theoretical methods for establishing cut-elimination properties using translation and simulation results with axiomatization of sufficient conditions for cut-elimination.

While parametrized calculi can be complex to work with, we think we managed to present the reduction rules in a simple way by considering a most-permissive sequent calculus, $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ , on which one can express cut-reduction rules then showing all subsequent calculi satisfying the cut-elimination axioms are closed by this set of reduction rules, providing a significant simplification of the presentation compared to a previous version.

While this work was initially motivated by making more systematic a key step in the recent proof of cut-elimination for the modal $\mu$ -calculus [5], it allows us to generalize that result (capturing directly the multi-modal $\mu$ -calculus without needing an ad hoc proof) but also to capture various extensions of light logics with induction and coinduction, notably a calculus close to Baillot’s $\text{EAL}_{\mu}$ system. Our system therefore encompasses various fixed-point extensions of existing linear logic systems, including well-known light logics extended with least and greatest fixed-points and a non-well-founded proof system. We provide a relatively simple and uniform proof of cut-elimination for these extensions. Quite interestingly, the addition of fixed-points provides a new cut-elimination proof for the fixed-point free setting.

Future work

The $\mu\text{superLL}^{\infty}$ system, as defined in this paper, does not include the digging rule. We plan to work on this question in future work, at least for restrictions of the digging rule. Indeed, digging is a very challenging rule with respect to its possible modelling using fixed-points as it would contradict the finiteness of the Fischer-Ladner closure, a basic property of fixed-point systems. On the other hand, incorporating digging would enable us to cover all the super exponential versions from [6] while our current system is incomparable with that of [6]. It could also be relevant for modal calculus, as the digging rule for modal formulas is equivalent to Axiom 4 of modal logic. Other modal logic axioms, such as Axiom T and co-dereliction rules from differential linear logic can be viewed as rules in linear logic.

Another natural future work would be to explore linear translations of affine linear logic and/or intuitionistic/classical translations of these systems, facilitating the study of proof theory closer to [3]. In the same direction, we also plan to investigate specifically the fragment of $\mu\text{ELL}^{\infty}$ corresponding to Baillot’s system.

Finally, while we started with non-wellfounded proofs, studying how these results can be adapted to finitary versions of $\mu\text{superLL}^{\infty}$ is another interesting open question.

References

[1] David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533375.
[2] David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In CSL 2016, volume 62 of LIPIcs, pages 42:1–42:17, 2016. doi:10.4230/LIPIcs.CSL.2016.42.
[3] Patrick Baillot. On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy. Information and Computation, 241:3–31, 2015. doi:10.1016/j.ic.2014.10.005.
[4] Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Information and Computation, 261:55–77, 2018. Developments in Implicit Computational Complexity (DICE) 2014 and 2015. doi:10.1016/j.ic.2018.05.005.
[5] Esaïe Bauer and Alexis Saurin. On the cut-elimination of the modal $\mu$ -calculus: Linear logic to the rescue. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures, pages 133–154, Cham, 2025. Springer Nature Switzerland. doi:10.1007/978-3-031-90897-2_7.
[6] Esaïe Bauer and Olivier Laurent. Super exponentials in linear logic. Electronic Proceedings in Theoretical Computer Science, 353:50–73, December 2021. doi:10.4204/eptcs.353.3.
[7] Esaïe Bauer and Alexis Saurin. A uniform cut-elimination theorem for linear logics with fixed points and super exponentials, 2025. doi:10.48550/arXiv.2506.14327.
[8] Aloïs Brunel and Kazushige Terui. Church => Scott = Ptime: an application of resource sensitive realizability. In Patrick Baillot, editor, Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010, volume 23 of EPTCS, pages 31–46, 2010. doi:10.4204/EPTCS.23.3.
[9] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions. Annals of Pure and Applied Logic, 163(3):266–290, 2012. doi:10.1016/j.apal.2011.09.003.
[10] Agata Ciabattoni, Lutz Straßburger, and Kazushige Terui. Expanding the realm of systematic proof theory. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, pages 163–178, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. doi:10.1007/978-3-642-04027-6_14.
[11] Agata Ciabattoni and Kazushige Terui. Modular cut-elimination: Finding proofs or counterexamples. In Miki Hermann and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 135–149, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11916277_10.
[12] Ugo Dal Lago and Patrick Baillot. On light logics, uniform encodings and polynomial time. Mathematical Structures in Computer Science, 16(4):713–733, 2006. doi:10.1017/S0960129506005421.
[13] Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. IC, 183(1):123–137, May 2003. doi:10.1016/S0890-5401(03)00010-5.
[14] Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: Linear logic. J. Symb. Log., 62(3):755–807, 1997. doi:10.2307/2275572.
[15] Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.
[16] Jean-Yves Girard. Light linear logic. IC, 143(2):175–204, June 1998. doi:10.1006/inco.1998.2700.
[17] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.
[18] Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318(1–2):163–180, June 2004. doi:10.1016/j.tcs.2003.10.018.
[19] Lê Thành Dũng Nguyen. On the elementary affine lambda-calculus with and without fixed points. Electronic Proceedings in Theoretical Computer Science, 298:15–29, August 2019. doi:10.4204/eptcs.298.2.
[20] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In PPDP 2009, pages 129–140, New York, NY, USA, 2009. ACM. doi:10.1145/1599410.1599427.
[21] Luca Roversi and Luca Vercelli. Safe recursion on notation into a light logic by levels. In Patrick Baillot, editor, Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010, volume 23 of EPTCS, pages 63–77, 2010. doi:10.4204/EPTCS.23.5.
[22] Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points. In Automated Reasoning with Analytic Tableaux and Related Methods, pages 203–222. Springer, 2023. doi:10.1007/978-3-031-43513-3_12.
[23] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
[24] Kazushige Terui. Which structural rules admit cut elimination? an algebraic criterion. Journal of Symbolic Logic, 72(3):738–754, 2007. doi:10.2178/jsl/1191333839.
[25] Kazushige Terui. Proof theory and algebra in substructural logics. In Kai Brünnler and George Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 20–20, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.

Appendix A Details on the background section

A.1 Proof of Axiom Expansion property

Lemma 41 (Axiom Expansion).

One-step axiom expansion holds for formulas $\wn_{\sigma}A$ and $\oc_{\sigma}A$ in $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ if $\sigma$ satisfies the following expansion axiom: $\sigma\leq_{\text{u}}\sigma\quad\lor\quad\sigma\leq_{\text{f}}\sigma\quad\lor% \quad(\sigma\leq_{\text{g}}\sigma\land\sigma(\wn_{\text{m}_{1}})).$

The axiom expansion holds in $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{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$ :

$\blacksquare$

If $\sigma\leq_{\text{u}}\sigma$ is true, then we have:
$\blacksquare$

If $\sigma\leq_{\text{f}}\sigma$ is true, it is similar to the previous case:
$\blacksquare$

And if $\sigma\leq_{\text{g}}\sigma$ and $\overline{(\sigma)}(\wn_{\text{m}_{1}})$ :

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

Appendix B Details on the super exponentials with fixed-points section

B.1 Details on the modal mu-calculus as super exponential system

We check that the system $\textnormal{{$\mu\text{superLL}^{\infty}$}}(\mathcal{E},\leq_{\text{g}},\leq_{% \text{f}},\leq_{\text{u}})$ presented in Section 4.2.1 satisfies the cut-elimination axioms of Table 1:

$\blacksquare$

The hypotheses of axiom $(\mathsf{Ax_{c})}$ are satisfied only for $i=2$ , in two cases: either $\sigma=\sigma^{\prime}=\bullet$ , in which case $\bar{\sigma}(\wn_{\text{c}_{2}})$ holds because $\sigma(\wn_{\text{c}_{2}})$ does; or $\sigma=\bullet$ and $\sigma^{\prime}=\star$ , in which case the axiom is satisfied because $\sigma^{\prime}(\wn_{\text{c}_{2}})$ holds.
$\blacksquare$

The hypotheses of axiom $(\mathsf{Ax^{g}_{m})}$ are satisfied for $i=0$ when $\sigma=\sigma^{\prime}=\bullet$ , or for $\sigma=\bullet$ and $\sigma^{\prime}=\star$ , in both cases we have $\bar{\sigma^{\prime}}(\wn_{\text{c}_{0}})$ true because $\sigma^{\prime}(\wn_{\text{m}_{0}})$ is true.
$\blacksquare$

Axiom $(\mathsf{Ax^{g}_{m})}$ is always true for $i=1$ .
$\blacksquare$

The hypotheses of axiom $(\mathsf{Ax^{g}_{m})}$ are never satisfied for $i>1$ .
$\blacksquare$

The hypotheses of axiom $(\mathsf{Ax^{fu}_{m})}$ are satisfied only for $\sigma=\sigma^{\prime}=\star$ , in which case it holds.
$\blacksquare$

Axiom $(\mathsf{Ax_{trans})}$ is satisfied since $\leq_{\text{g}}$ and $\leq_{\text{f}}$ are transitive.
$\blacksquare$

The hypotheses of axiom $(\mathsf{Ax_{\leq}^{gs})}$ are satisfied only for $\sigma=\bullet$ and $\sigma^{\prime}=\sigma^{\prime\prime}=\star$ , in which case the conclusion is already one of the hypotheses.
$\blacksquare$

The hypotheses of the other axioms are never fully satisfied.

Appendix C Details on the cut-elimination section

C.1 Details on Definition 26

Below is a graphical picture of Definition 26 in the second case ( $S^{\oc}=S^{\oc_{\text{f}}}$ or $S^{\oc}=S^{\oc_{\text{u}}}$ ) when all its sons (for the tree relation induced by $\perp\!\!\!\perp$ ) are of the form $S_{i}^{\oc_{\text{g}}}$ (which illustrates both cases of the definition in one picture):

C.2 Rule permutations

Definition 42 (Permutation of rules).

We define a one-step rule permutation on (pre-)proofs of $\mu\text{LL}^{\infty}$ as the permutation of two consecutive $\wn$ -rules.

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

$\blacksquare$

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

$\text{perm}(q(\pi^{\prime}),i\cdot p^{\prime}):=q(\text{perm}(\pi^{\prime},p^{% \prime}))$ if defined, else undefined;
$\blacksquare$

$\text{perm}(q(\pi_{l},\pi_{r}),l\cdot p^{\prime}):=q(\text{perm}(\pi_{l},p^{% \prime}),\pi_{r})$ if defined, else undefined;
$\blacksquare$

$\text{perm}(q(\pi_{l},\pi_{r}),r\cdot p^{\prime}):=q(\pi_{l},\text{perm}(\pi_{% r},p^{\prime}))$ if defined, else undefined;
$\blacksquare$

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

A sequence of rule permutations starting from a $\mu\text{LL}^{\infty}$ pre-proof $\pi$ is a (possibly empty) sequence $(p_{i})_{i\in\lambda}$ , with $\lambda\in\omega$ and $p_{i}\in\{l,r,i\}^{*}$ , such that if we let $\pi_{0}:=\pi$ , then the sequence $(\pi_{i})_{i\in 1+\lambda}$ defined inductively by $\pi_{i+1}:=\text{perm}(\pi_{i},p_{i})$ is well-defined at each step (i.e., each permutation is defined). We call $(\pi_{i})_{i\in 1+\lambda}$ the associated sequence of proofs to this sequence of rule permutations.

If $\lambda$ is finite, we say that the sequence ends at $\pi_{\lambda}$ ; we may also write $\text{perm}(\pi,(p_{i})_{i\in\lambda})$ to denote the proof obtained after the whole sequence of permutations.

Definition 43 (Finiteness of permutation of rules).

Let $\pi$ be a $\mu\text{LL}^{\infty}$ (pre-)proof, $(p_{i})_{i\in\lambda}$ a sequence of rule permutations starting from $\pi$ , and $(\pi_{i})_{i\in 1+\lambda}$ the associated sequence of proofs. Let $q\in\{l,r,i\}^{*}$ be a path to the conclusion sequent of a rule $(r)$ in $\pi$ . We define the sequence of residuals $(q_{i})_{i\in 1+\lambda}$ of $(r)$ in $\pi_{i}$ as a sequence of paths defined inductively on $i$ :

$\blacksquare$

if $i=0$ , set $q_{0}=q$ ;
$\blacksquare$

if $p_{i}=q_{i}$ , then $q_{i+1}:=q_{i}\cdot i$ ;
$\blacksquare$

if $q_{i}=p_{i}\cdot i$ , then $q_{i+1}:=p_{i}$ ;
$\blacksquare$

otherwise, $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 every rule of $\pi_{0}$ is finitely permuted.

C.3 Illustration of the reduction sequence translation corollary

Example 44.

Taking $C=A^{\perp}=B^{\perp}=\mu X.\wn_{\sigma}X$ , we consider the proof:

This proof reduces to:

then, we have for instance a $\mu,\nu$ key-case and then commutations of some $\nu$ :

which reduces to:

This sequence translates to:

The rules in red are the rules that have just permuted down the multicut. There exists a permutation between them that gets to the translation of the second proof of the sequence:

The translation of the reduction sequence continues:

Again, we have that permuting the rules in red together gives us the translation of the intermediary step in our translation. Then we obtain:

When permuting the rules in red together and then the rules in blue together, we obtain the translation of the final proof of our sequence:

For a finite sequence, we have a finite number of permutations; thus, the validity of the proof with permuted rules follows from the validity of the original by Proposition 34. However, infinite sequences may ultimately result in an infinite number of permutations, so we must prove that each rule is only finitely permuted in order to apply Proposition 34. The argument is that rules that need to be permuted must only be permuted with rules that were part of the same cut-step: in our example, the blue rules are permuted together, and the red rules are permuted together.

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

[bib.bib2] [2] David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In CSL 2016, volume 62 of LIPIcs, pages 42:1–42:17, 2016. doi:10.4230/LIPIcs.CSL.2016.42.

[bib.bib3] [3] Patrick Baillot. On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy. Information and Computation, 241:3–31, 2015. doi:10.1016/j.ic.2014.10.005.

[bib.bib4] [4] Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Information and Computation, 261:55–77, 2018. Developments in Implicit Computational Complexity (DICE) 2014 and 2015. doi:10.1016/j.ic.2018.05.005.

[bib.bib5] [5] Esaïe Bauer and Alexis Saurin. On the cut-elimination of the modal $\mu$ -calculus: Linear logic to the rescue. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures, pages 133–154, Cham, 2025. Springer Nature Switzerland. doi:10.1007/978-3-031-90897-2_7.

[bib.bib6] [6] Esaïe Bauer and Olivier Laurent. Super exponentials in linear logic. Electronic Proceedings in Theoretical Computer Science, 353:50–73, December 2021. doi:10.4204/eptcs.353.3.

[bib.bib7] [7] Esaïe Bauer and Alexis Saurin. A uniform cut-elimination theorem for linear logics with fixed points and super exponentials, 2025. doi:10.48550/arXiv.2506.14327.

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

[bib.bib9] [9] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions. Annals of Pure and Applied Logic, 163(3):266–290, 2012. doi:10.1016/j.apal.2011.09.003.

[bib.bib10] [10] Agata Ciabattoni, Lutz Straßburger, and Kazushige Terui. Expanding the realm of systematic proof theory. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, pages 163–178, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. doi:10.1007/978-3-642-04027-6_14.

[bib.bib11] [11] Agata Ciabattoni and Kazushige Terui. Modular cut-elimination: Finding proofs or counterexamples. In Miki Hermann and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 135–149, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11916277_10.

[bib.bib12] [12] Ugo Dal Lago and Patrick Baillot. On light logics, uniform encodings and polynomial time. Mathematical Structures in Computer Science, 16(4):713–733, 2006. doi:10.1017/S0960129506005421.

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

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

[bib.bib15] [15] Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

[bib.bib16] [16] Jean-Yves Girard. Light linear logic. IC, 143(2):175–204, June 1998. doi:10.1006/inco.1998.2700.

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

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

[bib.bib19] [19] Lê Thành Dũng Nguyen. On the elementary affine lambda-calculus with and without fixed points. Electronic Proceedings in Theoretical Computer Science, 298:15–29, August 2019. doi:10.4204/eptcs.298.2.

[bib.bib20] [20] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In PPDP 2009, pages 129–140, New York, NY, USA, 2009. ACM. doi:10.1145/1599410.1599427.

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

[bib.bib22] [22] Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points. In Automated Reasoning with Analytic Tableaux and Related Methods, pages 203–222. Springer, 2023. doi:10.1007/978-3-031-43513-3_12.

[bib.bib23] [23] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[bib.bib24] [24] Kazushige Terui. Which structural rules admit cut elimination? an algebraic criterion. Journal of Symbolic Logic, 72(3):738–754, 2007. doi:10.2178/jsl/1191333839.

[bib.bib25] [25] Kazushige Terui. Proof theory and algebra in substructural logics. In Kai Brünnler and George Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 20–20, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.

A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

On the redundancy of cut-elimination proofs.

Linear modal 𝝁-calculus.

Light logics with least and greatest fixed points.

Organization and contributions of the paper.

2 Background on LL, fixed-points and non-wellfounded proofs

2.1 Formulas, sequent calculi and non-wellfounded proofs

Definition 1 (Negation).

Definition 2 (MALL, LL and μ⁢LL∞ inference rules).

Definition 3 (Pre-proofs).

Example 4 (Regular proof).

Definition 5 (Validity and proofs).

Example 6.

2.2 Cut-elimination for linear logic with fixed-point

Example 7.

Definition 8 (Restriction of a multicut context).

Definition 9.

Theorem 10.

3 Super exponentials

Definition 11 (Superexponential formulas).

Notation 12 (List of exponential signatures).

Definition 13.

Definition 14.

Remark 15.

Definition 16 (superLL⁢(ℰ,≤g,≤f,≤u)).

Definition 17 (Derivability closure).

Proposition 18.

Notation 19.

Definition 20 (Cut-elimination axioms).

Theorem 21 (Cut Elimination).

Example 22.

4 Super exponentials with fixed-points

4.1 Definition of 𝝁superLL∞

4.2 Some instances of 𝝁superLL∞

4.2.1 A linear modal 𝝁-calculus

4.2.2 ELL with fixed points

Remark 23.

4.2.3 𝝁superLL⊤∞

Lemma 24.

5 Cut-elimination

5.1 (mcut)-elimination steps

Notation 25 ((!)-contexts).

Definition 26 (𝒪mpxS!⁢(𝒞!) contexts).

Definition 27 (μ⁢superLL⊤∞⁢(ℰ) cut-relation).

Lemma 28 (Soundness of the mcut-steps).

Proof sketch.

Definition 29 (μ⁢superLLℰ∞ cut-reduction steps).

5.2 Translating 𝝁superLL∞ into 𝝁LL∞

Definition 30 ((−)∘-translation).

Lemma 31 ((−)∘ preserves validity).

Lemma 32.

Proof sketch.

Lemma 33 (Completeness of the (mcut)-reduction system).

Proposition 34.

Corollary 35.

Proof sketch.

Theorem 36.

Proof sketch.

Theorem 37.

Proof.

Proof of Theorem 21.

Remark 38.

Corollary 39 (Cut Elimination for μ⁢LL□∞).

Corollary 40 (Cut Elimination for μ⁢ELL∞).

6 Conclusion

Future work

References

Appendix A Details on the background section

A.1 Proof of Axiom Expansion property

Linear modal $\mu$ -calculus.

Definition 2 (MALL, LL and $\mu\text{LL}^{\infty}$ inference rules).

Definition 16 ( $\textnormal{{$\text{superLL}$}}(\mathcal{E},\leq_{\text{g}},\leq_{\text{f}},% \leq_{\text{u}})$ ).

4.1 Definition of $\mu$ superLL^∞

4.2 Some instances of $\mu$ superLL^∞

4.2.1 A linear modal $\mu$ -calculus

4.2.3 $\mu$ superLL ${}^{\infty}_{\top}$

Notation 25 ( $(\oc)$ -contexts).

Definition 26 ( ${{\scriptstyle\mathcal{O}}_{\text{mpx}}}_{S^{\oc}}(\mathcal{C}^{\oc})$ contexts).

Definition 27 ( $\textnormal{{$\mu\text{superLL}^{\infty}_{\top}$}}(\mathcal{E})$ cut-relation).

Definition 29 ( $\mu\text{superLL}^{\infty}_{\mathcal{E}}$ cut-reduction steps).

5.2 Translating $\mu$ superLL^∞ into $\mu$ LL^∞

Definition 30 ( $(-)^{\circ}$ -translation).

Lemma 31 ( $(-)^{\circ}$ preserves validity).

Corollary 39 (Cut Elimination for $\mu\text{LL}_{\Box}^{\infty}$ ).

Corollary 40 (Cut Elimination for $\mu\text{ELL}^{\infty}$ ).