# Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Abhishek De, Farzad Jafarrahmani, Alexis Saurin

► To cite this version:

Abhishek De, Farzad Jafarrahmani, Alexis Saurin. Phase Semantics for Linear Logic with Least and Greatest Fixed Points. FSTTCS 2022 - 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2022, Chennai, India. pp.35:1–35:23, 10.4230/LIPIcs.FSTTCS.2022.35 . hal-04061582

HAL Id: hal-04061582

https://hal.science/hal-04061582

Submitted on 6 Apr 2023

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Abhishek De ☐

IRIF, Université Paris Cité, CNRS & INRIA π.r², France

Farzad Jafarrahmani ☐

IRIF, Université Paris Cité, CNRS & INRIA π.r², France

Alexis Saurin ☐

IRIF, CNRS, Université Paris Cité & INRIA π.r², France

## Abstract

The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (μMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively.

In this paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to μMALL with explicit (co)induction (i.e. μMALL<sup>ind</sup>). We introduce a Tait-style system for μMALL called μMALL<sub>ω</sub> where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.

**2012 ACM Subject Classification** Theory of computation → Linear logic; Theory of computation → Proof theory

**Keywords and phrases** Linear logic, fixed points, phase semantics, closure ordinals, cut elimination

**Digital Object Identifier** 10.4230/LIPIcs.FSTTCS.2022.35

**Funding** This research has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01.

*Abhishek De*: This author has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 754362.

**Acknowledgements** We would like to thank anonymous reviewers for their valuable comments that enhanced the clarity and presentation of this paper. We would like to thank Amina Doumane, Graham Leigh and Rémi Nollet for helpful discussions in the early phase of this work.

## 1 Introduction

**Fixpoint logics: from truth to proofs.** Fixpoint logics were first introduced in the study of inductive definability [1] in recursion theory which predates its first application in computer science as an expressive database query language [3]. In order to define the language of a fixpoint logic, one introduces explicit fixpoint construct(s) and closes it under these construct(s) thus obtaining a richer language. First order logic extended with various fixpoint operators have been extensively explored in model theory [38]. In the propositional case, the (multi)modal μ-calculus (the extension of basic modal logic K with least and greatest fixpoint operators) is probably the most well-studied. Introduced by Scott and Bakker in an unpublished manuscript, the logic has been historically studied in the formal methods and verification community [16]. More recently, there has been a growing interest in its structural proof-theory. The most important result in this direction is the completeness of Hilbert-style axiomatisations for the logic, which has turned out to be notoriously difficult [34, 51, 50].

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

© Abhishek De, Farzad Jafarrahmani, and Alexis Saurin;
licensed under Creative Commons License CC-BY 4.0

42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
(FSTTCS 2022).

Editors: Anuj Dawar and Venkatesan Guruswami; Article No. 35; pp. 35:1–35:23

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

Leibniz International Proceedings in Informatics
LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
**Various proof systems for fixpoint logics.** The setting of our paper is µMALL, the extension of multiplicative additive linear logic by fixpoints viz. the propositional fragment of the logic introduced by Baelde and Miller in [7] who proposed the sequent calculus system µMALL<sup>ind</sup> for the logic. All these formalisations viz. the Hilbert-style axiomatisations of µ-calculus and µMALL<sup>ind</sup> employ inference rules that express an *explicit* (co)induction scheme i.e. the induction hypothesis must be provided explicitly. However, sequent calculi with explicit (co)induction do not have the subformula property in spite of having analyticity. In fact, it is generally accepted that we do not have *true* cut elimination for any logic equipped with a theory of inductive definitions [40]. However, one can consider an alternative formalisation of inductive reasoning *viz.* *implicit* induction, which avoids the need for explicitly specifying (co)induction invariants. This formalism generally recovers true cut elimination but at the price of infinitary axiomatisation of the fixpoints. There are two approaches to this.

The first approach is to consider a Tait-style system i.e. infinitary wellfounded derivations which use a so-called ω-rule with infinitely many premises of finite approximations of a fixpoint. Such rules arise in various areas of logic, notably as Carnap's rule [15] in arithmetic. A complete Tait-style system has been proposed for fixpoint logics viz. for the μ-calculus [35] and star-continuous action lattices [43] (where the ω-rule construes the Kleene star as an ω-iteration of finite concatenations).

The second approach is to define a non-wellfounded and/or a circular proof system with finitely branching inferences. Such systems have been extensively studied in the setting of µMALL [44, 28, 6, 23]. Circular proofs have deep roots in the history of logic and mathematical reasoning: starting with Euclid's [27] heuristic of infinite descent through the more rigorous studies of Fermat [22]. A systematic investigation of the connection between circular proofs and reasoning by infinite descent has been carried out by Brotherston and Simpson [11, 12, 13].

**Proof systems difficult to compare.** Brotherston and Simpson conjectured that (in the setting of Martin-Löf's inductive definitions) circular proofs derive the same statements as finitary proofs with explicit induction. The so-called *Brotherston-Simpson conjecture* remained open for about a decade until Berardi and Tatsuta [8, 10] answered it negatively for the general case. On the other hand, if the logic contains arithmetic, the conjecture is known to be true; proved independently by Simpson [47], and Berardi and Tatsuta [9].

Note that the Brotherston-Simpson conjecture is heavily dependent on the base logic since the availability of structural rules or modal constructs induce subtle differences. For instance, the modal µ-calculus coincides on all systems. On the other hand, in Kleene Algebras, which is a substructural logic, the wellfounded, circular, and Tait-style systems are indeed different. In the setting of linear logic, in a recent work [20], the circular and the non-wellfounded system has been shown to be separate. However, the exact relation between finitary and circular system is still open. There is good reason for the difficulty. The very restricted use of structural rules in the linear setting induces a much more refined provability relation. Therefore, in this paper, we study the provability semantics *a.k.a.* the *phase semantics* of these logics as a first step of tackling the Brotherston-Simpson conjecture. Categorical semantics of circular proofs of the additive fragment have been studied in [44]. More recently, coherence space semantics have been studied for µMALL<sup>ind</sup> [24] as well as preliminary results on µMALL<sub>ω</sub> denotational semantics [26]. These semantics interpret formulas as well as their proofs thereby preserving their computational content. On the other hand, phase semantics is a coarser interpretation that allows for expressing strong invariant of linear logic provability and has been notably used to prove decidability results [36, 19] and cut admissibility results [42].
**Contributions.** In this paper, we shall develop a phase semantics for various proof systems for $\mu$MALL. Our first contribution is the notion of $\mu$-phase models which are bespoke mathematical objects that are shown to be sound and complete interpretation for $\mu$MALL<sup>ind</sup>. The completeness proof is intricate via Tait-Girard reducibility candidates and is inspired from [42]. Subsequently, we obtain the cut-admissibility of $\mu$MALL<sup>ind</sup> by semantic means. Furthermore, we design a new Tait-style proof system for $\mu$MALL *viz.* $\mu$MALL<sub>ω</sub> and obtain its phase semantics and cut-admissibility. In this case, the crux of the completeness proof is the obtention of a wellfounded notion of the rank of a formula. Cut-admissibility lets us show that $\mu$MALL<sub>ω</sub> and $\mu$MALL<sup>ind</sup> are different systems in terms of provability. Finally, we show that $\mu$MALL<sub>ω</sub> does not have a finite model property using an idea by Lafont [36].

**Organisation of the paper.** The paper is organised as follows. In Section 2, we give a brief exposition of linear logic and its phase semantics, relevant fixpoint theorems and describe the syntax and relevant properties of $\mu$MALL. In Section 3, we develop the phase semantics of $\mu$MALL *wrt.* the wellfounded proof system $\mu$MALL<sup>ind</sup>. In Section 4, we introduce the Tait-style proof system $\mu$MALL<sub>ω</sub> and study its semantics, cut-admissibility and finite model property. Finally, we conclude in Section 5 discussing directions of future work. Two appendices complement the paper: a table summarizing the proof systems used in this paper is provided in Appendix A, proof details are provided in Appendix B.

**Notation.** Let $F$ and $G$ be formulas. $F(G/x)$ denotes that every occurrence of $x$ in $F$ is replaced by $G$. If $x$ is clear from the context, we simply write it as $F(G)$. A special case is $F^n(x)$ which denotes $\overbrace{F(F(\cdots(F(x))\cdots)}}^n$. We write $a^n$ as a macro for $\overbrace{a\mathfrak{g}\cdots\mathfrak{g}a}^n$. Let $\Gamma$ be any sequent. Then, $\mathcal{L} \vdash \Gamma$ ($\mathcal{L} \vdash_{cf} \Gamma$ respectively) denotes that there is a proof (cut-free proof respectively) of $\Gamma$ in the system $\mathcal{L}$. Finally, for any finite set $S$, its cardinality is $|S|$.

# 2 Background

## 2.1 Linear logic and phase semantics

*Substructural logics* are logics lacking at least one of the usual structural rules. In *linear logic* [30], one of the most well-studied substructural logics, sequents are effectively multisets and the use of contraction and weakening is carefully controlled. Conjunction and disjunction each have two versions in linear logic: *multiplicative* and *additive*. Consequently the units have multiplicative and additive versions as well.

<table><thead><tr><th></th><th>conjunction</th><th>disjunction</th><th>true</th><th>false</th></tr></thead><tbody><tr><td>multiplicative</td><td>&#9787;</td><td>&#9788;</td><td><b>1</b></td><td>&#9789;</td></tr><tr><td>additive</td><td>&#9788;</td><td>&#9789;</td><td>&#9790;</td><td><b>0</b></td></tr></tbody></table>

The logical system thus obtained is called multiplicative-additive linear logic (MALL) and its inference rules are depicted in Figure 1 (sequents being construed as finite multisets). Full linear logic extends MALL by incorporating certain “exponential” modalities, written $?F$ and, dually, $!F$. Because of the absence of contraction and weakening, linear logic is resource-conscious *i.e.* one is concerned over the number of times that a given sentence is used in the proof of another sentence. To get a flavour of *phase semantics*, the provability semantics of linear logic [30], it is informative to characterise the set of lists $\Gamma$ of formulas that make a formula $F$ provable.
<table><caption>Figure 1 Inference rules for MALL, where $i \in \{1, 2\}$.</caption><thead><tr><th></th><th>Γ, F, F<sup>⊥</sup> (id)</th><th>Γ<sub>1</sub>, F, Γ<sub>2</sub>, F<sup>⊥</sup> (cut)</th></tr></thead><tbody><tr><td><strong>Identity rules</strong></td><td>Γ, F<sub>1</sub>, F<sub>2</sub> (⊗)</td><td>Γ<sub>1</sub>, F<sub>1</sub>, Γ<sub>2</sub>, F<sub>2</sub> (⊗)</td></tr><tr><td><strong>Logical rules</strong></td><td>Γ, F<sub>1</sub> ⊗ F<sub>2</sub> (⊗)</td><td>Γ<sub>1</sub>, Γ<sub>2</sub>, F<sub>1</sub> ⊗ F<sub>2</sub> (⊗)</td></tr><tr><td><strong>multiplicative connectives</strong></td><td>Γ, F<sub>i</sub> (⊕<sub>i</sub>)</td><td>Γ, F<sub>1</sub>, Γ, F<sub>2</sub> (⊗)</td></tr><tr><td><strong>additive connectives</strong></td><td>Γ, F<sub>1</sub> ⊕ F<sub>2</sub> (⊕<sub>i</sub>)</td><td>Γ, F<sub>1</sub> &amp; F<sub>2</sub> (⊗)</td></tr></tbody></table>

**Definition 1.** For a formula $F$, define $\Pr(F) = \{\Gamma \mid \text{MALL} \vdash \Gamma, F\}$ and $\Pr_{cf}(F) = \{\Gamma \mid \text{MALL} \vdash_{cf} \Gamma, F\}$.

Let us examine some properties of $\Pr(F)$. First, notice that the axiom rule ensures that for any $F$, $F^\perp \in \Pr(F)$. Invertibility of the ($\perp$) rule gives us $\Pr(\perp)$ is the set of all provable sequents. Similar observations on the invertibility of the ($\&$) rule inform that $\Pr(G \& G) = \Pr(F) \cap \Pr(G)$. For the (non-invertible) connectives $\otimes$ and $\oplus$, we only have $\Pr(F \otimes G) \supseteq \Pr(F) \cdot \Pr(G) = \{\Gamma, \Delta \mid \Gamma \in \Pr(F), \Delta \in \Pr(G)\}$ and $\Pr(F \oplus G) \supseteq \Pr(F) \cup \Pr(G)$. This suggests that the algebraic model for linear logic should simultaneously be a monoid and lattice i.e. a *residuated lattice*.

$\Pr(\perp)$ plays a major role in this approach, especially when considering it together with the cut inference. Indeed, for any $F$, one has that $\Pr(F^\perp) = \{\Gamma \mid \forall \Delta \in \Pr(F), \Gamma, \Delta \in \Pr(\perp)\}$. This naturally suggests to consider the operation $S^\perp = \{\Gamma \mid \forall \Delta \in S, \Gamma \cdot \Delta \in \Pr(\perp)\}$ which induces a closure operator ($\bullet$)$^{\perp\perp}$ on the set of multisets of linear formulas. As we will soon see, $\Pr(F)$ is closed under the double negation operation for any $F$.

These are the basic design principles of phase semantics: interpreting linear formulas as closed subsets of a monoid for the closure operation induced by the orthogonality relation w.r.t. a specific subset $\perp$ of the monoid which is an *abstraction of the provable sequents*.

**Definition 2.** A phase space is a 4-tuple $\mathcal{M} = (M, 1, \cdot, \perp)$ where $(M, 1, \cdot)$ is a commutative monoid and $\perp \subseteq M$. For $X, Y \subseteq M$, define the following operations: $XY := \{x \cdot y \mid x \in X, y \in Y\}$ and $X^\perp := \{y \mid \forall x \in X, x \cdot y \in \perp\}$.

Facts are those $X \subseteq M$ such that $X = X^{\perp\perp}$. (Equivalently, $X = Y^{\perp}$ for some $Y \subseteq M$.)

**Example 3.** Consider the additive monoid $(\mathbb{Z}, 0, +)$ and let $\perp = \{0\}$. For any set $S \subseteq \mathbb{Z}$, $S^\perp = \{y \mid \forall x \in S, x + y = 0\}$. Therefore, if $S$ is not singleton then $S^\perp = \emptyset$; so, $S^{\perp\perp} = \mathbb{Z}$. On the other hand, $\{x\}^\perp = \{-x\}$. The facts of this phase space are $\emptyset$, singleton sets, and $\mathbb{Z}$.

**Proposition 4.** Let $X, Y \subseteq M$. Then the following properties hold.

$$1. X \subseteq Y^{\perp} \iff XY \subseteq \perp$$

$$2. XX^{\perp} \subseteq \perp$$

$$3. X \subseteq Y \implies Y^{\perp} \subseteq X^{\perp}$$

$$4. X \subseteq X^{\perp\perp}$$

$$5. X^{\perp\perp\perp} = X^{\perp}$$

$$6. (X \cup Y)^{\perp} = X^{\perp} \cap Y^{\perp}$$

Let $X$ and $Y$ be facts. We define the following operations on facts.

$$X \otimes Y := (XY)^{\perp\perp}$$

$$X \& Y := X \cap Y$$

$$X \otimes Y := (X^{\perp}Y^{\perp})^{\perp}$$

$$X \oplus Y := (X \cup Y)^{\perp\perp}$$

**Proposition 5.** Let $X, Y$ be facts. Then, $1 \in X \otimes Y \iff X^{\perp} \subseteq Y$.
Fix a phase space $\mathcal{M}$ and let $\mathcal{X}$ be its set of facts. Fix $V: \mathcal{A} \to \mathcal{X}$ where $\mathcal{A}$ is the set of atoms. A phase space along with such a valuation $V$ is called a **phase model**. The semantics $[[F]]$ of a MALL formula $F$ is parameterised by a valuation (suppose, $V$) which we will denote by $[[F]]^V$. We are now ready to define the semantics which is defined inductively as follows:

$$
\begin{align*}
[[a]]^V &= V(a) & [[a^\perp]]^V &= [[a]]^V \perp & a \in \mathcal{A} \\
[[1]]^V &= \{1\}^{\perp \perp} & [[\perp]]^V &= \perp \\
[[0]]^V &= \{\emptyset\}^{\perp \perp} & [[\top]]^V &= M \\
[[F_1 \odot F_2]]^V &= [[F_1]]^V \odot [[F_2]]^V & \odot & \in \{\otimes, \mathcal{X}, \& , \oplus\}
\end{align*}
$$

When $V$ is clear from the context, we shall drop it, simply writing $[[F]]$. Finally, we generalise
the interpretation to sequents of the form $\Gamma = F_1, \dots, F_n$ as $[[\Gamma]] = [[F_1]\mathcal{X} F_2]\mathcal{X} \dots \mathcal{X} F_n]$.

► **Theorem 6** (MALL Soundness [30]). If MALL $\vdash \Gamma$ then for all phase models $(\mathcal{M}, V)$, $1 \in [[\Gamma]]^V$.

**Example 7.** To illustrate the utility of the phase semantics, we show that in any provable multiplicative formula $F$ (i.e. a MALL formula with only multiplicative connectives), an atom occurs exactly as many times as its negation. Fix an arbitrary atom $a$ occurring in $F$. Let $[[F]]^V$ be the interpretation of $F$ in the phase space in Example 3 w.r.t. the valuation $V$ that maps the atom $a$ to $\{1\}$ and every other atom to $\{0\}$. In this phase space, it is easy to see that $X \otimes Y = X \mathcal{X} Y = \{x+y \mid x \in X, y \in Y\}$. By Theorem 6, if $F$ is provable, $0 \in [[F]]^V$ hence number of occurrences of $a$ in $F$ is equal to the number of occurrences of $a^\perp$.

Note that a syntactic proof would require the heavy tool of MALL cut-admissibility.

**Definition 8.** The syntactic model (MALL•, 0, •, ⊥, V) is a phase model such that:

(MALL•, 0, •), called **syntactic monoid**, is the free commutative monoid generated by all formulas. In other words, MALL• is the set of all sequents construed as finite multisets, the empty multiset ∅ is the monoid identity, and multiset union is the monoid operation.

$\perp = \text{Pr}(\perp)$ i.e. $\perp$ is set of all provable sequents.

$V(a) = \text{Pr}(a)$ for all atoms $a \in \mathcal{A}$.

► **Remark 9.** Note that for the syntactic model to be well-defined one needs to show that $\text{Pr}(a)$ is a fact in the phase space (MALL•, 0, •, ⊥).

**Lemma 10 (Adequation Lemma for MALL).** For all formulas $F$, $[[F]]^V \subseteq \text{Pr}(F)$.

**Theorem 11 (MALL Completeness [30]).** If for all phase models $(\mathcal{M}, V)$, $1 \in [[\Gamma]]^V$ then MALL $\vdash \Gamma$.

**Proof sketch.** Suppose for any phase model $(\mathcal{M}, V)$, $1 \in [[\Gamma]]^V$. In particular, this holds for the syntactic model. By Lemma 10, $[[\Gamma]]^V \subseteq \text{Pr}(\Gamma)$ (construing $\Gamma$ as a parr formula). Therefore, $\emptyset \in \text{Pr}(\Gamma)$ (recall $\emptyset$ is the unit of syntactic monoid). Hence, $\vdash \Gamma$. ◀

Okada [42] observed that one can obtain the cut-admissibility of MALL for free by slightly
modifying the definition of the syntactic monoid. Now define $\perp = \text{Pr}_{cf}(\perp)$ and $V(a) = \text{Pr}_{cf}(a)$.
The refined adequation lemma $[[F]] \subseteq \text{Pr}_{cf}(F)$ follows exactly as in Lemma 10.

► **Theorem 12 (MALL cut-free completeness [42]).** If for any phase model $(\mathcal{M}, V)$, $1 \in [[\Gamma]]^V$ then MALL $\vdash_{cf} \Gamma$.

**Corollary 13.** MALL admits cuts.

**Proof.** Suppose MALL $\vdash \Gamma$. By Theorem 6, $\emptyset \in [[\Gamma]]^V$ for the syntactic model of MALL. By Theorem 12, MALL $\vdash_{cf} \Gamma$. ◀
## 2.2 Fixpoint theory and fixpoint logic

In this section we will recall some background on the fundamental fixpoint theorems of lattice theory. Not only will we use them several times in our technical proofs, but also, they will provide the intuition about the design of proof systems with fixpoint rules and their corresponding semantics. For the rest of this subsection, let $(S, \leq_S)$ be a complete lattice with least element $\bot$ and greatest element $\top$.

**Theorem 14** ([33, 49]). Let $f: S \to S$ be a monotonic function. The set of fixpoints of $f$ is non-empty and equipped with $\leq_S$ forms a complete lattice.

**Definition 15.** Let $f: S \to S$ be a monotonic function. $f$ is said to be **Scott-continuous** if for each directed subset $S$ we have $f(\bigvee_{S_i \in S} S_i) = \bigvee_{S_i \in S} f(S_i)$.

**Theorem 16** (Kleene Fixed Point Theorem). Every Scott-continuous function $f$ has the least fixpoint $\bigvee_{n \in \omega} f^n(\bot)$.

Observe that this is a constructive formulation of a fixpoint. Cousot and Cousot proved a constructive version of Theorem 14 without using the Scott-continuity hypothesis [17]. Let $f: S \to S$ be a monotonic function. The **lower iteration sequence** for $f$ starting with $x \in S$ is the sequence $\langle U_\alpha | \alpha \in \text{Ord} \rangle$ of elements of $S$ defined by transfinite induction as follows: (i) $U_0 = x$; (ii) $U_{\alpha+1} = f(U_\alpha)$; and, (iii) $U_\lambda = \bigwedge_{\alpha<\lambda} U_\alpha$ for $\lambda$ a limit ordinal.

**Theorem 17** ([17]). Let $f: S \to S$ be a monotonic function. The lower iteration sequence for $f$ starting from $\bot$ is increasing and there exists an ordinal $\theta$ (called the **closure ordinal** of $f$) such that $U_\theta = U_{\theta+1}$. Moreover, $U_\theta$ is the least fixpoint of $f$.

Note that one defines upper iteration sequence by taking supremums at limit ordinals. Dually, the greatest fixpoint is the stationary point of the decreasing upper iteration sequence starting from $\top$.

**Remark 18.** The closure ordinal of a Scott-continuous function is at most $\omega$.

## 2.3 Multiplicative additive linear logic with fixpoints

In this subsection we recall the propositional version of logic $\mu$MALL and its wellfounded proof system $\mu$MALL<sup>ind</sup> introduced in [7]. (See Appendix A for details)

**Definition 19.** Fix a countable set of atoms $\mathcal{A} = \{a, b, \dots\}$ and variables $\mathcal{V} = \{x, y, \dots\}$ such that $\mathcal{A} \cap \mathcal{V} = \emptyset$. $\mu$MALL **pre-formulas** are given by the following grammar:

$$F, G ::= \mathbf{0} \mid \top \mid \bot \mid \mathbf{1} \mid a \mid a^{\bot} \mid x \mid F \ominus G \mid F \otimes G \mid F \oplus G \mid F \& G \mid \mu x.F \mid \nu x.F$$

where $a \in \mathcal{A}$, $x \in \mathcal{V}$, and $\mu, \nu$ bind the variable $x$ in $F$. When a pre-formula is closed (i.e. no free variables), we simply call it a **formula**.

Negation, $(\bullet)^{\bot}$, defined as a meta-operation on pre-formulas, will be used only on formulas. As it is not part of the syntax, we do not need any positivity condition on the fixed-point expressions. As expected, least and greatest fixed points are the dual of each other.

**Definition 20.** Negation of a pre-formula is defined inductively as follows.

$$\begin{align*}
\mathbf{0}^{\bot} &= \top; & \top^{\bot} &= \mathbf{0}; & \bot^{\bot} &= \mathbf{1}; & \mathbf{1}^{\bot} &= \bot; & (a)^{\bot} &= a^{\bot}; & a^{\bot \bot} &= a; \\
x^{\bot} &= x; & (F \ominus G)^{\bot} &= F^{\bot} \otimes G^{\bot}; & (F \otimes G)^{\bot} &= F^{\bot} \ominus G^{\bot}; & (F \oplus G)^{\bot} &= F^{\bot} \& G^{\bot}; \\
(F \& G)^{\bot} &= F^{\bot} \oplus G^{\bot}; & (\mu x.F)^{\bot} &= \nu x.F^{\bot}; & (\nu x.F)^{\bot} &= \mu x.F^{\bot}. & & &
\end{align*}$$
35:8 Phase Semantics for μMALL

In order to extend the phase semantics of MALL to μMALL<sup>ind</sup> we extend valuations to variables i.e. for any valuation V, dom(V) = 𝒜 ∪ 𝒱 and define [[F]]<sup>V</sup> by induction on F with the usual interpretation of section 2.1 for atoms, units, and multiplicative-additive connectives and as follows for fixpoints formulas:

$$ [[\mu x.F]]^V = \bigcap_{X \in \mathcal{X}} \{X \mid [[F]]^{V[x \mapsto X]} \subseteq X\} \quad ; \quad [[\nu x.F]]^V = \left( \bigcup_{X \in \mathcal{X}} \{X \mid X \subseteq [[F]]^{V[x \mapsto X]}\} \right)^{\perp\perp} $$

$$ \text{where } V[x \mapsto X](y) := \begin{cases} V(y) & \text{if } y \neq x; \\ X & \text{if } y = x. \end{cases} $$

However completeness fails for such an interpretation. Indeed, not all facts necessarily have a pre-image, therefore [[F]]<sup>V</sup>[xmapsto X] does not exactly correspond to syntactic substitution and the tentative syntactic model is not a phase model. We need to allow strict subsets of 𝒜 for building fixpoints. Obviously, one cannot consider any subsets of 𝒜 for this purpose and we shall require that they satisfy some closure properties. Therefore we restrict the codomain of [[•]]<sup>V</sup> to subspaces of 𝒜 closed under μMALL operations. For any set of facts D ⊆ 𝒜, the set of contexts is given by the following grammar where ⊙ ∈ {⊗, ⊗, &, ⊕}. Let F<sub>D</sub> denote the set of contexts with exactly one hole.

$$ f,g ::= [] | X \in D | f \odot g $$

For $f \in \mathbb{F}_D$, define $\mu f = \bigcap_{X \in \mathcal{D}} \{X \mid f(X) \subseteq X\}$ and $\nu f = (\bigcup_{X \in \mathcal{D}} \{X \mid X \subseteq f(X)\})^{\perp\perp}$.

**Definition 26.** *D* ⊆ 𝒜 is said to be *μ-closed* if

- {⊥, ⊥, M, M⊥} ⊆ D;

- D is closed under the operations ⊗, ⊖, &, and ⊕; and

- for all $f \in \mathbb{F}_D$, $\mu f \in D$ and $\nu f \in D$.

A phase space 𝒜 equipped with a μ-closed set of facts D is called a μ-phase space.

A *D*-valuation is a map of the form $V: \mathcal{A} \cup \mathcal{V} \to \mathcal{D}$. A μ-phase space along with a *D*-valuation is called a μ-phase model. The μ-phase semantics [[•]] is a function that takes a μMALL pre-formula *F* and returns a fact in *D*.

Note that [[μx.F]]<sup>V</sup> and [[νx.F]]<sup>V</sup> are defined as before except *X* ranges over *D*. A priori, the semantics of pre-formula is only an element of 𝒜. The closure properties of *D* ensures [[F]]<sup>V</sup> ∈ *D* for every formula *F* and *D*-valuation *V*.

**Lemma 27 (Monotonicity).** Let *F* be a μMALL pre-formula. If *X* ⊆ *Y* then [[F]]<sup>V</sup>[*x*→*X*] ⊆ [[F]]<sup>V</sup>[*x*→*Y*].

**Proof.** A proof can be found in Appendix B.1.1.

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

An application of monotonicity is showing that the interpretation of the fixpoint operators are indeed fixpoints in the mathematical sense:

**Theorem 28.** Let *D* be μ-closed and $f \in \mathbb{F}_D$. Then μf and νf are the least and greatest fixpoints of f in *D*.

**Proof.** A proof can be found in Appendix B.1.2.

<figure><img src="image_5.png" /></figure>
35:10 Phase Semantics for μMALL

of the cut formula which reduces with each step of cut-elimination. This problem is solved
in [5] by invoking a technique similar to the Tait-Girard reducibility candidates (originally
formulated to establish certain properties of various typed lambda calculi [48, 29]). Recall
that the completeness of phase semantics gives cut admissibility for free. Therefore, it is not
surprising that in order to prove completeness one needs to invoke reducibility candidates.

► **Definition 31.** Let $(\mathcal{M}, \mathcal{D}, V)$ be a $\mu$-phase model. Given a $\mu$MALL formula $F$, the reducibility candidates of $F$, denoted $\langle F \rangle$, is given by $\{X \in \mathcal{X} \mid F^{\perp} \in X \subseteq \text{Pr}_{cf}(F)\}$.

► **Proposition 32.** $X \in \langle F \rangle \iff X^{\perp} \in \langle F^{\perp} \rangle$

**Proof.** We first note that $\mathrm{Pr}_{cf}(\bullet)$ can be straightforwardly generalised to sets of formulas as follows: $\mathrm{Pr}_{cf}(\{F_1, \dots, F_n\}) = \bigcup_{i \in [n]} \mathrm{Pr}_{cf}(F_i)$. Let $X \in \langle F \rangle$. Then $\{F^{\perp}\} \subseteq X \implies X^{\perp} \subseteq \{F^{\perp}\}^{\perp} = \mathrm{Pr}_{cf}(F^{\perp})$. Also, $X \subseteq \mathrm{Pr}_{cf}(F) \implies \mathrm{Pr}_{cf}(F)^{\perp} = \mathrm{Pr}_{cf}(\mathrm{Pr}_{cf}(F)) \subseteq X$. But $F \in \mathrm{Pr}_{cf}(\mathrm{Pr}_{cf}(F))$. Hence done. ◀

We are now ready to define the μ-syntactic model. Recall that $\mathrm{Pr}_{cf}(F)$ is the set of all sequents $\Gamma$ such that $\vdash \Gamma, F$ is cut-free provable.

**Definition 33.** The μ-syntactic model, denoted (μMALL<sup>•</sup>, 0, ·, ⊥, V), is defined as:

■ (μMALL<sup>•</sup>, 0, ·) is the free commutative monoid generated by all formulas.

■ $\bot = \mathrm{Pr}_{cf}(\bot)$

■ $V(p) = \mathrm{Pr}_{cf}(p)$ for all $p \in \mathcal{A} \cup \mathcal{V}$.

■ $\mathcal{D} = \bigcup_{F \in \mathcal{F}_{\mathrm{Form}}} \langle F \rangle$ where Form is the set of all μMALL formulas.

Observe that $\bot = \mathrm{Pr}_{cf}(\bot) \in \mathcal{D}$ and that $\mathcal{D}$ indeed contains $\bot^\perp$, $\mu\mathrm{MALL}^\bullet$ and $\mu\mathrm{MALL}^\bullet_\perp$.

**Lemma 34 (Adequation Lemma for μMALL<sup>ind</sup>)**. Let $F(\bar{x})$ be a pre-formula, $\bar{G} \equiv G_1, \dots, G_m$ with $\bar{x} \equiv x_1, \dots, x_m$ be an m-tuple of pre-formulas and let $\bar{X} \equiv X_1 \dots X_m$ be an m-tuple of facts such that $X_i \in \langle G_i \rangle$. We have $[[F]]^{V[\bar{x} \to \bar{X}]} \subseteq \mathrm{Pr}_{cf}(F(\bar{G}/\bar{x}))$.

**Proof.** By induction on $F$. Multiplicative additive cases are treated as in the proof of Lemma 10; we detail fixed-point cases only.

**Case 1.** Suppose $F = \mu y.F'$. Let $\xi = \mu y.F'(\bar{G}/\bar{x})$. In the proof of Theorem 30, we showed that for any formula $F_0$, $\mathrm{Pr}_{cf}(F_0(\mu x.F_0/x)) \subseteq \mathrm{Pr}_{cf}(\mu x.F_0)$. Therefore, $\mathrm{Pr}_{cf}(F'(\bar{G}/\bar{x}, \xi/y)) \subseteq \mathrm{Pr}_{cf}(\xi)$. Let $Y^* = [[F']]]^{V[\bar{x} \to \bar{X}, y \to \mathrm{Pr}_{cf}(\xi)]}$. By induction hypothesis and that fact that $\mathrm{Pr}_{cf}(F_0) \in \langle F_0 \rangle$ for all formulas $F_0$, we have the following.

$$
Y^* \subseteq \mathrm{Pr}_{cf}(F'(\bar{G}/\bar{x}, \xi/y)) \quad (1)
$$

Therefore, it is enough to show that $[[\mu y.F']^{V[\bar{x} \to \bar{X}]}] \subseteq Y^*$. Take $\Gamma \in [[\mu y.F']^{V[\bar{x} \to \bar{X}]}}$. For any fact $Y \in \mathcal{D}$, to show $\Gamma \in Y$ it is enough to show $[[F']^{V[\bar{x} \to \bar{X}, y \to Y]}] \subseteq Y$. Therefore we need to check that $[[F']^{V[\bar{x} \to \bar{X}, y \to Y^*]}] \subseteq Y^* = [[F']^{V[\bar{x} \to \bar{X}, y \to \mathrm{Pr}_{cf}(\xi)]}}$. This follows by Lemma 27 from 1.

**Case 2.** Suppose $F = \nu y.F'$. For any fact $Y$, define $Z_Y = [[F']^{V[\bar{x} \to \bar{X}, y \to Y]}}$. Let $\Gamma \in \bigcup \{Y \in \mathcal{D} \mid Y \subseteq Z_Y\}$. Therefore, there exists, $Y^* \in \mathcal{D}$ such that $\Gamma \in Y^* \subseteq Z_{Y^*}$. Since $Y^* \in \mathcal{D}$, $Y^* \in \langle \xi \rangle$ for some formula $\xi$. By induction hypothesis, $[[F']^{V[\bar{x} \to \bar{X}, y \to Y^*]}] \subseteq \mathrm{Pr}_{cf}(F'(\bar{G}/\bar{x}, \xi/y))$.

We will now show that $\mathrm{Pr}_{cf}(F'(\bar{G}/\bar{x}, \xi/y)) \subseteq \mathrm{Pr}_{cf}(F(\bar{G}/\bar{x}))$. Let $\Delta \in \mathrm{Pr}_{cf}(F'(\bar{G}/\bar{x}, \xi/y))$. If we show that $\xi^{\perp} \in \mathrm{Pr}_{cf}(F'(\bar{G}/\bar{x}, \xi/y))$, we have the following.
$$ \frac{\frac{\vdash \xi^{\perp}, F'(\overline{G}/\bar{x}, \xi/y)}{\vdash \Delta, F'(\overline{G}/\bar{x}, \xi/y)} \frac{\vdash (F'(\overline{G}/\bar{x}, \xi/y))^{\perp}, F'(\overline{G}/\bar{x}, F'(\overline{G}/\bar{x}, \xi/y)/y)}{\vdash \Delta, \nu x. F'(\overline{G}/\bar{x})} (\text{func})}{(\nu)} $$

In order to show $\xi^{\perp} \in \mathrm{Pr}_{cf}(F'(\overline{G}/\bar{x}, \xi/y))$, we use the induction hypothesis to reduce the problem to showing $\xi^{\perp} \in [[F']^{V[\bar{x} \to \bar{X}, y \to Y^*]}]$ which is true since $Y^* \in \langle\xi\rangle$. Therefore we have,

$$ \Gamma \in \mathrm{Pr}_{cf}(\nu y. F'(\overline{G}/\bar{x})) \Rightarrow \bigcup \{Y \in \mathcal{D} \mid Y \subseteq Z_Y\} \subseteq \mathrm{Pr}_{cf}(\nu y. F'(\overline{G}/\bar{x})) \\ \Rightarrow \left(\bigcup \{Y \in \mathcal{D} \mid Y \subseteq Z_Y\}\right)^{\perp\perp} \subseteq \mathrm{Pr}_{cf}(\nu y. F'(\overline{G}/\bar{x})) $$

This concludes our proof.

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

**Lemma 35.** Using notations of the previous lemma, we have that $F^{\perp}(\overline{G}/\bar{x}) \in [[F]^{V[\bar{x} \to \bar{X}]}}$.

**Proof.** Observe that Lemma 34 and Proposition 32 imply $[[F^{\perp}]^{V[\bar{x} \to \bar{X}^{\perp}]}] \subseteq \mathrm{Pr}_{cf}(F^{\perp}(\overline{G}^{\perp}/\bar{x}))$. Therefore, $\{F^{\perp}(\overline{G}^{\perp}/\bar{x})\}[[F^{\perp}]^{V[\bar{x} \to \bar{X}^{\perp}]}] \subseteq \{F^{\perp}(\overline{G}^{\perp}/\bar{x})\}$. $\mathrm{Pr}_{cf}(F^{\perp}(\overline{G}^{\perp}/\bar{x})) \subseteq \mathrm{Pr}_{cf}(\perp) = \perp$. By Proposition 4.1, $F^{\perp}(\overline{G}^{\perp}/\bar{x}) \subseteq ([[F^{\perp}]^{V[\bar{x} \to \bar{X}^{\perp}]}]^{\perp})$ which is $[[F]^{V[\bar{x} \to \bar{X}]}]$ by Lemma 29. ◀

Observe that by Lemma 34 and Lemma 35 we have $[[F]^{V[x \to X]}] \in \langle F(\overline{G}/\bar{x}) \rangle$. This ensures that $\mathcal{D}$ is $\mu$-closed. Consequently, $(\mu\mathrm{MALL}^{\bullet}, \emptyset, \cdot, \perp, V)$ is a $\mu$-phase space model.

**Theorem 36** ($\mu\mathrm{MALL}^{\mathrm{ind}}$ cut-free completeness). If for any $\mu$-phase model $(\mathcal{M}, \mathcal{D}, V)$, $1 \in [[\Gamma]]^V$ then $\mu\mathrm{MALL}^{\mathrm{ind}} \vdash_{cf} \Gamma$.

**Corollary 37.** $\mu\mathrm{MALL}^{\mathrm{ind}}$ admits cuts.

**Remark 38.** Note that this is an alternate proof of Theorem 25.

## 3.3 Closure ordinals

Closure ordinals are a standard measure of the complexity of any (class of) monotone functions. The closure ordinal of a fixed-point formula is essentially the closure ordinal of the corresponding monotone function in the truth semantics. In [21], the closure ordinal is construed as a function of the size of the finite model. The study of closure ordinals of modal logic formulas is a young and exciting area of research [18, 2, 31]. It departs from the previous notion of closure ordinals in its model-independence. In this case, closure ordinal really serves as a measure of complexity of a formula.

**Definition 39.** Let $F$ be a pre-formula such that $x \in \mathfrak{f}(F)$ and let $\mathcal{M} = (\mathcal{M}, \mathcal{D}, V)$ be a $\mu$-phase model. We define the **closure ordinal** of $F$ with respect to $x$ and $\mathcal{M}$, denoted $\mathcal{O}_{\mathcal{M}}(F)$, as the closure ordinal of $\lambda X. [[F]]^{V[x \to X]}$. The closure ordinal of $F$ with respect to $x$ (across all models) is defined as $\mathcal{O}(F) := \sup_{\mathcal{M}}\{\mathcal{O}_{\mathcal{M}}(F)\}$. Finally, $F$ is said to be **constructive** if its closure ordinal is at most $\omega$.

For any pre-formula $F$ and phase model $\mathcal{M}$, $\mathcal{O}_{\mathcal{M}}(F)$ exists since $\lambda X. [[F]]^{V[x \to X]}$ is mono- tonic. Consequently, the supremum $\mathcal{O}(F)$ exists since the class of all $\mu$-phase models is indeed a set.
**► Example 40.** Consider the pre-formula $a\&x$. Let $\langle \mathcal{U}_{\alpha}^{a\&x} | \alpha \in \text{Ord} \rangle$ be the iteration sequence of its approximations. $\mathcal{U}_0^{a\&x} = \emptyset^{\perp\perp}$ and $\mathcal{U}_1^{a\&x} = [[a\&x]]^{V[x \to \mathcal{U}_0^{a\&x}]} = V(a) \cap \emptyset^{\perp\perp}$. Therefore, $\mathcal{O}(a\&x) = 0$.

In the tradition of µ-calculus, the name “constructive” is used loosely here, motivated by the observation that if $\mathcal{O}(F)$ is a finite ordinal strictly below $\omega$ for any pre-formula $F$, then $\mu x.F$ is provably equivalent to $F^{\mathcal{O}(F)}(0)$. Therefore, the class of µMALL formulas with closure ordinal strictly less than $\omega$ can be embedded in MALL and enjoys several good properties like finite model property and decidability. Observe that if the interpretation of a formula in any phase model is Scott-continuous, then it is constructive by Theorem 16. The converse does not hold in general. In the following section we consider a proof system of µMALL where fixed points are approximated by their $\omega$th approximation.

**4 µMALL<sub>ω</sub>: an infinitary proof system**

For a constructive formula $F$,

$$ [[\mu x.F]]^V = \left( \bigcup_{n \ge 0} [[F^n(0)]^V] \right)^{\perp\perp} ; \quad [[\nu x.F]]^V = \bigcap_{n \ge 0} [[F^n(\top)]^V] \qquad (2) $$

Therefore, syntactically, $\mu x.F$ (respectively $\nu x.F$) is equivalent to an infinitary $\oplus$-formula $\bigoplus_{n \in \omega} F^n(0)$ (respectively, an infinitary $\&$-formula $\&_{n \in \omega} F^n(\top)$). We enrich the language of µMALL with the operators $\mu^n$ and $\nu^n$ for all $n \in \omega$. We call this language as well as the corresponding proof system, $\mu MALL_\omega$. (See Appendix A for details.)

**► Definition 41.** A $\mu MALL_\omega$ proof is a wellfounded (possibly infinitely branching) tree generated from the inference rules of MALL given in Figure 1 and the following rules for fixpoint operators where $\eta \in \{\mu, \nu\}$.

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \frac{\vdash \Gamma, \mathbf{0}}{\vdash \Gamma, \mu^0 x.F} (\mu^0) & ; & \frac{\vdash \Gamma, F(\eta^n x.F/x)}{\vdash \Gamma, \eta^{n+1} x.F} (\eta^{n+1}) & ; & \frac{\vdash \Gamma, \mu^n x.F}{\vdash \Gamma, \mu x.F} (\mu_n^\omega) \\ \frac{\vdash \Gamma, \top}{\vdash \Gamma, \nu^0 x.F} (\nu^0) & ; & \frac{\vdash \Gamma, \nu^0 x.F \quad \vdash \Gamma, \nu^1 x.F \quad \vdash \Gamma, \nu^2 x.F \quad \dots}{\vdash \Gamma, \nu x.F} (\nu^\omega) \end{array} $$

**► Example 42.** Let $H = (\mu x.a\mathcal{X}x)^{\perp}\mathcal{X}(a^{\perp p}\mathcal{X}0)$ for some $p \in \omega$.

$$ \frac{\frac{\frac{\frac{\frac{\{\vdash \nu^n y.F, \mu^{2n} x.a\mathcal{X}x\}_{n \in \omega}}{\{\vdash \nu^n y.F, \mu x.a\mathcal{X}x\}_{n \in \omega}}(\mu_{2n}^\omega)} \quad \frac{\frac{\vdash \mu^p x.a^{\perp} \mathcal{X}x, (a^{\perp p} \mathcal{X} 0)^{\perp}}{\vdash \nu y.F, \mu x.a\mathcal{X}x} (\nu^\omega)}(\otimes)}(\text{id})}{\frac{\vdash a^{\perp}, a}{\vdash a^{\perp}, \mu^p x.a^{\perp} \mathcal{X}x, a \otimes (\nu y.F), H^{\perp}}(\otimes)}(\otimes)}(\otimes) \\
\frac{\frac{\frac{\frac{\{\vdash \mu^p x.a^{\perp} \mathcal{X}x, a \otimes (\nu y.F), H^{\perp}}{\vdash a^{\perp} \mathcal{X}(\mu^p x.a^{\perp} \mathcal{X}x), a \otimes (\nu y.F), H^{\perp}}(\mu^{p+1})}{\vdash \mu^{p+1} x.a^{\perp} \mathcal{X}x, a \otimes (\nu y.F), H^{\perp}}(\mu_{p+1}^\omega)}(\otimes)}(\otimes) \\
\frac{\frac{\{\vdash \nu^n y.F, \mu^{2n} x.a\mathcal{X}x\}_{n \in \omega}}{\{\vdash \nu^n y.F, \mu x.a\mathcal{X}x\}_{n \in \omega}}(\mu_{2n}^\omega) \quad \frac{\frac{\{\vdash \nu^n y.F, \mu x.a\mathcal{X}x\}_{n \in \omega}}{\{\vdash \nu^n y.F, \mu x.a\mathcal{X}x\}_{n \in \omega}}(\nu^\omega)}(\otimes) \quad \frac{\frac{\{\vdash \mu^p x.a^{\perp} \mathcal{X}x, (a^{\perp p} \mathcal{X} 0)^{\perp}}{\frac{\vdash \mu^n x.F}{\vdash \Gamma, \mu^n x.F} (\mu_n^\omega)}(\otimes)}(\otimes) \quad \frac{\frac{\{\vdash \mu^n x.F}{\vdash \Gamma, \mu x.F} (\mu_n^\omega)}(\otimes)}(\otimes) \quad \frac{\{\vdash \nu^n y.F, \mu^{2n} x.a\mathcal{X}x\}_{n \in \omega}}{\{\vdash \nu^n y.F, \mu^{2n} x.a\mathcal{X}x\}_{n \in \omega}}(\mu_{2n}^\omega) $$

It is easy to show that for all $p, n \in \omega$, $\vdash \mu^p x.a^{\perp} \mathcal{X}x, (a^{\perp p} \mathcal{X} 0)^{\perp}$ and $\vdash \nu^n y.F, \mu^{2n} x.a\mathcal{X}x$ are provable by induction on $p$ and $n$ respectively.
Note that the set of inference rules (as schema) is infinite since {$\mu_n^\omega$}$_{n \in \omega}$ is a collection of $\omega$-many rules. Such infinitary systems (called Tait-style systems) where proof trees are wellfounded with possible infinite branching are studied in various areas of logic viz. arithmetic [15, 41] and fixpoint logics [35, 32]. It is quite tricky to define a proper notion of the complexity of a fixpoint formula in such settings. Closely based on [32], our notion of the rank of a $\mu$MALL$_\omega$ formula is a finite sequence of ordinals.

First we will set up some notion. If $\alpha_1, \dots, \alpha_n$ are ordinals, we write $\langle\alpha_1, \dots, \alpha_n\rangle$ for the sequence $\sigma$ whose length $|\sigma|$ is $n$ and whose $i$th component $\sigma_i$ is the ordinal $\alpha_i$. Let $<_{lex}$ be the strict lexicographical ordering of finite sequences of ordinals and $\leq_{lex}$ its reflexive closure. Note that $<_{lex}$ is a well-ordering on any set of sequences of bounded lengths but not a well-ordering in general. In particular, $\langle 1 \rangle, \langle 0, 1 \rangle, \langle 0, 0, 1 \rangle, \dots$ is an infinite descending chain in $<_{lex}$. Given two finite sequences of ordinals $\sigma, \tau$, we define the component-wise ordering $\sqsubseteq$ as $\sigma, \tau$ iff $|\sigma| \le |\tau|$ and $(\sigma)_i \le (\tau)_i$ for all $1 \le i \le |\sigma|$. Clearly, the relation $\sqsubseteq$ is transitive. We denote the standard concatenation of sequences by $*$. Finally we define a component-wise maximum operation $\sqcup$ by setting: (i) $\sigma \sqcup \langle \rangle := \langle \rangle$; (ii) if $\sigma = \langle b_1, \dots, b_m \rangle$ and $\tau = \langle b'_1, \dots, b'_n \rangle$, then

$$ \sigma \sqcup \tau = \begin{cases} \langle \max(b_1, b'_1), \dots, \max(b_m, b'_m), b'_{m+1}, \dots, b'_n \rangle & \text{if } m \le n; \\ \langle \max(b_1, b'_1), \dots, \max(b_n, b'_n), b_{n+1}, \dots, b_m \rangle & \text{otherwise.} \end{cases} $$

Now we are ready to define the rank of a $\mu$MALL$_\omega$ formula. The rank of every $\mu$MALL$_\omega$ formula will be a finite sequence of ordinals less than or equal to $\omega$.

**► Definition 43.** The rank of a $\mu$MALL$_\omega$ formula $F$, denoted $rk(F)$, is defined by induction on $F$ as follows.

- if $F$ is an atom, a variable, or a unit, then $rk(F) = \langle 0 \rangle$;

- if $F = G \odot G'$, then $rk(F) = (rk(G) \sqcup rk(G')) * \langle 0 \rangle$ where $\odot \in \{\mathcal{G}, \otimes, \oplus, \&\}$;

- if $F = \eta^n x.G$, then $rk(F) = rk(G) * \langle n \rangle$ where $\eta \in \{\mu, \nu\}$;

- if $F = \eta x.G$, then $rk(F) = rk(G) * \langle \omega \rangle$ where $\eta \in \{\mu, \nu\}$.

**► Example 44.** Consider $H = (\nu x.a^\perp \otimes x)\mathcal{G}(a^p\mathcal{G}0)$ from Example 42.

$$ \begin{aligned} rk(H) &= rk(\nu x.a^\perp \otimes x) \sqcup rk(a^p\mathcal{G}0) * \langle 0 \rangle \\ &= \left( (rk(a^\perp \otimes x) * \langle \omega \rangle) \sqcup \langle 0, \dots, 0 \rangle \right) * \langle 0 \rangle \\ &= \left( \langle 0, 0, \omega \rangle \sqcup \langle 0, \dots, 0 \rangle \right) * \langle 0 \rangle \\ &= \langle 0, 0, \omega, \overbrace{0, \dots, 0}^{\max(1, p-1)} \rangle \end{aligned} $$

**► Lemma 45.** Let $F$ be a $\mu$MALL$_\omega$ pre-formula such that $x \in \mathfrak{fv}(F)$. Let $\xi$ be a preformula such that $rk(F) \sqsubseteq rk(\xi)$. Then, there exists a finite (possibly empty) sequence of ordinals $\sigma$ such that $rk(F(\xi/x)) = rk(\xi) * \sigma$.

**Proof.** A proof can be found in Appendix B.2.1.

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

**► Theorem 46.** The following hold for any $\mu$MALL$_\omega$ formula $F$:

1. $rk(F) <_{lex} rk(F \odot G)$ and $rk(G) <_{lex} rk(F \odot G)$;

2. $rk(0) <_{lex} rk(\mu^0 x.F)$, $rk(\top) <_{lex} rk(\nu^0 x.F)$;

3. $rk(F(\eta^n x.F/x)) <_{lex} rk(\eta^{n+1} x.F)$ for all $n < \omega$;

4. $rk(\eta^n x.F) <_{lex} rk(\eta x.F)$ for all $n < \omega$.
**Proof.** The first, second, and fourth assertions are immediate from Definition 43. For the third one, we have two cases:

Suppose $x \notin fv(F)$. Then, $F(\eta^n x.F/x) = F$ and the result follows from Definition 43.

Otherwise, note that we have $rk(F) \trianglelefteq rk(\eta^n x.F)$. By Lemma 45, $rk(F(\eta^n x.F/x)) = rk(\eta^n x.F) * \sigma = rk(F) * \langle n \rangle * \sigma$ for some $\sigma$. But $rk(\eta^{n+1} x.F) = rk(F) * \langle n+1 \rangle$. Hence we are done. ◀

**Definition 47.** *The strong closure $\mathcal{SC}(F)$ of a $\mu$MALL$_{\omega}$ formula $F$ is the least set s.t.:*

$F \in \mathcal{SC}(F);$

$G \odot H \in \mathcal{SC}(F) \implies \{G, H\} \subset \mathcal{SC}(F) \text{ where } \odot \in \{\ominus, \otimes, \oplus, \&\};$

$\mu^0 x.G \in \mathcal{SC}(F) \implies \mathbf{0} \in \mathcal{SC}(F);$

$\nu^0 x.G \in \mathcal{SC}(F) \implies \top \in \mathcal{SC}(F);$

$\eta^{n+1} x.G \in \mathcal{SC}(F) \implies G(\eta^n x.G/x) \in \mathcal{SC}(F) \text{ for all } n \in \omega \text{ and } \eta \in \{\mu, \nu\};$

$\eta x.G \in \mathcal{SC}(F) \implies \eta^n x.G \in \mathcal{SC}(F) \text{ for all } n \in \omega \text{ and } \eta \in \{\mu, \nu\}.$

Define $F^-$ to be image of $F$ under the forgetful functor that erases the explicit approximations occurring in $F$. For example, $(a \otimes \mu^0 x.\nu y.x \oplus y)^- = a \otimes \mu x.\nu y.x \oplus y$.

**Theorem 48.** *For any formula $F$, the set $\{rk(G) \mid G \in \mathcal{SC}(F)\}$ is a well-order with respect to the $<_{lex}$ ordering.*

**Proof.** By contradiction. Note that $|rk(G)| = |rk(G^-)|$. Furthermore, if $G \in \mathcal{SC}(F)$ then $G^- \in FL(F)$. But $FL(F)$ is a finite set, therefore the set $\{|rk(G)| \mid G \in \mathcal{SC}(F)\}$ is finite.

Assume there exists $\{\sigma_i\}_{i \in I}$ an infinite descending chain in $\{rk(G) \mid G \in \mathcal{SC}(F)\}$. By the Infinite Ramsey Theorem, there is an infinite subsequence $\{\sigma_i\}_{i \in \omega}$ such that for all $j, i_j \in I$ and for all $j, j', |\sigma_{i_j}| = |\sigma_{i_{j'}}| = n$. Then, there exist $k \le n$ and $N \in \mathbb{N}$ such that $\{(\sigma_{i_j})_k\}_{j>N}$ is a descending chain. This contradicts the wellfoundedness of natural numbers. ◀

## 4.1 Soundness and completeness of $\mu$MALL$_{\omega}$

The phase semantics for $\mu$MALL$_{\omega}$ is much simpler to define. Like MALL the semantics can be defined given a phase space and a valuation (without the extra structure over the set of facts and extension of valuations to variables as in $\mu$MALL$^{ind}$). Given a phase space $\mathcal{M}$ and a valuation function $V: \mathcal{A} \to \mathcal{X}$, we define the interpretation of multiplicative-additive connectives and units as usual, of $\mu x.F$ and $\nu x.F$ as in Equation (2), and of $\eta^n x.F$ (for $\eta \in \{\mu, \nu\}$) as follows: $[[\mu^0 x.F]] = [[\mathbf{0}}]$, $[[\nu^0 x.F]] = [[\top}}$, and $[[\eta^{n+1} x.F]] = [[F(\eta^n x.F/x)]]$.

**Theorem 49 ($\mu$MALL$_{\omega}$ soundness).** If $\Gamma \vdash \Gamma$ then for all phase models $(\mathcal{M}, V)$, $1 \in [[\Gamma]]^V$.

The proof of Theorem 49 is by a straightforward induction on the structure of the proof.

**Lemma 50 (Adequation Lemma for $\mu$MALL$_{\omega}$).** For all formula $F$, $[[F]]^V \subseteq \text{Pr}_{cf}(F)$.

**Proof.** By induction on $rk(F)$. The base case is when $F$ is an atom or a unit in which case by definition $[[F]] = \text{Pr}_{cf}(F)$. Suppose $F = G \odot H$ for $\odot \in \{\ominus, \oplus, \&\}$. By Theorem 46.1, $rk(G) <_{lex} rk(F)$ and $rk(H) <_{lex} rk(F)$. By IH, $[[G]]^V \subseteq \text{Pr}_{cf}(G)$ and $[[H]]^V \subseteq \text{Pr}_{cf}(H)$. Using standard techniques in the proof of Lemma 10 (cf. [30]), we can conclude that $[[F]] = \text{Pr}_{cf}(F)$.

The case $F = \eta^0 x.G$ is trivial. Suppose $F = \eta^{n+1} x.G$ where $\eta \in \{\mu, \nu\}$. By Theorem 46.3, $rk(G(\eta^n x.G)) <_{lex} rk(\eta^{n+1} x.G)$. By IH, $[[F]] = [[G(\eta^n x.G)]]^V \subseteq \text{Pr}_{cf}(G(\eta^n x.G)) \subseteq \text{Pr}_{cf}(F)$.

Suppose $F = \mu x.G$. Noting that $\text{Pr}_{cf}(F)$ is a fact for all $F$, it is enough to show that $\bigcup_{n \ge 0} [[\mu^n x.G]] \subseteq \text{Pr}_{cf}(\mu x.G)$. By Theorem 46.4, $rk(\mu^n x.G) <_{lex} rk(F)$. By IH, for all $n$, $[[\mu^n x.G]] \subseteq \text{Pr}_{cf}(\mu^n x.G)$. Observe that $\text{Pr}_{cf}(\mu^n x.G) \subseteq \text{Pr}_{cf}(\mu x.G)$ for all $n$. Therefore, $\bigcup_{n \ge 0} \text{Pr}_{cf}(\mu^n x.G) \subseteq \text{Pr}_{cf}(\mu x.G)$. The case for $F = \nu x.G$ works similarly. ◀
**Theorem 51** ($\mu$MALL$_\omega$ cut-free completeness). If for any phase model $(\mathcal{M}, V)$, $1 \in [[\Gamma]]^V$ then $\mu$MALL$_\omega \vdash_{cf} \Gamma$.

**Corollary 52.** $\mu$MALL$_\omega$ admits cuts.

Standard cut-elimination techniques for Tait-like systems employ techniques from Schütte [45] where proofs are assigned a cut rank. One shows that if there is a proof $\pi$ of a sequent $\vdash \Gamma$ with cut-rank $rk(\pi) > 0$ then there is a proof $\pi'$ of $\vdash \Gamma$ such that $rk(\pi') = 0$ (possibly incurring a blowup in the size of the proof). Cut-admissibility has been proved previously for Tait-style systems of fixpoints logics in [43, 14] using this technique. Semantic proofs of cut-admissibility have been explored in various logics [46, 39, 4] but, to our knowledge, this is the first semantic proof of cut-admissibility in a Tait-style system.

## 4.2 Finite model property

In this subsection, we show that $\mu$MALL$_\omega$ does not have the finite model property. Since MALL has finite model property, this implies that $\mu$MALL$_\omega$ cannot be embedded in MALL.

**Lemma 53.** $\vdash \Gamma_0$ is not provable in $\mu$MALL$_\omega$.

*Proof.* A proof can be found in Appendix B.2.2.

**Corollary 54.** $\mu$MALL$_\omega$ does not prove the same theorems as $\mu$MALL$^{ind}$.

*Proof.* From Example 23 obtain $\mu$MALL$^{ind} \vdash \Gamma_0$. The result now follows from Lemma 53.

**Theorem 55.** $\mu$MALL$_\omega$ does not have finite model property.

*Proof.* The proof goes by contradiction. A finite phase model $(\mathcal{M}, V)$ has finitely many facts. Therefore, by pigeonhole principle, there exists $p, q$ such that $p < q$ and $[[a^p \frown 0]]^V = [[a^q \frown 0]]^V$. Therefore, $[[\mu x.a \frown x]]^V = [[a^p \frown 0]]^V$. Consequently, $1 \in [[H]]^V$ where $H = (\mu x.a \frown x)^{\perp} \frown (a^{\perp p} \frown 0)$. By Theorem 51, $\mu$MALL$_\omega \vdash H$. In Example 42, we show that $\mu$MALL$_\omega \vdash \Gamma_0, H^\perp$. By an application of the cut-rule, we have $\mu$MALL$_\omega \vdash \Gamma_0$ is provable. This is a contradiction by Lemma 53.

# 5 Conclusion

In this work, we provided a sound and complete provability semantics for linear logic with fixpoints ($\mu$MALL) for the proof system with explicit induction due to Baelde and Miller [5, 7]. The completeness proof goes via an adaptation of Tait-Girard reducibility candidates. We then introduced a Tait-style proof system where fixpoints are approximated by their $\omega$-th approximants ($\mu$MALL$_\omega$) and we get a direct proof of completeness. Finally, we show that $\mu$MALL$_\omega$ does not have finite model property and hence is a logic with non-trivial expressivity. We conclude by mentioning pertinent directions for future work.

- Exploring the phase semantics of $\mu$MALL$^\circ$ and $\mu$MALL$^\infty$, circular and non-wellfounded systems for $\mu$MALL respectively [6, 23], are relevant questions especially because that would help settle the Brotherston-Simpson conjecture by semantic techniques. If the conjecture is true, then it suffices to show that $\mu$MALL$^\circ$ is sound with respect to $\mu$-phase models. If the conjecture is false, there are two possibilities for using phase semantics. Firstly, if we have a $\mu$MALL$^\circ$ theorem $F$ which we wish to prove is not a $\mu$MALL$^{ind}$ theorem, then we can use the $\mu$-phase model. Secondly, if one can devise the phase semantics of $\mu$MALL$^\circ$, then the proof is reduced to checking that the space of $\mu$-phase models and its counterpart for $\mu$MALL$^\circ$ are the same.
■ The computation of closure ordinals in phase semantics seems quite difficult and deserves a closer study. An important problem is to compute an upper bound possibly by embedding $\mu\text{MALL}^{\text{ind}}$ in some arithmetic theory.

■ Techniques involving cut ranks used to obtain cut-admissibility also provide upper bounds on the size of the cut-free proof. It would be interesting to see if Theorem 51 can be refined to obtain such bounds.

■ $\mu\text{MALL}^{\text{ind}}$ has the focusing property [7] but assigning polarities to fixed point operators is not a priori clear. In fact, it holds for both possible assignments (the proofs being quite different). In the implicit case, one can syntactically argue that $\mu$ has to be positive (consequently $\nu$ should be negative). Categorical semantics of polarised $\mu\text{MALL}^{\text{ind}}$ informs us that $\mu$ should indeed be positive [25]. Can phase semantics also shed light on the polarisation of fixed points?

■ We showed that $\mu\text{MALL}^{\text{ind}} \not\subseteq \mu\text{MALL}_{\omega}$. Noting that the Park's rule can be simulated with the $(\nu_{\omega})$ rule, we conjecture that $\mu\text{MALL}_{\omega} \not\subseteq \mu\text{MALL}^{\text{ind}}$. Moreover, $\mu\text{MALL}^{\text{ind}}$ can encode the provability of linear logic exponentials but this is not clear for $\mu\text{MALL}_{\omega}$. We conjecture that $\mu\text{MALL}_{\omega}$ cannot simulate *digging*, but it can, indeed, encode *soft promotion* and *multiplexing*, thereby being at least as powerful as soft linear logic [37].

References

1. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, *Handbook of Mathematical Logic*, volume 90 of *Studies in Logic and the Foundations of Mathematics*, pages 739–782. Elsevier, 1977.

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

3. Alfred V. Aho and Jeffrey D. Ullman. Universality of data retrieval languages. In *Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages*, POPL '79, pages 110–119, New York, NY, USA, 1979. Association for Computing Machinery. doi:10.1145/567752.567763.

4. Jeremy Avigad. Algebraic proofs of cut elimination. *The Journal of Logic and Algebraic Programming*, 49(1):15–30, 2001. doi:10.1016/S1567-8326(01)00009-1.

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

6. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In *25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 – September 1, 2016, Marseille, France*, volume 62 of *LIPIcs*, pages 42:1–42:17. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2016. doi:10.4230/LIPIcs.CSL.2016.42.

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

8. Stefano Berardi and Makoto Tatsuta. Classical system of martin-lof's inductive definitions is not equivalent to cyclic proof system. In *FoSSaCS*, volume 10203 of *Lecture Notes in Computer Science*, pages 301–317, 2017.

9. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In *LICS*, pages 1–12. IEEE Computer Society, 2017.

10. Stefano Berardi and Makoto Tatsuta. Classical system of martin-lof's inductive definitions is not equivalent to cyclic proofs. *Log. Methods Comput. Sci.*, 15(3), 2019.

11. James Brotherston. *Sequent Calculus Proof Systems for Inductive Definitions*. PhD thesis, University of Edinburgh, November 2006.
12 James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In *22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)*, pages 51–62. IEEE, 2007.

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

14 Kai Brünnler and Thomas Studer. Syntactic cut-elimination for a fragment of the modal mu-calculus. *Annals of Pure and Applied Logic*, 163(12):1838–1853, 2012. doi:10.1016/j.apal.2012.04.006.

15 Rudolf Carnap. *Logical Syntax of Language*. Kegan Paul, Trench and Truber, 1937.

16 Edmund M Clarke, Orna Grumberg, and Doron A. Peled. Model checking for the μ-calculus. In *Model checking*, chapter 7, pages 97–108. MIT Press, London, Cambridge, 1999.

17 Patrick Cousot and Radhia Cousot. Constructive versions of Tarski's fixed point theorems. *Pacific Journal of Mathematics*, 82(1):43–57, 1979.

18 Marek Czarnecki. How fast can the fixpoints in modal mu-calculus be reached? In Luigi Santocanale, editor, *7th Workshop on Fixed Points in Computer Science, FICS 2010, Brno, Czech Republic, August 21-22, 2010*, pages 35–39. Laboratoire d’Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=36.

19 Ugo Dal Lago and Simone Martini. Phase semantics and decidability of elementary affine logic. *Theoretical Computer Science*, 318(3):409–433, 2004. doi:10.1016/j.tcs.2004.02.037.

20 Anupam Das, Abhishek De, and Alexis Saurin. Decision problems for linear logic with least and greatest fixed points. In *FSCD*, volume 228 of *LIPIcs*, pages 20:1–20:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022.

21 Anuj Dawar and Yuri Gurevich. Fixed Point Logics. *Bulletin of Symbolic Logic*, 8(1):65–88, 2002. doi:10.2178/bsl/1182353853.

22 Pierre Simon de Fermat. *Oeuvres de Fermats, T.2*. Gauthier-Villars et Fils, Paris, 1894.

23 Amina Doumane. *On the infinitary proof theory of logics with fixed points*. (Théorie de la démonstration infinitaire pour les logiques à points fixes). PhD thesis, Paris Diderot University, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01676953.

24 Thomas Ehrhard and Farzad Jafarrahmani. Categorical models of linear logic with fixed points of formulas. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–13, 2021. doi:10.1109/LICS52264.2021.9470664.

25 Thomas Ehrhard, Farzad Jafarrahmani, and Alexis Saurin. Polarized linear logic with fixpoints (technical report). URL: https://drive.google.com/file/d/1eQd5evwcUXYBT5f-TZbs8o4eIE4PhN9m/view?usp=sharing.

26 Thomas Ehrhard, Farzad Jafarrahmani, and Alexis Saurin. On relation between totality semantic and syntactic validity. In *5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)*, Rome (virtual), Italy, June 2021. URL: https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271408.

27 Euclid. *The Elements of Euclid*. Dover Publications Inc., New York, 2nd edition, 1956. URL: https://archive.org/details/euclid_heath_2nd_ed.

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

29 J. Y. Girard. Une extension de l'interpretation de Godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. *Proceedings of the second Scandinavian logic symposium*, 63:63–92, 1971.

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

31 Maria João Gouveia and Luigi Santocanale. Aleph1 and the Modal mu-Calculus. In Valentin Goranko and Mads Dam, editors, *26th EACSL Annual Conference on Computer Science Logic*
(CSL 2017), volume 82 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 38:1–38:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPIcs.CSL.2017.38.

32 Gerhard Jäger, Mathis Kretz, and Thomas Studer. Canonical completeness of infinitary μ-logic. In *The Journal of Logic and Algebraic Programming*, 76(2):270–292, 2008. Logic and Information: From Logic to Constructive Reasoning. doi:10.1016/j.jlap.2008.02.005.

33 Bronislaw Knaster and Alfred Tarski. Un théorème sur les fonctions d'ensembles. *Annales de la Société Polonaise de Mathématique*, 6:133–134, 1927.

34 Dexter Kozen. Results on the propositional μ-calculus. *Theoretical Computer Science*, 27(3):333–354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. doi:10.1016/0304-3975(82)90125-6.

35 Dexter Kozen. A finite model theorem for the propositional μ-calculus. *Studia Logica*, 47(3):233–241, September 1988. doi:10.1007/BF00370554.

36 Yves Lafont. The finite model property for various fragments of linear logic. *The Journal of Symbolic Logic*, 62(4):1202–1208, 1997. URL: http://www.jstor.org/stable/2275637.

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

38 Leonid Libkin. *Elements of Finite Model Theory*. Springer, August 2004.

39 Shoji Maehara. Lattice-valued representation of the cut-elimination theorem. *Tsukuba journal of mathematics*, 15:509–521, 1991.

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

41 Grigori Mints. Finite investigations of transfinite derivations. *Journal of Soviet Mathematics*, 10:548–596, 1978.

42 Mitsuhiro Okada. Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. *Theoretical Computer Science*, 227(1):333–396, 1999. doi:10.1016/S0304-3975(99)00058-4.

43 Ewa Palka. An infinitary sequent system for the equational theory of *-continuous action lattices. Fundam. Inf.*, 78(2):295–309, April 2007.

44 Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, *Foundations of Software Science and Computation Structures*, volume 2303 of *Lecture Notes in Computer Science*, pages 357–371. Springer, 2002. doi:10.1007/3-540-45931-6_25.

45 Kurt Schütte. *Vollständige Systeme modaler und intuitionistischer Logik*. Springer Berlin Heidelberg, 1968. doi:10.1007/978-3-642-88664-5.

46 Kurt Schütte. Syntactical and semantical properties of simple type theory. *The Journal of Symbolic Logic*, 25(4):305–326, 1960. URL: http://www.jstor.org/stable/2963525.

47 Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In *FoSSaCS*, volume 10203 of *Lecture Notes in Computer Science*, pages 283–300, 2017.

48 William W. Tait. A realizability interpretation of the theory of species. In Rohit Parikh, editor, *Logic Colloquium*, pages 240–251, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg.

49 Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. *Pacific Journal of Mathematics*, 5:285–309, 1955.

50 Igor Walukiewicz. *A complete deductive system for the μ-calculus*. PhD thesis, Warsaw University, 1994.

51 Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. In *LICS 95, San Diego, California, USA, June 26-29, 1995*, pages 14–24, 1995.
## A Summary of $\mu$MALL systems used in the paper

$\mu$MALL preformulas:

$$F, G ::= \mathbf{0} | \top | \bot | \mathbf{1} | a | a^{\perp} | F \otimes G | F \otimes G | F \oplus G | F \& G \\ | x | \mu x.F | \nu x.F$$

$\mu$MALL$^{approx}$, preformulas with fixed-point approximants:

$$F, G ::= \mathbf{0} | \top | \bot | \mathbf{1} | a | a^{\perp} | F \otimes G | F \otimes G | F \oplus G | F \& G \\ | x | \mu x.F | \nu x.F | \mu^n x.F | \nu^n x.F \quad n \in \mathbb{N}$$

<table><thead><tr><th></th><th>Formula language</th><th>Inference rules</th><th>Proof trees</th></tr></thead><tbody><tr><td>$\mu$MALL<sup>ind</sup></td><td>$\mu$MALL</td><td>Definition 22</td><td>finite</td></tr><tr><td>$\mu$MALL<sub>ω</sub></td><td>$\mu$MALL<sup>approx</sup></td><td>Definition 41</td><td>wellfounded infinitely branching</td></tr><tr><td>$\mu$MALL<sup>∞</sup></td><td>$\mu$MALL</td><td>Figure 1 of [6]</td><td>non-wellfounded finitely branching</td></tr><tr><td>$\mu$MALL<sup>&</sup></td><td>$\mu$MALL</td><td>Figure 1 of [6]</td><td>non-wellfounded regular</td></tr></tbody></table>

► **Remark.** Note that, contrary to the convention used in the present paper, in [6] notation $\mu$MALL$_ω$ is used to refer to the circular proof system (that is regular non-wellfounded trees).

## B Detailed proofs and clarifications

### B.1 Proofs of Section 3

#### B.1.1 Proof of Lemma 27

Before we prove the lemma, we will prove the following claim.

▷ Claim 56. If $S, T, U, V$ are subsets of $M$ such that $S \subseteq T$ and $U \subseteq V$ then $SU \subseteq TV$.

**Proof.** Suppose $x = su \in SU$ such that $s \in S$ and $u \in U$. Then, $s \in T$ and $u \in V$. Hence $x = st \in TV$. △

**Proof.** By induction on $F$. The base case is when $F$ is an atom, a variable, or a unit which are trivial.

- Suppose $F = p \in A \cup \{\perp, \mathbf{1}, 0, \top\}$. Then, $[[F]]^{V[x \mapsto X]} = [[F]]^{V[x \mapsto Y]} = V(p)$.

- Suppose $F = y \in V$. There are two cases. If $y \neq x$, then $[[F]]^{V[x \mapsto X]} = [[F]]^{V[x \mapsto Y]} = V(y)$. Otherwise, we have $[[F]]^{V[x \mapsto X]} = X \subseteq Y = [[F]]^{V[x \mapsto Y]}$.

There are several subcases for the induction case.

- Suppose $F = G \otimes G'$.

$$ \begin{align*} & [[G]]^{V[x \mapsto X]} \subseteq [[G]]^{V[x \mapsto Y]}; [[G')]^{V[x \mapsto X]} \subseteq [[G')]^{V[x \mapsto Y]} && \text{[By IH]} \\ \Rightarrow & [[G]]^{V[x \mapsto X]} [[G')]^{V[x \mapsto X]} \subseteq [[G]]^{V[x \mapsto Y]} [[G')]^{V[x \mapsto Y]} && \text{[By Claim 56]} \\ \Rightarrow & ([[G]]^{V[x \mapsto X]} [[G')]^{V[x \mapsto X]})^{\perp\perp} \subseteq ([[G]]^{V[x \mapsto Y]} [[G']])^{V[x \mapsto Y]}^{\perp\perp} && \text{[By Proposition 4]} \\ \Rightarrow & [[F]]^{V[x \mapsto X]} \subseteq [[F]]^{V[x \mapsto Y]} \end{align*} $$
Suppose $F = G \prec G'$.

$$
\begin{align*}
& [\! [G]^V[x \to X] \subseteq [\! [G]^V[x \to Y]]; [\! [G']^V[x \to X] \subseteq [\! [G']^V[x \to Y]] \tag*{[By IH]} \\
& \Rightarrow ([\! [G]^V[x \to Y]]^\perp \subseteq ([\! [G]^V[x \to X]]^\perp; ([\! [G']^V[x \to Y]]^\perp \subseteq ([\! [G']^V[x \to X]]^\perp) \tag*{[By Proposition 4]} \\
& \Rightarrow ([\! [G]^V[x \to Y]]^\perp \oplus ([\! [G']^V[x \to Y]]^\perp \subseteq ([\! [G]^V[x \to X]]^\perp \oplus ([\! [G']^V[x \to X]]^\perp) \tag*{[By Claim 56]} \\
& \Rightarrow (([\! [G]^V[x \to X]]^\perp \oplus ([\! [G']^V[x \to X]]^\perp))^\perp \subseteq (([\! [G]^V[x \to Y]]^\perp \oplus ([\! [G']^V[x \to Y]]^\perp))^\perp \tag*{[By Proposition 4]} \\
& \Rightarrow [\! [F]^V[x \to X] \subseteq [\! [F]^V[x \to Y]]
\end{align*}
$$

Suppose $F = G \& G'$.

$$
\begin{align*}
& [\! [G]^V[x \to X] \subseteq [\! [G]^V[x \to Y]]; [\! [G']^V[x \to X] \subseteq [\! [G']^V[x \to Y]] \tag*{[By IH]} \\
& \Rightarrow [\! [G]^V[x \to X] \cap [\! [G']^V[x \to X] \subseteq [\! [G]^V[x \to Y] \cap [\! [G']^V[x \to Y]} \\
& \Rightarrow [\! [F]^V[x \to X] \subseteq [\! [F]^V[x \to Y]]
\end{align*}
$$

Suppose $F = G \oplus G'$.

$$
\begin{align*}
& [\! [G]^V[x \to X] \subseteq [\! [G]^V[x \to Y]; [\! [G']^V[x \to X] \subseteq [\! [G']^V[x \to Y]] \tag*{[By IH]} \\
& \Rightarrow [\! [G]^V[x \to X] \cup [\! [G']^V[x \to X] \subseteq [\! [G]^V[x \to Y] \cup [\! [G']^V[x \to Y]} \\
& \Rightarrow ([\! [G]^V[x \to X] \cup [\! [G']^V[x \to X])^\perp \subseteq ([\! [G]^V[x \to Y] \cup [\! [G']^V[x \to Y])^\perp \tag*{[By Proposition 4]} \\
& \Rightarrow [\! [F]^V[x \to X] \subseteq [\! [F]^V[x \to Y]]
\end{align*}
$$

Suppose $F = \mu y.G$. Observe that $y \neq x$ since we assumed that $x$ is not a bound variable in $F$. Now by hypothesis, for any fact $Z$, $[\! [G]^V[x \to X, y \to Z] \subseteq [\! [G]^V[x \to Y, y \to Z]]$. Therefore for every $Z$ such that $[\! [G]^V[x \to Y, y \to Z] \subseteq Z$ we have $[\! [G]^V[x \to X, y \to Z] \subseteq Z$. Therefore, $\{Z | [\! [G]^V[x \to Y, y \to Z] \subseteq Z\} \subseteq \{Z | [\! [G]^V[x \to X, y \to Z] \subseteq Z\}$. Hence, $\bigcap [\! [G]^V[x \to X, y \to Z] \subseteq Z \{Z\} \subseteq \bigcap [\! [G]^V[x \to Y, y \to Z] \subseteq Z \{Z\}$. We conclude $[\! [F]^V[x \to X] \subseteq [\! [F]^V[x \to Y]$.

Suppose $F = \nu y.G$. As before we comment that $y \neq x$ and therefore by hypothesis, for any fact $Z$, $[\! [G]^V[x \to X, y \to Z] \subseteq [\! [G]^V[x \to Y, y \to Z]$. Therefore for every $Z$ such that $Z \subseteq [\! [G]^V[x \to X, y \to Z]$ we have $Z \subseteq [\! [G]^V[x \to Y, y \to Z]$. Therefore, $\{Z | Z \subseteq [\! [G]^V[x \to X, y \to Z]\} \subseteq \{Z | Z \subseteq [\! [G]^V[x \to Y, y \to Z]\}$. Hence, $\bigcup_{Z \subseteq [\! [G]^V[x \to X, y \to Z]} \{Z\} \subseteq \bigcup_{Z \subseteq [\! [G]^V[x \to Y, y \to Z]} \{Z\}$. Applying Proposition 4 twice, we conclude $[\! [F]^V[x \to X] \subseteq [\! [F]^V[x \to Y]]$. $\quad \blacksquare$

## B.1.2 Proof of Theorem 28

**Proof.** We show it for $\mu f$. First of all, $\{X \mid f(X) \subseteq X\}$ is non-empty since $M^\perp \in \mathcal{D}$. First, we show that it is indeed a fixpoint. Observe that $\mu_f \subseteq X$ for any $X \in \mathcal{D}$ which is a pre-fixpoint of $f$. By Lemma 27, one can apply $f$ on both sides. So $f(\mu f) \subseteq f(X)$ for all $X \in \mathcal{D}$ satisfying $f(X) \subseteq X$ and therefore $f(\mu f) \subseteq \cap_{X \in \mathcal{D}} \{X \mid f(X) \subseteq X\} = \mu f$. So $\mu f$ is a prefixpoint.

But then, since $\mu_f \in \mathcal{D}$, and thanks to the closure properties of $\mathcal{D}$, so is $f(\mu_f)$. By monotonicity of $f$, one gets that $f(f(\mu_f)) \subseteq f(\mu_f)$, ensuring that $f(\mu_f)$ is a prefixpoint of $f$. But $\mu f$ is the least prefixpoint; so, we conclude that $\mu_f \subseteq f(\mu_f)$. Therefore, $\mu_f = f(\mu_f)$. Finally recall $\mu f \subseteq X$ for any pre-fixpoint $X$ in $\mathcal{D}$, so it is the least fixpoint in $\mathcal{D}$. $\quad \blacksquare$

## B.1.3 Proof of Lemma 29

**Proof.** By induction on $F$. The base case is when $F$ is an atom, a variable or a unit.

Suppose $F = a \in \mathcal{A}$. Then, $[\! [F]^\perp]^V = V^\perp(a^\perp) = V(a^\perp) = V(a)^\perp = ([\! [F]^V]^\perp)$.

Suppose $F = x \in \mathcal{V}$. Then, $[\! [F]^\perp]^V = V^\perp(x^\perp) = V(x^\perp) = V(x)^\perp = ([\! [F]^V]^\perp)$.

The case for the units is easy.
There are several subcases for the induction case.

Suppose $F = G \otimes G'$.

$$
\begin{align*}
\llbracket (G \otimes G')^{\perp} \rrbracket^{V^{\perp}} &= \llbracket G^{\perp} \otimes G'^{\perp} \rrbracket^{V^{\perp}} \\
&= ((\llbracket G^{\perp} \rrbracket^{V^{\perp}})^{\perp} ((\llbracket G'^{\perp} \rrbracket^{V^{\perp}})^{\perp}))^{\perp} \tag*{[By IH]} \\
&= (\llbracket G^{\perp \perp} \rrbracket^{V} \llbracket G'^{\perp \perp} \rrbracket^{V})^{\perp} \\
&= (\llbracket G \rrbracket^{V} \llbracket G' \rrbracket^{V})^{\perp} \tag*{[By Proposition 4]} \\
&= (\llbracket (G \otimes G') \rrbracket^{V})^{\perp}
\end{align*}
$$

Negating both sides we have, $((\llbracket G \otimes G' \rrbracket^{\perp})^{V^{\perp}})^{\perp} = ((\llbracket (G \otimes G') \rrbracket^{V})^{\perp \perp})$. Hence, $((\llbracket G^{\perp} \otimes G'^{\perp} \rrbracket^{V^{\perp}})^{\perp} = ((\llbracket G^{\perp} \otimes G'^{\perp} \rrbracket^{V})^{\perp})^{V}$. This takes care of the case when the outermost connective of $F$ is a $\otimes$.

Suppose $F = G' \oplus G'$.

$$
\begin{align*}
\llbracket (G' \oplus G')^{\perp} \rrbracket^{V^{\perp}} &= \llbracket G^{\perp} \& G'^{\perp} \rrbracket^{V^{\perp}} \\
&= \llbracket G^{\perp} \rrbracket^{V^{\perp}} \cap \llbracket G'^{\perp} \rrbracket^{V^{\perp}} \\
&= (\llbracket G \rrbracket^{V})^{\perp} \cap (\llbracket G' \rrbracket^{V})^{\perp} \tag*{[By IH]} \\
&= (\llbracket G \rrbracket^{V} \cup \llbracket G' \rrbracket^{V})^{\perp} \\
&= (\llbracket G \rrbracket^{V} \cup \llbracket G' \rrbracket^{V})^{\perp \perp} \tag*{[By Proposition 4]} \\
&= (\llbracket G \oplus G' \rrbracket^{V})^{\perp}
\end{align*}
$$

As in the previous case, negating both sides, we derive the case when the outermost connective of $F$ is a $\&$.

Suppose $F = \mu x.G$.

$$
\begin{align*}
\llbracket (\mu x.G)^{\perp} \rrbracket^{V^{\perp}} &= \llbracket \nu x.G^{\perp} \rrbracket^{V^{\perp}} \\
&= \left( \bigcup_{X \in \mathcal{D}} \left\{ X \mid X \subseteq \llbracket G^{\perp} \rrbracket^{V^{\perp}[x \mapsto X]} \right\} \right)^{\perp \perp} \\
&= \left( \bigcup_{X \in \mathcal{D}} \left\{ X \mid X \subseteq \llbracket G^{\perp} \rrbracket^{(V[x \mapsto X^{\perp}])^{\perp}} \right\} \right)^{\perp \perp} \\
&= \left( \bigcup_{X \in \mathcal{D}} \left\{ X \mid X \subseteq (\llbracket G \rrbracket^{V[x \mapsto X^{\perp}]})^{\perp} \right\} \right)^{\perp \perp} \tag*{[By IH]} \\
&= \left( \bigcap_{X \in \mathcal{D}} \left\{ X^{\perp} \mid X \subseteq (\llbracket G \rrbracket^{V[x \mapsto X^{\perp}]})^{\perp} \right\} \right)^{\perp} \tag*{[By Proposition 4]} \\
&= \left( \bigcap_{X \in \mathcal{D}} \left\{ X^{\perp} \mid \llbracket G \rrbracket^{V[x \mapsto X^{\perp}]} \subseteq X^{\perp} \right\} \right)^{\perp} \tag*{[By Proposition 4]} \\
&= \left( \bigcap_{X \in \mathcal{D}} \left\{ X \mid \llbracket G \rrbracket^{V[x \mapsto X]} \subseteq X \right\} \right)^{\perp} \tag*{[Closure property of $\mathcal{D}$]} \\
&= (\llbracket \mu x.G \rrbracket^{V})^{\perp}
\end{align*}
$$

As in the previous case, negating both sides, we derive the case when the outermost operator of $F$ is a $\nu$.

<figure><img src="image_8.png" /></figure>
## B.2 Proofs of Section 4

### B.2.1 Proof of Lemma 45

**Proof.** We induct on $|rk(F)|$. The base case is when $|rk(F)| = 1$. Since $x \in \text{fv}(F)$, $F$ cannot be an atom or a unit. Therefore, $F = x$. Plugging $\sigma = \langle \rangle$, we are done. The induction case has several subcases.

Suppose $F = G \odot G'$ where $\odot \in \{\otimes, \ominus, \&\}$, $\oplus$}. We have two cases. Either $x \in \text{fv}(G) \cap \text{fv}(G')$ or $x$ is free in only one of them. Note that $rk(G), rk(G') \leq rk(F)$. Therefore if $x$ is free in them, the induction hypothesis can be fired. In the first case, we have $rk(G(\xi/x)) = rk(\xi) * \sigma_1$ and $rk(G'(\xi/x)) = rk(\xi) * \sigma_2$. Therefore,

$$ 
\begin{align*}
\mathrm{rk}(F(\xi/x)) &= \mathrm{rk}(G(\xi/x) \odot \mathrm{rk}(G'(\xi/x))) \\
&= (\mathrm{rk}(G(\xi/x)) \sqcup \mathrm{rk}(G'(\xi/x))) * \langle 0 \rangle \\
&= ((\mathrm{rk}(\xi) * \sigma_1) \sqcup (\mathrm{rk}(\xi) * \sigma_2)) * \langle 0 \rangle \\
&= \mathrm{rk}(\xi) * (\sigma_1 \sqcup \sigma_2) * \langle 0 \rangle
\end{align*}
$$

Therefore by plugging $\sigma = (\sigma_1 \sqcup \sigma_2) * \langle 0 \rangle$, we are done. In the other case, wlog assume $x \notin \text{fv}(G')$. Therefore, we have $G'(\xi/x) = G'$. Firing the induction hypothesis for $G$, we have $\mathrm{rk}(G(\xi/x)) = \mathrm{rk}(\xi) * \sigma_1$ as before. Therefore,

$$ 
\begin{align*}
\mathrm{rk}(F(\xi/x)) &= \mathrm{rk}(G(\xi/x) \odot \mathrm{rk}(G'(\xi/x))) \\
&= (\mathrm{rk}(G(\xi/x)) \sqcup \mathrm{rk}(G')) * \langle 0 \rangle \\
&= ((\mathrm{rk}(\xi) * \sigma_1) \sqcup \mathrm{rk}(G')) * \langle 0 \rangle \\
&= \mathrm{rk}(\xi) * \sigma_1 * \langle 0 \rangle \qquad [\text{Since } \mathrm{rk}(G') \leq \mathrm{rk}(\xi)]
\end{align*}
$$

Therefore by plugging $\sigma = \sigma_1 * \langle 0 \rangle$, we are done.

Suppose $F = \eta^\beta y.G$ where $\eta \in \{\mu, \nu\}$, $\beta < \omega$, and $y \neq x$. Clearly, $x \in \text{fv}(G)$ and $\mathrm{rk}(G) \leq \mathrm{rk}(F)$. Therefore, by hypothesis, $\mathrm{rk}(G(\xi/x)) = \mathrm{rk}(\xi) * \sigma'$.

$$ 
\begin{align*}
\mathrm{rk}(F(\xi/x)) &= \mathrm{rk}(\eta^\beta y.G(\xi/x)) \\
&= \mathrm{rk}(G(\xi/x)) * \langle \beta \rangle \\
&= (\mathrm{rk}(\xi) * \sigma' * \langle \beta \rangle)
\end{align*}
$$

By plugging $\sigma = \sigma' * \langle \beta \rangle$, we are done. The case $F = \eta y.G$ goes exactly similarly. ▼

### B.2.2 Proof of Lemma 53

**Proof.** We recall that $\Gamma_0 = \mu x.G, a \otimes \nu y.F$ and we will show that this sequent is not provable in $\mu MALL_\omega$. Suppose there is a proof. By Corollary 52, we can assume that this proof is cut-free. Therefore, the only possibilities for the first rule are $(\otimes)$ or one of $\{(\mu_n^\omega)\}_{n \in \omega}$. If it is the former, then the left premisse has to contain $\mu x.G$ since $\vdash a$ cannot be proved. Consequently, the right premisse is $\vdash \nu y.F$. If it were provable, so would be $\vdash \nu^n x.F$ for all $n \in \omega$. It is easy to observe that $\vdash \nu^n x.F$ is not provable for all $n > 0$.
Now suppose the first rule is a $(\mu_n^\omega)$ for some $n \in \omega$. We note that the $(\mu^n)$ rule is invertible. Moreover, the $(\omega)$ rule is also invertible. Therefore, it suffices to show that $\vdash (a^\perp)^n, \mathbf{0}, a \otimes \nu y.F$ is not provable. The only possible rule here is the $(\otimes)$. The only splitting of the context which renders the left premisse provable is one where the right premisse is $\vdash \underbrace{a^\perp, \dots, a^\perp, \mathbf{0}}_{n-1}, \nu y.F$. The only possible rule that can be applied here is the $(\nu^\omega)$ rule. Consider any premisse other than the $\lfloor \frac{n-1}{2} \rfloor$th premisse. Since the number of $a$ and $a^\perp$ are different in it, it is not provable by Example 7. ◀