| Sbornik: Mathematics |
|
|
|
|
|
Fragments of arithmetic and cyclic proofs L. D. Beklemisheva, D. S. Shamkanova, I. N. Smirnovabc a Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia b Ivannikov Institute for System Programming of the Russian Academy of Science, Moscow, Russia c Moscow Institute of Physics and Technology, Dolgoprudny, Moscow Region, Russia
§ 1. IntroductionCyclic proof systems are well adapted for the axiomatization of logics enhanced with fixed points and recursion or induction mechanisms. Such systems are known for extensions of linear logic with fixed points [3], [29], for the modal $\mu$-calculus [28], [13], [17], [44], [22], [43], for the separation logic [9], [24], as well as for the Gödel–Löb provability logic [35] and arithmetic [41], [6]. They seem to be promising for tasks of proof search, since they allow one, in a certain sense, to search simultaneously for more complex types of induction, which can result in shorter proofs. So the task of guessing the induction formula is replaced by the task of detecting possible cycles in a proof. Brotherston with coauthors developed a generic theorem prover Cyclist based on the cyclic proof format [10]. Similar but weaker mechanisms are also known in the context of resolution-based first-order provers (such as Vampire), when these are enhanced by some basic forms of induction (see the analysis by Hetzl and Vierling [20] of some of such systems in terms of so-called clause set cycles). Since the cyclic proof format is relatively new, there is also a lot of research activity on the theoretical side of such proofs and non-well-founded proofs in general. Researchers are attracted both by the semantic aspect of non-well-founded and cyclic systems [32], [18], [37] and by prospects for studying them from the point of view of structural proof theory [3], [16], [33], [30], [40], [38]. In addition, cyclic systems are used to obtain interpolation properties [35], [2], [1], and also to prove realization theorems that relate modal and justification logics [36], [39]. A special and interesting direction is the study of cyclic proofs in the context of arithmetic [41], [6], [14], [25], [12] and first-order logic with inductive definitions [8], [11], [7]. The goal of this paper is to design an alternative cyclic proof system for Peano arithmetic that can be simpler than the existing ones and well adapted both for proof analysis and for automatizing inductive proof search. In addition, we will show how various traditional subsystems of Peano arithmetic defined by restricted forms of induction can be represented as fragments of the proposed system. A cyclic proof is a derivation tree where hypotheses (leaves) are axioms, as in the usual proof, or are connected by ‘back-links’ with identical formulae or subsequents occurring below in the proof. Traversing such a proof backwards from conclusions to premisses may result in infinite loops. Therefore, in order for such a proof figure to correspond to a correct argument (rather than a vicious circle), one imposes a global soundness condition, which, in the case of arithmetic, can be formulated in terms of the variables occurring in the proof. Details of such conditions can vary, but they can roughly be stated as requiring that every path in an infinite ‘unfolding’ of a cyclic proof goes infinitely often through a rule (called the progress point) that ensures the descent of the parameters. This allows explicit induction rules in such a system to be abandoned in favour of simpler case rules (which correspond to the axiom that every natural number is either $0$ or a successor). The proofs using the induction axioms can be modelled by rather simple cyclic proofs where back-links are independent from one another. However, more complex cyclic proofs can be difficult to transform into usual induction proofs, and establishing exact correspondence with traditional Hilbert or Gentzen-style systems is often quite involved. There are three systems related to first-order cyclic arithmetic in the current literature.
In this paper we also deal with a cyclic proof system for the first-order arithmetic. However, there are two main aspects in which the proposed system differs from those in the literature. Firstly, the soundness conditions in our system are simpler than those of $\mathrm{CA}$ and $\mathrm{C}\Sigma_n$ which hopefully makes both the proof analysis and the proof search more straightforward. Secondly, and more importantly, our proof system differs from the others in the variable discipline. In other words, our system is based on sequents annotated with finite sets of individual variables, which allows us to impose concisely various conditions on cyclic proofs. As a result, by suitable restrictions of the quantifier complexity of formulae in the proof we obtain the familiar series of fragments of $\mathrm{PA}$ that are important in the metamathematics of Peano arithmetic, such as the fragments $\mathit{I\Sigma}_n$ defined by $\Sigma_n$-induction schemata and fragments $\mathit{I\Sigma}_n^R$ axiomatized by $\Sigma_n$-induction rules. The systems $\mathrm{C}\Sigma_n$ studied in [14] are obtained by restricting the complexity of all formulae in a $\mathrm{CA}$ proof to the class $\Sigma_n$ or $\Pi_n$. However, under such a restriction the set of provable statements will not, in general, be closed under logical consequence, since the complexity of cuts is also restricted to $\Sigma_n$ or $\Pi_n$. To deal with this problem, Das defines $\mathrm{C}\Sigma_n$ as the closure under the ordinary logical consequence of the set of formulae provable by $\Sigma_n$-restricted cyclic proofs. He then shows that the resulting theory corresponds to the fragment of Peano arithmetic defined by all $\Pi_{n+1}$-consequences of $\Sigma_{n+1}$-induction schema. In particular, the theory $\mathrm{C}\Sigma_0$ can be axiomatized by the set of $\Pi_1$-consequences of $\mathit{I\Sigma}_1$, which is of the consistency strength of $\mathit{I\Sigma}_1$ yet strictly weaker than the primitive recursive arithmetic PRA and the equivalent fragment $\mathit{I\Sigma}_1^R$ in the language of $\mathrm{PA}$. An explicit Hilbert-style formulation of the theory axiomatized by $\Pi_{n+1}$-consequences of $\mathit{I\Sigma}_{n+1}$ is known. By the so-called Schmerl formula (see [5], Theorem 4) it is deductively equivalent to the uniform $\Pi_{n+1}$-reflection schema over $\mathrm{EA}$ iterated $\omega^\omega$ times. This paper arose out of the natural question, inspired by the work of Das, which restrictions on cyclic proofs would yield systems deductively equivalent to the more fundamental fragments of Peano arithmetic such as $\mathit{I\Sigma_n}$ or $\mathit{I\Sigma_n^R}$. Our methods are considerably simpler than those of the previous papers. In particular, we use elementary syntactic arguments without any references to Büchi automata. This can be explained by the more explicit character of our notion of cyclic proof. The plan of the paper is as follows. In § 2 we introduce necessary preliminaries on first-order arithmetic and specify a Tait-style sequent calculus for Robinson’s arithmetic $\mathsf{Q}$. In § 3 we introduce non-well-founded proof systems and show that they are sufficiently strong to prove all true arithmetical sentences. In § 4 we define annotated proofs and cyclic proofs. Finally, in §§ 5 and 6, we relate cyclic systems to the main fragments of Peano arithmetic: $\mathit{I\Sigma_n}$, $\mathit{I\Pi}^R_{n}$ and $\mathit{I\Sigma}_n^R$. § 2. PreliminariesWe assume the reader’s familiarity with the standard Hilbert-style axiomatization of first-order Peano arithmetic (see [19], for example). The language of Peano arithmetic has the constant $0$, the function symbols $s$ (successor), $+$ and $\cdot$ , and the relation symbol $=$ . The formula $x\leqslant y$ is an abbreviation for $\exists\,z\ (z+x=y)$. Bounded quantifiers are abbreviations for
$$
\begin{equation*}
\begin{gathered} \, \forall\, y \leqslant t \ \varphi := \forall\, y \ (y \leqslant t \to \varphi) \quad\text{and}\quad \exists\, y \leqslant t \ \varphi := \exists\, y \ (y \leqslant t \wedge \varphi), \end{gathered}
\end{equation*}
\notag
$$
where $t$ is a term and $y$ does not occur in $t$. A bounded formula is an arithmetical formula built from atomic formulae by logical connectives and bounded quantifiers alone. The set of all such formulae is denoted by $\Delta_0$. The classes of $\Sigma_n$ and $\Pi_n$ formulae are inductively defined as follows. We let $\Sigma_0 = \Pi_0=\Delta_0$. An arithmetical formula is $\Sigma_{n+1}$ ($\Pi_{n+1}$) if it is obtained from $\Pi_n$ ($\Sigma_n$) formulae using existential (universal) quantifiers and positive propositional connectives ($\land$ and $\lor$). Robinson’s arithmetic $\mathsf{Q}$ is axiomatized by the axioms and rules of the first-order predicate logic with equality and also by (the universal closures of) the following basic axioms:
Peano arithmetic $\mathrm{PA}$ is axiomatized by $\mathsf{Q}$ in combination with the induction schema
$$
\begin{equation*}
\mathrm{(Ind)} \qquad \varphi(0)\land \forall\,x\ (\varphi(x)\to \varphi(s(x))) \to \forall\,x\ \varphi(x)
\end{equation*}
\notag
$$
for all formulae $\varphi$ (possibly containing free variables different from $x$). The theories $\mathit{I\Sigma}_n$ ($\mathit{I\Pi}_n$) are obtained by extending $\mathsf{Q}$ by the induction schema $\mathrm{(Ind)}$ for all $\Sigma_n$ (respectively, $\Pi_n$) formulae $\varphi$. It is well known that $\mathit{I\Sigma}_n$ and $\mathit{I\Pi}_n$ are deductively equivalent. The theories $\mathit{I\Sigma}_n$ constitute a strictly increasing hierarchy of fragments of $\mathrm{PA}$; the union of this hierarchy is $\mathrm{PA}$ itself. For all $n>0$ the theories $\mathit{I\Sigma}_n$ are finitely axiomatizable.1 The induction rule is the inference rule
$$
\begin{equation*}
(\mathrm{IR})\qquad \frac{\varphi(0) \quad \forall\,x\ (\varphi(x)\to \varphi(s(x)))}{\forall\,x\ \varphi(x)}.
\end{equation*}
\notag
$$
It is well known that the closure of $\mathsf{Q}$ under $(\mathrm{IR})$ is equivalent to Peano arithmetic. We let $\mathit{I\Sigma}_n^R$ ($\mathit{I\Pi}_n^R$) denote the theory axiomatized over $\mathsf{Q}$ by $(\mathrm{IR})$ restricted to $\Sigma_n$ ($\Pi_n$) formulae $\varphi$. It is known that $\mathit{I\Sigma}_n^R$ is deductively equivalent to $\mathit{I\Pi}_{n+1}^R$ and strictly weaker than $\mathit{I\Sigma}_n$, for $n>0$. For $n=0$ the fragment $I\Delta_0^R$ is equivalent to $I\Delta_0$. None of the theories $\mathit{I\Sigma}_n^R$ for $n>0$ is finitely axiomatizable, and it is known that $\mathit{I\Sigma}_n$ conservatively extends $\mathit{I\Sigma}_n^R$ for $\Pi_{n+1}$ sentences. See [4] for more information on the fragments of arithmetic axiomatized by induction rules. Next we introduce a proof system $\mathsf{SQ}$ for Robinson’s arithmetic $\mathsf{Q}$ which is based on a one-sided variant of a sequent calculus for predicate logic due to Tait (see [34]). We partly follow Negri and von Plato’s approach to sequent calculi for axiomatic theories (see [27] or [26], Ch. 6) to incorporate the rules for the equality axioms and the mathematical axioms of $\mathsf{Q}$. Recall that arithmetical terms are built from a countable set of individual variables $\mathrm{Var}=\{x_0, x_1, x_2,\dots\}$ and the constant $0$ by means of the unary function symbol $s$ and the binary symbols $+$ and $\cdot$ in a standard way. Arithmetical formulae, denoted by $\varphi$, $\psi$ and so on, are built up as follows:
$$
\begin{equation*}
\varphi ::= t=t \mid t\neq t \mid (\varphi \wedge \varphi) \mid (\varphi \vee \varphi) \mid \forall\, y\ \varphi \mid \exists\, y\ \varphi ,
\end{equation*}
\notag
$$
where $t$ denotes arithmetical terms and $y$ represents an arbitrary individual variable. The negation $\overline{\varphi}$ of a formula $\varphi$ in Tait calculus is a syntactic operation defined by the law of double negation, de Morgan’s laws and the duality laws for quantifiers, that is, we inductively define:
$$
\begin{equation*}
\begin{gathered} \, \overline{t_0=t_1} := t_0\neq t_1, \qquad \overline{t_0\neq t_1} := t_0=t_1, \\ \overline{(\varphi_0 \wedge \varphi_1)} := (\overline{\varphi_0} \vee \overline{\varphi_1}), \qquad \overline{(\varphi_0 \vee \varphi_1)} := ( \overline{\varphi_0} \wedge \overline{\varphi_1}), \\ \overline{\forall\, y\ \varphi} := \exists\, y\ \overline{\varphi}, \qquad \overline{\exists\, y\ \varphi} := \forall\, y\ \overline{\varphi}. \end{gathered}
\end{equation*}
\notag
$$
Note that the operation of negation is idempotent. In other words, $\overline{\overline{\varphi}}$ is equal to $\varphi$ for any formula $\varphi$. We further fix
$$
\begin{equation*}
\top := 0=0, \quad \bot:= 0\neq 0, \quad \varphi\to \psi := \overline{\varphi} \vee \psi\quad\text{and} \quad \varphi \leftrightarrow \psi := (\varphi\to \psi) \wedge (\psi\to \varphi).
\end{equation*}
\notag
$$
We define sequents as finite multisets of arithmetical formulae. For a sequent $\Gamma$, its intended interpretation as a formula is $\bigvee \Gamma$, where $\bigvee \varnothing := \bot$. Recall that sequents are often written without any curly braces, and the comma in the expression $\Gamma, \Delta$ means the multiset union. The initial sequents and inference rules of $\mathsf{SQ}$ are as follows: Here $\psi [y\mapsto t]$ ($\Gamma [y\mapsto t]$) denotes the formula (sequent) obtained from $\psi$ (from $\Gamma$) by replacing all free occurrences of $y$ in $\psi$ (in formulae of $\Gamma$, respectively) by the term $t$. As usual, we require that no variable of $t$ becomes bound after the replacement. In what follows, if the variable $y$ is clear from the context, we often write $\psi [y\mapsto t]$ and $\Gamma [y\mapsto t]$ as $\psi (t)$ and $\Gamma (t)$, respectively.For the inference rules $(\wedge)$, $(\vee)$, $(\forall)$ and $(\exists)$ the formula explicitly displayed in the conclusion of a rule is called the principal formula of the corresponding inference. For the rules $(\mathsf{\forall})$ (or $\mathsf{(case)}$) $z$ (or $y$, respectively) is called the active variable of the given inference. The rules $(\land)$, $(\lor)$, $(\exists)$, $(\forall)$, $(\mathsf{weak})$ and $(\mathsf{cut})$ are the standard rules of the Tait calculus. The rules $(\mathsf{ref})$ and $(\mathsf{rep})$ account for the equality axioms. The rest of the rules and $(\mathsf{ax}_s)$ correspond to the mathematical axioms of $\mathsf{Q}$. We also emphasize, though it is inessential for what follows, that we have chosen this slightly uncommon formulation of the arithmetical rules of $\mathsf{SQ}$ since the proofs constructed according to these rules, excluding the rule $\mathsf{(case)}$, enjoy cut elimination [27], [26]. The following lemma is standard, so we leave it essentially without proof. Using Lemma 2.1 it is routine to prove that the following proposition holds. Proposition 2.2. (1) If $\mathsf{Q}\vdash \varphi$, then $\mathsf{SQ}\vdash \varphi$; (2) If $\mathsf{SQ}\vdash \Gamma$, then $\mathsf{Q}\vdash \bigvee\Gamma$. We only notice that the rule (case) is equivalent to axiom (2) of $\mathsf{Q}$ modulo the other rules. § 3. Non-well-founded proofsIn this section we introduce a series of arithmetical sequent calculi $\mathsf{S}_n$, which allow non-well-founded proofs. These systems have the axioms and inference rules of $\mathsf{SQ}$, differing only in the notion of proof. For brevity, by the tail of an infinite sequence $(a_i)_{i\in \mathbb N}$ we mean below an arbitrary subsequence of the form $(a_i)_{i\geqslant n}$. Definition 3.1. An (unrestricted) $\infty$-proof is a possibly infinite tree whose nodes are marked by sequents and that is constructed according to the rules of the calculus $\mathsf{SQ}$. In addition, every leaf in an $\infty$-proof is marked by an initial sequent of $\mathsf{SQ}$ and, for every infinite branch in it, there is a tail of the branch satisfying the following conditions: Note that in the above definition we do not require that the variable $y$ occurs freely in each sequent of the tail. Moreover, there can be infinitely many sequents of this tail where $y$ does not appear free. Definition 3.2. An $\infty$-proof is $\Pi_n$-restricted if every infinite branch in it has a tail satisfying conditions (a)–(c) of Definition 3.1 and the following conditions: As expected, the following soundness lemma holds for unrestricted $\infty$-proofs. Lemma 3.3. If $\Gamma$ has an $\infty$-proof, then $\mathbb{N}\models v(\bigvee \Gamma)$ for all assignments $v\colon \mathrm{Var}\to \mathbb{N}$. Proof. Assume, towards a contradiction, that $v(\bigvee\Gamma)$ is false for some $v$. In this case $\Gamma$ cannot be an axiom of $\mathsf{SQ}$. All the inference rules of $\mathsf{SQ}$ preserve the validity of sequents in $\mathbb{N}$. Hence there exists an infinite branch $P$ in the proof tree such that all sequents in $P$ are not valid.
We construct $P$ inductively by working from the conclusion to the premisses of the rules. Denote by $\Gamma_i$ the $i$th sequent in $P$ counting from $\Gamma_0:=\Gamma$. Let $v_i$ be the assignment such that Consider the tail $T$ of the branch $P$ satisfying conditions (a)–(c) of Definition 3.1, and let $y$ be the variable active in infinitely many applications of $\mathsf{(case)}$ in $T$ according to (c). Taking a shorter tail if necessary we can assume that $T$ begins with an application of $\mathsf{(case)}$ with $y$ active, hence by condition (b) $y$ is not active in applications of $(\forall)$ anywhere in $T$. It follows that the assignment $v_i(y)$ can only be changed by applications of the rule $\mathsf{(case)}$ and is weakly decreasing with $i$, and $T$ goes through infinitely many of such applications. Therefore, the sequence of natural numbers $v_0(y), v_1(y), v_2(y),\dots$ contains an infinite decreasing subsequence, which is a contradiction. The lemma is proved. Our next observation shows that the set of sequents having a $\Pi_n$-restricted $\infty$-proof is closed under a version of the $\Pi_n$-restricted $\omega$-rule with side formulae. We denote by $\overline k$ the numeral for the number $k\in\mathbb{N}$, that is, the term $s(s(\dots(0)\dots))$ ($k$ symbols $s$). Lemma 3.4. Suppose that for each $k$ $\pi_k$ is an $\infty$-proof of $\Gamma,\varphi(\overline k)$. Then there is an $\infty$-proof $\pi$ of $\Gamma,\varphi(x)$ where $x\notin \mathit{FV}(\Gamma)$. Moreover, if $\varphi$ is $\Pi_n$ and all the $\pi_k$ are $\Pi_n$-restricted, then so is $\pi$. Proof. Let $x\notin\mathit{FV}(\Gamma)$. If $x$ does not actually occur free in $\varphi(x)$, the claim is trivial. Otherwise, the proof $\pi$ looks as follows: Observe that there is one new infinite branch in $\pi$, the rightmost one, and it clearly satisfies the necessary conditions.
The lemma is proved. From this lemma we obtain that $\infty$-proofs are sufficient to prove all true arithmetical sentences, even under the strongest assumption of being $\Pi_0$-restricted. We call a sequent $\Gamma$ true if $\Gamma$ is a set of sentences such that $\mathbb{N}\models\bigvee\Gamma$. Proof. Within this proof we say that a sequent is provable if it has a $\Pi_0$-restricted $\infty$-proof. By induction on $n$ we show that every true sequent $\Gamma\subseteq \Pi_{2n}$ is provable. By weakening, it is sufficient to prove that every true $\Pi_{2n}$-sentence is provable.
For the case $n=0$ we just recall that $\mathsf{Q}$ proves every true bounded sentence and apply Proposition 2.2. Assume the claim holds for $n$, which we call the main induction hypothesis. We show that every true $\Pi_{2n+2}$ sentence is provable by a secondary induction on its syntactic structure. First, as the secondary induction basis, we prove that every true $\Sigma_{2n+1}$ sentence is provable. We argue by subinduction on the syntactic structure of such a sentence. For $\Pi_{2n}$ sentences this holds by the main induction hypothesis. For sentences obtained by conjunction, disjunction or an existential quantifier the claim follows easily using the inference rules $(\land)$, $(\lor)$, $(\exists)$ and ($\mathsf{weak}$). Second, as the secondary induction step, if $\Pi_{2n+2}$ sentences $\varphi$ and (or) $\psi$ are provable, then so are $\varphi\land\psi$ (respectively, $\varphi\lor\psi$), by the rules $(\land)$, $(\lor)$ and ($\mathsf{weak}$). Finally, we consider a true $\Pi_{2n+2}$ sentence of the form $\forall\,x\ \psi(x)$ with $\psi$ in $\Pi_{2n+2}$. We must show that $\forall\,x\ \psi(x)$ is provable. First, we observe that $\mathsf{SQ}$ proves the sequent
$$
\begin{equation*}
\overline{\psi(\overline m)}, x\neq \overline m, \psi(x),
\end{equation*}
\notag
$$
which is an instance of the equality schema valid in predicate logic. By the secondary induction hypothesis, for each $m$, the formula $\psi(\overline m)$ is provable. Hence by $\mathsf{(cut)}$, for each $m$ we have a proof of $x\neq \overline m, \psi(x)$. Applying Lemma 3.4 we obtain a proof of $x\neq z,\psi(x)$, where $z$ is a fresh variable. (The proof is $\Pi_0$-restricted since $x\neq z$ is $\Pi_0$.) It follows that $\forall\,z\ x\neq z,\psi(x)$ is provable, hence by $\mathsf{(cut)}$ with the formula $\exists\,z\ x=z$ , which is provable in predicate logic, we obtain $\psi(x)$, so $\forall\,x\ \psi (x)$ follows by $(\forall)$.
The lemma is proved. We conclude that the notion of $\Pi_0$-restricted $\infty$-proof is as powerful as the (unrestricted) $\omega$-proof in first order arithmetic. Now we introduce a series of arithmetical sequent calculi $\mathsf{S}_n$. In what follows we also call $\Pi_{n+1}$-restricted $\infty$-proofs $\infty$-proofs of $\mathsf{S}_n$. However, in order to obtain notions of proof adequate for axiomatizable theories, such as Peano arithmetic, we will restrict the set of $\infty$-proofs to regular ones. An $\infty$-proof is called regular if it contains only finitely many nonisomorphic subtrees with respect to the marking of sequents. We say that a sequent $\Gamma$ is provable in $\mathsf{S}_n$ if there is a regular $\infty$-proof of $\mathsf{S}_n$ with the root marked by $\Gamma$. Consider an example of an infinite regular $\infty$-proof of $\mathsf{S}_n$: where the subtree $\pi$ is isomorphic to the whole $\infty$-proof, $\sigma_0$ and $\sigma_1$ are given by Lemma 2.1, $\psi$ is $\overline{\forall\, x \ (\varphi (x) \to \varphi (s(x)))}$ and $\varphi$ is an arbitrary $\Pi_{n+1}$-formula such that $x\in \mathit{FV}(\varphi)$. Here the unique infinite branch passes infinitely many times through the right premiss of the rule $\mathsf{(case)}$ with active variable $x$. We immediately see that the required conditions on infinite branches hold if we view the given branch as its own tail. The above example essentially shows that any instance of $\Pi_{n+1}$-induction schema is provable in $\mathsf{S}_n$, so we immediately obtain the following result. § 4. Cyclic proofs and annotationsIn this section, in order to facilitate our treatment of provability in $\mathsf{S}_n$, we introduce annotated versions of sequents and inference rules of this calculus. We also define finite representations of regular $\infty$-proofs, called cyclic (or circular) proofs. An annotated sequent is an expression of the form $\Gamma \upharpoonright V$, where $\Gamma$ is an ordinary sequent and $V$ is a finite set of individual variables. Annotated versions of initial sequents of $\mathsf{S}_n$ are $\Gamma, t_0=t_1, t_0\neq t_1 \upharpoonright V $ and $\Gamma, s(t)\neq 0 \upharpoonright V$. Annotated versions of inference rules of $\mathsf{S}_n$, except the rules ($\wedge$), ($\forall$), $\mathsf{(case)}$ and ($\mathsf{cut}$), are obtained by annotating the premiss and the conclusion of a rule so that they have the same annotation $V$. We define annotated versions of ($\wedge$), ($\forall$) and $\mathsf{(case)}$ by and where
$$
\begin{equation*}
\begin{gathered} \, V_0 := \begin{cases} V & \text{if } \varphi \in \Pi_{n+1}, \\ \varnothing & \text{otherwise}, \end{cases} \qquad V_1 := \begin{cases} V & \text{if } \psi\in \Pi_{n+1}, \\ \varnothing & \text{otherwise}, \end{cases} \\ V_2 := \begin{cases} V & \text{if }z\notin V\text{ and }\varphi [y\mapsto z]\in \Pi_{n+1}, \\ \varnothing & \text{otherwise,} \end{cases} \end{gathered}
\end{equation*}
\notag
$$
and
$$
\begin{equation*}
V_3 := \begin{cases} V \cup \{y\} & \text{if }y\text{ occurs freely only in $\Pi_{n+1}$-formulae of }\Gamma, \\ \varnothing & \text{otherwise}. \end{cases}
\end{equation*}
\notag
$$
The annotated version of ($\mathsf{cut}$) has the form where
$$
\begin{equation*}
\begin{gathered} \, V_0 := \begin{cases} V & \text{if }\varphi \in \Pi_{n+1}, \\ \varnothing & \text{otherwise}, \end{cases}\quad\text{and} \quad V_1 := \begin{cases} V & \text{if }\overline{\varphi} \in \Pi_{n+1}, \\ \varnothing & \text{otherwise}. \end{cases} \end{gathered}
\end{equation*}
\notag
$$
An annotated $\infty$-proof of $\mathsf{S}_n$ is a (possibly infinite) tree whose nodes are marked by annotated sequents and that is constructed in accordance with the annotated versions of inference rules of $\mathsf{S}_n$. In addition, all leaves of an annotated $\infty$-proof are marked by annotated initial sequents, and every infinite branch in it must contain a tail satisfying the following conditions: (i) there are no sequents in the tail annotated with $\varnothing$ and (ii) there is a variable $y$ such that the tail passes through the right premiss of the rule $\mathsf{(case)}$ with the active variable $y$ infinitely many times. An annotated $\infty$-proof is regular if it contains only finitely many nonisomorphic subtrees with respect to annotations. Note that if we erase all annotations in an annotated $\infty$-proof of the system $\mathsf{S}_n$, then the resulting tree is a normal $\infty$-proof of the same system, that is, a $\Pi_{n+1}$-restricted $\infty$-proof. Let us prove the converse. Lemma 4.1. Suppose $\pi$ is an $\infty$-proof of $\mathsf{S}_n$ with the root marked by $\Gamma$ and $V$ is a finite set of individual variables. Then $\pi$ can be annotated so that the root of the resulting tree is marked by $\Gamma \upharpoonright V$. Moreover, the annotated $\infty$-proof obtained is finite (regular) if $\pi $ is finite (regular). Proof. Note that, for any application of an inference rule of $\mathsf{S}_n$ and any annotation of its conclusion one can annotate its premisses and obtain an application of the annotated version of the rule. Moreover, the choice of annotations for the premisses is unique.
Now assume we have an $\infty$-proof $\pi$ of $\mathsf{S}_n$ with the root marked by a sequent $\Gamma$. We annotate $\Gamma$ in $\pi$ with the set $V$ and, moving upwards away from the root, replace all applications of inference rules in $\pi$ by their annotated versions. Let us check that the resulting tree, denoted by $\pi'$, is an annotated $\infty$-proof. Consider an arbitrary infinite branch of $\pi'$. We must show that there exists a tail $T'$ of the branch satisfying the following conditions:
By the definition of an $\infty$-proof the given branch of $\pi$ contains a tail $T$ satisfying conditions (a)–(g). By condition (c) there is a variable $y$ such that the tail passes through the right premiss of the rule $\mathsf{(case)}$ with the active variable $y$ infinitely many times. If on $T$ the annotation $V$ is never empty, we put $T':=T$. Otherwise, there is a node $h$ of $T$ where $V=\varnothing$; then we can find the first application of the rule $\mathsf{(case)}$ above $h$ in $T$. By condition (a) the tail $T$ passes through the right premiss $\Delta$ of this application of the rule. We also see that the conclusion of this application is annotated by $\varnothing$ and the annotation of $\Delta$ is nonempty. We denote by $T'$ the end part of $T$ starting from $\Delta$. Note that all annotations $V$ in $T'$ consist of the active variables of applications of the rule $\mathsf{(case)}$ in $T'$: all other applications of rules do not increase the set $V$. Also, $T'$ trivially satisfies condition (ii) by (c). Next we show by induction along $T'$, moving away from the root, that all annotations $V$ in $T'$ are nonempty. We have already established the basis of induction. The induction step for all the rules except $(\land)$, $(\forall)$, $\mathsf{(cut)}$ and $\mathsf{(case)}$ is trivial ($V$ does not change). The induction step for the rules $(\land)$, $\mathsf{(cut)}$ and $\mathsf{(case)}$ follows from the $\Pi_{n+1}$-restriction of $\pi$, that is, from conditions (d)–(g). The annotation $V$ remains the same for $(\land)$ and $\mathsf{(cut)}$ and can only grow for $\mathsf{(case)}$. Finally, if a sequent is obtained by $(\forall)$ with an active variable $z$ and a principal formula $\forall\,y\ \varphi$, then by (e) the formula $\varphi[y\mapsto z]$ is $\Pi_{n+1}$. Moreover, $z\notin V$. Otherwise, there is an application of $\mathsf{(case)}$ with the active variable $z$ in $T'$ below this point, which contradicts condition (b). Hence this rule application also preserves $V$. Thus, we have established that $T'$ satisfies conditions (i) and (ii), hence $\pi'$ is an annotated $\infty$-proof. Trivially, $\pi'$ is finite if $\pi$ is finite. Now assume that the $\infty$-proof $\pi$ is regular. We show that $\pi'$ is also regular by reductio ad absurdum. Suppose there is an infinite sequence of pairwise nonisomorphic subtrees of $\pi'$. Since $\pi'$ is obtained from a regular $\infty$-proof, there are only finitely many nonisomorphic subtrees disregarding annotations. Therefore, there is a subsequence $(\mu_i)_{i\in \mathbb{N}}$ of the given sequence where all members are isomorphic disregarding annotations. We see that the roots of $(\mu_i)_{i\in \mathbb{N}}$ are marked by nonidentical annotated sequents obtained from a single unannotated sequent $\Delta$. However, any annotation occurring in $\pi'$ is a subset of the union of $V$ and the finite set of variables that are active in applications of the inference rule $\mathsf{(case)}$ in $\pi'$. Consequently, there can only be finitely many nonidentical annotated sequents obtained from $\Delta$ in $\pi'$, which is a contradiction. We conclude that the annotated $\infty$-proof $\pi'$ is regular. The lemma is proved. A cyclic annotated proof of the system $\mathsf{S}_n$ is a pair $(\kappa, d)$, where $\kappa$ is a finite tree of annotated sequents constructed in accordance with the annotated versions of inference rules of $\mathsf{S}_n$ and $d$ is a function with the following properties: the function $d$ is defined on the set of all leaves of $\kappa$ that are not marked by initial sequents; the image $d(a)$ of a leaf $a$ lies on the path from the root of $\kappa$ to the leaf $a$ and is not equal to $a$; $d(a)$ and $a$ are marked by the same sequents; all sequents on the path from $d(a)$ to $a$, including the endpoints, have the same nonempty annotation $V$; the path from $d(a)$ to $a$ intersects an application of the rule $\mathsf{(case)}$ in the right premiss. If the function $d$ is defined at a leaf $a$, then we say that the nodes $a$ and $d(a)$ are connected by a back-link. For example, consider a cyclic annotated proof of the system $\mathsf{S}_n$ where $\varphi$ is an arbitrary $\Pi_{n+1}$-formula such that $x\in \mathit{FV(\varphi)}$ and $\overline{\varphi(s(x))} \notin\Pi_{n+1}$, $\pi_0$ and $\pi_1$ are finite annotated $\infty$-proofs given by Lemmas 2.1 and 4.1, and $\psi$ is equal to $\overline{\forall\, x\ (\varphi(x)\to\varphi(s(x)))}$.Obviously, every cyclic annotated proof can be unravelled into a regular one. We prove the converse result. Lemma 4.2. Any regular annotated $\infty$-proof of the system $\mathsf{S}_n$ can be obtained by unravelling a cyclic annotated proof of the same system. Proof. Assume we have a regular annotated $\infty$-proof $\pi$ of the system $\mathsf{S}_n$. Notice that each node $a$ of this tree determines the subtree $\pi_a$ with root $a$. Let $m$ denote the number of nonisomorphic subtrees of $\pi$. Consider any simple path $a_0,a_1,\dots,a_m$ in $\pi$ that starts at the root of $\pi$ and has length $m$. This path defines the sequence of subtrees $\pi_{a_0},\pi_{a_1},\dots,\pi_{a_m}$. Since $\pi$ contains precisely $m$ nonisomorphic subtrees, the path contains a pair of different nodes $b$ and $c$ determining isomorphic subtrees $\pi_b$ and $\pi_c$. Without loss of generality assume that $c$ is farther from the root than $b$.
Note that the path from $b$ to $c$ intersects an application of the rule $\mathsf{(case)}$ in the right premiss and each sequent on the path has a nonempty annotation, because otherwise there is an infinite branch in $\pi$ that violates the corresponding condition on infinite branches of annotated $\infty$-proofs. Note also that $b$ and $c$ are annotated with the same set $V$ since $\pi_b$ and $\pi_c$ are isomorphic. From the definition of annotated inference rules we see that annotations can only weakly increase as we move along the path from $b$ to $c$. Therefore, all sequents on this path have the same nonempty annotation $V$. We cut the path $a_0,a_1,\dots,a_m$ at the node $c$ and connect $c$, which has become a leaf, with $b$ by a back-link. By applying a similar operation to each of the remaining paths of length $m $ that start at the root, we ravel the regular annotated $\infty$-proof $\pi$ into the required cyclic annotated one. The lemma is proved. § 5. From cyclic proofs to ordinary onesIn this section we prove the converse of Corollary 3.6. Proof. By Lemmas 4.1 and 4.2 it is sufficient to prove that $\mathit{I\Sigma}_{n+1}\vdash\bigvee\Gamma$ whenever there exists a cyclic annotated proof $\pi = (\kappa, d)$ of the sequents $\Gamma \upharpoonright V$ in the system $\mathsf{S}_n$ for some finite set of individual variables $V$. We proceed by induction on the number of nodes in $\pi$ (we call this main induction in what follows).
Case 1. Suppose that there are no leaves of $\pi$ connected by back-links with the root. If $\pi$ consists of a single node, then $\Gamma \upharpoonright V$ has the form $\Delta, t_0 = t_1, t_0 \neq t_1 \upharpoonright V$ or $\Delta, s(t) \neq 0 \upharpoonright V$. Therefore, we obtain $\mathit{I\Sigma}_{n+1} \vdash \bigvee \Gamma$. Otherwise, consider the last application of an inference rule in $\pi$. Since the subcases of all inference rules are similar, we consider only the subcase of the rule $\mathsf{(case)}$. Suppose $\pi$ has the form where $\pi'$ and $\pi''$ are cyclic annotated proofs in $\mathsf{S}_n$. Applying the induction hypothesis for $\pi'$ and $\pi''$, we obtain $\mathit{I\Sigma}_{n+1}\vdash \bigvee \Gamma[y \mapsto 0]$ and $\mathit{I\Sigma}_{n+1}\vdash \bigvee \Gamma[y \mapsto s(y)]$. Consequently, $\mathit{I \Sigma}_{n+1} \vdash \bigvee \Gamma$ since $\mathit{I \Sigma}_{n+1} \vdash \forall\, y\ (y = 0 \vee \exists\,z\ y = s(z))$.Case 2. Suppose that there is a leaf of $\pi = (\kappa, d)$ connected by a back-link with the root. In this case all sequents on the path from the root to the leaf have the same nonempty annotation $V$. In what follows, a directed path is a path along edges of $\kappa$ directed away from the root and back-links. Let $M$ denote the following set of nodes of $\pi$: $a \in M$ if and only if there is a finite directed path from $a$ to the root of $\pi$. Note that for any $a \in M$ the sequent of the node $a$ has the form $\Phi_a, \Psi_a \upharpoonright V$, where $\Psi_a$ is the multiset of all $\Pi_{n+1}$-formulae of the sequent. Since $V$ is the same for all $a\in M$, we consider it as fixed for the rest of the proof. We put $\Gamma_a := \Phi_a, \Psi_a$ and $\varphi_a := \overline{\bigvee \Phi_a}$, $\psi_a := \bigvee \Psi_a$. In addition, we denote the root of $\pi$ by $r(\pi)$. We proceed with the following lemma. Lemma 5.2. For any two nodes $a,b\in M$, the formulae $\varphi_a$ and $\varphi_b$ are equivalent in predicate logic: Proof. It is sufficient to prove that $ \vdash \varphi_a \to \varphi_b$ since $a$ and $b$ are arbitrary elements of $M$. By the definitions of $\varphi_a$ and $\varphi_b$ and the principle of contraposition, it is sufficient to demonstrate that $\vdash \bigvee \Phi_b \to \bigvee \Phi_a$.
Observe that there exists a finite directed path from $a$ to $b$, since there is a finite directed path from $a$ to the root $r(\pi)$, as well as a finite directed path from the root to any other node in $M$. We continue the argument using induction on the length of the shortest directed path between $a$ and $b$. The basis of induction. If $a = b$, then $\Phi_a = \Phi_b$, hence the result trivially holds. The induction step. We denote by $a'$ the next node on the directed path from $a$ to $b$. If $a$ is a leaf of $\pi$ and $d(a) = a'$, then $\Phi_a = \Phi_{a'}$. By the induction hypothesis we also have $\vdash \bigvee \Phi_b \to \bigvee \Phi_{a'}$. Hence $\vdash \bigvee \Phi_b \to \bigvee \Phi_a$. Otherwise, the sequent at $a$ is derived by applying some inference rule to the sequent of node $a'$ and possibly some other sequent. Clearly, $a'$ is an element of $M$, hence $a'$ is annotated with $V$. By the induction hypothesis we have $\vdash \bigvee \Phi_b \to \bigvee \Phi_{a'}$, therefore it is sufficient to demonstrate that We prove this claim by analyzing various cases according to different inference rules.Case A. Most of the rules do not change the $\Phi$-part of the sequent. This holds for the rules $\mathsf{(ref)}$, $\mathsf{(rep)}$, $\mathsf{(add_0)}$, $\mathsf{(add_s)}$, $\mathsf{(mult_0)}$, $\mathsf{(mult_s)}$ and $\mathsf{(pred)}$: in all these cases $\Gamma_a$ and $\Gamma_{a'}$ can only differ in atomic formulae. Case B. If $\Gamma_a$ is obtained from $\Gamma_{a'}$ by $\mathsf{(weak)}$, then $\Phi_{a'}\subseteq \Phi_a$ and the claim trivially follows. Case C. Suppose $\Gamma_{a'}$ is a premiss of an application of the rule ($\mathsf{\vee}$) and $\Gamma_a$ is its conclusion. Let $\alpha \vee \beta$ be its principal formula. If $\alpha \vee \beta \notin \Pi_{n+1}$, then $\alpha\notin \Pi_{n+1} $ or $\beta\notin \Pi_{n+1} $. We have $\vdash \bigvee \Phi_{a'} \to \bigvee \Phi_a$ since $\vdash\alpha\to \alpha \vee \beta$ and $\vdash\beta\to \alpha \vee \beta$. Otherwise, $\alpha \vee \beta$ is $\Pi_{n+1}$ and so are $\alpha$ and $\beta$ (by the definition of $\Pi_{n+1}$), hence $\Phi_{a'} = \Phi_a$. Case D. Suppose $\Gamma_a$ is obtained from $\Gamma_{a'}$ by $\mathsf{(\exists)}$. If $\varphi[y\mapsto t]$ is $\Pi_{n+1}$, then $\Phi_{a'}=\Phi_a$. Otherwise, both $\varphi[y\mapsto t]$ and $\exists\,y\ \varphi$ belong to $\Phi_{a'}$. We observe that $\vdash \varphi[y\mapsto t]\to \exists\,y\ \varphi$, hence $\vdash \bigvee \Phi_{a'} \to \bigvee \Phi_a$. The remaining rules are handled more-or-less similarly by using the annotation conditions. Case E. Suppose $\Gamma_a$ is obtained from $\Gamma_{a'}$ by $\mathsf{(\forall)}$. As these sequents have the same nonempty annotation $V$, the principal formula has to be $\Pi_{n+1}$. Hence in this case $\Phi_{a'} = \Phi_a$. Case F. Suppose $\Gamma_{a'}$ is a premiss of an application of $\mathsf{(\wedge)}$ and $\Gamma_a$ is its conclusion. As these sequents have the same nonempty annotation $V$, $\Phi_{a'} \subseteq \Phi_a$ and the claim follows. Case G. Suppose $\Gamma_{a'}$ is a premiss an application of $\mathsf{(cut)}$ and $\Gamma_a$ is its conclusion. As these sequents have the same nonempty annotation $V$, the cut formula has to be $\Pi_{n+1}$, and therefore $\Phi_{a'} = \Phi_a$. Case H. Suppose $\Gamma_{a'}$ is the right premiss of an application of $\mathsf{(case)}$ and $\Gamma_a$ is its conclusion. As the annotation $V$ of these sequents is nonempty, we conclude that the active variable in the application of the rule $\mathsf{(case)}$ is permitted to occur freely only within the $\Pi_{n+1}$-formulae in $\Gamma_a$. It follows that $\Phi_{a'} = \Phi_a$. This completes the proof of Lemma 5.2. Consider the set of all applications of the rule ($\mathsf{\forall}$) in $\pi$ whose conclusions belong to $M$. Let $\mathit{B}$ denote the set of active variables of these applications. We also set
$$
\begin{equation*}
\theta := \forall_\mathit{B} \bigwedge_{c \in C} \psi_c,
\end{equation*}
\notag
$$
where ${\forall}_\mathit{B}$ means the finite sequence of universal quantifiers for variables of $\mathit{B}$ and $C$ is the set of conclusions of applications of the rule $\mathsf{(case)}$ in $M$. Note that $\theta$ belongs to $\Pi_{n+1}$. For any $a \in M$ we define its rank $\mathrm{rk}(a)$ as the length of the longest directed path from $a$ to a node $c$ in $C$ such that only the last node of the path belongs to $C$. Note that $\mathrm{rk}(c) = 0$ if $c \in C$. The notion of rank is well defined since any infinite directed path in $\pi$ must intersect applications of the rule $\mathsf{(case)}$. The following lemma demonstrates that all sequents in $M$ are implied in $\mathit{I\Sigma_{n+1}}$ by a single formula $\theta$. Proof. Observe that this is equivalent to $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Gamma_a$. We prove the lemma by induction on $\mathrm{rk}(a)$.
Case A. If $a$ is an element of $C$, the claim holds trivially, as $\mathit{I \Sigma}_{n+1} \vdash \theta \to \psi_a$. If $a$ is a leaf of $\pi$ and $d(a) = b$, then the claim follows from the induction hypothesis since $\Gamma_a=\Gamma_b$. Assume that the sequent at the node $a$ results from an application of an inference rule to the sequent at the node $a' \in M$ and possibly some other sequent, and $\mathrm{rk}(a') < \mathrm{rk}(a)$. Note that this rule is not $\mathsf{(case)}$ because $a \notin C$. Without loss of generality we can assume that $\Gamma_{a'}$ is the left premiss of the rule in the case of any inference rule with two premisses. Case B. Suppose the sequent $\Gamma_a$ is derived by an application of the rule ($\mathsf{\wedge}$). Thus the proof fragment at the node $a$ has the form Observe that $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Gamma_{a'}$ holds by the induction hypothesis, hence $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Delta \vee \alpha$. If the node corresponding to the right premiss of the rule is an element of $M$, then $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Delta \vee \beta$ holds by the analogous reasoning. Otherwise, no back-links exist from the nodes of the tree $\kappa''$ to those within $M$. The proof $\kappa''$ is a cyclic proof with fewer nodes than $\pi$, consequently by the main induction hypothesis $\mathit{I \Sigma}_{n+1} \vdash \bigvee \Delta \vee \beta$, and therefore $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Delta \vee \beta$. As a result, $\mathit{I \Sigma}_{n+1} \vdash \theta \to \Delta \vee (\alpha \wedge \beta)$.Case C. The case of rule $\mathsf{(cut)}$ is similar to the case of $\mathsf{(\wedge)}$. Case D. Suppose $\Gamma_a$ is the conclusion of an application of rule $\mathsf{(\forall)}$. The corresponding fragment of the proof at the node $a$ has the form The induction hypothesis $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Gamma_{a'}$ means that
$$
\begin{equation*}
\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Delta \vee \alpha[y\mapsto z].
\end{equation*}
\notag
$$
Observe that $z$ is an element of $B$, thereby $z \notin \mathit{FV}(\theta)$. Furthermore, $z \notin \mathit{FV}(\Delta, \forall\, y\ \alpha)$ by the definition of $\mathsf{(\forall)}$. Hence we obtain $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Delta \vee \forall\, y\ \alpha$ by predicate logic.
Case E. For any other rule it is obvious that $\mathit{I \Sigma}_{n+1} \vdash \bigvee \Gamma_{a'} \to \bigvee \Gamma_a$. By the induction hypothesis $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Gamma_{a'}$, hence $\mathit{I \Sigma}_{n+1} \vdash \theta \to \bigvee \Gamma_a$ and the proof of Lemma 5.3 is complete. Let $y_1, \dots, y_m$ be the list of all active variables of applications of the rule $\mathsf{(case)}$ whose conclusions belong to $M$. We set
$$
\begin{equation*}
\zeta(z) := \forall\, y_1\leqslant z \dotsc \forall\, y_m\leqslant z \ (y_1 + \dotsb + y_m = z \to \theta),
\end{equation*}
\notag
$$
where $z \notin \mathit{FV}(\theta)$, $z\notin B$ and $z \notin \mathit{FV}(\varphi_{r(\pi)})$. Note that $\zeta(z)$ is a $\Pi_{n+1}$-formula. Proof. For each $c$ from $C$, the corresponding fragment of the proof has the form where $y_j$ is the active variable of the inference. Note that $y_j \notin \mathit{FV}(\Phi_c)$ as $V$ is nonempty, and in this case the active variable of the rule $\mathsf{(case)}$ occurs freely only in $\Pi_{n+1}$-formulae of the conclusion. Since there are no left premisses of the rule $\mathsf{(case)}$ in between any two nodes connected by a back-link, we have an annotated cyclic proof $\pi' =(\kappa', d')$ of $\Phi_c,\Psi_c[y_j \mapsto 0] \upharpoonright \varnothing$ in $\mathsf{S}_n$. From the main induction hypothesis for $\pi'$ we obtain $\mathit{I \Sigma}_{n+1} \vdash \varphi_c \to \psi_c[y_j \mapsto 0]$. Applying Lemma 5.2 we obtain $\mathit{I \Sigma}_{n+1} \vdash \varphi_c \leftrightarrow \varphi_{r(\pi)}$ and $\mathit{I \Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to \psi_c[y_j \mapsto 0]$. As $y_j \notin FV(\Phi_c)$, we conclude that $\varphi_{r(\pi)}$ does not depend on $y_j$:
$$
\begin{equation*}
\mathit{I\Sigma}_{n+1}\vdash \varphi_{r(\pi)}[y_j\mapsto 0]\leftrightarrow \varphi_{r(\pi)}.
\end{equation*}
\notag
$$
The same holds for every $j \in \{1, \dots, m\}$, and therefore Consequently,
Now we argue in a similar manner that $\varphi_{r(\pi)}$ does not depend on the variables in $B$. Let $x_i\in B$ be the active variable in an application of $\mathsf{(\forall)}$ whose conclusion $\Gamma_a = \Phi_a,\Psi_a$ is in $M$. Since $V$ is nonempty, its principal formula $\forall\,x\ \psi\in \Pi_{n+1}$ does not occur in $\Phi_a$, so $x_i\notin\mathit{FV}(\Phi_a)$. Using Lemma 5.2 we obtain that $\varphi_{r(\pi)}$ is equivalent to the formula $\varphi_a$ in which $x_i$ does not occur, and the claim follows. Now, applying Bernays’ rule to (5.1) we obtain
$$
\begin{equation*}
\mathit{I \Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to \theta[y_1 \mapsto 0, \dotsc, y_m \mapsto 0],
\end{equation*}
\notag
$$
and therefore $\mathit{I \Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to \zeta(0)$.
In order to prove $\mathit{I \Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to \forall\, z\ (\zeta(z) \to \zeta(s(z)))$, it is sufficient to show
$$
\begin{equation*}
\mathit{I \Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to (\zeta(z) \to (y_1 + \dotsb + y_n = s(z) \to \psi_c))
\end{equation*}
\notag
$$
for each $c$ from $C$, because $\varphi_{r(\pi)}$ does not depend on the variables in $B \cup \{z, y_1, \dots, y_m\}$. Let $y_j$ be the active variable in an application of the rule $\mathsf{(case)}$ at the node $c$. Arguing in $\mathit{I \Sigma}_{n+1}$, we consider two cases: $y_j = 0$ or $y_j = s(y'_j)$. If $y_j = 0$, then $\varphi_{r(\pi)} \to \psi_c[y_j \mapsto 0]$ is provable in $\mathit{I \Sigma_{n+1}}$ as we have seen.
Assume that $y_j = s(y'_j)$, $\varphi_{r(\pi)}$, $\zeta(z)$ and
$$
\begin{equation*}
y_1 + \dotsb + y_{j-1} + s(y'_j) + y_{j+1} + \dotsb + y_n = s(z).
\end{equation*}
\notag
$$
Then
$$
\begin{equation}
y_1 + \dotsb + y_{j-1} + y'_j + y_{j+1} + \dotsb + y_n = z.
\end{equation}
\tag{5.2}
$$
From (5.2) and $\zeta(z)$ we obtain $\theta[y_j \mapsto y'_j]$.
Recall that the node $c$ is the conclusion of an application the rule $\mathsf{(case)}$. Let $b$ be the node corresponding to the right premiss of this application. From Lemma 5.3 and $\theta[y_j \mapsto y'_j]$ we have $\varphi_b \to \psi_b[y_j \mapsto y'_j]$, as $y_j \notin \mathit{FV}(\varphi_b)$. Applying Lemma 5.2 and $\varphi_{r(\pi)}$, we obtain $\psi_b[y_j \mapsto y'_j]$. As $b$ is the right premiss of the rule $\mathsf{(case)}$ for the node $c$, we have $\psi_b[y_j \mapsto y'_j] = \psi_c[y_j \mapsto s(y'_j)]$. We recall that $y_j = s(y'_j)$ and obtain the required formula $\psi_c$. The second case has been checked, and the lemma is proved. Recall that the induction principle for $\Pi_{n+1}$-formulae is provable in $\mathit{I \Sigma}_{n+1}$; see [19]. Therefore, we derive that $\mathit{I\Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to \forall\, z\ \zeta(z)$ from Lemma 5.4. The formula $\forall\,z\ \zeta(z)$ clearly implies $\forall\,y_1\ \dots \forall\,y_m\ \theta(y_1,\dots,y_m)$ in $\mathit{I\Sigma}_0$, so we obtain
$$
\begin{equation*}
\mathit{I\Sigma}_{n+1}\vdash \varphi_{r(\pi)}\to \theta.
\end{equation*}
\notag
$$
By Lemma 5.3, we also have $\mathit{I \Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to (\theta \to \psi_{r(\pi)})$. Therefore, $\mathit{I\Sigma}_{n+1} \vdash \varphi_{r(\pi)} \to \psi_{r(\pi)}$. Since $\mathit{I\Sigma}_{n+1} \vdash \bigvee \Gamma \leftrightarrow (\varphi_{r(\pi)} \to \psi_{r(\pi)})$, we conclude that $\mathit{I\Sigma}_{n+1} \vdash \bigvee \Gamma$. Theorem 5.1 is proved. Thus, we have established that the system $\mathsf{S}_n$ is deductively equivalent to $\mathit{I\Sigma}_{n+1}$. As a corollary, we also obtain that unrestricted regular $\infty$-proofs correspond to proofs in Peano arithmetic. Corollary 5.5. A formula $\varphi$ is provable in $\mathrm{PA}$ if and only if $\varphi$ has a regular $\infty$-proof. Proof. The left-to-right implication is straightforward. If $\mathrm{PA} \vdash \varphi$, then ${\mathit{I\Sigma}_{n+1}\vdash \varphi}$ for some $n$. By Corollary 3.6 the formula $\varphi$ is provable in $\mathsf{S}_n$. Therefore, $\varphi$ has a regular $\infty$-proof. Let us prove the right-to-left implication. Assume that $\varphi$ has a regular $\infty$-proof. Since this proof contains only finitely many different formulae, there is a natural number $n$ such that all formulae in this proof belong to $\Pi_{n+1}$. Therefore, this regular $\infty$-proof is $\Pi_{n+1}$-restricted. Hence $\mathsf{S}_n\vdash \varphi$, and by Theorem 5.1, $\mathit{I \Sigma}_{n+1} \vdash \varphi$. Consequently, $\varphi$ is provable in $\mathrm{PA}$.
The corollary is proved. § 6. Proof systems for induction rulesFragments of Peano arithmetic defined by restricted forms of induction rules have well been studied in proof theory; see [4] and [21] for detailed surveys. Here we are interested in the axiomatization of such theories using non-well-founded and cyclic proofs. First, we introduce a natural modification of $\mathsf{S}_n$ that yields a system deductively equivalent to $\mathit{I\Pi}_{n+1}^R$, that is, to the closure of $\mathsf{Q}$ under the $\Pi_{n+1}$-induction rule. More generally, given an extension $T$ of $\mathsf{Q}$ by some set of additional axioms we would like to characterize the closure of $T$ under the $\Pi_{n+1}$-induction rule. To do this we introduce proofs from assumptions. Given a set $T$ of sentences, an $\infty$-proof from the assumptions $T$ is an $\infty$-proof in which the rules of the calculus $\mathsf{SQ}$ are extended by the initial sequents of the form $\{\varphi\}$ for all $\varphi\in T$. As before, a regular $\infty$-proof from assumptions is an $\infty$-proof from assumptions such that the proof tree has only finitely many nonisomorphic subtrees. Note also that assumptions never occur in infinite branches of the proof tree. Therefore, the notion of $\Pi_{n}$-restricted $\infty$-proof is essentially unaffected by the presence of assumptions. We say that a $\Pi_{n+1}$-restricted $\infty$-proof (from the assumptions $T$) is an $\infty$-proof of $\mathsf{S}^{\Pi}_n$ ( from $T$) whenever every infinite branch in it has a tail satisfying, instead of condition (g), the following stronger condition: if the tail passes through the right premiss $\Gamma [z\mapsto s(z)]$ of the rule $\mathsf{(case)}$, then $\Gamma$ consists entirely of $\Pi_{n+1}$-formulae. Analogously to the definition of $\mathsf{S}_n$, a sequent $\Gamma$ is provable in $\mathsf{S}^{\Pi}_n$ ( from the assumptions $T$) if there is a regular $\infty$-proof of $\mathsf{S}^{\Pi}_n$ (from $T$) with root marked by $\Gamma $. For this calculus, the notions of annotated $\infty$-proof and cyclic annotated proof of $\mathsf{S}_n$ are modified appropriately. Lemma 6.1. The set of formulae provable in $\mathsf{S}^{\Pi}_n$ (from assumptions $T$) is closed under the induction rule $(\mathrm{IR})$ for $\Pi_{n+1}$-formulae. Proof. Assume that $\varphi(x)$ is $\Pi_{n+1}$, $x\in \mathit{FV}(\varphi)$ and both formulae $\varphi(0)$ and $\forall\,x\ (\varphi(x)\to \varphi(s(x)))$ are provable in $\mathsf{S}^{\Pi}_n$. Then the sequents $\{\varphi(0)\}$ and $\{\overline{\varphi(x)},\varphi(s(x))\}$ have regular $\infty$-proofs of $\mathsf{S}^{\Pi}_n$ denoted by $\sigma_0$ and $\sigma_1$, respectively. We combine them into the following regular $\infty$-proof $\pi$:
Here the subtree $\pi$ is isomorphic to the whole $\infty$-proof. It is easy to check that the proof displayed is a regular $\infty$-proof of $\mathsf{S}^{\Pi}_n$. The lemma is proved. The converse of Lemma 6.1 also holds. Let $T+\Pi_{n}\text{-}\mathsf{IR}$ denote the closure of $T$ under the induction rule for $\Pi_{n}$ formulae. Theorem 6.2. If $\Gamma$ is provable in $\mathsf{S}^{\Pi}_n$ from the assumptions $T$, then $\Gamma$ is a theorem of $\mathsf{Q}+T+\Pi_{n+1}\text{-}\mathsf{IR}$. Proof. The proof is almost the same as the proof of Theorem 5.1. Read $\mathsf{Q}+T+\Pi_{n+1}\text{-}\mathsf{IR}$ instead of $\mathit{I\Sigma}_{n+1}$ throughout that proof. Observe that Lemma 5.2 stays the same. The proof of Lemma 5.3 does not change except for the reference to the — now stronger — main induction hypothesis. Lemma 5.4 also goes without change.
Now we arrive at the final part of the proof. The crucial point there is to apply the $\Pi_{n+1}$-induction rule with a side formula $\varphi_{r(\pi)}$. From Lemma 5.2 we observe that $\varphi_{r(\pi)}$ is logically equivalent to $\varphi_a$, where $a$ is the conclusion of some application of the rule $\mathsf{(case)}$ in $M$. However, $\varphi_a=\overline{\bigvee\Phi_a}$ where $\Phi_a=\varnothing$ by our definition of $\mathsf{S}^{\Pi}_n$. Hence, $\varphi_{r(\pi)}$ must be logically provable. It follows that $\mathsf{Q}+T+\Pi_{n+1}\text{-}\mathsf{IR}$ proves $\forall\,z\ \zeta(z)$ and we finish the argument as before. The theorem is proved. We conclude that the system $\mathsf{S}^{\Pi}_n$ precisely axiomatizes the fragment $\mathit{I\Pi}^R_{n+1}$ of Peano arithmetic axiomatized by the $\Pi_{n+1}$-induction rule over $\mathsf{Q}$. By a well-known result of Parsons [31], for $n>0$ the theories $\mathit{I\Pi}^R_{n+1}$ and $\mathit{I\Sigma}_n^R$ are deductively equivalent. However, this need not be so over an arbitrary extension $T$ of $\mathsf{Q}$: for example, $\mathit{I\Sigma}_n$ is closed under the $\Sigma_n$-induction rule, but not under the $\Pi_{n+1}$-induction rule; see [4] for exact characterizations of the closures of theories under induction rules. Also, $n=0$ is an exception. As shown by Jeřábek (private communication), $\mathit{I\Pi}^R_1$ is strictly stronger than $\mathit{I\Sigma}^R_0\equiv \mathit{I\Delta}_0$. In fact, $\mathit{I\Pi}^R_1$ can be characterized as the set of $\Pi_1$-sentences provable in elementary arithmetic $\mathrm{EA}$ (also known as $\mathit{I\Delta}_0+\mathrm{exp}$); this result is reproduced in § 7. In order to formulate a version of $\mathsf{S}_n$ closely related to the $\Sigma_n$-induction rule, we need to modify the definition of a $\Pi_n$-restricted $\infty$-proof as follows. Definition 6.3. An $\infty$-proof (possibly from assumptions) is $\Sigma_n$-restricted if every infinite branch in it has a tail satisfying conditions (a)–(c) from Definition 3.1 of an $\infty$-proof and the following conditions: Since $\Sigma_n\subseteq \Pi_{n+1}$, we see that each $\Sigma_n$-restricted $\infty$-proof is also $\Pi_{n+1}$-restricted. However, by condition $\rm(e')$, a $\Pi_{n}$-restricted $\infty$-proof need not be $\Sigma_{n+1}$-restricted. Now we say that a sequent $\Gamma$ is provable in $\mathsf{S}^{\Sigma}_n$ (from the assumptions $T$) if there is a $\Sigma_n$-restricted regular $\infty$-proof (from $T$) with the root marked by $\Gamma$. We also naturally modify the notions of annotated $\infty$-proof and cyclic annotated proof of $\mathsf{S}_n$ in order to obtain the corresponding notions for $\mathsf{S}^{\Sigma}_n$. At first glance, the system $\mathsf{S}^{\Sigma}_n$ looks similar to the systems $\mathrm{C}\Sigma_n$ studied in [14]. However, $\mathrm{C}\Sigma_n$ was defined using two-sided sequents, and converting it to the one-sided format yields a system obtained by restricting the complexity of each formula in a cyclic proof to the class $\Sigma_n$ or $\Pi_n$, which is clearly different from $\mathsf{S}^{\Sigma}_n$. Now we notice that analogues of Lemma 6.1 and Theorem 6.2 hold for $\mathsf{S}^{\Sigma}_n$ with similar proofs. Lemma 6.4. The set of formulae provable in $\mathsf{S}^{\Sigma}_n$ (from the assumptions $T$) is closed under the induction rule $(\mathrm{IR})$ for $\Sigma_{n}$-formulae. Theorem 6.5. If $\Gamma$ is provable in $\mathsf{S}^{\Sigma}_n$ from the assumptions $T$, then $\Gamma$ is a theorem of $\mathsf{Q}+T+\Sigma_{n}\text{-}\mathsf{IR}$. Proof. We only observe that in this case the formulae $\Psi_a$ are $\Sigma_n$. By condition $\rm(e')$ the set of variables $B$ is empty, hence the formula $\theta$ is $\bigwedge_{c\in C}\psi_c$. Therefore, $\theta\in\Sigma_n$ and $\zeta$ is obtained from a $\Sigma_n$-formula by bounded universal quantifiers. As in Theorem 6.2, the final part of the proof boils down to an application of the induction rule (without side formulae) for $\zeta$. For $n=0$ such an inference is clearly admissible by $\Sigma_{0}\text{-}\mathsf{IR}$.
For $n>0$ the following lemma shows that such an application is also reducible to some applications of $\Sigma_{n}\text{-}\mathsf{IR}$. We state it for one bounded quantifier, but the proof clearly extends to any number of them. Lemma 6.6. Let $T$ be an extension of $\mathsf{Q}$ and $\psi(z)$ be a formula of the form $\forall\,{x\leqslant z}\ \exists\,y\ \varphi(x,y,z)$ with $\varphi\in\Pi_{n}$. Assume that $T\vdash \psi(0)$ and $T\vdash \forall\,z\ (\psi(z)\to \psi(s(z)))$. Then $T+\Sigma_{n+1}\text{-}\mathsf{IR}\vdash \forall\,z\ \psi(z).$ Proof. Without loss of generality we may assume $T$ to be an extension of $\mathit{I\Delta}_0$, since $\mathit{I\Delta}_0$ is contained in (and is equivalent to) $\mathit{I\Sigma}_0^R$. Now consider the formula Notice that $\varphi'(z,v)$ is equivalent to a $\Pi_n$ formula, say $\varphi''(z,v)$, in $\mathit{I\Sigma}_n$, since $\mathit{I\Sigma}_n$ proves the $\Sigma_n$-collection schema for $n>0$. The fragment $\mathit{I\Sigma}^R_{n+1}$ contains $\mathit{I\Sigma}_n$, hence the equivalence also holds in $T+\Sigma_{n+1}\text{-}\mathsf{IR}$.
Further, it is easy to see from our assumptions that $T$ proves $\exists\,v\ \varphi'(0,v)$ and $\forall\,z\ (\exists\,v\ \varphi'(z,v)\to \exists\,v\ \varphi'(s(z),v))$. Hence $T+\Sigma_{n+1}\text{-}\mathsf{IR}$ proves $\exists\,v\ \varphi''(0,v)$ and $\forall\,z\ (\exists\,v\ \varphi''(z,v)\,{\to}\, \exists\,v\ \varphi''(s(z),v))$. From $\Sigma_{n+1}\text{-}\mathsf{IR}$ we conclude that $\forall\,z\ \exists\,v\ \varphi''(z,v)$, from which $\forall\,z\ \exists\,v\ \varphi'(z,v)$ and $\forall\,z\ \psi(z)$ follow. The lemma is proved. Applying Lemma 6.6 to $\zeta$ we obtain $\forall\,z\ \zeta(z)$, hence $\theta$, and prove the claim of the theorem. Notice that by Theorem 6.5 the system $\mathsf{S}^{\Sigma}_0$ is deductively equivalent to the fragment of arithmetic $\mathit{I\Delta}_0$. § 7. On $\Pi_1$-induction ruleThe following theorem was proposed by Emil Jeřábek (private communication) and is reproduced here with his kind permission. Recall that $\mathrm{EA}$ is the extension of $\mathit{I}\mathit{\Delta}_0$ by the axiom stating the totality of the exponentiation function $\exp(x)=2^x$. We denote by $2_n^x$ the $n$th iterate of $\exp$. Theorem 7.1. $\mathit I\Pi_1^R$ is deductively equivalent to the theory axiomatized by all the $\Pi_1$ theorems of $\mathrm{EA}$. Proof. Clearly, $\mathit{I\Pi}_1^R$ is $\Pi_1$ axiomatizable. The inclusion of $\mathit{I\Pi}_1^R$ in $\mathrm{EA}$ follows from a theorem of Kaye, Paris, and Dimitracopoulos (see [23], Theorem 0.5) stating that $\Pi_2$-theorems of the parameter-free induction schema $\mathit{I\Pi}_1^-$ are contained in $\mathrm{EA}$. It is easy to see that $\mathit{I\Pi}_1^R$ is equivalent to its parameter-free variant and therefore is contained in $\mathit{I\Pi}_1^-$.
To prove the opposite inclusion we consider an arbitrary $\Pi_1$-sentence of the form $\forall\,x\ \varphi(x)$ with $\varphi\in\Delta_0$. If $\mathrm{EA}\vdash \forall\,x\ \varphi(x)$, then (by a simple compactness argument: see [45]) there is $k$ such that $\mathit{I\Delta}_0\vdash \forall\,x\ (\exists\,y\ 2_k^x=y \to \varphi(x))$. Here $2_k^x=y$ is expressed as a $\Delta_0$-formula using a standard $\Delta_0$-definition of the graph of exponentiation in $\mathit{I\Delta}_0$; see [19]. Notice that for each $k$ the formula $\forall\,x\ (\exists\,y\ 2_k^x=y \to \varphi(x))$ is logically equivalent to a $\Pi_1$-sentence. Lemma 7.2. For any $\varphi\in\Pi_1$ the closure of $\mathit{I\Delta}_0+\forall\,x\ (\exists\,y\ 2^x=y \to \varphi(x))$ under one application of $\Pi_{1}\text{-}\mathsf{IR}$ proves $\forall\,x\ \varphi(x)$. Proof. Let $\pi(z)$ denote the $\Pi_1$-formula In $\mathit{I\Delta}_0+\forall\,x\ (\exists\,y\ 2^x=y \to \varphi(x))$ it is easy to prove $\pi(0)$ and $\forall\,z\ (\pi(z)\to \pi(s(z)))$. (This is because $\mathit{I\Delta}_0$ knows that if $2^x$ exists, then so does $2^x+2^x=2^{s(x)}$.) Applying the induction rule we obtain $\forall\,z\ \pi(z)$, hence (putting $x=0$) $\forall\,z\ \varphi(z)$, as required.
The lemma is proved. Let $[T,R]_k$ denote the closure of a theory $T$ under $k$-nested applications of the inference rule $R$. Using meta-induction on $k$ we prove that for any $T$ containing $\mathit{I\Delta}_0$ and an arbitrary bounded $\varphi$, if $T\vdash \forall\,x\ (\exists\,y\ 2_k^x=y \to \varphi(x))$, then $[T,\Pi_{1}\text{-}\mathsf{IR}]_k\vdash \forall\,x\ \varphi(x)$. For $k=0$ the claim is trivial. We assume that the claim holds for $k$ and prove it for $k+1$. Suppose $T\vdash \forall\,x\ (\exists\,y\ 2_{k+1}^x=y\to \varphi(x))$. Then
$$
\begin{equation*}
T\vdash \forall\,u\ (\exists\,y\ 2^u=y \to \forall\,x\leqslant u\ (2_k^x=u \to \varphi(x))).
\end{equation*}
\notag
$$
By Lemma 7.2,
$$
\begin{equation*}
[T,\Pi_{1}\text{-}\mathsf{IR}]\vdash \forall\,u\ \forall\,x\leqslant u\ (2_k^x=u\to \varphi(x)),
\end{equation*}
\notag
$$
hence $[T,\Pi_{1}\text{-}\mathsf{IR}]\vdash \forall\,x\ (\exists\,u\ 2_k^x=u \to \varphi(x))$. Thus, by the induction hypothesis for $[T,\Pi_{1}\text{-}\mathsf{IR}]$, $[T,\Pi_{1}\text{-}\mathsf{IR}]_{k+1}\vdash \forall\,x\ \varphi(x)$, as required.
§ 8. ConclusionIn this paper we have defined a number of cyclic systems axiomatizing the main fragments of Peano arithmetic with the axioms or rules of induction restricted to classes of the arithmetical hierarchy. This opens a number of directions for further research. Firstly, we would like to do some experiments with inductive proof search based on cyclic systems of arithmetic and type theory, akin to the ones introduced in this paper. Some preliminary work in this direction has already been done (see [42]). Secondly, we would like to study the possibilities of using cyclic proofs for proof-theoretic analysis of arithmetic and other systems. In particular, there is a need to develop (partial) cut-elimination techniques in this context.
Citation in format AMSBIB
\Bibitem{BekShaSmi25} |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Contact us: |
Terms of Use
|
Registration to the website |
Logotypes |
|