Cyclic Proof Theory of Generalised Inductive Definitions

Curzi, Gianluca; Melgaard, Lukas

doi:10.4230/LIPIcs.CSL.2026.15

Cyclic Proof Theory of Generalised Inductive Definitions

Gianluca Curzi

Gothenburg University, Sweden Lukas Melgaard

University of Birmingham, UK

Abstract

We study cyclic proof systems for $\mu\mathsf{PA}$ , an extension of Peano arithmetic by generalised inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ by Möllerfeld.

The main result of this paper is that cyclic and inductive $\mu\mathsf{PA}$ have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam’s systems for first-order $\mu$ -calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ , leveraging Möllerfeld’s conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem.

As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and “plain” cyclic proofs for $\mu\mathsf{PA}$ prove the same theorems.

This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson’s Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.

Keywords and phrases:

cyclic proofs, positive inductive definitions, arithmetic, fixed points, proof theory, reset proof systems

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof theory ; Theory of computation

\rightarrow

Higher order logic

Related Version:

Full Version: https://arxiv.org/abs/2507.13057 [13]

Acknowledgements:

We would like to thank Anupam Das for his continuous support, and Graham Leigh for his valuable suggestions during the development of this paper.

Funding:

This work was supported by a UKRI Future Leaders Fellowship, “Structure vs Invariants in Proofs” (project reference MR/S035540/1), by the Wallenberg Academy Fellowship Prolongation project “Taming Jörmungandr: The Logical Foundations of Circularity” (project reference 251080003), and by the VR starting grant “Proofs with Cycles in Computation” (project reference 251088801).

DOI:

10.4230/LIPIcs.CSL.2026.15

Event:

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

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

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

1 Introduction

Non-wellfounded proof theory explores generalized notions of proof that allow for infinite branches, where logical soundness is guaranteed by global specifications such as so-called progressivity conditions. A central concept in this area is that of cyclic (or circular) proofs – non-wellfounded proofs that exhibit a regular tree structure often represented as finite graphs. Compared to more traditional notions of proofs, cyclic proofs are particularly well-suited for formalizing (co)inductive reasoning. In particular, they provide a more “analytic” approach to (co)inductive invariants, which is crucial for the mechanisation of proof search [9, 26, 34, 33]. The modern development of cyclic proofs can be traced back to the work of Niwiński and Walukiewicz [24], who anticipated them in the context of tableau methods for the modal $\mu$ -calculus. The topic was subsequently advanced by Simpson and Brotherston, who initiated the systematic investigation of cyclic proof theory [8, 11].

Progressivity conditions are the most common validity criterions studied in the literature and they represent a quite robust and logic-independent requirement. However, because of their non-local (and non-modular) nature, checking progressivity is in general PSPACE-complete (see, e.g., [5]). More “efficient” alternatives to validity have been explored in [2, 3, 4, 22] with so-called (cyclic) reset proofs, in which sequents can be annotated to keep track of “progress” in a local way. In particular, Sprenger and Dam introduced in [30, 31] a reset system for first-order $\mu$ -calculus where cyclic proofs are decorated with variables ranging over ordinals and equipped with order-theoretic constraints on those ordinals. Their work was later refined by Leigh et al. in [1]. The analysis of the trade-off between progressing and reset conditions has been recently thoroughly conducted in a general, abstract setting by Afshari and Wehr through the connection between Safra automata and reset proofs [20].

One of the primary goals of cyclic proof theory is to study the expressivity of cyclic proofs – for instance, with respect to provability, logical complexity, or proof-theoretic strength – and to compare them with standard, inductive(ly defined) proofs. Because of the non-wellfounded nature of cyclic proofs, this analysis often requires indirect arguments, typically involving formalisation of mathematical principles in first-order or second-order arithmetical theories. In the context of first-order logic with inductive definitions, for example, Berardi and Tatsuta showed that inductive and cyclic proof systems do not prove the same set of theorems [6], and that the equivalence between the two systems can be obtained when these are extended with Peano Arithmetic ( $\mathsf{PA}$ ) [7]. The latter statement was proven by extracting an induction principle from the progressivity condition using (an extension of) Podelski-Rybalchenko termination theorem, and requires formalising infinite Ramsey Theorem within $\mathsf{PA}$ .

Berardi and Tatsuta’s result was implicitly proven by Simpson, who independently showed that the cyclic variant of Peano Arithmetic ( $\mathsf{CA}$ ) is equivalent to $\mathsf{PA}$ [28]. To establish this, he formalised the meta-theory of cyclic proofs in subsystems of second-order arithmetic using some results from reverse mathematics [29].

Simpson’s work was later refined by Das in two directions. First, he showed in [14] that the logical complexity of inductive invariants in $\mathsf{CA}$ is strictly simpler than $\mathsf{PA}$ . Then, in joint work with Melgaard [16], he studied the extension of $\mathsf{PA}$ with arithmetic (finitely iterated) inductive definitions ( $\mathsf{ID}_{<\omega}$ ) and showed that this system and its cyclic version $\mathsf{CID}_{<\omega}$ prove the same arithmetic statements, and so have the same proof-theoretic strength.

This paper continues the line of research initiated by Simpson, by exploring the cyclic proof theory of generalised inductive definitions. Its main focus is $\mu\mathsf{PA}$ , an extension of $\mathsf{PA}$ by least and greatest fixed points of formulas (see [12]). Proof-theoretically, $\mu\mathsf{PA}$ was first studied by Möllerfeld [23], inspired by Lubarsky’s work on “ $\mu$ -definable sets” [21]. The theory was later used by Curzi and Das to characterise the computational expressivity of constructive fixed point logics [12]. Because of the presence of interleaving (or parametric) fixed points, the expressivity of $\mu\mathsf{PA}$ far exceeds that of $\mathsf{ID}_{<\omega}$ . Indeed, Möllerfeld proved that $\mu\mathsf{PA}$ has the same proof-theoretic strength as $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ , an (impredicative) subsystem of second-order arithmetic where the comprehension scheme is restricted to $\Pi^{1}_{2}$ -formulas, one of the strongest theories for which we have an ordinal analysis [25].

The main result of this paper can be stated as follows:

Theorem 1.

Cyclic $\mu\mathsf{PA}$ ( $\mathsf{C}\mu\mathsf{PA}$ ) is arithmetically equivalent to $\mu\mathsf{PA}$ .

Our argument is summarized in Figure 1. We first introduce a reset system for $\mu\mathsf{PA}$ inspired by [1], called $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ . Compared to $\mathsf{C}\mu\mathsf{PA}$ , $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ is defined by a stronger validity condition that allows for a more local and direct soundness proof. Despite being apparently more permissive, cyclic progressing proofs can be duly turned into cyclic reset proofs (Theorem 25). We then adopt Simpson’s method and we formalise the soundness argument for reset proofs within $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ , using some results from reverse mathematics from [12] as well as reflection principles (Theorems 37 and 34). We then conclude by appealing to Möllerfeld’s arithmetic conservativity of $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ over $\mu\mathsf{PA}$ [23]. As a consequence of our proof methods, we also establish the equivalence between progressing-based cyclic proofs and cyclic reset proofs, thus bridging the gap between two major routes to cyclic proof theory in the context of first-order $\mu$ -calculi.

Outline of the paper.

This paper is structured as follows. In Section 2 we recall the syntax and the semantics of $\mu\mathsf{PA}$ , as well as its sequent calculus system. In Section 3 we define the cyclic proof system $\mathsf{C}\mu\mathsf{PA}$ and show that the latter can simulate $\mu\mathsf{PA}$ (Theorem 15). Section 4 introduces the reset system $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ and its soundness theorem (Theorem 21), while Section 5 shows that cyclic progressing proofs of $\mathsf{C}\mu\mathsf{PA}$ can be translated into cyclic reset proofs (Theorem 25). Finally, Section 6 formalises the soundness argument for $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ of Section 4 within $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ (Theorem 37). Full proofs of our results, as well as further discussion and examples, can be found in the extended version of this paper [13].

Figure 1: Diagram illustrating the main results.

Preliminary definitions.

We assume that the reader is familiar with the syntax of sequent calculus (e.g. [27]) as well as basic graph theory. The following two definitions summarise the main notions and notational conventions adopted in this paper.

Definition 2 (Trees).

A (possibly infinite, binary) tree is a non-empty set $T\subseteq\{0,1\}^{<\omega}$ that is prefix-closed, i.e., $b_{1}\ldots b_{n}\in T$ implies $b_{1}\ldots b_{i}\in T$ for all $0\leq i\leq n$ . Elements of the tree are called nodes, which are denoted by $u,v,\ldots$ . A successor of a node $u\in T$ is a node $ub\in T$ for some $b\in\{0,1\}$ . $\varepsilon$ is the root of $T$ and a node with no successor is a leaf. A branch of $T$ is a family $(v_{i})_{i\in\alpha}$ ( $\alpha\leq\omega$ ) such that $v_{0}=\varepsilon$ and $v_{i+1}=v_{i}b$ for some $b\in\{0,1\}$ .

Definition 3 (Rules and (co)derivations).

We consider (inference) rules of the form with $n\in\{0,1,2\}$ , where $\Gamma_{1},\ldots,\Gamma_{n}$ are called premises and $\Gamma$ is called conclusion. A coderivation over a set of rules $X$ is a pair $\mathcal{D}=(T,\ell)$ where $T$ is a tree called the support of $\mathcal{D}$ and $\ell:T\to X$ is a label function such that, whenever $\ell(v)$ is a rule with $n$ premises $\Gamma_{1},\dots,\Gamma_{n}$ , then $v$ has precisely successors $v_{1},\ldots,v_{n}$ and $\ell(v_{i})$ is a rule with conclusion $\Gamma_{i}$ for all $1\leq i\leq n$ . A coderivation with finite support is called a derivation. The conclusion of a (co)derivation is the conclusion of the rule $\ell(\varepsilon)$ . Given some $u\in T_{\mathcal{D}}$ , we write $\mathcal{D}_{u}$ for the (co)derivation with support $T_{\mathcal{D}_{u}}=\{v:uv\in T_{\mathcal{D}}\}$ given by $\ell(v):=\ell(uv)$ . We call such $\mathcal{D}_{u}$ a sub-(co)derivation of $\mathcal{D}$ . If $\mathcal{D}$ has only finitely many sub-coderivations, we call it cyclic (or regular). Cyclic coderivations can be represented as finite graphs.

2 Arithmetical theories of generalised inductive definitions

In what follows, we introduce the theory $\mu\mathsf{PA}$ and its semantics¹¹1This theory is often called $\mu$ -calculus in the literature (see, e.g., [17, 23]). To date, however, $\mu$ -calculi represent a rather diverse family of systems. In this paper we adopt the formulation of the theory from [12], which is referred to as $\mu\mathsf{PA}$ to stress its arithmetic component.. The theory can be constructed as a formal extension of second-order arithmetic by defining least fixed points $\mu Xx\varphi$ as relation symbols, as done in [23]. Instead, we choose to treat them syntactically as “binders” and formulate the theory in a first-order fashion following [12].

2.1 Language of arithmetic with fixed points

The language of $\mu\mathsf{PA}$ , written $\mathcal{L}_{\mu}$ , is an extension of the language of first-order arithmetic (with inequality) $\mathcal{L}_{1}:=\{0,\mathsf{s},+,\times,<\}$ where, as usual, $0$ is a constant symbol (i.e. a $0$ -ary function symbol), $\mathsf{s}$ is a unary function symbol, $+$ and $\times$ are binary function symbols, and $<$ is a binary relation symbol. Specifically, the language of $\mu\mathsf{PA}$ is obtained from $\mathcal{L}_{1}$ by adding countably many set variables ²²2W.l.o.g., in this paper we restrict the language to second-order variables ranging over sets of individuals., written $X, Y$ etc, and fixed point binders $\mu$ and $\nu$ .

Definition 4 (Terms and (pre-)formulas).

The (number) terms, the pre-set terms and the pre-formulas of $\mu\mathsf{PA}$ are respectively simultaneously generated by the following grammars:

\begin{array}[]{rcll}t,s&:=&x\ |\ 0\ |\ \mathsf{s}\,t\ |\ s+t\ |\ s\times t\\[% 8.61108pt] \varphi,\psi&:=&s<t\ |\ s\nless t\ |\ s=t\ |\ s\neq t\ |\ t\in S\ |\ t\notin S% \ |\ \varphi\wedge\psi\ |\ \varphi\vee\psi\ |\ \forall x\varphi\ |\ \exists x% \varphi\\[8.61108pt] S&:=&X\ |\ \mu Xx\varphi\ |\ \nu Xx\varphi\end{array}

The notions of free first-order variable and free second-order variable are standard. Notice that $\nu$ and $\mu$ bind the free (individual and set) variables $X$ and $x$ in $\varphi$ . We denote with $FV_{0}(\varphi)$ , $FV_{0}(t)$ , and $FV_{1}(\varphi)$ the set of free first-order variable in $\varphi$ and $t$ and the set of free second-order variable in $\varphi$ , respectively. We will use the standard notation for (capture-avoiding) first-order and second-order substitution $\varphi[S/X]$ , $\varphi[s/x]$ , and $t[s/x]$ .

Pre-formulas of the form $s<t$ , $s\nless t$ , $s=t$ , $s\neq t$ , $t\in S$ and $t\notin S$ are called atomic. We define negation $\neg\varphi$ as a shorthand using De Morgan equations, e.g., $\neg t\in\mu Xx\varphi(X):=t\in\nu Xx\neg\varphi(\neg X)$ , where $y\in\neg X$ is shorthand for $\neg y\in X$ . Note that $\neg\neg\varphi=\varphi$ .

Given a set variable $X$ , we say that $X$ occurs positively in a pre-formula $\varphi$ if $\varphi$ contains no pre-formulas of the form $t\notin X$ for any term $t$ . We say $\varphi$ is a formula if, for any sub-pre-formula in $\varphi$ of the form $t\in\mu Xx\psi$ or $t\in\nu Xx\psi$ , $X$ occurs positively in $\psi$ . We say a pre-set-term $S$ is a set-term if $t\in S$ is a formula for some $t$ .

From now on, we will work with formulas where every second-order variable is bound. We adopt the standard abbreviations for connectives, such as $\varphi\to\psi:=\neg\varphi\vee\psi$ , and $\varphi\leftrightarrow\psi:=(\varphi\to\psi)\wedge(\psi\to\varphi)$ . Finally, we will write $\varphi(\nu Xx\varphi(X),t)$ for $\varphi[\nu Xx\varphi(X)/X,t/x]$ .

Example 5 (Some fixed point formulas).

Consider the following formulas of $\mathcal{L}_{\mu}$ :

$\blacksquare$

${N}(X,x):=x=0\vee\exists y(y\in X\wedge x=\mathsf{s}y)$
$\blacksquare$

${L}(X,Y,x):=x=\varepsilon\vee\exists z,w(z\in X\wedge w\in Y\wedge x=z::w)$ .

where the term $\varepsilon$ encodes the empty list, and the term $x : : y$ encodes the operation of appending (the encoding of) an element $y$ to (the encoding of) a list $x$ ³³3With a small abuse of notation we will often not distinguish between lists and numbers coding lists in $\mu\mathsf{PA}$ . Moreover, since the append operation is primitive recursive, we will treat $: :$ as a binary function symbol, so $x : : y$ will be considered a term of $\mathcal{L}_{\mu}$ .. By definition, $\mathcal{L}_{\mu}$ contains the set terms $\mathbf{N}:=\mu Xx.N(X,x)$ , $\mathbf{L}(Y):=\mu Xx.L(X,Y,x)$ , and $\mathbf{T}:=\mu Yy.y\in\mathbf{L}(Y)$ . As we will also see later, the latter formula illustrates a key aspect of $\mu\mathsf{PA}$ , the ability to define mutually (co)inductive predicates, thanks to the interdependencies of fixed points.

2.2 Interpreting generalised inductive definitions

We now define the standard model of $\mathcal{L}_{\mu}$ , where $\mu Xx\varphi$ and $\nu Xx\varphi$ are interpreted as least and greatest fixed points of the (parametrised) operator induced by $\varphi$ .

To this end, we recall (a version of) the Knaster-Tarski theorem on power sets:

Proposition 6 (Knaster-Tarski).

Let $S$ be a set and let $f:\mathcal{P}(S)\to\mathcal{P}(S)$ be monotone (w.r.t. $\subseteq$ ). Then $f$ has a least fixed point $\mu f$ and a greatest fixed point $\nu f$ . Moreover:

$\blacksquare$

$\mu f=\bigcap\{A\subseteq S\mid f(A)\subseteq A\}$ and $\nu f=\bigcup\{A\subseteq S\mid A\subseteq f(A)\}$
$\blacksquare$

$\mu f=\bigcup_{\kappa\in\mathrm{Ord}}\mu^{\kappa}f$ and $\nu f=\bigcap_{\kappa\in\mathrm{Ord}}\nu^{\kappa}f$

where the $\kappa$ -approximants $\mu^{\kappa}f$ and $\nu^{\kappa}f$ are inductively defined by $\mu^{\kappa}f=\bigcup_{\lambda<\kappa}f(\mu^{\lambda}f)$ and $\nu^{\kappa}f=\bigcap_{\lambda<\kappa}f(\nu^{\lambda}f)$ . Notice that $\mu^{0}f=\varnothing$ and $\nu^{0}f=S$ .

Definition 7 (Standard model and satisfaction).

The standard model for $\mathcal{L}_{\mu}$ is the $\mathcal{L}_{\mu}$ -structure $\mathfrak{N}$ , whose domain is $\mathbb{N}$ , $0^{\mathfrak{N}}=0$ , $\mathsf{s}^{\mathfrak{N}}$ is the successor, $+^{\mathfrak{N}}$ is the addition, $\times^{\mathfrak{N}}$ is the multiplication, and $<^{\mathfrak{N}}$ is the natural (strict) order on natural numbers.

An assignment is a map $\rho$ associating an element $\rho{(x)}\in|\mathfrak{N}|$ (resp., a set $\rho{(X)}\subseteq\mathfrak{N}$ ) with every first-order variable $x$ (resp., set variable $X$ ). We denote with $\rho[x\mapsto a]$ (resp., $\rho[X\mapsto A]$ ) the assignment that sends $x$ to $a$ (resp., $X$ to $A$ ) and otherwise preserves $\rho$ .

The extension of assignments to terms $t$ , written $\rho(t)$ , and the satisfaction relation $\mathfrak{N},\rho\vDash\varphi$ are defined by induction in the standard way, e.g.:

\begin{array}[]{ll}\mathfrak{N},\rho\vDash t\in\mu Xx\varphi\text{ iff }\rho(t% )\in(\mu Xx\varphi)^{\mathfrak{N}}&\qquad\mathfrak{N},\rho\vDash t\in\nu Xx% \varphi\text{ iff }\rho(t)\in(\nu Xx\varphi)^{\mathfrak{N}}\end{array}

where, given the monotone function $\varphi_{\rho,x,{X}}^{\mathfrak{N}}:A\mapsto\{a\in|\mathfrak{N}|\ |\ \mathfrak% {N},\rho[x,X\mapsto a,A]\vDash\varphi\}$ , we set $(\mu Xx\varphi)^{\mathfrak{N}}:=\mu\varphi_{\rho,x,{X}}^{\mathfrak{N}}$ and $(\nu Xx\varphi)^{\mathfrak{N}}:=\nu\varphi_{\rho,x,{X}}^{\mathfrak{N}}$ (see Proposition 6). We simply write $\varphi^{\mathfrak{N}}$ to denote $\varphi_{\rho,x,{X}}^{\mathfrak{N}}$ when it is clear from the context.

Example 8.

Let $\rho$ be an assignment in $\mathfrak{N}$ . Revisiting Example 5, we have that:
$\begin{array}[]{rclrclrcl}\mu^{0}N^{\mathfrak{N}}&=&\varnothing&\mu^{0}L^{% \mathfrak{N}}&=&\varnothing&\mu^{0}T^{\mathfrak{N}}&=&\varnothing\\ \mu^{1}N^{\mathfrak{N}}&=&\{0\}&\mu^{1}L^{\mathfrak{N}}&=&\{\varepsilon\}&\mu^% {1}T^{\mathfrak{N}}&=&\{\varepsilon\}\\ \mu^{2}N^{\mathfrak{N}}&=&\{0,1\}&\mu^{2}L^{\mathfrak{N}}&=&\rho(Y)^{<1}&\mu^{% 2}T^{\mathfrak{N}}&=&(\mu^{1}T^{\mathfrak{N}})^{<\omega}\\ \mu^{3}N^{\mathfrak{N}}&=&\{0,1,2\}&\mu^{3}L^{\mathfrak{N}}&=&\rho(Y)^{<2}&\mu% ^{3}T^{\mathfrak{N}}&=&(\mu^{2}T^{\mathfrak{N}})^{<\omega}\\ &\vdots&&&\vdots&&&\vdots&\\ \mu^{\omega}N^{\mathfrak{N}}&=&\mu^{\omega+1}N^{\mathfrak{N}}=\mathbb{N}&\mu^{% \omega}L^{\mathfrak{N}}&=&\mu^{\omega+1}L^{\mathfrak{N}}=\rho(Y)^{<\omega}&\mu% ^{\omega}T^{\mathfrak{N}}&=&\mu^{\omega+1}T^{\mathfrak{N}}=\mathrm{HFL}\end{array}$

where the set of lists over $X$ with length at most $n$ (resp. with finite length) is denoted $X^{<n}$ (resp., $X^{<\omega}$ ), and $\mathrm{HFL}$ is the set of (the encodings of) hereditarily finite lists. Therefore, we have: $\mathbf{N}^{\mathfrak{N}}=(\mu Xx.N)^{\mathfrak{N}}=\mu N^{\mathfrak{N}}=% \mathbb{N}$ , $\mathbf{L}(Y)^{\mathfrak{N}}=(\mu Xx.L(X,Y,x))^{\mathfrak{N}}=\mu L^{\mathfrak% {N}}=\rho(Y)^{<\omega}$ , and $\mathbf{T}^{\mathfrak{N}}=(\mu Yy.T(Y,y))^{\mathfrak{N}}=\mu T^{\mathfrak{N}}=% \mathrm{HFL}$ . Alternatively, we can see $\mathbf{T}^{\mathfrak{N}}$ as the set of (the encodings) of rose trees, i.e., trees with unbounded (but finite) branching.

2.3 The theory $\mu\mathsf{PA}$

The theory $\mu\mathsf{PA}$ over the language $\mathcal{L}_{\mu}$ as presented in this paper is essentially the first-order part of Möllerfeld’s $\mathsf{A}{\mathsf{CA}_{0}}(\mathcal{L}_{\mu})$ [23], which extends Peano arithmetic by the axiom schemas $(\mathrm{pre}\text{-}\mu)$ and $(\mathrm{ind}\text{-}\mu)$ defined as follows, for formulas $\psi(x)$ and $\varphi(X,x)$ positive in $X$ :

\begin{array}[]{ll}\forall y(\varphi(\mu Xx\varphi,y)\to y\in\mu Xx\varphi)% \qquad\quad\forall y(\varphi(\psi,y)\to\psi(y))\to\forall y(y\in\mu Xx\varphi% \to\psi(y))\end{array}

and dually for $\nu$ . The first axiom states that $\mu Xx\varphi$ is a pre-fixed point. The second axiom states that it is the least among the pre-fixed points.

We will express $\mu\mathsf{PA}$ in sequent calculus style. In particular, thanks to the dualities of classical logic, we adopt so-called “one-sided” presentation, thus omitting the turnstile symbol “ $\vdash$ ”.

Definition 9 (Sequent calculus for $\mu\mathsf{PA}$ ).

A sequent $\Gamma$ is a list of formulas. The sequent calculus for $\mu\mathsf{PA}$ extends $\mathsf{L}\mathsf{K}_{=}$ (first-order logic with equality) in Figure 2 (top) by:

$\blacksquare$

the axioms of Peano arithmetic, where arithmetic induction is replaced by the rule
$\blacksquare$

the rules $\mu$ and $\mathsf{ind}(\varphi)$ in Figure 2 (bottom).

referring to Figure 2, we call $\Gamma$ , $\Delta$ , $\theta(\Gamma)$ , $\Gamma(t)$ , $\Gamma(s)$ contexts, which are lists of formulas called side formulas. All the other formulas in the conclusion (resp., in a premise) of a rule are called principal formulas (resp., active formulas).

The one-sided sequent calculus streamlines the proofs. However, the more intuitive two-sided system will still be used for examples to facilitate the reading, and so the notation $\Delta\vdash\varphi$ will be considered as shorthand for $\neg\Delta,\varphi$ . As an example, the rule $\mathsf{ind}(\varphi)$ becomes . Also, in the examples, we will omit applications of structural rules as well as some arithmetical rules, and use double lines to abbreviate multiple applications of rules.

Figure 2: Sequent calculus rules for

\mathsf{L}\mathsf{K}_{=}

(first-order logic with equality), where

\theta

is a substitution, i.e. a map from variables to terms, extended to formulas and sequents in the expected way (top figure), and sequent calculus rules for least and greatest fixed points (bottom figure).

$\blacktriangleright$ Remark 10 (Post-fixed points and numerical induction).

It is easy to see that the sequent calculus system $\mu\mathsf{PA}$ derives the axioms ( $\mathrm{pre}$ - $\mu$ ) and ( $\mathrm{ind}$ - $\mu$ ) (as well as their dual for $\nu$ ). On the other hand, the following derivations show that we can recover the rule $\nu$ (Figure 2, bottom) and that, in presence of $\mathsf{ind}(\varphi)$ , numeric induction and the rule $\mathbf{N}$ are equivalent:

In the latter derivation we let $\Gamma=\forall x(\varphi(x)\to\varphi(\mathsf{s}x))$ . Notice that the double lines labelled with $\varphi$ express a “functoriality” property.

In fact, the choice of $\mathbf{N}$ over numerical induction has the only purpose of simplifying the definition of progressing trace in the next section.

3 Cyclic proofs for generalised inductive definitions

In this section we introduce a cyclic version of the theory $\mu\mathsf{PA}$ based on ideas from the modal $\mu$ -calculus [24, 32, 2] and calculi of first-order logic with inductive definitions [8, 10]. Notice that this section borrows notions and notation from Definitions 2 and 3.

3.1 Progressivity and cyclic proofs

We define a notion of non-wellfounded (but finitely branching) proof we call “coderivation”.

Definition 11 (Coderivations).

A ( $\mu\mathsf{PA}$ -)coderivation, is a coderivation over the set of rules extending the rules of $\mathsf{L}\mathsf{K}_{=}$ (Figure 2, top) by:

$\blacksquare$

the axioms of Peano arithmetic, where arithmetic induction is replaced by the rule
$\blacksquare$

the fixed point rules $\mu$ and $\nu$ in Figure 2 (bottom).

Intuitively, ( $\mu\mathsf{PA}$ -)coderivations are built from the same set of rules as $\mu\mathsf{PA}$ except that the rule $\nu$ replaces fixed point induction $\mathsf{ind}(\varphi)$ . We will show that the latter can be subsumed by the former in the context of cyclic proofs.

We adapt to our setting a well-known validity criterion from non-wellfounded proof theory.

Definition 12 (Traces and progress).

Let $\mathcal{D}$ be a coderivation, and let $(v_{i})_{i\in\omega}$ be an infinite branch along $\mathcal{D}$ . A trace along $(v_{i})_{i\in\omega}$ is a sequence of occurrences formulas ${\tau=}(\varphi_{i})_{i\geq k}$ such that for all $i\geq k$ , $\varphi_{i}$ is in the conclusion of a rule $\mathsf{r}$ , $\varphi_{i+1}$ is in a premise of $\mathsf{r}$ , and one of the following cases applies:

$\blacksquare$

$\varphi_{i}$ is the principal formula and $\mathsf{r}=\mathsf{e}$ with conclusion $\Gamma,\varphi_{i},\psi,\Delta$ and premise $\Gamma,\psi,\varphi_{i+1},\Delta$
$\blacksquare$

$\varphi_{i}$ is the principal formula and $\mathsf{r}=\mathsf{e}$ with conclusion $\Gamma,\psi,\varphi_{i},\Delta$ and premise $\Gamma,\varphi_{i+1},\psi,\Delta$
$\blacksquare$

$\varphi_{i}$ is the principal formula of $\mathsf{r}\neq\mathsf{e}$ and $\varphi_{i+1}$ is an active formula
$\blacksquare$

$\varphi_{i}$ and $\varphi_{i+1}$ are the $n$ -th side formulas in the context, for some $n$ (so they are equal modulo term substitution).

We say that $\varphi_{k+1}$ is an immediate ancestor of $\varphi_{k}$ if they extend to some trace $(\varphi_{i})_{i\geq k}$ . If $\varphi_{i}=t\in\nu Xx.\varphi$ (respectively $\varphi_{i}=t\in\mu Xx.\varphi$ ) for some $t$ , the rule $\mathsf{r}$ is $\nu$ (respectively $\mu$ ) and $\varphi_{i}$ is principal then we say $\nu Xx.\varphi$ (respectively $\mu Xx.\varphi$ ) progresses at $i$ . A trace $(\varphi_{i})_{i\geq k}$ is progressing if there is a $\nu$ -term $\nu Xx.\varphi$ such that $\nu Xx.\varphi$ progresses infinitely often and $\nu Xx.\varphi$ is minimal (w.r.t number of symbols) among all set-terms progressing infinitely often.

Definition 13 (Progressing and cyclic proofs).

A progressing proof is a coderivation $\mathcal{D}$ for which each infinite branch has a progressing trace. We write $\mathsf{C}\mu\mathsf{PA}$ for the class of cyclic progressing proofs, and $\mathsf{C}\mu\mathsf{PA}\vdash\varphi$ if there is a cyclic progressing proof of $\varphi$ .

Henceforth, we may mark two rule steps by a special symbol (e.g., $\bullet$ or $\star$ ) in a cyclic coderivation to indicate roots of identical sub-coderivations.

Example 14.

Consider the following two cyclic coderivations (see Example 5):

The left coderivation is not progressing, as its (only) branch looping at $\bullet$ has no $\nu$ -formula, and so any trace traversing such branch cannot be progressing. On the other hand, the right coderivation is a progressing proof. It syntactically shows that (the encodings of) hereditarily finite lists are natural numbers, a trivial statement. Nonetheless, its argument is rather complex, and involves nesting of cycles because of the interleaving fixed points within $\mathbf{T}$ .

Now, for any infinite branch $\mathfrak{b}$ one of the following cases applies:

$\blacksquare$

$\mathfrak{b}$ eventually loops only at $\star$ : the trace alternating ${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}orange}$ and ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}blue}$ formulas is progressing, and the smallest $\nu$ -term unfolding infinitely often is $\mathbf{L}(\mathbf{T})$ (in negative position).
$\blacksquare$

$\mathfrak{b}$ eventually loops only at $\bullet$ : the trace alternating ${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}orange}$ and ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}red}$ formulas is progressing, and the smallest $\nu$ -term unfolding infinitely often is $\mathbf{T}$ (in negative position).
$\blacksquare$

$\mathfrak{b}$ loops infinitely often at both $\star$ and $\bullet$ : the trace alternating ${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}orange}$ and ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}blue}$ formulas along $\star$ , and ${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}orange}$ and ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}red}$ formulas along $\bullet$ , is progressing, and the smallest $\nu$ -term unfolding infinitely often is $\mathbf{T}$ (in negative position).

Thus, any infinite branch has a progressing trace, and so the right coderivation is progressing.

3.2 Simulating inductive proofs

Our cyclic system $\mathsf{C}\mu\mathsf{PA}$ subsumes $\mu\mathsf{PA}$ by a standard argument:

Theorem 15 (Induction to cycles).

If $\mu\mathsf{PA}\vdash\varphi$ then $\mathsf{C}\mu\mathsf{PA}\vdash\varphi$ .

Proof sketch.

By induction on the structure of $\mu\mathsf{PA}$ proofs. The critical step is $\mathsf{ind}(\varphi)$ , for which we do not have a corresponding rule in $\mathsf{C}\mu\mathsf{PA}$ . We simulate this rule by the following:

where the rule steps marked $\varphi$ can be defined by induction on the structure of $\varphi$ . To check progressivity of the above coderivation, notice that any infinite branch is either progressing by the induction hypothesis, or loops infinitely on $\bullet$ and has the progressing trace coloured in blue. $\hfill\blacktriangleleft$

4 A reset proof system for $\mu\mathsf{PA}$

In this section we introduce an alternative route to cyclic proofs that allows for a more local and simpler (although more constrained) validity condition: so-called reset proofs (e.g., [2, 3, 4, 22]. Specifically, we define a cyclic reset proof system for $\mu\mathsf{PA}$ , called $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ , inspired by the annotated systems for first-order $\mu$ -calculus in [31, 1]. A key property of reset proof systems is the introduction of variables ranging over ordinals annotating fixed point formulas in a coderivation. Intuitively, an annotated fixed point $\mu^{\kappa}Xx\varphi$ , where $\kappa$ is an ordinal variable, expresses syntactically an ordinal approximant of $\mu Xx\varphi$ (see Proposition 6). The advantage of this approach is the possibility to internalise certain features of the progressivity condition, which can be then subsumed in a much simpler condition called reset condition. This allows for a more straightforward soundness argument. Soundness for $\mathsf{C}\mu\mathsf{PA}$ can then be established by defining a translation of progressing proofs of $\mathsf{C}\mu\mathsf{PA}$ into reset proofs.

4.1 Syntax and semantics of $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$

The language of $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ , written $\mathcal{L}_{\mu}^{\mathrm{ann}}$ , is a three-sorted language obtained by augmenting $\mathcal{L}_{\mu}$ by a countable set of ordinal variables $\mathcal{OV}$ ranging over $\kappa,\lambda$ . We extend Definition 4 to include new set terms $\mu^{\kappa}Xx\varphi$ and $\nu^{\kappa}Xx\varphi$ for any ordinal variable $\kappa$ .

Concerning semantics of $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ , the standard model is defined as in Definition 7, while assignments $\rho$ are extended to associate with every ordinal variable $\kappa\in\mathcal{OV}$ an ordinal $\rho(\kappa)$ . Satisfaction relation is then extended to the clauses $t\in\mu^{\kappa}Xx\varphi$ and $t\in\nu^{\kappa}Xx\varphi$ as follows:

\begin{array}[]{rclrcl}\mathfrak{N},\rho\vDash t\in\mu^{\kappa}Xx\varphi&\text% {iff}&\rho(t)\in\mu^{\rho(\kappa)}\varphi^{\mathfrak{N}}_{\rho,x,X}\qquad\quad% \mathfrak{N},\rho\vDash t\in\nu^{\kappa}Xx\varphi&\text{iff}&\rho(t)\in\nu^{% \rho(\kappa)}\varphi^{\mathfrak{N}}_{\rho,x,X}\end{array}

All the remaining definitions and conventions smoothly adapt to the new setting.

$\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ derives extended sequents, i.e., sequents equipped with conditions on ordinal variables called constraints. These are pairs $\mathcal{O}=(V_{\mathcal{O}},<_{\mathcal{O}})$ where $V_{\mathcal{O}}$ is a finite set of ordinal variables and $<_{\mathcal{O}}$ is a strict partial order such that, for each $\kappa\in V_{\mathcal{O}}$ , the set $\{\lambda\in V_{\mathcal{O}}\ |\ \kappa<_{\mathcal{O}}\lambda\}$ is linearly ordered by $<_{\mathcal{O}}$ . Intuitively, the condition $\lambda<_{\mathcal{O}}\kappa$ is interpreted as the assumption that $\lambda$ is “smaller” than $\kappa$ . Notice that $\mathcal{O}$ can be seen as a collection of trees with $V_{\mathcal{O}}$ the set of vertices, and the descendant relation is the converse of the order $<_{\mathcal{O}}$ : the children of $\kappa\in V_{\mathcal{O}}$ are then $\lambda\in V_{\mathcal{O}}$ where $\lambda<_{\mathcal{O}}\kappa$ and for no $\xi\in V_{\mathcal{O}}$ do we have $\lambda<_{\mathcal{O}}\xi<_{\mathcal{O}}\kappa$ .

We will sometimes write $\mathcal{O}\vdash\lambda<\kappa$ instead of $\lambda<_{\mathcal{O}}\kappa$ . Also, we write $\kappa\in\mathcal{O}$ as shorthand for $\kappa\in V_{\mathcal{O}}$ , and with $\varnothing$ we denote the empty constraint. We set $\lambda\leq_{\mathcal{O}}\kappa:=\lambda<_{\mathcal{O}}\kappa$ or $\lambda=\kappa$ .

Definition 16 (Extended sequents).

An (annotated) sequent $\Gamma$ is a finite list of formulas over $\mathcal{L}_{\mu}^{\mathrm{ann}}$ . An extended sequent is an expression $\mathcal{O}:\Gamma$ where $\Gamma$ is an annotated sequent and $\mathcal{O}$ is a constraint such that $V_{\mathcal{O}}$ contains all ordinal variables in $\Gamma$ . Given an annotated sequent $\Gamma$ , we denote with $\Gamma^{-}$ the sequent without ordinal variables.

The standard interpretation for $\mathcal{L}_{\mu}^{\mathrm{ann}}$ can be generalised to extended sequents in the obvious way. Given a constraint $\mathcal{O}$ , and assignment $\rho$ , we define $\rho\vDash\mathcal{O}$ iff $\lambda<_{\mathcal{O}}\kappa$ implies $\rho(\lambda)<_{\mathcal{O}}\rho(\kappa)$ for all $\lambda,\kappa\in\mathcal{O}$ . An extended sequent $\mathcal{O}:\Gamma$ is satisfied in $\mathfrak{N}$ if, for all assignments $\rho$ for $\mathfrak{N}$ , $\rho\vDash\mathcal{O}$ implies $\mathfrak{N},\rho\vDash\bigvee\Gamma$ .

4.2 Annotated coderivations and reset proofs

For the purpose of presenting the inference rules we require three operations on constraints:

\begin{array}[]{rcl}\mathcal{O}+\lambda&:=&(V_{\mathcal{O}}\cup\{\lambda\},<_{% \mathcal{O}})\\ \mathcal{O}+_{\kappa}\lambda&:=&(V_{\mathcal{O}}\cup\{\lambda\},<_{\mathcal{O}% }\cup\ \{(\lambda,\xi)\ |\ \kappa\leq_{\mathcal{O}}\xi\})\end{array}\quad% \qquad\mathcal{O}\setminus V:=(V_{\mathcal{O}}\setminus V,<_{\mathcal{O}}\cap% \ (V_{\mathcal{O}}\setminus V)^{2})

where $V\subset V_{\mathcal{O}}$ . The top left operation adds $\lambda$ as a fresh ordinal variable, which becomes the root of a new tree in $\mathcal{O}$ . In the bottom left operation $\lambda$ is added as a fresh child of the ordinal variable $\kappa$ . Note that these operations preserve the condition that the set $\{\lambda\in V_{\mathcal{O}}\ |\ \kappa<_{\mathcal{O}}\lambda\}$ is linearly ordered by $<_{\mathcal{O}}$ for every $\kappa\in V_{\mathcal{O}}$ , and so the tree structure is also preserved. The right operation restricts a constraint set to a subset $V$ of ordinal variables.

Figure 3: Inference rules for annotated coderivations (notation

\Gamma^{-}

is introduced in Definition 16).

The rules of our reset system are in Figure 3. They essentially “lift” the rules of $\mathsf{C}\mu\mathsf{PA}$ to extended sequents, replacing $\nu$ with decorated versions ( $\nu$ and $\nu^{\kappa}$ ) internalising fixed points approximants (see Proposition 6), and with the rule $\mathsf{cw}$ removing a set $L\subseteq\mathcal{O}$ from the constraint. Validity condition will be defined via so-called reset rule ( $RS(\kappa)$ ), a special case of $\mathsf{cw}$ , where $C(\kappa)$ is the set of the children of $\kappa$ in $\mathcal{O}$ and must be non-empty, and $\kappa$ does not occur in $\Gamma$ . Translating from $\mu\mathsf{PA}$ to $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ requires another special case of $\mathsf{cw}$ , a novelty of this paper called the pruning rule, where $P(\Gamma)$ is the set of all ordinal variables that have no descendants occurring in $\Gamma$ (i.e., $\{\kappa\in\mathcal{O}\ |\ \forall\lambda\in\mathcal{O}(\lambda\leq_{\mathcal{% O}}\kappa\implies\lambda\text{ does not occur in $\Gamma$})\}$ ), and must be non-empty. Intuitively, the pruning rule is used to “refresh” constraints preventing unbounded increase of ordinal variables along infinite branches of reset proofs.

Definition 17 (Annotated coderivations).

An annotated coderivation is a coderivation over the rules in Figure 3.

We are now ready to define the reset condition, which represents a counterpart to the progressivity condition in the setting of annotated coderivations.

Definition 18 (Reset proofs).

Let $\mathcal{D}$ be an annotated coderivation, and let $\mathfrak{b}=(\mathcal{O}_{i}:\Gamma_{i})_{i\geq 0}$ be an infinite branch of $\mathcal{D}$ . We say that $\kappa$ is a stable variable in $\mathfrak{b}$ if there is $i_{0}\geq 0$ such that $\kappa\in\mathcal{O}_{i}$ , for every $i\geq i_{0}$ . We say that $\kappa$ is a reset variable in $\mathfrak{b}$ if there are infinitely many occurrences of $RS(\kappa)$ in $\mathfrak{b}$ . We say that $\mathcal{D}$ is a reset proof if every infinite branch has a stable reset variable. We denote with $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ the class of cyclic reset proofs⁴⁴4 $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ is based on the reset system for the $\mu$ -calculus from [31], and later refined in [1], but differs in many respects. Concerning syntax, $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ is endowed with the language of $\mathsf{PA}$ and omits quantification over ordinal variables. Concerning the proof system, it is formulated in one-sided sequent calculus style. Also, we avoid working with finite representations of cyclic proofs, which allows us to bypass some syntactic technicalities /such as so-called order-coherence in [1] to check validity and cyclicity conditions). .

Example 19.

Consider the following annotated coderivation of the formula $t\in\nu Xx(x\in X)$ .

It has only one infinite branch (looping at $\bullet$ ) that unfolds infinitely often (annotations of) the formula $t\in\nu Xx(x\in X)$ . The branch contains a stable reset variable $\lambda$ . Therefore, the annotated coderivation is a (cyclic) reset proof.

The main result of this section is soundness for cyclic reset proofs. This is a standard argument towards contradiction that leverages a preliminary lemma, which shows that inference rules locally preserve soundness, and constructs an infinite branch of the reset proof that reflects falsity. Specifically, our argument is essentially borrowed from [1].

Lemma 20 (Local soundness).

For any inference rule $\mathsf{r}$ of $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ with conclusion $\mathcal{O}:\Sigma$ , if $\mathfrak{N},\rho\nvDash\mathcal{O}:\Sigma$ then there is a premise $\mathcal{O}^{\prime}:\Sigma^{\prime}$ of $\mathsf{r}$ and assignment $\rho^{\prime}$ s.t.

1.

$\mathfrak{N},\rho^{\prime}\nvDash\mathcal{O}^{\prime}:\Sigma^{\prime}$ and
2.

for any $\kappa\in\mathcal{O}\cap\mathcal{O}^{\prime}$ we have $\rho^{\prime}(\kappa)\leq\rho(\kappa)$ . If moreover, $\mathsf{r}=RS(\kappa)$ then $\rho^{\prime}(\kappa)<\rho(\kappa)$ .

Theorem 21 (Soundness).

For any reset proof $\mathcal{D}$ with conclusion $\mathcal{O}:\Gamma$ , $\mathfrak{N}\vDash\mathcal{O}:\Gamma$ .

Proof.

Assume by contradiction that $\mathcal{D}$ is a reset proof with conclusion $\mathcal{O}:\Gamma$ s.t. $\mathfrak{N},\rho\nvDash\mathcal{O}:\Gamma$ for some assignment $\rho$ . By Lemma 20 we can construct an infinite branch $(\mathcal{O}_{i}:\Gamma_{i})_{i\geq 0}$ of $\mathcal{D}$ and a sequence of assignments $(\rho_{i})_{i<\omega}$ such that $\mathcal{O}_{0}:\Gamma_{0}:=\mathcal{O}:\Gamma$ , $\rho_{0}:=\rho$ and for all $i\geq 0$ :

1.

$\mathfrak{N},\rho_{i}\nvDash\mathcal{O}_{i}:\Gamma_{i}$
2.

for any $\kappa\in\mathcal{O}_{i}\cap\mathcal{O}_{i+1}$ we have $\rho_{i+1}(\kappa)\leq\rho_{i}(\kappa)$
3.

if $\kappa\in\mathcal{O}_{i}$ and $\mathcal{O}_{i}:\Gamma_{i}$ is the conclusion of a reset rule $RS(\kappa)$ then $\rho_{i+1}(\kappa)<\rho_{i}(\kappa)$ .

Since $\mathcal{D}$ is a reset proof, there will be some stable reset variable $\kappa$ along this branch, and so for some $m$ we have $\kappa\in\mathcal{O}_{n}$ for every $n\geq m$ . Consider the ordinal sequence $(\rho_{n}(\kappa))_{n\geq m}$ . By construction we have $\rho_{n+1}(\kappa)\leq\rho_{n}(\kappa)$ for every $n\geq m$ and $\rho_{n+1}(\kappa)<\rho_{n}(\kappa)$ at every reset step. Since $\kappa$ is reset infinitely many times this contradicts wellfoundedness of ordinals. $\hfill\blacktriangleleft$

5 From progressing proofs to reset proofs

In this section we show that sequents provable in $\mathsf{C}\mu\mathsf{PA}$ are also provable in $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ . To this end, we define a (parametrised) translation $(\_)^{\mathcal{O}\mid\ell_{1},\ldots,\ell_{n}}$ from ( $\mu\mathsf{PA}$ -)coderivations $\mathcal{D}$ with conclusion $\varphi_{1},\ldots,\varphi_{n}$ into annotated coderivations with conclusion $\mathcal{O}:\varphi_{1}^{\ell_{1}}\ldots,\varphi_{n}^{\ell_{n}}$ , where each $\ell_{i}$ “decorates” occurrences of $\nu$ in $\varphi_{i}$ with ordinal variables. Specifically, the translation corecursively (i.e., bottom-up) turns sequents of $\mathcal{D}$ into extended sequents (modifying inference rules accordingly). We show that the translation maps, in particular, cyclic progressing proofs into cyclic reset proofs, from which we can derive soundess of $\mathsf{C}\mu\mathsf{PA}$ .

Definition 22 (Ordinal assignments).

Let $\varphi$ be a formula of $\mathcal{L}_{\mu}$ and $V\subseteq\mathcal{OV}$ . A list $\ell=a_{1}\cdots a_{n}$ over $V\cup\{\star\}$ is called an ( $V$ -)ordinal assignment for $\varphi$ , written $\ell\triangleleft_{V}\varphi$ (sometimes $\ell\triangleleft\varphi$ ), if the length of $\ell$ is equal to the number of occurrences of $\nu$ in $\varphi$ . We define $\varphi^{\ell}$ to be the formula $\mathcal{L}_{\mu}^{\mathrm{ann}}$ obtained by replacing the $i$ -th occurrence of $\nu$ (from left) with $\nu^{a_{i}}$ if $a_{i}\neq\star$ , and with $\nu$ itself otherwise. We extend ordinal assignments to sequents $\Gamma=\varphi_{1},\ldots,\varphi_{n}$ by setting $\ell_{1},\ldots,\ell_{n}\triangleleft_{V}\Gamma$ if $\ell_{i}\triangleleft_{V}\varphi_{i}$ for all $1\leq i\leq n$ , and $\Gamma^{\ell_{1},\ldots,\ell_{n}}:=\varphi_{1}^{\ell_{1}},\ldots,\varphi_{n}^{% \ell_{n}}$ .

Example 23.

Consider $\varphi:=t\in\nu Xx(s\in\nu Yy(x\in X\vee y\in Y\vee\mathbf{N}))$ , and let $\kappa\in\mathcal{OV}$ . Then, $\ell:=\kappa\star$ is an ordinal assignment for $\varphi$ , and $\varphi^{\ell}=t\in\nu^{\kappa}Xx(s\in\nu^{\star}Yy(x\in X\vee y\in Y\vee% \mathbf{N}))=t\in\nu^{\kappa}Xx(s\in\nu Yy(x\in X\vee y\in Y\vee\mathbf{N}))$ .

Definition 24 (Translation).

Let $\mathcal{D}$ be a $\mu\mathsf{PA}$ -coderivation with conclusion $\Sigma$ , and let $\mathcal{O}=(V_{\mathcal{O}},<_{\mathcal{O}})$ be a constraint such that $\ell_{1},\ldots,\ell_{n}\triangleleft_{V_{\mathcal{O}}}\Sigma$ . We define coinductively the translation $(\cdot)^{\mathcal{O}\mid\ell_{1},\ldots,\ell_{n}}$ mapping $\mathcal{D}$ into an annotated coderivation $\mathcal{D}^{\mathcal{O}\mid\ell_{1},\ldots,\ell_{m}}$ with conclusion $\mathcal{O}:\Sigma^{\ell_{1},\ldots,\ell_{n}}$ . We consider only the most relevant case where the coderivation ends with a $\nu$ step, with $\Sigma:=\Gamma,t\in\nu Xx\varphi$ . If $\ell_{n}:=\lambda\ell$ then:

The case $\ell_{n}:=\star\ell$ is similar.

Theorem 25.

If $\mathsf{C}\mu\mathsf{PA}\vdash\varphi$ then $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}\vdash\varnothing:\varphi$ .

Proof idea.

Let $\mathcal{D}$ be a $\mathsf{C}\mu\mathsf{PA}$ coderivation with conclusion $\varphi$ . Let $\mathfrak{b}=(\mathcal{O}_{i}:\Gamma_{i})_{i\geq 0}$ be an infinite branch in ${\mathcal{D}}^{\varnothing\mid\star\cdots\star}$ . There exists a unique infinite branch $\widehat{\mathfrak{b}}=(\Delta_{i})_{i\geq 0}$ of $\mathcal{D}$ that translates into $\mathfrak{b}$ . By hypothesis, $\widehat{\mathfrak{b}}$ has a progressing trace $\widehat{\tau}=(\varphi_{i})_{i\geq i_{0}}$ for some $i_{0}\geq 0$ . Let $\nu Xx.\varphi$ be the smallest infinitely progressing set-term in $\widehat{\tau}$ . Recalling notation $(\cdot)^{-}$ (Definition 16), $\hat{\tau}$ induces a trace $\tau=(\psi_{i})_{i\geq i_{1}}$ of $\mathfrak{b}$ such that $\tau^{-}:=(\psi_{i}^{-})_{i\geq i_{1}}$ enumerates $(\varphi_{i})_{i\geq i_{0}}$ (possibly with repetitions). Moreover, by progressivity of $\widehat{\tau}$ , there is $i_{2}\geq i_{1}$ and a sequence of ordinal variables $(\kappa_{i})_{i\geq i_{2}}$ such that, for all $i\geq i_{2}$ :

(i)

$\nu^{\kappa_{i}}Xx.\varphi$ occurs in $\psi_{i}$ .
(ii)

Either $\kappa_{i+1}=\kappa_{i}$ or $\kappa_{i+1}$ is the child of $\kappa_{i}$ in $\mathcal{O}_{i+1}$ (i.e., in any case, $\kappa_{i}\geq_{\mathcal{O}_{i+1}}\kappa_{i+1}$ ).
(iii)

There exists $j\geq i$ s.t. $\kappa_{j+1}$ is the child of $\kappa_{j}$ in $\mathcal{O}_{j+1}$ .

Let us show that $\mathfrak{b}$ has a stable variable. For $i\geq i_{2}$ set $A_{i}:=\{\lambda\in\mathcal{O}_{i}\mid\mathcal{O}_{i}\vdash\lambda\geq\kappa_{% i}\}$ . This is a finite linear order (non-empty by i), and we pick a maximal element $\theta\in A_{i_{2}}$ (which is also maximal in $\mathcal{O}_{i_{2}}$ ). By ii if $\theta\in A_{i}$ then $\theta\in A_{i+1}$ unless $\theta$ is removed by a reset or a pruning rule. But $\theta$ cannot be pruned because of i. Also, no $\nu$ -rule or $\nu^{\kappa}$ -rule can introduce a parent of $\theta$ , so $\theta$ cannot be removed by a reset rule either.

Now, since $A_{i_{2}}$ contains a stable variable $\theta$ , it also contains a minimal one $\theta^{*}$ . Since $\nu$ is applied infinitely often in $\widehat{\mathfrak{b}}$ , the reset and pruning rules are applied infinitely often along $\mathfrak{b}$ (see Definition 24, case $\nu$ ). From this fact, using iii, we can show that $RS(\theta^{*})$ is applied infinitely often along $\mathfrak{b}$ .

By inspecting the translation it is not too hard to see that $\mathcal{D}^{\varnothing\mid\star\cdots\star}$ is cyclic when $\mathcal{D}$ is. $\hfill\blacktriangleleft$

Soundness for progressing proofs follows as a straightforward corollary:

Corollary 26 (Soundness for $\mathsf{C}\mu\mathsf{PA}$ ).

Let $\mathcal{D}\in\mathsf{C}\mu\mathsf{PA}$ with conclusion $\varphi$ . Then, $\mathfrak{N}\vDash\varphi$ .

Proof.

By Theorem 25 we have that ${\mathcal{D}}^{\varnothing\mid\star\cdots\star}$ is a cyclic reset proof of $\varnothing:\varphi^{\star\cdots\star}=\varphi$ . By Theorem 21 we have $\mathfrak{N}\vDash\varnothing:\varphi$ , and so $\mathfrak{N}\vDash\varphi$ . $\hfill\blacktriangleleft$

6 Formalising the soundness argument in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

The final section of this paper is devoted to proving the converse of Theorem 15. To this end, taking inspiration from previous work [28, 14], we use second-order theories to formalise the soundness theorem for the reset system $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ (Theorem 21), and then we appeal to conservativity results (Theorem 33).

6.1 Theories of second-order arithmetic

We shall work with common subsystems of second-order arithmetic, as found in textbooks such as [29], and assume basic facts about them. In particular, recall that $\mathsf{A}{\mathsf{CA}_{0}}$ is a two-sorted extension of basic arithmetic by:

$\blacksquare$

Arithmetical comprehension. $\exists X\forall x(X(x)\leftrightarrow\varphi(x))$ for each arithmetical formula $\varphi(x)$ .
$\blacksquare$

Set induction. $\forall X(X(0)\to\forall x(X(x)\to X(\mathsf{s}x))\to\forall xX(x))$

From here, $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ is the extension of $\mathsf{A}{\mathsf{CA}_{0}}$ by the comprehension schema for all $\Pi^{1}_{2}$ formulas. We shall freely use established principles of $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ (as seen, e.g., in [29]) such as $\Sigma^{1}_{2}$ -comprehension, $\Sigma^{1}_{2}$ -choice and $\Sigma^{1}_{2}$ -dependent choice. The term $\Sigma^{1}_{k}$ will denote formulas provably equivalent under $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ to a formula of the form $\exists X_{0}\forall X_{1}\ldots Q_{n}\varphi$ with $\varphi$ arithmetical, and similarly for $\Pi^{1}_{k}$ and $\Delta^{1}_{k}$ . We use the notation $\langle-\rangle$ for the code of a tuple. If the tuple contains a set then $\langle-\rangle$ will be a second-order object. For any set $F$ we can consider $F$ as a function $F:\mathbb{N}\rightarrow SET$ by setting $F(x):=\{y\ |\ \langle x,y\rangle\in F\}$ .

For the formalised soundness argument we will need that $\Delta^{1}_{2}$ formulas are closed under positive arithmetical combinations (over $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ ).

Theorem 27.

Let $\psi(\varphi_{0},\ldots\varphi_{n})$ be a positive arithmetical combination of $\varphi_{0},\ldots\varphi_{n}$ . If $\varphi_{0},\ldots\varphi_{n}\in\Sigma^{1}_{2}$ (resp., $\Pi^{1}_{2}$ ) then $\psi(\varphi_{0},\ldots\varphi_{n})\in\Sigma^{1}_{2}$ (resp., $\Pi^{1}_{2}$ ).

6.2 Countable orders in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

A basic theory of (countable) ordinals can be developed even within weak second-order theories, as shown in [Sim99] and also comprehensively surveyed in [Hir05].

A (countable) binary relation is a pair $(X,\leq)$ where $X$ and $\leq$ are sets, the latter construed as ranging over pairs. We shall write $\alpha$ , $\beta$ etc. to range over countable binary relations. If $\alpha=(X,\leq)$ we may write $x\leq_{\alpha}y:=x,y\in X\wedge x\leq y$ , and similarly for $x<_{\alpha}y$ . We may also write $x\in\alpha$ instead of $x\in X$ . We write $WO(\alpha)$ for the $\Pi^{1}_{1}$ statement that $\alpha$ is a well-order.

Following Simpson in [Sim99], given $\alpha$ , $\beta\in WO$ we write $\alpha\prec\beta$ if there is an order-isomorphism from $\alpha$ onto a proper initial segment of $\beta$ , $\alpha\approx\beta$ if $\alpha$ and $\beta$ are order-isomorphic and $\alpha\preceq\beta$ if $\alpha\prec\beta\vee\alpha\approx\beta$ . We have the following basic facts about comparison:

Proposition 28.

$\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ proves that:

1.

$\prec$ , $\preceq$ and $\approx$ are all $\Delta^{1}_{1}$ .
2.

$\prec$ is a total linear order
3.

$\prec$ is well-founded: $\ \forall F:\mathbb{N}\rightarrow WO\ ((\forall x\exists y>x\ F(y+1)\prec F(y)% )\rightarrow\exists x(F(x)\prec F(x+1)))$

6.3 Knaster-Tarski Theorem and approximants

We have two ways of interpreting the $\mu$ - and $\nu$ -binders in second-order arithmetic. First:

	$\displaystyle t\in\mu Xx.\varphi$	$\displaystyle:=\forall X(\forall x(\varphi(X,x)\to x\in X)\to t\in X)$		(1)
	$\displaystyle t\in\nu Xx.\varphi$	$\displaystyle:=\exists X(\forall x(x\in X\rightarrow\varphi(X,x))\wedge t\in X)$		(2)

Another way of interpreting $\mu$ and $\nu$ is through approximants:

Definition 29 (Approximants).

We write:

$t\in\mu^{\alpha}Xx.\varphi$	$\!\!\!\!:=\!\!$	$\exists F:\alpha\rightarrow SET\ \exists a\in\alpha\,(\forall b\in\alpha\,% \forall y\,(y\in F(b)\rightarrow\exists c<_{\alpha}b\ \varphi(F(c),y))\wedge t% \in F(a))$
$t\in\mu^{\mathrm{WO}}Xx.\varphi$	$\!\!\!\!:=\!\!$	$\exists\alpha\in WO\ t\in\mu^{\alpha}Xx.\varphi$
$t\in\nu^{\alpha}Xx.\varphi$	$\!\!\!\!:=\!\!$	$\forall F:\alpha\rightarrow SET\ \forall a\in\alpha\,(\forall b\in\alpha\,% \forall y\,(\forall c<_{\alpha}b\ \varphi(F(c),y)\rightarrow y\in F(b))% \rightarrow t\in F(a))$
$t\in\nu^{\mathrm{WO}}Xx.\varphi$	$\!\!\!\!:=\!\!$	$\forall\alpha\in WO\ t\in\nu^{\alpha}Xx.\varphi$

For the remainder of this section, assume $\varphi(X,x)\in\Delta^{1}_{2}$ and that $\varphi(X,x)$ is positive in $X$ . The results of this section are all proven in [12] for $\mu$ -terms and the dual properties for $\nu$ -terms can then be obtained using the fact $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}\vdash t\in\mu Xx.\varphi(X,x)% \leftrightarrow t\notin\nu Xx.\neg\varphi(\neg X,x)$ and similar for $\mu^{\alpha}Xx.\varphi$ and $\mu^{WO}Xx.\varphi$ .

The first proposition shows that $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ has access to the recursive characterizations of $\nu$ -approximants as well as the fact that $\mu Xx.\varphi$ is a fixed points.

Proposition 30 (Recursion and Knaster-Tarski).

$\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ proves

$t\in\nu^{\alpha}Xx.\varphi$	$\leftrightarrow$	$\forall\beta\prec\alpha\ \varphi(\nu^{\beta}Xx.\varphi,t)$
$t\in\mu Xx.\varphi(X,x)$	$\leftrightarrow$	$\varphi(\mu Xx.\varphi,y)$

In [12] it is shown that if $WO(\alpha)$ then $\mu^{\alpha}Xx.\varphi$ and $\nu^{\alpha}Xx.\varphi$ are in $\Delta^{1}_{2}$ . Using this fact and standard prenexing we see that $\mu^{WO}Xx.\varphi\in\Sigma^{1}_{2}$ . Also, by standard prenexing and $\Sigma^{1}_{2}$ -choice we see that $\mu Xx.\varphi\in\Pi^{1}_{2}$ . In [12] it is also shown that the two interpretations of $\mu$ and $\nu$ are provably equivalent in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ , i.e. $\mu Xx.\varphi=\mu^{WO}Xx.\varphi$ and $\nu Xx.\varphi=\nu^{WO}Xx.\varphi$ . Putting all this together we get that for $WO(\alpha)$ :

Corollary 31.

$\mu^{\alpha}Xx.\varphi$ , $\nu^{\alpha}Xx.\varphi$ , $\mu Xx.\varphi$ , $\mu^{WO}Xx.\varphi$ , $\nu Xx.\varphi$ and $\nu^{WO}Xx.\varphi$ are all $\Delta^{1}_{2}$ .

6.4 Interpreting $\mathsf{C}\mu\mathsf{PA}$ and $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

We may define an interpretation $(\_)^{\dagger}$ from $\mathsf{C}\mu\mathsf{PA}$ to $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ defined by $(t\in\mu Xx\varphi)^{\dagger}:=t\in\mu Xx\varphi$ and $(t\in\nu Xx\varphi)^{\dagger}:=t\in\nu Xx\varphi$ . Similarly, we can define an interpretation $(\_)^{\dagger}$ from $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ to $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ by $(t\in\mu Xx.\varphi)^{\dagger}:=t\in\mu Xx.\varphi$ , $(t\in\nu Xx.\varphi)^{\dagger}:=t\in\nu^{WO}Xx.\varphi$ and $(t\in\nu^{\kappa}.Xx\varphi)^{\dagger}:=t\in\nu^{\kappa}Xx.\varphi$ . Writing the two different interpretations of $\nu Xx\varphi$ the same is justified by $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}\vdash\nu Xx.\varphi=\nu^{WO}Xx.\varphi$ [12]. By Corollary 31 and Theorem 27 we have:

Theorem 32.

If $\varphi$ is a formula of $\mathsf{C}\mu\mathsf{PA}$ then $\varphi^{\dagger}$ is $\Delta^{1}_{2}$ .

Theorem 32 allows $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ to readily verify the axioms of $\mu\mathsf{PA}$ using $\Pi^{1}_{2}$ -comprehension, and so $\mu\mathsf{PA}$ can be considered a fragment of $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ . In fact, by a result of Möllerfeld’s, $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ not only extends $\mu\mathsf{PA}$ but does so conservatively.

Theorem 33 (Implied by [23]).

$\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ is arithmetically conservative over $\mu\mathsf{PA}$ .

This is a nontrivial result in proof theory whose details we shall not recount. We will use this theorem as a “black box” henceforth.

6.5 Formalizing $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ satisfaction in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

We will employ standard metamathematical notations and conventions for coding, e.g. we write $\ulcorner E\urcorner$ for the Gödel code of an expression $E$ . As usual, a predicate language cannot contain its own universal truth predicate for Tarskian reasons. However we may define partial truth predicates for fragments of the language, in particular, each of our partial satisfaction predicates will be relativized to a single $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ proof $\mathcal{D}$ containing only finitely many ordinal variables and set-terms.

We let $\mathrm{Sat}_{\mathcal{D}}(\rho,m,\vec{A},\vec{\alpha}):=\ \langle\rho,m% \rangle\in\mu Zz.\chi(z,Z,\vec{A},\vec{\alpha})$ where $\chi(z,Z,\vec{A},\vec{\alpha})$ is a $\Delta^{1}_{2}$ formula and so $\mathrm{Sat}_{\mathcal{D}}(\rho,m,\vec{A},\vec{\alpha})\in\Delta^{1}_{2}$ . There are two main properties that we need our partial satisfaction predicate to satisfy. The first is reflection.

Theorem 34 (Reflection).

Let $\varphi(\vec{X},\vec{x},\vec{\kappa})$ be a subformula of a formula in $\mathcal{D}$ . Then $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ proves $\mathrm{Sat}_{\mathcal{D}}(\rho,\ulcorner\varphi(\vec{X},\vec{x},\vec{\kappa})% \urcorner,\vec{A},\vec{\alpha})\leftrightarrow\varphi(\vec{A},\rho(\vec{x}),% \vec{\alpha})$ .

Secondly, our partial satisfaction predicate needs to satisfy the proper inductive characterization of satisfaction e.g. $\mathrm{Sat}_{\mathcal{D}}(\rho,\ulcorner\exists x\varphi\urcorner,\vec{A},% \vec{\alpha})\leftrightarrow\exists n\,\mathrm{Sat}_{\mathcal{D}}(\rho\{x% \mapsto n\},\ulcorner\varphi\urcorner,\vec{A},\vec{\alpha})$ and
$\small\textstyle\bigwedge\limits_{i,j=0}^{k}\mathrm{Sat}_{\mathcal{D}}(\rho,% \ulcorner t\in\nu^{\kappa_{j}}X_{i}x_{i}.\varphi_{i}\urcorner,\vec{A},\vec{% \alpha})\leftrightarrow\rho(t)\in\nu^{\alpha_{j}}Y_{i}y_{i}.\mathrm{Sat}_{% \mathcal{D}}(\rho\{x_{i}\mapsto y_{i}\},\ulcorner\varphi_{i}\urcorner,A_{0},% \ldots Y_{i},\ldots A_{k},\vec{\alpha}))$

Theorem 35 (Formalised satisfaction).

$\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ proves that $\mathrm{Sat}_{\mathcal{D}}(\rho,m,\vec{A},\vec{\alpha})$ satisfies the inductive characterization of satisfaction for every connective.

For the formalized soundness proof we also need to extend our satisfaction predicate $\mathrm{Sat}_{\mathcal{D}}$ so that it works with constraints and extended sequents. This is done in the expected way.

6.6 Formalizing soundness for $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$

Recall that in Theorem 21, after showing the existence of the branch witnessing falsity, we invoke the reset condition to extract a stable reset variable along the false branch and thereby get a contradiction. To mimic this step inside $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ it is crucial that $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ “knows” that the proof satisfies the reset condition.

Lemma 36.

Let $\mathcal{D}$ be a $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ proof. Then $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ proves that for all branches $\mathfrak{b}$ in $\mathcal{D}$ there exists a stable reset variable $\kappa$ along $\mathfrak{b}$ .

Proof.

The idea is standard and is covered in detail in [14]. It is provable in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ (and much weaker theories) that for a $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ derivation $\mathcal{D}$ , satisfying the reset condition is equivalent to language inclusion of two Büchi automata which can both be computed from $\mathcal{D}$ . Since by [19] language inclusion for Büchi automata is decidable it follows that, if $\mathcal{D}$ satisfies the reset condition, then $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ proves that fact. $\hfill\blacktriangleleft$

Theorem 37 (Formalising soundness).

Let $\mathcal{D}$ be a $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ proof with conclusion $\mathcal{O}_{\mathcal{D}}:\Gamma_{\mathcal{D}}$ . Then $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}\vdash\forall\vec{\alpha}\in WO\ \forall\rho% ,\vec{A}\ \mathrm{Sat}_{\mathcal{D}}(\rho,\ulcorner\mathcal{O}_{\mathcal{D}}:% \Gamma_{\mathcal{D}}\urcorner,\vec{A},\vec{\alpha})$

Proof.

Assume for contradiction that $\neg\mathrm{Sat}_{\mathcal{D}}(\rho_{\mathcal{D}},\ulcorner\mathcal{O}_{% \mathcal{D}}:\Gamma_{\mathcal{D}}\urcorner,\vec{A},\vec{\alpha}_{\mathcal{D}})$ . As in Theorem 21 we will show the existence of a false branch satisfying certain conditions. The key to this is Lemma 20 which says that whenever we have a false extended sequent then we can find a premise which is false and satisfies the right conditions on ordinal variables. To state Lemma 20 inside $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ we define the following formulas:

\begin{array}[]{rcl}\xi(X)&:=&X=\langle\rho,\ulcorner\mathcal{O}:\Gamma% \urcorner,\vec{\alpha}\rangle\wedge\mathcal{O}:\Gamma\text{ is in }\mathcal{D}% \wedge WO(\vec{\alpha})\wedge\neg\mathrm{Sat}_{\mathcal{D}}(\rho,\ulcorner% \mathcal{O}:\Gamma\urcorner,\vec{A},\vec{\alpha})\end{array}

\begin{array}[]{rcl}\chi(X,Y)&:=&X=\langle\rho,\ulcorner\mathcal{O}:\Gamma% \urcorner,\vec{\alpha}\rangle\wedge Y=\langle\rho^{\prime},\ulcorner\mathcal{O% }^{\prime}:\Gamma^{\prime}\urcorner,\vec{\alpha}^{\prime}\rangle\wedge\mathcal% {O}^{\prime}:\Gamma^{\prime}\text{ is a premise in $\mathcal{D}$ of }\mathcal{% O}:\Gamma\\ &&\wedge\ \forall n\leq k\Big(\kappa_{n}\in\mathcal{O}\cap\mathcal{O}^{\prime}% \rightarrow\big((\alpha_{n}^{\prime}\preceq\alpha_{n})\ \wedge\ \text{(the % rule is }RS(\kappa_{n})\rightarrow\alpha_{n}^{\prime}\prec\alpha_{n})\big)\Big% )\end{array}

Note that both $\xi(X)$ and $\chi(X,Y)$ are arithmetical in $\mathrm{Sat}_{\mathcal{D}}$ , $\prec$ and $W O$ , and so they are $\Delta^{1}_{2}$ by Theorem 27. Let $Z_{\mathcal{D}}=\langle\rho_{\mathcal{D}},\ulcorner\mathcal{O}_{\mathcal{D}}:% \Gamma_{\mathcal{D}}\urcorner,\vec{\alpha}_{\mathcal{D}}\rangle$ . The formal equivalent of Lemma 20 is:

\forall X\exists Y\ ((\xi(X)\rightarrow(\xi(Y)\wedge\chi(X,Y)))\wedge(\neg\xi(% X)\rightarrow Y=Z_{\mathcal{D}}))

(3)

To see that this can be proven within $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$ , first note that for $X$ with $\neg\xi(X)$ we just let $Y=Z_{\mathcal{D}}$ , so the hard case is when $\xi(X)$ holds. The proof of this case mimics directly the meta-level proof of Lemma 20 using the inductive characterization of satisfaction Theorem 35. We also need Proposition 30(1) for the $\nu^{\kappa}$ -rule, Proposition 30(2) for the $\mu$ -rule and Proposition 28 for the reset rule. More details can be found in the appendix.

Since $\xi(X)$ and $\chi(X,Y)$ are $\Delta^{1}_{2}$ we can apply $\Sigma^{1}_{2}$ -dependent choice⁵⁵5( $\text{$\Sigma^{1}_{2}$-dependent choice})\ \ \ \forall X\exists Y\varphi(X,Y)% \implies\exists F:\mathbb{N}\rightarrow SET\ \forall n\varphi(F(n),F(n+1))\ \ % \ \varphi\in\Sigma^{1}_{2}$ to (3) to get a suitable branch. By $\Sigma^{1}_{2}$ -dependent choice there exists $F:\mathbb{N}\rightarrow SET$ s.t.

\forall n\ ((\xi(F(n))\rightarrow(\xi(F(n+1))\wedge\chi(F(n),F(n+1))))\wedge(% \neg\xi(F(n))\rightarrow F(n+1)=Z_{\mathcal{D}}))

Note that if $\neg\xi(F(0))$ then $F(1)=Z_{\mathcal{D}}$ and so $\xi(F(1))$ , which means by an easy induction that $\forall n\geq 1\ \xi(F(n))$ . By comprehension we define $B(n):=F(n+1)$ and so $B$ is a branch witnessing falsity satisfying $\forall n\ \chi(B(n),B(n+1))$ .

Now we apply Lemma 36 to get a stable reset variable $\kappa_{j}$ such that, for some $m$ and all $n\geq m$ , $\kappa_{j}$ occurs in $\mathcal{O}$ , where $B(n)=\langle\rho,\ulcorner\mathcal{O}:\Gamma\urcorner,\vec{\alpha}\rangle$ . Finally, using this stable reset variable we want to show the existence of an infinitely descending ordinal sequence. By comprehension we get $G:\mathbb{N}\rightarrow WO$ s.t. $G:n\mapsto\alpha\ \leftrightarrow\ B(n+m)=\langle\rho,\ulcorner\mathcal{O}:% \Gamma\urcorner,\alpha_{0},\ldots\alpha_{j-1},\alpha,\ldots\alpha_{k}\rangle.$ Then, since $\forall n\ \chi(B(n),B(n+1))$ we see that $G$ contradicts Proposition 28(3). $\hfill\blacktriangleleft$

7 Conclusions and future works

We studied the cyclic proof theory of arithmetic with generalised inductive definitions. Specifically, we extended Simpson’s equivalence result between Peano arithmetic and its cyclic formulation [28], further generalising Das and Melgaard’s work on (finitely iterated) arithmetical inductive definitions [15]. Along the way, we also established an equivalence between two alternative validity conditions for cyclic proofs in our setting: the commonly adopted condition based on the notion of progressing trace and so-called reset condition for annotated proof systems (e.g., [31, 1]).

Our results easily apply to the intuitionistic context, essentially using negative translations studied in [35, 12]. Because of the absence of classical logic dualities, we can identify weaker versions of generalised inductive definitions, such as the strictly positive ones (defined by fixed points where $\mu$ does not bind set variables to the left of an implication). Such subsystems are of great importance for implementation perspectives, as proof assistants (such as Coq or Agda) typically enforce strict positivity conditions on (co)inductive types for consistency reasons. Despite being apparently more restrictive, strictly positive fixed points are commonly believed to have the same proof theoretic strength of the (hereditarily) positive ones (see [18]). These considerations deserve further investigations.

References

[1] Bahareh Afshari, Sebastian Enqvist, and Graham E. Leigh. Cyclic proofs for the first-order $\mathrm{\mu}$ -calculus. Log. J. IGPL, 32(1):1–34, 2024. 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] Bahareh Afshari and Graham E. Leigh. Lyndon interpolation for modal $\mu$ -calculus. In Language, Logic, and Computation: 13th International Tbilisi Symposium, TbiLLC 2019, Batumi, Georgia, September 16–20, 2019, Revised Selected Papers, pages 197–213, Berlin, Heidelberg, 2019. Springer-Verlag. doi:10.1007/978-3-030-98479-3_10.
[4] Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. Uniform interpolation from cyclic proofs: The case of modal $\mu$ -calculus. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, pages 335–353, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-86059-2_20.
[5] Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. Math. Struct. Comput. Sci., 34(7):552–577, 2024. doi:10.1017/S0960129524000070.
[6] Stefano Berardi and Makoto Tatsuta. Classical system of martin-löf’s inductive definitions is not equivalent to cyclic proof system. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 301–317, 2017. doi:10.1007/978-3-662-54458-7_18.
[7] Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. 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.8005114.
[8] James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, pages 78–92. Springer, 2005. doi:10.1007/11554554_8.
[9] James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 131–146. Springer, 2011. doi:10.1007/978-3-642-22438-6_12.
[10] James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 51–62. IEEE Computer Society, 2007. doi:10.1109/LICS.2007.16.
[11] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput., 21(6):1177–1216, 2011. doi:10.1093/LOGCOM/EXQ052.
[12] Gianluca Curzi and Anupam Das. Computational expressivity of (circular) proofs with fixed points. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175772.
[13] Gianluca Curzi and Lukas Melgaard. Cyclic proof theory of positive inductive definitions, 2025. doi:10.48550/arXiv.2507.13057.
[14] Anupam Das. On the logical complexity of cyclic arithmetic. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. doi:10.23638/LMCS-16(1:1)2020.
[15] Anupam Das. On the logical strength of confluence and normalisation for cyclic proofs. In Naoki Kobayashi, editor, FSCD ’21, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 29:1–29:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.29.
[16] Anupam Das and Lukas Melgaard. Cyclic proofs for arithmetical inductive definitions. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 27:1–27:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.FSCD.2023.27.
[17] Jacobus W de Bakker and Dana Scott. A theory of programs. In IBM seminar, Vienna, 1969.
[18] Solomon Feferman, W Sieg, and W Buchholz. Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Springer, 1981.
[19] Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The logical strength of Büchi’s decidability theorem. Log. Methods Comput. Sci., 15(2), 2019. doi:10.23638/LMCS-15(2:16)2019.
[20] Graham E. Leigh and Dominik Wehr. From GTC to : Generating reset proof systems from cyclic proof systems. Ann. Pure Appl. Log., 175(10):103485, 2024. doi:10.1016/J.APAL.2024.103485.
[21] Robert S. Lubarsky. $\mu$ -definable sets of integers. Journal of Symbolic Logic, 58:291–313, 1993. doi:10.2307/2275338.
[22] Johannes Marti and Yde Venema. A focus system for the alternation-free $\mu$ -calculus. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, pages 371–388, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-86059-2_22.
[23] Michael Möllerfeld. Generalized inductive definitions. PhD thesis, University of Münster, Germany, 2003. URL: https://nbn-resolving.org/urn:nbn:de:hbz:6-85659549572.
[24] 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.
[25] Michael Rathjen. Recent advances in ordinal analysis: $\Pi^{1}_{2}$ -CA and related systems. Bulletin of Symbolic Logic, 1(4):468–485, 1995. doi:10.2307/421132.
[26] Reuben N. S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 53–65. ACM, 2017. doi:10.1145/3018610.3018623.
[27] Harold Schellinx. Basic proof theory, A.S. troelstra and h. schwichtenberg. J. Log. Lang. Inf., 7(2):221–223, 1998. doi:10.1023/A:1008226228293.
[28] Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, FOSSACS ’17, Held as Part of ETAPS ’17, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283–300, 2017. doi:10.1007/978-3-662-54458-7_17.
[29] Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer, 1999.
[30] Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: Circular and tree-shaped proofs in the $\mathrm{\mu}$ -calculus. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 425–440. Springer, 2003. doi:10.1007/3-540-36576-1_27.
[31] Christoph Sprenger and Mads Dam. On global induction mechanisms in a $\mathrm{\mu}$ -calculus with explicit approximations. RAIRO Theor. Informatics Appl., 37(4):365–391, 2003. doi:10.1051/ita:2003024.
[32] Thomas Studer. On the proof theory of the modal mu-calculus. Stud Logica, 89(3):343–363, 2008. doi:10.1007/s11225-008-9133-6.
[33] Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 491–508. Springer, 2017. doi:10.1007/978-3-319-63046-5_30.
[34] Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. J. Autom. Reason., 64(3):555–578, 2020. doi:10.1007/s10817-019-09532-0.
[35] Sergei Tupailo. On the intuitionistic strength of monotone inductive definitions. J. Symb. Log., 69(3):790–798, 2004. doi:10.2178/jsl/1096901767.

[bib.bib1] [1] Bahareh Afshari, Sebastian Enqvist, and Graham E. Leigh. Cyclic proofs for the first-order $\mathrm{\mu}$ -calculus. Log. J. IGPL, 32(1):1–34, 2024. doi:10.1093/JIGPAL/JZAC053.

[bib.bib2] [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.

[bib.bib3] [3] Bahareh Afshari and Graham E. Leigh. Lyndon interpolation for modal $\mu$ -calculus. In Language, Logic, and Computation: 13th International Tbilisi Symposium, TbiLLC 2019, Batumi, Georgia, September 16–20, 2019, Revised Selected Papers, pages 197–213, Berlin, Heidelberg, 2019. Springer-Verlag. doi:10.1007/978-3-030-98479-3_10.

[bib.bib4] [4] Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. Uniform interpolation from cyclic proofs: The case of modal $\mu$ -calculus. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, pages 335–353, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-86059-2_20.

[bib.bib5] [5] Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. Math. Struct. Comput. Sci., 34(7):552–577, 2024. doi:10.1017/S0960129524000070.

[bib.bib6] [6] Stefano Berardi and Makoto Tatsuta. Classical system of martin-löf’s inductive definitions is not equivalent to cyclic proof system. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 301–317, 2017. doi:10.1007/978-3-662-54458-7_18.

[bib.bib7] [7] Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. 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.8005114.

[bib.bib8] [8] James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, pages 78–92. Springer, 2005. doi:10.1007/11554554_8.

[bib.bib9] [9] James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 131–146. Springer, 2011. doi:10.1007/978-3-642-22438-6_12.

[bib.bib10] [10] James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 51–62. IEEE Computer Society, 2007. doi:10.1109/LICS.2007.16.

[bib.bib11] [11] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput., 21(6):1177–1216, 2011. doi:10.1093/LOGCOM/EXQ052.

[bib.bib12] [12] Gianluca Curzi and Anupam Das. Computational expressivity of (circular) proofs with fixed points. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175772.

[bib.bib13] [13] Gianluca Curzi and Lukas Melgaard. Cyclic proof theory of positive inductive definitions, 2025. doi:10.48550/arXiv.2507.13057.

[bib.bib14] [14] Anupam Das. On the logical complexity of cyclic arithmetic. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. doi:10.23638/LMCS-16(1:1)2020.

[bib.bib15] [15] Anupam Das. On the logical strength of confluence and normalisation for cyclic proofs. In Naoki Kobayashi, editor, FSCD ’21, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 29:1–29:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.29.

[bib.bib16] [16] Anupam Das and Lukas Melgaard. Cyclic proofs for arithmetical inductive definitions. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 27:1–27:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.FSCD.2023.27.

[bib.bib17] [17] Jacobus W de Bakker and Dana Scott. A theory of programs. In IBM seminar, Vienna, 1969.

[bib.bib18] [18] Solomon Feferman, W Sieg, and W Buchholz. Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Springer, 1981.

[bib.bib19] [19] Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The logical strength of Büchi’s decidability theorem. Log. Methods Comput. Sci., 15(2), 2019. doi:10.23638/LMCS-15(2:16)2019.

[bib.bib20] [20] Graham E. Leigh and Dominik Wehr. From GTC to : Generating reset proof systems from cyclic proof systems. Ann. Pure Appl. Log., 175(10):103485, 2024. doi:10.1016/J.APAL.2024.103485.

[bib.bib21] [21] Robert S. Lubarsky. $\mu$ -definable sets of integers. Journal of Symbolic Logic, 58:291–313, 1993. doi:10.2307/2275338.

[bib.bib22] [22] Johannes Marti and Yde Venema. A focus system for the alternation-free $\mu$ -calculus. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, pages 371–388, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-86059-2_22.

[bib.bib23] [23] Michael Möllerfeld. Generalized inductive definitions. PhD thesis, University of Münster, Germany, 2003. URL: https://nbn-resolving.org/urn:nbn:de:hbz:6-85659549572.

[bib.bib24] [24] 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.

[bib.bib25] [25] Michael Rathjen. Recent advances in ordinal analysis: $\Pi^{1}_{2}$ -CA and related systems. Bulletin of Symbolic Logic, 1(4):468–485, 1995. doi:10.2307/421132.

[bib.bib26] [26] Reuben N. S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 53–65. ACM, 2017. doi:10.1145/3018610.3018623.

[bib.bib27] [27] Harold Schellinx. Basic proof theory, A.S. troelstra and h. schwichtenberg. J. Log. Lang. Inf., 7(2):221–223, 1998. doi:10.1023/A:1008226228293.

[bib.bib28] [28] Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, FOSSACS ’17, Held as Part of ETAPS ’17, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283–300, 2017. doi:10.1007/978-3-662-54458-7_17.

[bib.bib29] [29] Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer, 1999.

[bib.bib30] [30] Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: Circular and tree-shaped proofs in the $\mathrm{\mu}$ -calculus. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 425–440. Springer, 2003. doi:10.1007/3-540-36576-1_27.

[bib.bib31] [31] Christoph Sprenger and Mads Dam. On global induction mechanisms in a $\mathrm{\mu}$ -calculus with explicit approximations. RAIRO Theor. Informatics Appl., 37(4):365–391, 2003. doi:10.1051/ita:2003024.

[bib.bib32] [32] Thomas Studer. On the proof theory of the modal mu-calculus. Stud Logica, 89(3):343–363, 2008. doi:10.1007/s11225-008-9133-6.

[bib.bib33] [33] Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 491–508. Springer, 2017. doi:10.1007/978-3-319-63046-5_30.

[bib.bib34] [34] Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. J. Autom. Reason., 64(3):555–578, 2020. doi:10.1007/s10817-019-09532-0.

[bib.bib35] [35] Sergei Tupailo. On the intuitionistic strength of monotone inductive definitions. J. Symb. Log., 69(3):790–798, 2004. doi:10.2178/jsl/1096901767.

Cyclic Proof Theory of Generalised Inductive Definitions

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Theorem 1.

Outline of the paper.

Preliminary definitions.

Definition 2 (Trees).

Definition 3 (Rules and (co)derivations).

2 Arithmetical theories of generalised inductive definitions

2.1 Language of arithmetic with fixed points

Definition 4 (Terms and (pre-)formulas).

Example 5 (Some fixed point formulas).

2.2 Interpreting generalised inductive definitions

Proposition 6 (Knaster-Tarski).

Definition 7 (Standard model and satisfaction).

Example 8.

2.3 The theory 𝝁⁢𝗣𝗔

Definition 9 (Sequent calculus for μ⁢𝖯𝖠).

▶ Remark 10 (Post-fixed points and numerical induction).

3 Cyclic proofs for generalised inductive definitions

3.1 Progressivity and cyclic proofs

Definition 11 (Coderivations).

Definition 12 (Traces and progress).

Definition 13 (Progressing and cyclic proofs).

Example 14.

3.2 Simulating inductive proofs

Theorem 15 (Induction to cycles).

Proof sketch.

4 A reset proof system for 𝝁⁢𝗣𝗔

4.1 Syntax and semantics of 𝗖⁢𝝁⁢𝗣𝗔𝐚𝐧𝐧

Definition 16 (Extended sequents).

4.2 Annotated coderivations and reset proofs

Definition 17 (Annotated coderivations).

Definition 18 (Reset proofs).

Example 19.

Lemma 20 (Local soundness).

Theorem 21 (Soundness).

Proof.

5 From progressing proofs to reset proofs

Definition 22 (Ordinal assignments).

Example 23.

Definition 24 (Translation).

Theorem 25.

Proof idea.

Corollary 26 (Soundness for 𝖢⁢μ⁢𝖯𝖠).

Proof.

6 Formalising the soundness argument in 𝚷𝟐𝟏⁢-⁢𝗖𝗔𝟎

6.1 Theories of second-order arithmetic

Theorem 27.

6.2 Countable orders in 𝚷𝟐𝟏⁢-⁢𝗖𝗔𝟎

Proposition 28.

6.3 Knaster-Tarski Theorem and approximants

Definition 29 (Approximants).

Proposition 30 (Recursion and Knaster-Tarski).

Corollary 31.

6.4 Interpreting 𝗖⁢𝝁⁢𝗣𝗔 and 𝗖⁢𝝁⁢𝗣𝗔𝐚𝐧𝐧 in 𝚷𝟐𝟏⁢-⁢𝗖𝗔𝟎

Theorem 32.

Theorem 33 (Implied by [23]).

6.5 Formalizing 𝗖⁢𝝁⁢𝗣𝗔𝐚𝐧𝐧 satisfaction in 𝚷𝟐𝟏⁢-⁢𝗖𝗔𝟎

Theorem 34 (Reflection).

Theorem 35 (Formalised satisfaction).

6.6 Formalizing soundness for 𝗖⁢𝝁⁢𝗣𝗔𝐚𝐧𝐧

Lemma 36.

Proof.

Theorem 37 (Formalising soundness).

Proof.

7 Conclusions and future works

References

2.3 The theory $\mu\mathsf{PA}$

Definition 9 (Sequent calculus for $\mu\mathsf{PA}$ ).

$\blacktriangleright$ Remark 10 (Post-fixed points and numerical induction).

4 A reset proof system for $\mu\mathsf{PA}$

4.1 Syntax and semantics of $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$

Corollary 26 (Soundness for $\mathsf{C}\mu\mathsf{PA}$ ).

6 Formalising the soundness argument in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

6.2 Countable orders in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

6.4 Interpreting $\mathsf{C}\mu\mathsf{PA}$ and $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

6.5 Formalizing $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$ satisfaction in $\Pi^{1}_{2}\text{-}\mathsf{CA}_{0}$

6.6 Formalizing soundness for $\mathsf{C}\mu\mathsf{PA}_{\mathrm{ann}}$