# Comparing Infinitary Systems for Linear Logic with Fixed Points

Anupam Das, Abhishek De, Alexis Saurin

► To cite this version:

Anupam Das, Abhishek De, Alexis Saurin. Comparing Infinitary Systems for Linear Logic with Fixed Points. FSTTCS 2023 - 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2023, Telangana, India. pp.40:1-40:17, 10.4230/LIPIcs.FSTTCS.2023.40 . hal-04799652

HAL Id: hal-04799652

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

Submitted on 23 Nov 2024

**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
# Comparing Infinitary Systems for Linear Logic with Fixed Points

Anupam Das

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

School of Computer Science, University of Birmingham, UK

Abhishek De

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

School of Computer Science, University of Birmingham, UK

Alexis Saurin

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

IRIF, CNRS, Université Paris Cité, France
INRIA $\pi^3$, Paris, France

## Abstract

Extensions of Girard's *linear logic* by least and greatest fixed point operators ($\mu MALL$) have been an active field of research for almost two decades. Various proof systems are known *viz.* *finitary* and *non-wellfounded*, based on explicit and implicit (co)induction respectively. In this paper, we compare the relative expressivity, at the level of provability, of two complementary infinitary proof systems: finitely branching non-wellfounded proofs ($\mu MALL^\infty$) vs. infinitely branching well-founded proofs ($\mu MALL_{\omega,\infty}$). Our main result is that $\mu MALL^\infty$ is strictly contained in $\mu MALL_{\omega,\infty}$.

For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that yields a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on $\mu MALL^\infty$ provability from $\Pi_1^0$-hard to $\Sigma_1^1$-hard, by encoding a sort of Büchi condition for Minsky machines.

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

**Keywords and phrases** linear logic, fixed points, non-wellfounded proofs, omega-branching proofs, analytical hierarchy

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

**Funding** The first and second authors are supported by a UKRI Future Leaders Fellowship, *Structure vs. Invariants in Proofs*, project reference MR/S035540/1. The third author is partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.

## 1 Introduction

*Fixed point logics* have garnered significant interest from computational logicians over the years. In particular the extension of languages by least and fixed point operators, $\mu$ and $\nu$ respectively, has been comprehensively explored in modal logic [23, 38], arithmetic [22, 31], first-order logic [32, 14, 1], and linear logic [36, 7].

In terms of reasoning, least fixed points allow for *inductive* proof, while greatest fixed points, being dual to least fixed points, allow for *coinductive* proof. Naturally, the corresponding (co)induction proof rules must incorporate an arbitrary (co)invariant, a fundamental barrier to both proof theoretic investigations and (automated) proof search. To this end various alternative proof methods have been proposed, incorporating “infinitary behaviour” at the level of proofs:

- *Infinitary branching* (but wellfounded) systems have origins in the proof theory of arithmetic [10] and have been applied to numerous areas, including the modal $\mu$-calculus [24, 37] and extensions of Kleene algebra [34, 27].

- More recently, *non-wellfounded* (but finitely branching) and *cyclic* proofs have been proposed for (co)inductive reasoning, originating in the modal $\mu$-calculus [33, 2] and applied to theories of arithmetic [8, 9], type systems [26, 12, 11], and linear logic [36, 19, 6].

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

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

43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
(FSTTCS 2023).

Editors: Patricia Bouyer and Srikanth Srinivasan; Article No. 40; pp. 40:1–40:17

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

Leibniz International Proceedings in Informatics
LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 40:2 Comparing Infinitary Systems for Linear Logic with Fixed Points

A natural question to ask is whether all these approaches prove the same theorems or not. In this work, we examine this question in the setting of linear logic, $\mu$MALL. In particular, we compare the non-wellfounded system $\mu$MALL$^\infty$ from [6] with a wellfounded infinitary branching system $\mu$MALL$_{\omega,\infty}$ inspired by [16]. This builds on previous work [13] that focused on comparing the various *finitary* systems for $\mu$MALL. Our main result is that $\mu$MALL$_{\omega,\infty}$ proves strictly more theorems than $\mu$MALL$^\infty$:

**► Theorem 1.** $\mu$MALL$^\infty \subsetneq \mu$MALL$_{\omega,\infty}$

**Organisation and contributions.** In Section 2, we recall the language of $\mu$MALL and present its various systems, in particular $\mu$MALL$^\infty$ and $\mu$MALL$_{\omega,\infty}$. In Section 3 we prove the inclusion part of Theorem 1. Namely, we give a coinductive translation from $\mu$MALL$^\infty$ to $\mu$MALL$_{\omega,\infty}$, and then exploit the correctness condition of $\mu$MALL$^\infty$ to deduce that the image of this translation is wellfounded, Theorem 14. In Section 4 we reduce a “Büchi condition” for Minsky machines to $\mu$MALL$^\infty$ provability, Proposition 32, implying the latter is $\Sigma_1^1$-hard by [3], Theorem 33, yielding the strictness part of Theorem 1. Finally in Section 5 we give a $\Pi_2^1$ upper bound for $\mu$MALL$^\infty$, Theorem 35, by appealing to analytic determinacy of its “proof search game”. We present conclusions in Section 6. Our results are summarised in Figure 1.

**Notation.** For a formula $\varphi$ we write $\varphi^n(x)$ for $\varphi(\varphi(\cdots(\varphi(x))\cdots))$. We shall also frequently suppress or explicitly indicate variables as convenient, e.g. we often identify $\varphi$ and $\varphi(x)$, using the latter when we want to distinguish (some occurrences of) the variable $x$. When working with binders, e.g. $\mu$ and $\nu$, we shall employ a standard convention of using dots, e.g. $\mu x.\varphi$ or $\nu x.\psi$ to signify that the $\mu$ or $\nu$ binds as far as possible to the right.

**A note on (effective) descriptive set theory.** In this work, we shall assume some familiarity with notions from (effective) descriptive set theory, namely the classes of the analytical hierarchy, $\Pi_1^1$, $\Sigma_1^1$, $\Pi_2^1$ etc. All necessary notions can be found in well-known textbooks like [29, 35] and via online resources.

## 2 Background

Linear logic, introduced by Girard [20], refines usual disjunction and conjunction into two orthogonal pairs of connectives: the multiplicatives $\otimes$, $\oplus$ and the additives $\oplus$, $\&$. Together with their units $\perp$, $1$, $0$, $\top$ respectively, the resulting logic MALL ("multiplicative additive linear logic") is given in Figure 2 (colours may be ignored for now). Note here that the rules operate on sequents, which are finite multisets of formulas: commas denote multiset union, and set braces are omitted. Sequents are "one-sided", i.e. $\Gamma$ should be read as $\vdash \Gamma$.

MALL is distinguished from usual logics by its notable absence of structural rules for the multiplicatives: $\varphi\otimes\varphi \vdash \varphi$ and $0\vdash\varphi$ are not always satisfied. This is why sequents must be multisets (or lists), not sets. In a sense linear logic can be seen as a "symmetrisation" of intuitionistic logic, which only controls structural rules on one side of an implication, resulting in a sort of constructive logic that nonetheless enjoys a form of De Morgan duality, hence admitting the one-sided presentation herein.

This lack of structural behaviour is crucially what leads to the high complexity of provability in the presence of "exponentials" in usual linear logic or, in this work, in the presence of fixed points. See [13, Sect. 2] for some further discussion on the peculiarities of linear logic with fixed points compared to other similar logics.
<figure><img src="image_7.png" /><figcaption>Figure 1 Relationships between systems in this work. Solid arrows → denote inclusion, dashed arrows denote conservative extensions, negated arrows ⊢ denote non-inclusion.</figcaption></figure>

In the remainder of this section, we shall introduce the language of (multiplicative additive) linear logic with fixed points, and present the systems investigated in this work.

## 2.1 µMALL preliminaries

Let us fix two disjoint countable sets of propositional constants $\mathcal{A} = \{a, b, \dots\}$ and variables $\mathcal{V} = \{x, y, \dots\}$.

**► Definition 2** ((Pre)-formulas). µMALL pre-formulas are given by the following grammar.

$$ \varphi, \psi ::= \mathbf{0} \mid \mathbf{T} \mid \mathbf{\bot} \mid \mathbf{1} \mid a \mid a^{\perp} \mid x \mid \varphi \circled{\varphi} \mid \varphi \otimes \psi \mid \varphi \oplus \psi \mid \varphi \& \psi \mid \mu x \varphi \mid \nu x \varphi $$

where $a \in \mathcal{A}$, $x \in \mathcal{V}$, and $\mu, \nu$ bind the variable $x$ in $\varphi$. Free and bound variables, and capture-avoiding substitution are defined as usual. The subformula ordering is denoted $\leq$. When a pre-formula is closed (i.e. has no free variable), we simply call it a **formula**.

$\mu x \varphi$ and $\nu x \varphi$ are intended to denote the least and greatest fixed points of the operator $\lambda x \varphi$ in an appropriate semantics (cf., e.g., [16]). $a^{\perp}$ is intended to be the negation of $a$. Note that, since variables have no negated instances, positivity of fixed point operators is implicit and no further condition is required.

Thanks to De Morgan duality in linear logic we may extend negation to all (pre-)formulas as a meta-operation, in the same way as for classical logic:

**► Definition 3.** Negation of a pre-formula $\varphi$, denoted $\varphi^{\perp}$, is the unique involution that satisfies the following.

$$ (\mathbf{0})^{\perp} = \mathbf{T}; \quad (\mathbf{\bot})^{\perp} = \mathbf{1}; \quad a^{\perp} = a; \quad x^{\perp} = x; $$

$$ (\varphi \circled{\varphi})^{\perp} = \varphi^{\perp} \otimes \psi^{\perp}; \quad (\varphi \oplus \psi)^{\perp} = \varphi^{\perp} \& \psi^{\perp}; \quad (\mu x \varphi)^{\perp} = \nu x \varphi^{\perp}. $$

As expected, $\mu$ and $\nu$ are dual to each other; note also that fixed point variables are simply invariant under negation.

The first systems for µMALL, here called µMALL<sup>ind</sup>, incorporate explicit (co)induction rules for the fixed points, inspired by similar developments in other fixed point logics like the µ-calculus [23, 39]. In our one-sided setting, µMALL<sup>ind</sup> is formally the extension of the system MALL in Figure 2 by:

$$ \frac{\Gamma, \varphi(\mu x \varphi)}{\Gamma, \mu x \varphi} \stackrel{(\mu)}{\longrightarrow} \frac{\psi^{\perp}, \varphi(\psi)}{\Gamma, \nu x \varphi} \stackrel{(\text{coind})}{\longrightarrow} \quad (1) $$
40:4 Comparing Infinitary Systems for Linear Logic with Fixed Points

<figure><img src="image_8.png" /><figcaption>Figure 2 Inference rules for MALL, where $i \in \{1, 2\}$. Purple formulas in premiss(es) and conclusion are called auxiliary and principal respectively.</figcaption></figure>

These rules are inspired by the second-order encoding of fixed points: $\nu x\varphi = \exists x((x \not\to \varphi) \otimes \varphi)$. Proofs of $\mu$MALL<sup>ind</sup> are defined as usual, but the system plays little role in this work; we present it only for context. At the level of their rules, the other systems considered in this work will only differ from $\mu$MALL<sup>ind</sup> in their $\nu$-rules, using alternatives for (coind). All systems we consider will have the ($\mu$) rule above (differing from the development in [16]).

## 2.2 Non-wellfounded system $\mu$MALL<sup>∞</sup>

The standard “non-wellfounded” system for $\mu$MALL, here called $\mu$MALL<sup>∞</sup>, was introduced in [6], building on earlier work for the fragment without multiplicatives [36, 19]. It is an adaptation of systems for the modal $\mu$-calculus from [33, 37] to the setting of linear logic.

**► Definition 4 ($\mu$MALL<sup>∞</sup> pre-proofs).** The rules of $\mu$MALL<sup>∞</sup> extend MALL by:

$$ \frac{\Gamma, \varphi(\mu x \varphi)}{\Gamma, \mu x \varphi} (\mu) \qquad \frac{\Gamma, \varphi(\nu x \varphi)}{\Gamma, \nu x \varphi} (\nu) \qquad (2) $$

A pre-proof of $\mu$MALL<sup>∞</sup>, denoted $P, P', \dots$, is a possibly non-wellfounded tree generated from the inference rules of $\mu$MALL<sup>∞</sup>.

Arbitrary non-wellfounded derivations may be fallacious, hence the affectation “pre-” above. Thus bona fide “proofs” must further satisfy a standard correctness criterion from non-wellfounded proof theory. At the same time the progressing criterion distinguishes the two fixed points, which have the same rules in Equation (2).

**► Definition 5 (Ancestry).** A formula occurrence $\varphi$ in the conclusion of a rule instance is a **immediate ancestor** of an occurrence $\psi$ in a premiss if they have the same colour, as typeset in Figure 2 and Equation (2). If $\varphi$ and $\psi$ are in a context $\Gamma, \Gamma_1, \Gamma_2$, we furthermore require that they are the same occurrences in the premiss and the conclusion.

**► Remark 6 (On occurrences in multisets).** Note that, in the definition above, we are implicitly assuming that the data structure of a sequent allows us to distinguish different occurrences of the same formula. This is a standard convention in structural proof theory that avoids low-level peculiarities of working with lists (necessitating additional exchange/permutation rules). To be clear, “sequents-as-multisets” should be construed as a sets of occurrences of formulas, e.g. by assigning a name to each occurrence. This is often made explicit in, e.g., type systems with explicit term annotations, but we gloss over this formality in favour of lightening the exposition.

**► Definition 7 (Threads and proof).** Given a branch $B$ through a pre-proof, a **thread** is a maximal path in the graph of immediate ancestry of $B$. A thread is **progressing** if it has a minimal infinitely often principal formula, called **progress points**, (under $\le$) that is a $\nu$-formula. A pre-proof is a **proof** if each of its infinite branches has a progressing thread.
<figure><img src="image_9.png" /><figcaption>(a) A pre-proof of arbitrary $\Gamma$.</figcaption></figure>

<caption>(b) $\nu$-fairness $\nleftarrow$ progress.</caption>

<caption>(c) A $\mu$MALL$^{\infty}$ proof.</caption>

**Figure 3** Some $\mu$MALL$^{\infty}$ pre-proofs. We use identifiers like “•” to describe infinite proofs in a finite manner. Progressing, non-progressing, and “stable” threads are indicated in green, red, and yellow respectively.

**► Example 8.** In Figure 3 we give several examples of (pre-)proofs. Figure 3a is a pre-proof of an arbitrary sequent $\Gamma$, exemplifying the inconsistency of arbitrary pre-proofs. It is not a proof because the left infinite branch has no progressing thread. Figure 3b is also not a proof, despite its only infinite branch having infinitely many $(\nu)$-steps. This is because the thread indicated in red has the $\mu$-formula $\varphi$ as its minimal infinitely often principal formula, not the $\nu$-formula $\psi$. Note that every other thread is eventually stable on $\psi$ (and hence not progressing). Finally Figure 3c is indeed a $\mu$MALL$^{\infty}$ proof, as its only infinite branch has a progressing thread on $\nu xx$. (It also happens to have a non-progressing red thread on $\mu y \nu z y$.)

In this work we shall make crucial use of a (nontrivial) cut-elimination result for $\mu$MALL$^{\infty}$:

**► Theorem 9** ([6, 5]). Every provable $\mu$MALL$^{\infty}$ sequent has a proof without the (cut) rule.

Finally, we briefly describe an important subsystem of $\mu$MALL$^{\infty}$ where the underlying proof trees are *regular*.

**► Definition 10.** A $\mu$MALL$^{\infty}$ pre-proof is *cyclic* (a.k.a. *regular*) if it has finitely many distinct sub-pre-proofs. $\mu$MALL$^{\circ}$ is the class of formulas with cyclic $\mu$MALL$^{\infty}$.

For instance the pre-proofs Figure 3a and Figure 3c are indeed regular whereas Figure 3b is not since at each iteration of the bullet the sequent has an extra occurrence of $\psi$ (which is thenceforth non-principal). Like $\mu$MALL$^{\text{ind}}$, the circular system $\mu$MALL$^{\circ}$ will not play a significant role in this work.

**► Remark 11** (On exponentials). For the reader familiar with the exponentials of linear logic, it would be reasonable to ask about the expressivity of extensions of $\mu$MALL$^{\text{ind}}$, $\mu$MALL$^{\circ}$, $\mu$MALL$^{\infty}$ by the exponentials $!$, $?$. It turns out that the resulting system is fully conservative over $\mu$MALL$^{\text{ind}}$, $\mu$MALL$^{\circ}$, $\mu$MALL$^{\infty}$ respectively, thanks to the fact that exponentials can be “coded” by fixed point formulas, as noticed by Baelde in [4]. On the other hand, our previous work [13] showed the systems $\mu$MALL$^{\text{ind}}$ and $\mu$MALL$^{\circ}$ are already $\Sigma_1^0$-complete, matching the complexity of full linear logic with exponentials [28].

## 2.3 A well-founded system $\mu$MALL$_{\omega,\infty}$

One of the main points of this work is to compare the non-wellfounded system $\mu$MALL$^{\infty}$ with an orthogonal notion of infinite proof: well-founded but infinitely branching. Such systems are common in proof theory and mathematical logic [10, 30] and have been compared to non-wellfounded systems in other settings [37]. To this end, we consider an “$\omega$-rule” for $\nu$, motivated by continuous models, e.g. the phase semantics of [16].
► **Definition 12.** $\mu\text{MALL}_{\omega,\infty}$ is the extension of MALL by the rules:

$$ \frac{\Gamma, \varphi(\mu x \varphi)}{\Gamma, \mu x \varphi} \quad (\mu) \qquad \frac{\Gamma, \top \quad \Gamma, \varphi(\top) \quad \Gamma, \varphi(\varphi(\top)) \quad \dots \quad \Gamma, \nu x \varphi}{\Gamma, \nu x \varphi} \quad (\omega) \qquad (3) $$

*Proofs of $\mu\text{MALL}_{\omega,\infty}$ are defined as usual: they are well-founded (possibly infinite) trees generated by the rules of $\mu\text{MALL}_{\omega,\infty}$.*

The $(\omega)$ rule is inspired by the inflationary construction of fixed points, $\nu x \varphi = \bigcap_{\alpha \in \text{Ord}} \varphi^{\alpha}(\top)$. It is implicit in $\mu\text{MALL}_{\omega,\infty}$ that the $\nu$ operator is in a sense continuous, closing at ordinal $\omega$, like in the models of phase semantics of [16]. In that work, a similar $\omega$-branching system $\mu\text{MALL}_{\omega,\omega}$ has been proposed for $\mu\text{MALL}$ but it further restricts $\mu$-rules to:

$$ \frac{\Gamma, \varphi^n(\mathbf{0})}{\Gamma, \mu x \varphi} \quad (\mu^n) $$

[16] shows that $\mu\text{MALL}_{\omega,\omega}$ is actually quite weak and does not even contain $\mu\text{MALL}^{\text{ind}}$. Retaining the usual $(\mu)$ rule in $\mu\text{MALL}_{\omega,\infty}$ is rather inspired by the signatures (a.k.a. markings or assignments) from [33, 11, 17]. In this work, we shall see that $\mu\text{MALL}_{\omega,\infty}$ in fact contains all the systems we have presented. In particular, note that, since there is no rule for $\mathbf{0}$ in MALL, we immediately have:

► **Observation 13.** $\mu\text{MALL}_{\omega,\omega} \subseteq \mu\text{MALL}_{\omega,\infty}$

### 3 Inclusion of $\mu\text{MALL}^{\infty}$ in $\mu\text{MALL}_{\omega,\infty}$

In this section, we show one of our main results:

► **Theorem 14** (Simulating infinite height by infinite width). $\mu\text{MALL}^{\infty} \subseteq \mu\text{MALL}_{\omega,\infty}$.

Note in particular the stark contrast with the system $\mu\text{MALL}_{\omega,\omega}$ from [16], which does not even contain $\mu\text{MALL}^{\text{ind}}$, cf. Figure 1. To prove this result, throughout this section we work only with cut-free $\mu\text{MALL}^{\infty}$ proofs, without loss of generality by Theorem 9. Furthermore, to prevent issues with productivity along a coinductive definition, we will employ a standard technique (e.g.[30]) of “bootstrapping” our $\mu\text{MALL}$ systems with an explicit repetition rule $\frac{\Gamma}{\Gamma} (=)^{1}$. While this does affect the notion of pre-proof it does not affect the notion of proof in $\mu\text{MALL}^{\infty}$: the progressing condition implies that no infinite branch can have a tail of repetitions, and so $(=)$ steps can be contracted while preserving closedness (each sequent still concludes a step).

#### 3.1 Projections

In order to prove Theorem 14 we first need to define notion of “proof projection” that allows us to extract from a $\mu\text{MALL}^{\infty}$ proof its “finite approximations”. Throughout this section we will consider sequents $\Gamma = \Gamma(\psi_1, \dots, \psi_k)$ where some occurrences of $\psi_1, \dots, \psi_k$ in $\Gamma$ are distinguished. Note that the distinguished occurrences of, say $\psi_i$, may include some, none,

<footnote n="1">¹ Note that this addition could be avoided by using “explicit” approximants à la [37, 16].</footnote>
or all of the occurrences of $\psi_i$ in $\Gamma$. This notation allows for distinguished $\psi_i$ occurrences to be subformulas of formulas in $\Gamma$, and also for some $\psi_i$ and $\psi_j$ to be the same formula when $i \neq j$. For $\vec{\psi} = (\nu x_1 \varphi_1, \dots, \nu x_k \varphi_k)$, an **assignment** is simply a list $\vec{n} = (n_1, \dots, n_k) \in \omega^k$. We will write $\vec{\psi}^{\vec{n}} := (\varphi_1^{n_1}(\top), \dots, \varphi_k^{n_k}(\top))$, the list obtained by assigning each $n_i$ to each $\psi_i$.

**► Definition 15 (Projections).** For a pre-proof $P$ of $\Gamma(\vec{\psi})$, where $\vec{\psi} = (\nu x_1 \varphi_1, \dots, \nu x_k \varphi_k)$, and an assignment $\vec{n} = (n_1, \dots, n_k) \in \omega^k$, we define the **projection** $P(\vec{n})$ a pre-proof of $\Gamma(\vec{\psi}^{\vec{n}})$ by coinduction on $P$ as follows:

1. If $P$ ends with a step $\rho$ for which no distinguished formula occurrence is principal,

$$ \frac{\begin{tikzpicture}[baseline=(current bounding box.center)] \node[draw, shape=circle, inner sep=1pt] (center) at (0,0) {}; \node[left=1pt of center] (left) {}; \node[right=1pt of center] (right) {}; \node[above=1pt of center] (top) {}; \node[below=1pt of center] (bottom) {}; \node[above right=1pt of top] (topright) {}; \node[below right=1pt of bottom] (bottomright) {}; \node[left=1pt of left] (left) {$P_1(\vec{\psi})$} ; \node[right=1pt of right] (right) {$P_m(\vec{\psi})$} ; \node[above=1pt of center] (center) {$\Gamma_1(\vec{\psi})$} ; \node[below=1pt of center] (center) {$\Gamma_m(\vec{\psi})$} ; \node[above right=1pt of top] (top) {$\dots$} ; \node[below right=1pt of bottom] (bottom) {$\Gamma(\vec{\psi})$} ; \end{tikzpicture}}{\Gamma(\vec{\psi})} , \text{ then } P(\vec{n}) := \frac{\begin{tikzpicture}[baseline=(current bounding box.center)] \node[draw, shape=circle, inner sep=1pt] (center) at (0,0) {}; \node[left=1pt of center] (left) {}; \node[right=1pt of center] (right) {}; \node[above=1pt of center] (top) {}; \node[below=1pt of center] (bottom) {}; \node[above right=1pt of top] (topright) {}; \node[below right=1pt of bottom] (bottomright) {}; \node[left=1pt of left] (left) {$P_1(\vec{n})$} ; \node[right=1pt of right] (right) {$P_m(\vec{n})$} ; \node[above=1pt of center] (center) {$\Gamma_1(\vec{\psi}^{\vec{n}})$} ; \node[below=1pt of center] (center) {$\Gamma_m(\vec{\psi}^{\vec{n}})$} ; \node[above right=1pt of top] (top) {$\dots$} ; \node[below right=1pt of bottom] (bottom) {$\Gamma(\vec{\psi}^{\vec{n}})$} ; \end{tikzpicture}}{\Gamma(\vec{\psi}^{\vec{n}})} . $$

2. If $P$ ends with a step for which some distinguished formula occurrence is principal,

$$ \frac{P(0, \vec{n}) := \overline{\Gamma(\top, \vec{\psi}^{\vec{n}})}^{(\top)}}{\varphi(\nu x \varphi, \Gamma(\nu x \varphi, \vec{\psi}))}^{(\nu)} \quad , \text{ then} \quad P(n+1, \vec{n}) := \frac{\varphi(\varphi^{n}(\top)), \Gamma(\nu x \varphi, \vec{\psi})}{\varphi^{n+1}(\top), \Gamma(\varphi^{n+1}(\top), \vec{\psi}^{\vec{n}})}^{(=)} $$

Note that, in the final case of the definition above, the length of the assignment may increase if $\nu x \varphi$ distinguishes multiple occurrences in the sequent. This is why, even though we shall only ever use projections on a single formula later, we must make the definition above more general. This is also a barrier towards any arguments by explicit induction on assignments; e.g. Lemma 16 later is demonstrated rather by an argument by infinite descent, a now standard leitmotif of non-wellfounded proof theory.

## 3.2 Properties of branches along projections

For $\mu$MALL$^\infty$ pre-proofs $P$ we associate to each of its (maximal) branches $B$ its **induced** branch $B(\vec{n})$ in $P(\vec{n})$ in the expected way. Formally $B(\vec{n})$ is defined by coinduction on $B$, following the cases of Definition 15:

$$ \text{1. } \left( \frac{B_i}{\Gamma_i(\vec{\psi})} \right)_{(\vec{n})} := \frac{B_i(\vec{n})}{\Gamma(\vec{\psi}^{\vec{n}})} \quad (\rho) \\ \left( \frac{B'}{\varphi(\nu x \varphi, \Gamma(\nu x \varphi, \vec{\psi}))} \right)_{(\nu)} \quad (0, \vec{n}) \quad := \quad \overline{\Gamma(\top, \vec{\psi}^{\vec{n}})}^{(\top)} $$

$$ \text{2. } \left( \frac{B'}{\varphi(\nu x \varphi, \Gamma(\nu x \varphi, \vec{\psi}))} \right)_{(\nu)} \quad (n+1, \vec{n}) := \frac{B'(n, n+1, \vec{n})}{\varphi(\varphi^{n}(\top)), \Gamma(\varphi^{n+1}(\top), \vec{\psi}^{\vec{n}})} \quad (=) $$

Clearly the map $B \mapsto B(\vec{n})$ from branches of $P$ to branches of $P(\vec{n})$ is surjective. It is also clear that if $B$ is finite then so is $B(\vec{n})$. The remainder of this section is devoted to establishing a stronger property: as long as $B$ is finite or progressing, so is $B(\vec{n})$. To this end we need the following important properties of the action of projections on threads:
**► Lemma 16 (Projections on progressing threads terminate).** For a $\mu$MALL$^\infty$ pre-proof $P$ of $\Gamma(\nu x\varphi, \vec{\psi})$, a branch $B$ of $P$ along which $\nu x\varphi$ extends to a progressing thread, and $n \in \omega$, the branch $B(n, \vec{n})$ is finite.

**Proof sketch.** Suppose otherwise and take the (maximal) sequence $(n_i)_{i<\alpha} \le \omega$ of numbers assigned to the progressing thread $\nu x\varphi$ in the construction of $B(n, \vec{n})$ above. By local inspection notice that $(n_i)_{i<\alpha}$ is monotone non-increasing, and furthermore strictly decreases whenever $\nu x\varphi$ is principal. Thus $\alpha$ must be finite and bounds the length of $B(n, \vec{n})$. ◀

We also have that projections “lower threads” disjoint from their distinguished formulas, by inspection of the description of $B(\vec{n})$ above:

**► Lemma 17 (Projections preserve disjoint threads).** Let $P$ be a pre-proof of $\Gamma(\vec{\psi})$ and $B$ a branch of $P$ with $B(\vec{n})$ infinite. If $B$ is progressing then so is $B(\vec{n})$. Moreover, if $(\varphi_i)_{i<\omega}$ is a progressing thread$^2$ along $B$ disjoint from all $\vec{\psi}$ with progress points $(\varphi_{i_j})_{j<\omega}$, then $(\varphi_i)_{i<\omega}$ is also progressing in $B(\vec{n})$ with progress points $(\varphi_{i_j})_{j<\omega}$.

Note that $B(\vec{n})$ may still be finite when $B$ is infinite in case there is another progressing thread along $B$ on a distinguished formula, cf. Lemma 16. Recalling that the map $B \mapsto B(\vec{n})$ from branches of $P$ to branches of $P(\vec{n})$ is surjective, we have immediately from Lemma 17:

**► Proposition 18 (Projections on proofs are proofs).** If $P$ is a $\mu$MALL$^\infty$ proof, so is $P(\vec{n})$.

### 3.3 The $\omega$-translation

We need to give a translation from $\mu$MALL$^\infty$ proofs to $\mu$MALL$_{\omega,\infty}$ ones. We break this up into two steps: first we give the translation, and then prove that the image of this translation is wellfounded. To this end we shall refer to “pre-proofs” of $\mu$MALL$_{\omega,\infty}$ too, which may be both infinitely wide and infinitely deep.

**► Definition 19 ($\omega$-translation).** For $\mu$MALL$^\infty$ pre-proofs $P$, we define the $\mu$MALL$_{\omega,\infty}$ pre-proof $P^\omega$ by coinduction on $P$ as follows:

1. if $P = \frac{\bigtriangledown_{\Gamma_1}^{P_1} \dots \bigtriangledown_{\Gamma_k}^{P_k}}{\Gamma} (\rho)$ with $\rho \ne \nu$, then $P^\omega := \frac{\bigtriangledown_{\Gamma_1}^{P_1^\omega} \dots \bigtriangledown_{\Gamma_k}^{P_k^\omega}}{\Gamma} (\rho)$ (i.e. $\cdot^\omega$ commutes with $\rho$ when $\rho \ne \nu$).

2. Otherwise, if $P = \frac{\bigtriangledown_{\Gamma, \nu x \varphi}^{P'}}{\Gamma, \nu x \varphi} (\nu)$ then $P^\omega := \frac{\bigtriangledown_{\Gamma, \top}^{P'(0)^\omega} \bigtriangledown_{\Gamma, \varphi(\top)}^{P'(1)^\omega} \dots \bigtriangledown_{\Gamma, \nu x \varphi}^{P'(\omega)^\omega}}{\Gamma, \nu x \varphi} (\omega)$.

Note that, whichever rule $P$ ends with, the translation above is *productive* (it prints a rule for each coinductive case) and so $P^\omega$ is indeed well-defined by coinduction (just like projections and induced branches before). Note also that the translation is defined for arbitrary pre-proofs, not only proofs. Indeed a pre-proof $P$ may be sent to a non-wellfounded pre-proof $P^\omega$ by the translation, e.g. if $P$ has no $(\nu)$ step, then already $P^\omega = P$. In particular, simply having infinitely many $(\nu)$ steps along every infinite branch of $P$ does not suffice to imply wellfoundedness of $P^\omega$. Let us see some examples to illustrate this:

<footnote>$^2$ Recall that $P$ is cut-free, so we may assume the thread starts at the root.</footnote>
**► Example 20** ($\nu$-fairness $\Leftrightarrow$ wellfoundedness of $\cdot^\omega$). Consider the $\mu$MALL$^\infty$ pre-proof in Figure 3b. Recall that this pre-proof is not regular. This irregularity manifests in each branch of its image under the $\omega$ translation:

$$ \frac{\frac{\bullet, \top \frac{\vdots}{\varphi, \top} (\mu)}{\top, \varphi^\top \top} (\gamma)}{\bullet, \varphi^\top (\mu)} \frac{\frac{\bullet, \varphi^\top \frac{\vdots}{\varphi, \varphi^\top \top} (\mu)}{\varphi^\top (\varphi^\top \top)} (\gamma)}{\varphi^\top (\varphi^\top \top)} \dots \frac{\psi (\mu)}{\varphi} $$

**► Example 21.** Consider the $\mu$MALL$^\infty$ proof in Figure 3c. To compute its $\omega$-translation let us first note that:

- When $\varphi(x) = x$ we have that $\varphi^n(\top) = \top$ for all $n < \omega$.

- When $\varphi(z) = \mu y.\nu z.y$ we have $\varphi^n(\top) = \mu y.\nu z.y$ for all $n < \omega$.

From here we can readily compute the $\omega$-translation of Figure 3c as:

$$ \frac{\frac{\left\{ \frac{\overline{\top, \mu y.\nu z.y}^{(\top)}}{\overline{\top, \mu y.\nu z.y}} \right\}^{\omega}}{\overline{\top, \mu y.\nu z.y}}^{(\top)}}{\overline{\top, \mu y.\nu z.y}}^{(\top)} \frac{\left\{ \frac{\left\{ \frac{\overline{\top, \mu y.\nu z.y}^{(\top)}}{\overline{\top, \nu z.\mu y.\nu z.y}} \right\}^{\omega}}{\overline{\top, \mu y.\nu z.y}}^{(\omega)} \right\}^{\omega}}{\overline{\top, \mu y.\nu z.y}}^{(\omega)} \dots \frac{\nu x.x, \mu y.\nu z.y}{\nu x.x, \mu y.\nu z.y} $$

## 3.4 Finiteness of branches in the image of the $\omega$-translation

The above examples notwithstanding, we will indeed show that, as long as $P$ is progressing, $P^\omega$ is actually wellfounded, and so is a $\mu$MALL$_{\omega,\infty}$ proof after all. First we shall classify branches in the image of the $\omega$-translation, just like we did for projections. Note that every branch of $P^\omega$ is induced from a branch of $P$ by choosing, at each $\nu$-step, a corresponding projection given by some $n \in \omega$. Thus, we may specify an arbitrary (possibly non-maximal) branch of $P^\omega$ by the notation $B^{\vec{n}}$, where $B$ is a branch of $P$ and $\vec{n} \in \omega^{\le \omega}$ is some unique (possibly infinite) list of natural numbers, indexing the premisses of $\omega$-steps followed by the branch. Formally $B^{\vec{n}}$ is defined by coinduction on $B$, following Definition 19, with a case analysis on the head of $\vec{n}$ in the case of a $(\nu)$ step:

$$ \left( \frac{B'}{\Gamma, \nu x \varphi} \right)^{\varepsilon} := \Gamma, \nu x \varphi \\ \left( \frac{B'}{\Gamma, \nu x \varphi} \right)^{0\vec{n}} := \overline{\frac{\Gamma, \top}{\Gamma, \nu x \varphi}}^{(\top)} \quad (5) \\ \left( \frac{B'}{\Gamma, \nu x \varphi} \right)^{(n+1)\vec{n}} := \frac{B'(n)\vec{n}}{\Gamma, \nu x \varphi} \quad (\omega) $$
**► Observation 22.** If $B$ is finite, then so is $B^{\vec{n}}$.

This follows by induction on the length of $B$. From here we are able to show:

**► Lemma 23.** For $P$ a pre-proof, $B^{\vec{n}}$ a branch of $P^{\omega}$: if $B$ is progressing then $B^{\vec{n}}$ is finite.

Formally this follows by induction on the height of the first progress point of a progressing thread along $B$, following the definition of branches $B^{\vec{n}}$. During the argument we must often appeal to the properties of branches along projections from Section 3.2. Of course from here our main result immediately follows:

**Proof of Theorem 14.** Let $P$ be a $\mu$MALL$^{\infty}$ proof. By Lemma 23 above, all branches of its $\omega$-translation $P^{\omega}$ are finite. Thus $P^{\omega}$ is indeed wellfounded and so a proof of $\mu$MALL$_{\omega,\infty}$. ◀

## 4 $\mu$MALL$^{\infty}$ is $\Sigma_1^1$-hard

A natural question to ask now is if $\mu$MALL$_{\omega,\infty}$ can be embedded in $\mu$MALL$^{\infty}$.[37] shows that the $\omega$-branching calculus of the modal $\mu$-calculus can be embedded in its corresponding non-wellfounded calculus. The argument crucially depends on the fact that any proof of a formula $\varphi$ has finitely many distinct sequents (modulo identifying approximations); however, such a condition does not hold in $\mu$MALL due to the absence of structural rules. In fact, we prove that the inclusion result of the previous section, Theorem 14, is strict.

In order to do so we will give a $\Sigma_1^1$ lower bound for $\mu$MALL$^{\infty}$ that is incompatible with the natural $\Pi_1^1$ upper bound for $\mu$MALL$_{\omega,\infty}$. To this end, we encode a Büchi' condition for Minsky machines in terms of $\mu$MALL$^{\infty}$ provability. This significantly improves a $\Pi_1^0$ lower bound from previous work [13], which was proved by reduction from non-halting of Minsky machines.

Throughout this section we shall write $a^n$ for $\overbrace{a^\omega \dots \omega a}^n$ (which is equivalent to $a^n(\perp)$).

**► Definition 24.** A Minsky machine $\mathcal{M}$ is a tuple $(Q, r_1, r_2, I)$ where $Q$ is a finite set of states, $r_1, r_2$ are two registers and $I$ is a set of instructions of the form $\text{INC}(p, r_i, q)$ or $\text{JZDEC}(p, r_i, q_0, q_1)$, for $p, q, q_0, q_1 \in Q$ and $i \in \{1, 2\}$, that manipulate the current state and the contents of the registers.

The operational semantics of $\mathcal{M}$ is given by its configuration graph, whose vertices are configurations, of form $\langle q, a, b \rangle \in Q \times \mathbb{N} \times \mathbb{N}$, and whose edges are induced from $I$ by:

$$ \langle p, a, b \rangle \xrightarrow{\text{INC}(p, r_1, q)} \langle q, a + 1, b \rangle $$

$$ \langle p, a, b \rangle \xrightarrow{\text{INC}(p, r_2, q)} \langle q, a, b + 1 \rangle $$

$$ \langle p, 0, b \rangle \xrightarrow{\text{JZDEC}(p, r_1, q_0, q_1)} \langle q_0, 0, b \rangle $$

$$ \langle p, a, 0 \rangle \xrightarrow{\text{JZDEC}(p, r_2, q_0, q_1)} \langle q_0, a, 0 \rangle $$

$$ \langle p, a + 1, b \rangle \xrightarrow{\text{JZDEC}(p, r_1, q_0, q_1)} \langle q_1, a, b \rangle $$

$$ \langle p, a, b + 1 \rangle \xrightarrow{\text{JZDEC}(p, r_2, q_0, q_1)} \langle q_1, a, b \rangle $$

A run is a maximal path in the configuration graph.

**► Theorem 25 ([3]).** Given a Minsky machine $\mathcal{M}$ and a state $q_0$, checking whether there exists an infinite run starting from $\langle q_0, 0, 0 \rangle$ that visits $q_0$ infinitely often is $\Sigma_1^1$-hard.

For the rest of the section, let us fix a Minsky machine $\mathcal{M} = (Q, r_1, r_2, I)$. Construe $\{a, b, z_a, z_b\} \cup Q$ as a set of propositional constants (assuming $\{a, b, z_a, z_b\} \cap Q = \emptyset$) and $\{x, y\}$ as a set of variables. We use $a$ and $z_a$ (respectively, $b$ and $z_b$) to represent the contents of the register $r_1$ (respectively, $r_2$). Define **parity**: $Q \to \{x, y\}$ by $\text{parity}(q) = x$ if $q = q_0$ and $\text{parity}(q) = y$ otherwise. Define the following:
$$[\text{INC}(p, r_1, q)] := p^{\perp} \otimes (q \mathcal{a} a \mathcal{a} \text{parity}(q))$$

$$[\text{INC}(p, r_2, q)] := p^{\perp} \otimes (q \mathcal{a} b \mathcal{a} \text{parity}(q))$$

$$[\text{JZDEC}(p, r_1, q, q')] := p^{\perp} \otimes (((\text{parity}(q)\mathcal{a}q)\&z_a) \oplus (a^{\perp} \otimes (\text{parity}(q')\mathcal{a}q'))$$

$$[\text{JZDEC}(p, r_2, q, q')] := p^{\perp} \otimes (((\text{parity}(q)\mathcal{a}q)\&z_b) \oplus (b^{\perp} \otimes (\text{parity}(q')\mathcal{a}q'))$$

$$\psi := \mu y. \left( \bigoplus_{\text{ins} \in I} [\text{ins}] \right)$$

$$\varphi := \psi(\nu x.\psi)$$

Finally, define $\text{Inv} := ((b^{\perp})^* \otimes z_a^{\perp}) \oplus ((a^{\perp})^* \otimes z_b^{\perp})$ where we write $\varphi^* = \mu x.(1 \oplus (\varphi \otimes x))$.

**Proposition 26.** For any $n \in \mathbb{N}$, the sequents $b^n, z_a, \text{Inv}$ and $a^n, z_b, \text{Inv}$ are provable.

Define $\text{CP}: Q \to \{\nu x.\psi, \varphi\}$ such that $\text{CP}(q) = \nu x.\psi$ if $q = q_0$ and $\text{CP}(q) = \varphi$ otherwise.

**Lemma 27 (One step simulation).** Let $\langle p, m, n \rangle$ be a configuration such that $\langle p, m, n \rangle \xrightarrow{\text{ins}} \langle q, m', n' \rangle$, for $\text{ins} \in I$. The following “move” gadget has a finite $\mu\text{MALL}^{\infty}$ derivation:

$$\frac{\text{CP}(q), q, a^{m'}, b^{n'}, \text{Inv}}{\text{CP}(p), p, a^m, b^n, \text{Inv}} (mv_{\text{ins}})$$

Moreover, if $p = q_0$ then $(mv_{\text{ins}})$ has a $(\nu)$ step (for which $\nu x\psi$ is principal, necessarily).

**Lemma 28.** If there exists a run of $\mathcal{M}$ from $q_0$ such that $q_0$ is visited infinitely often, the sequent $\nu x.\psi, q_0, \text{Inv}$ has a $\mu\text{MALL}^{\infty}$ proof.

**Proof sketch.** Let $\mathcal{R}(p_0) = (\langle p_i, m_i, n_i \rangle)_{0 \le i < \omega}$ be an infinite run of $\mathcal{M}$ from $q_0$ (so $p_0 = q_0$). We construct a pre-proof $P(p_0)$ of $\nu x.\psi, q_0, \text{Inv}$ by coinduction on $\mathcal{R}(q_0)$, simply by simulating each step of the run by the one-step “move” gadgets from Lemma 27 (see Figure 4 for a visualisation). We now argue that $P(p_0)$ is progressing, and so is indeed a $\mu\text{MALL}^{\infty}$ proof.

First, observe that $P(p_0)$ has exactly one infinite branch that has infinitely many occurrences of “move” gadgets $(mv_{\text{ins}})$. Furthermore, every time there is a move rule with a conclusion of the form $\text{CP}(q_0), q_0, a^m, b^n, \text{Inv}$, there is a $(\nu)$ step, necessarily on $\text{CP}(q_0) = \nu x\psi$, by Lemma 27. So, since $q_0$ occurs infinitely often in the run, and by cut-freeness, there is an infinite thread $\tau$ along the formulas $\text{CP}(p_i)$ which is infinitely often principal for $\text{CP}(q_0) = \nu x\psi$ (the indicated green thread in Figure 4). Finally, by inspection of the formulas $\text{CP}(p_i)$ and the rules of $\mu\text{MALL}^{\infty}$, every formula occurring in $\tau$ must have $\nu x\psi$ as a subformula. Thus $\tau$ is indeed progressing, and so $P(p_0)$ is a $\mu\text{MALL}^{\infty}$ proof as required. ◀

## 4.1 Background on focusing

In order to prove the converse of Lemma 28 above, we have to account for all possible proofs. In order to tame the space of possibilities we shall appeal to “focusing”, a standard technique in proof search. Informally, focused proofs are a family of proofs that have more structure than usual sequent calculus proofs.

We first classify the connectives of $\mu\text{MALL}$ by two polarities: **positive** and **negative**. Inferences for negative connectives are *invertible*, i.e. they preserve provability bottom-up, but the positive inferences do not in general. The negative (respectively, positive) connectives of $\mu\text{MALL}^{\infty}$ are $\&$, $\mathcal{a}$, $\perp$, $\top$, $\nu$ (respectively, $\otimes$, $\oplus$, $1$, $0$, $\mu$).$^3$

<footnote>$^3$ Observe that both the $\mu$ and $\nu$ rules are invertible. See [6] for an explanation of the choice.</footnote>
<figure><img src="image_10.png" /><figcaption>Figure 4 Simulation of an infinite run by a $\mu$MALL$^\infty$ proof.</figcaption></figure>

By assigning arbitrary polarities to atomic variables one can extend the notion to formulas in such a way that each formula is either positive or negative, depending on its top-level connective. A sequent is **positive** if it contains *only* positive atomic formulas, otherwise it is **negative**. A **focused proof**, briefly, is one where bottom-up:

- only negative rules are applied on negative sequents; and,

- only positive rules are applied on positive sequents;

- any positive auxiliary formula of a positive rule must be principal for the next step;

Note that the focusing discipline described above ensure that, when reaching a positive sequent, bottom-up, positive rules are “hereditarily applied” on a particular positive formula, called the *focus*, until one reaches a negative sequent again. Importantly we have:

► **Theorem 29** ([6]). If $\Gamma$ has a cut-free $\mu$MALL$^\infty$ proof, it also has one that is focused.<fnref n="4" />

## 4.2 Provability implies run existence

In this subsection we prove the converse of Lemma 28 above:

► **Lemma 30.** If the sequent $v \cdot x \cdot \psi, q_0, \text{Inv}$ is provable in $\mu$MALL$^\infty$, then there exists a run of $\mathcal{M}$ from the configuration $\langle q_0, 0, 0 \rangle$ such that $q_0$ is visited infinitely often.

We shall henceforth assume that all $\mu$MALL$^\infty$ proofs are cut-free, under Theorem 9, and focused, under Theorem 29. More specifically we assign atomic polarities as follows: $a, b, z_a, z_b$ and $q$ are negative for any state $q \in Q$. We first make a simple observation that will aid our proof.

▷ **Claim 31.** $\text{Inv}$ is not principal in the lowest rule of any focused proof of $\psi, p, a^m, b^n, \text{Inv}$.

*Proof.* The sequent $\psi, p, a^m, b^n, \text{Inv}$ is positive so if $\text{Inv}$ is active, then it is the focus. Without loss of generality, assume that the first rule is $(\oplus_1)$ with principal formula $\text{Inv}$. Then, the auxiliary formula is $(b^\perp)^* \otimes z_a$. Since the outermost connective is positive, we must immediately apply the $(\otimes)$ rule. One of the premisses is of the form $\Delta, z_a^\perp$ with $z_a^\perp$ as focus and we cannot apply any inference rule. Because $\Delta$ cannot be $z_a$, the identity rule is ruled out and no other rules are possible since $z_a$ is an atom. △

We can now prove the main result of this subsection:

<footnote n="4">⁴ The focusing result in [6] is for a logic without atoms but the proof technique can be straightforwardly extended to account for atoms.</footnote>
**Proof.** The proof has two parts. We first show that one can carve out an infinite run $\mathcal{R}$ of $\mathcal{M}$ from $\langle q_0, 0, 0 \rangle$ from a focussed proof of $\nu x.\psi, q_0, \text{Inv}$. Then, we show that $q_0$ is visited infinitely often along $\mathcal{R}$.

Let $P$ be a focussed proof of $\nu x.\psi, q_0, \text{Inv}$. We claim that $P$ can be factored as follows where $p_0 = q_0, m_0 = 0$, and $n_0 = 0$.

This factorisation yields the required infinite run $(\langle p_i, m_i, n_i \rangle)_{i \in \omega}$ where for all $i$,

$$ \langle p_i, m_i, n_i \rangle \xrightarrow{\text{ins}_i} \langle p_{i+1}, m_{i+1}, n_{i+1} \rangle. $$

Furthermore, if $P$ is a proof, then there are infinitely many occurrences of $\nu x.\psi$ along this branch but, since $\text{CP}(p_i) = \nu x.\psi$ only when $p_i = q_0$ we obtain that $q_0$ occurs infinitely often in the run. Therefore, we are left to prove that $P$ can be factored as described.

We will give a proof-search argument to show that every pre-proof of $\text{CP}(p), p, a^m, b^n, \text{Inv}$ goes through $\text{CP}(q), q, a^{m'}, b^{n'}, \text{Inv}$ such that $\langle p, m, n \rangle \xrightarrow{\text{ins}} \langle p', m', n' \rangle$ for some instruction $\text{ins}$. If $p = q_0$ and $\text{CP}(p) = \nu x.\psi$ then the unique rule that can be applied is $(\nu)$ to obtain the sequent $\varphi, p, a^m, b^n, \text{Inv}$ (otherwise $\text{CP}(p)$ is anyway $\varphi$). From Claim 31, we get that $\text{Inv}$ cannot be the focus. Therefore, $\varphi$ is the focus and the next rules are necessarily $(\mu)$ and $\oplus$ respectively whence we have the sequent $[\text{ins}], p, a^m, b^n, \text{Inv}$ for some instruction $\text{ins}$. If $\text{ins}$ is not an instruction that can be fired at $p$, proof-search immediately fails. If $\text{ins}$ is an increment, it is trivial to obtain the result. If $\text{ins}$ is a decrement of the form $p^\perp \otimes (((\text{CP}(q)\gtrq q)\&z_a) \oplus (a^\perp \otimes (\text{CP}(q')\gtrq q')))$, we need to make sure that the control goes to the appropriate state depending on whether $r_1$ is zero or not. We will show that an erroneous choice fails proof-search. We have two cases:

**Case 1.** Suppose we have $a^\perp \otimes (\text{CP}(q')\gtrq q'), b^n, \text{Inv}$. Here $a^\perp \otimes (\text{CP}(q')\gtrq q')$ is the focus since in the earlier step $((\text{CP}(q)\gtrq q)\&z_a) \oplus (a^\perp \otimes (\text{CP}(q')\gtrq q'))$ was the focus. Therefore we have sequent of the form $\vdash \Delta, a^\perp$ where $a^\perp$ is the focus and $\Delta$ cannot be $\{a\}$.

**Case 2.** Suppose we have $(\text{CP}(q)\gtrq q)\&z_a, a^m, b^n, \text{Inv}$. This is a negative sequent, so the next rule is necessarily $(\&)$ and we have a premiss of the form $z_a, a^m, b^n, \text{Inv}$ where $\text{Inv}$ is the focus. It is easy to check that for choices $(\oplus_1)$ and $(\oplus_2)$, proof-search fails. $\blacksquare$

Putting Lemmas 28 and 30 together we have:

**Proposition 32 (Reduction).** $\mathcal{M}$ has an infinite run from $q_0$ visiting $q_0$ infinitely often if and only if there is a $\mu\text{MALL}^\infty$ proof of $\nu x.\psi, q_0, \text{Inv}$.

By Theorem 25 we thus have:

**Theorem 33.** $\mu\text{MALL}^\infty$ is $\Sigma_1^1$-hard.

From here, we can conclude strictness of the inclusion from Theorem 14:

**Corollary 34.** $\mu\text{MALL}^\infty$ and $\mu\text{MALL}_{\omega, \infty}$ prove different sets of theorems.

**Proof.** Clearly $\mu\text{MALL}_{\omega, \infty} \in \Pi_1^1$: $\mu\text{MALL}_{\omega, \infty}$ proves $\Gamma$ just if:

"every set of sequents closed under $\mu\text{MALL}_{\omega, \infty}$ rules contains $\Gamma$"

Note here that closure of a set $X$ of sequents under $\mu\text{MALL}_{\omega, \infty}$ is indeed arithmetical; in particular closure under the $(\omega)$-rule is $\Pi_2^0$: "for every sequent $\Gamma, \nu x\varphi$ not in $X$ there exists $n \in \omega$ such that $\Gamma, \varphi^n(\top)$ is not in $X$."

On the other hand, if $\mu\text{MALL}^\infty = \mu\text{MALL}_{\omega, \infty}$ then $\mu\text{MALL}_{\omega, \infty}$ would be $\Sigma_1^1$-hard, by Theorem 33, contradicting its $\Pi_1^1$ membership as $\Sigma_1^1 \not\subseteq \Pi_1^1$. $\blacksquare$

Finally Corollary 34 and Theorem 14 together imply Theorem 1, our main result.
5 A $\Pi_2^1$ upper bound on $\mu\mathrm{MALL}^\infty$

Our $\Sigma_1^1$-hardness result, Theorem 33, places $\mu\mathrm{MALL}^\infty$ definitively in the analytical hierarchy. Previously the best known lower bound was $\Pi_1^0$ from [13]. In terms of upper bounds, a naïve $\Sigma_3^1$ upper bound is readily obtained by the description of $\mu\mathrm{MALL}^\infty$-provability:

"there *exists* a preproof s.t., *for all* infinite branches, there *exists* a progressing thread."

Note here that checking whether a given thread is progressing is indeed arithmetical: "there *exists* some $n \in \mathbb{N}$ and a formula $\nu x \varphi$ that is *infinitely often* principal, and such that *every* formula in the thread after position $n$ has $\nu x \varphi$ as a subformula". In fact we can improve this upper bound considerably, comprising the main result of this section:

► **Theorem 35** ($\exists 0^#$). $\mu\mathrm{MALL}^\infty \in \Pi_2^1$.

Note that this result, strictly speaking, depends on the existence of $0^#$ (as indicated), a
principle independent of ZFC, but over which it is equivalent to lightface analytic determinacy
[21]. To demonstrate this result we employ ideas from proof search, namely game theoretic
formulations therein inspired by previous work [25, 18].

► **Definition 36** (Proof search game, for $\mu\mathrm{MALL}^\infty$). The proof search game for $\mu\mathrm{MALL}^\infty$ is a two-player game played between Prover ($\mathbf{P}$), whose positions are inference steps of $\mu\mathrm{MALL}^\infty$, and Denier ($\mathbf{D}$), whose positions are sequents of $\mu\mathrm{MALL}^\infty$. A play of the game starts from a particular sequent: at each turn, $\mathbf{P}$ chooses an inference step with the current sequent as conclusion, and $\mathbf{D}$ chooses a premiss of that step; the process repeats from this sequent and the two players continue taking turns as long as possible.

$\mathbf{P}$ wins an infinite play of the game if the branch constructed has a progressing thread.<fnref n="5" />

It is not hard to see that winning strategies for $\mathbf{P}$ correspond to non-wellfounded proofs:

► **Observation 37.** *P* has a winning strategy from Γ iff there is a *μMALL*<sup>*∞*</sup> proof of Γ.

When the state space is finite, e.g. for the $\mu$-calculus, the corresponding proof search game is
finite-memory determined, yielding regular completeness of the proof system [33]. We do
not have this property here, but the characterisation above nonetheless allows us to view $\mathbf{D}$
strategies as a form of “semantics” for $\mu\mathrm{MALL}^\infty$ under determinacy:

► **Proposition 38** ($\exists 0^#$). *The proof search game for *μMALL*<sup>*∞*</sup> is determined.*

This is a consequence of (lightface) analytic determinacy, as the winning condition is indeed
$\Sigma_1^1$: "there *exists* a progressing thread". From here we readily obtain our upper bound:

**Proof of Theorem 35.** There is a $\mu\mathrm{MALL}^\infty$ proof of a sequent $\Gamma$ if and only if $\mathbf{P}$ has a winning strategy from $\Gamma$ by Observation 37, if and only if there is no winning strategy for $\mathbf{D}$ from $\Gamma$, by Proposition 38. The latter is clearly a $\Pi_2^1$ property:

"for every D-strategy there *exists* a play for which there *exists* a progressing thread" ◀

<footnote n="5">⁵ In the case of deadlock, the player with no valid move loses.</footnote>
# 6 Conclusion

In this work, we compared the expressivity of the infinitary systems $\mu MALL^{\infty}$ and $\mu MALL_{\omega,\infty}$ for linear logic with fixed points, and improved bounds on their complexity, cf. Figure 1. We conclude this paper with some remarks on potential future directions of research.

- It would be pertinent to extend our comparison to systems with wider branching, indexed by some ordinal $\alpha$, say $\mu MALL_{\alpha,\infty}$. Similar systems were considered in [16, 15]. Such systems become weaker (i.e. have fewer theorems) as $\alpha$ increases, as more cases must be proved to derive a $\nu$ formula. In this sense it would be particularly interesting if we could show that $\mu MALL^{\infty}$ coincides with some $\mu MALL_{\alpha,\infty}$, calibrating the strength of $\mu MALL^{\infty}$ according to some ordinal measure. Let us point out that such an ordinal must be sufficiently large to evade a $\Pi_1^1$ upper bound, as for $\mu MALL_{\omega,\infty}$, due to $\Sigma_1^1$-hardness of $\mu MALL^{\infty}$; at the same time the systems $\mu MALL_{\alpha,\infty}$ must reach a limit by $\alpha = \omega_1$, for cardinality reasons, giving a naïve upper bound.

- It would also be interesting to prove bona fide metalogical properties, such as cut-elimination and focusing, for $\mu MALL_{\omega,\infty}$ (and friends), just like for $\mu MALL^{\infty}$ in [6] and for several other infinitely branching systems in related areas [30, 24, 34]. Let us point out that the embedding of $\mu MALL^{\infty}$ in $\mu MALL_{\omega,\infty}$ of Section 3 does not introduce cuts, arguably evidence that $\mu MALL_{\omega,\infty}$ might enjoy a well-behaved proof theory. We expect such a result to be easier to establish than the analogous results for $\mu MALL^{\infty}$, thanks to the underlying wellfoundedness of $\mu MALL_{\omega,\infty}$.

- What is the exact complexity of $\mu MALL^{\infty}$? This question remains open after this work, but we have significantly narrowed the gap to the range between $\Sigma_1^1$ and $\Pi_2^1$. It would also be pertinent to investigate the complexity of the infinitary wellfounded system $\mu MALL_{\omega,\infty}$ (and $\mu MALL_{\omega,\omega}$ and friends). Let us point out also that the (weaker) $\Pi_1^0$ lower bound for $\mu MALL^{\infty}$ from [13] applied already to the alternation-free fragment of $\mu MALL^{\infty}$.<fnref n="6" /> Our $\Sigma_1^1$ lower bound crucially uses a single alternation to mimic the Büchi condition on Minsky machines. It would be interesting to further investigate the effect of alternation on the complexity of systems we have investigated.

- Can the assumption of lightface analytic determinacy be dropped from Theorem 35? Attempting to do so has been beyond the scope of this work.

# References

1 Bahareh Afshari, Sebastian Enqvist, and Graham E Leigh. Cyclic proofs for the first-order $\mu$-calculus. Logic Journal of the IGPL, page jzac053, August 2022. doi:10.1093/jigpal/jzac053.

2 Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005088.

3 R. Alur and T.A. Henzinger. A really temporal logic. In 30th Annual Symposium on Foundations of Computer Science, pages 164-169, 1989. doi:10.1109/SFCS.1989.63473.

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

<footnote n="6">⁶ “Alternation-free” means that no $\mu$ occurs under a $\nu$ and vice-versa.</footnote>
40:16 Comparing Infinitary Systems for Linear Logic with Fixed Points

5 David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In *LICS '22*, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533375.

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 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.

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

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

11 Gianluca Curzi and Anupam Das. Non-uniform complexity via non-wellfounded proofs. In *Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland*, volume 252 of *LIPIcs*, pages 16:1-16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CSL.2023.16.

12 Anupam Das. On the logical complexity of cyclic arithmetic. *Log. Methods Comput. Sci.*, 16(1), 2020. doi:10.23638/LMCS-16(1:1)2020.

13 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. doi:10.4230/LIPIcs.FSCD.2022.20.

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

15 Abhishek De. *Linear logic with the least and greatest fixed points: truth semantics, complexity, and a parallel syntax*. PhD thesis, Université Paris Cité, 2022. URL: https://www.irif.fr/_media/users/ade/main.pdf.

16 Abhishek De, Farzad Jafarrahmani, and Alexis Saurin. Phase semantics for linear logic with least and greatest fixed points. In Anuj Dawar and Venkatesan Guruswami, editors, *42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India*, volume 250 of *LIPIcs*, pages 35:1-35:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.FSTTCS.2022.35.

17 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.

18 Walter Felscher. Dialogues, strategies, and intuitionistic provability. *Annals of Pure and Applied Logic*, 28(3):217-254, 1985. doi:10.1016/0168-0072(85)90016-8.

19 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.

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

21 Leo Harrington. Analytic determinacy and 0\#'. *The Journal of Symbolic Logic*, 43(4):685-693, 1978. doi:10.2307/2273508.
22 Gerhard Jäger. Fixed points in peano arithmetic with ordinals. *Annals of Pure and Applied Logic*, 60(2):119–132, 1993. doi:10.1016/0168-0072(93)90039-G.

23 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.

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

25 G Kreisel. P. lorenzen. ein dialogisches konstruktwitätskriterium. infinitistic methods, proceedings of the symposium on foundations of mathematics, warsaw, 2–9 september 1959, panstwowe wydawnictwo naukowe, warsaw, and pergamon press, oxford-london-new york-paris, 1961, pp. 193–200. *The Journal of Symbolic Logic*, 32(4):516–516, 1968.

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

27 Stepan Kuznetsov. Complexity of commutative infinitary action logic. In Manuel A. Martins and Igor Sedlár, editors, *Dynamic Logic. New Trends and Applications*, pages 155–169, Cham, 2020. Springer International Publishing.

28 Patrick Lincoln, John C. Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. *Ann. Pure Appl. Log.*, 56(1-3):239–311, 1992. doi:10.1016/0168-0072(92)90075-B.

29 R. Mansfield and G. Weitkamp. *Recursive Aspects of Descriptive Set Theory*. Oxford logic guides. Oxford University Press, 1985. URL: https://books.google.co.uk/books?id=jPzuAAAAMAAJ.

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

31 Michael Möllerfeld. *Generalized inductive definitions: the μ-calculus and Π₂¹-comprehension*. PhD thesis, Westfälische Universität Münster, 2002.

32 Yiannis N Moschovakis. *Elementary Induction on Abstract Structures (Studies in Logic and the Foundations of Mathematics)*. American Elsevier Pub. Co, 1974.

33 Damian Niwinski and Igor Walukiewicz. Games for the mu-calculus. *Theor. Comput. Sci.*, 163(1&2):99–116, 1996. doi:10.1016/0304-3975(95)00136-0.

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

35 Gerald E. Sacks. *Higher Recursion Theory*. Perspectives in Logic. Cambridge University Press, 2017. doi:10.1017/9781316717301.

36 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.

37 Thomas Studer. On the proof theory of the modal μ-calculus. *Stud Logica*, 89(3):343–363, 2008. doi:10.1007/s11225-008-9133-6.

38 M. Y. Vardi. A temporal fixpoint calculus. In *POPL '88*, pages 250–259, New York, NY, USA, 1988. Association for Computing Machinery. doi:10.1145/73560.73582.

39 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.