2.1 Treatment of theories

Recall that $\mathsf {EA}$ is a finitely axiomatizable theory in the language of arithmetic with the exponential function, i.e., in the signature $(0,1,+,\times ,2^x,\leq )$ . $\mathsf {EA}$ is characterized by the standard recursive axioms for addition, multiplication, and exponentiation as well as the induction schema for $\Delta _0$ formulas. Note that by $\Delta _0$ formulas we mean $\Delta _0$ formulas in the language with exponentiation. $\mathsf {EA}$ is strong enough to facilitate typical approaches to arithmetization of syntax. Moreover, $\mathsf {EA}$ proves its own $\Sigma _1$ completeness.

We will also be interested in $\mathsf {EA}^+$ . $\mathsf {EA}^+$ is a theory in the language of $\mathsf {EA}$ . $\mathsf {EA}^+$ extends $\mathsf {EA}$ by the additional axiom “superexponentiation is total.” By superexponentiation, we mean the function $2^x_x$ where $2^x_0=x$ and $2^x_{y+1}=2^{2^x_y}$ . $\mathsf {EA}^+$ is the weakest extension of $\mathsf {EA}$ in which the cut-elimination theorem is provable. Indeed, the cut-elimination theorem is equivalent to the totality of superexponentiation over $\mathsf {EA}$ . See [Reference Beklemishev4] for details on $\mathsf {EA}$ and $\mathsf {EA}^+$ ; see also [Reference Hájek and Pudlák15] for details on $\mathsf {EA}$ and $\mathsf {EA}^+$ in a slightly different formalism without an explicit symbol for exponentiation. We will use $\mathsf {EA}^+$ as a meta-theory for proving many of our results.

In this paper we will examine theories in three different languages. First the language of first-order arithmetic, i.e., the language of $\mathsf {EA}$ . Second the language of first-order arithmetic extended with one additional free set variable X; we also call this the pseudo- $\Pi ^1_1$ language. And finally the language of second-order arithmetic. The language of first-order arithmetic of course is a sublanguage of the other two languages. And we consider the pseudo- $\Pi ^1_1$ language to be a sublanguage of the language of second-order arithmetic by identifying each pseudo- $\Pi ^1_1$ sentence $\mathsf {F}$ with the second-order sentence $\forall X \;\mathsf {F}$ .

In the first-order context we are interested in the standard arithmetical complexity classes $\Pi _n$ and $\Sigma _n$ . We write $\Pi _\infty $ to denote the class of all arithmetical formulas. We write $ {\Pi }^0_n$ to denote the class of formulas that are just like $\Pi _n$ formulas except that their formulas (potentially) contain a free set variable X. Formulas in the complexity class $ {\Pi }^0_n$ cannot have set quantifiers, and so contain only free set variables. Of course, the class ${\Sigma }^0_n$ is defined dually to the class ${\Pi }^0_n$ . We write ${\Pi }^0_\infty $ to denote the class of boldface arithmetical formulas, i.e., the class of arithmetical formulas (potentially) with a free set variable.

In the second-order context we are mostly interested in the standard analytical complexity classes $\Pi ^1_1$ and $\Sigma ^1_1$ . However, we will also use other complexity classes. Suppose $\mathcal {C}\subset \mathcal {L}_2$ is one of the following classes of formulas: $\Pi ^0_m$ or $\Sigma ^0_m$ , for $m\ge 1$ . Then we denote by $\Pi ^1_n(\mathcal {C})$ the class of all the formulas of the form $\forall X_1\exists X_2\ldots Q X_n \; \mathsf {F}$ , where $\mathsf {F}\in \mathcal {C}$ . We define $\Sigma ^1_n(\mathcal {C})$ dually.

For a first-order theory T, we use $T(X)$ to denote the pseudo $\Pi ^1_1$ pendant of T. For example, the theory $\mathsf {PA}(X)$ contains (i) the axioms of $\mathsf {PA}$ and (ii) induction axioms for all formulas in the language, including those with free set variables. The theories $\mathsf {EA}(X)$ , $\mathsf {EA}^+(X)$ , and $\mathsf {I}{\Sigma }_1(X)$ are defined analogously, i.e., their induction axioms are extended to include formulas with the free set variable X.

Formulas in any of the three languages we are working with can naturally be identified with words in a suitable finite alphabet, which, in turn, are naturally one-to-one encoded by numbers. Accordingly, we can fix a Gödel numbering of these languages. We denote the Gödel number of an expression $\tau $ by $\ulcorner \tau \urcorner $ . Many natural syntactic relations (x is a logical axiom, z the result of applying Modus Ponens to x and y, x encodes a $\Pi _n$ formula, etc.) are elementary definable and their simplest properties can be verified within $\mathsf {EA}$ . We also fix a one-to-one elementary coding of finite sequences of natural numbers. $\langle x_1,\ldots ,x_n\rangle $ denotes the code of a sequence $x_1,\ldots ,x_n$ and, for any fixed n, is an elementary function of $x_1,\ldots ,x_n$ .

We are concerned with recursively enumerable theories. Officially, a theory T is a $\Sigma _1$ formula $\mathsf {Ax}_{T}(x)$ that is understood as a formula defining the (Gödel numbers of) axioms of T in the standard model of arithmetic, i.e., the set of axioms of T is $\{\varphi : \mathbb {N}\vDash \mathsf {Ax}_{T}(\varphi ) \}$ . Thus, we are considering theories intensionally, via their axioms, rather than as deductively closed sets of formulas.

Since our base theory $\mathsf {EA}$ is fairly weak, we have to be careful with our choice of formalizations of proof predicates. Namely, we want our provability predicate to be $\Sigma _1$ . And due to this we can’t use the straightforwardly defined predicates $\mathsf {PrfNat}_{T}(x,y)$ : x is a Hilbert-style proof of y, where all axioms are either axioms of first-order logic or axioms of T. The predicates $\mathsf {PrfNat}_{T}(x,y)$ are equivalent to $\forall ^b\Sigma _1$ -formulas over $\mathsf {EA}$ ( $\forall ^b\Sigma _1$ -formulas are the formulas starting with a bounded universal quantifier followed by $\Sigma _1$ -formula). However, $\mathsf {EA}$ is too weak to equivalently transform $\forall ^b\Sigma _1$ -formulas to $\Sigma _1$ -formulas; for this one needs the collection scheme $\mathsf {B}\Sigma _1$ , which isn’t provable in $\mathsf {EA}$ . We note that this doesn’t affect most natural theories T, in particular, for any T with $\Delta _0$ formula $\mathsf {Ax}_T$ , the predicate $\mathsf {PrfNat}_{T}(x,y)$ is equivalent to a $\Sigma _1$ formula over $\mathsf {EA}$ .

Nevertheless, to avoid this issue, we work with proof predicates that are forced to be $\Sigma _1$ in $\mathsf {EA}$ , which are sometimes called smooth proof predicates. In the definition of the smooth proof predicate, a “proof” is a pair consisting of an actual Hilbert style proof and a uniform bound for witnesses to the facts that axioms in the proof indeed are axioms. We simply write $\mathsf {Prf}_{T}(x,y)$ to formalize that x is a “smooth proof” of y in theory T. The predicates $\mathsf {Prf}_{T}(x,y)$ are $\Delta _0$ -formulas. The predicate $\mathsf {Pr}_T(y)$ is shorthand for $\exists x \mathsf {Prf}_T(x,y)$ . We use the predicate $\mathsf {Con}(T)$ as shorthand for $\neg \mathsf {Pr}_T(\bot )$ , where we fix $\bot $ to be some contradictory sentence.

The closed term $1+1+\cdots +1$ (n times) is the numeral of n and is denoted $\underline {n}$ . We often omit the bar when no confusion can occur. We also often omit the corner quotes from Gödel numbers when no confusion can occur. For instance, we can encode the notion of a formula $\varphi $ being provable in a theory T, by saying that there is a T-proof (a sequence subject to certain constraints) the last element of which is the numeral of the Gödel number of $\varphi $ . However, instead of writing $\mathsf {Pr}_T(\underline {\ulcorner \varphi \urcorner })$ to say that $\varphi $ is provable we simply write $\mathsf {Pr}_T( \varphi )$ .

Suppose T and U are recursively enumerable theories in the same language. We write $T\sqsubseteq U$ if T is a subtheory of U; we can formalize the claim that $T\sqsubseteq U$ in arithmetic with the formula $\forall \varphi \big (\mathsf {Pr}_{T}(\varphi ) \rightarrow \mathsf {Pr}_U(\varphi )\big )$ . We write $T \equiv U$ if $T\sqsupseteq U$ and $U\sqsupseteq T$ . For a class $\mathcal {C}$ of sentences of the language of T we write $T\sqsubseteq _{\mathcal {C}} U$ if the set of $\mathcal {C}$ -theorems of T is a subset of $\mathcal {C}$ -theorems of $\mathsf {U}$ ; this could be naturally formalized in arithmetic with the formula $\forall \varphi \in \mathcal {C} \big (\mathsf {Pr}_{T}(\varphi ) \rightarrow \mathsf {Pr}_U(\varphi )\big )$ . We write $T\equiv _{\mathcal {C}} U$ if $T\sqsubseteq _{\mathcal {C}} U$ and $U\sqsubseteq _{\mathcal {C}} T$ .

We will be interested in partial truth-definitions for various classes of formulas for which we could prove Tarski’s bi-conditionals. For a class $\mathcal {C}$ of formulas we call a formula $\mathsf {Tr}_{\mathcal {C}}(x)$ a partial truth definition for $\mathcal {C}$ over a theory T, if $\mathsf {Tr}_{\mathcal {C}}(x)$ is from the class $\mathcal {C}$ and

$$\begin{align*}T\vdash \varphi(\vec{x})\leftrightarrow \mathsf{Tr}_{\mathcal{C}}(\varphi(\vec{x}))\mbox{, for all } \varphi(\vec{x}) \mbox{ from } \mathcal{C}.\end{align*}$$

Moreover, we will work only with truth definitions such that the above property is provable in $\mathsf {EA}$ .

In the book by Hájek and Pudlák [Reference Hájek and Pudlák15, Section I.1(d)] there is a construction of partial truth definitions for classes $\Pi _n$ and $\Sigma _n$ , $n\ge 1$ , over $\mathsf {I}\Sigma _1$ . However, we will use a sharper construction of partial truth definitions for classes $\Pi _n$ and $\Sigma _n$ , $n\ge 1$ , over $\mathsf {EA}$ which could be found in [Reference Beklemishev and Pakhomov9, Appendix A]. And we will use truth definitions for classes ${\Pi }_n$ and ${\Sigma }_n$ , $n\ge 1$ , over $\mathsf {EA}(X)$ that as well were constructed in [Reference Beklemishev and Pakhomov9, Appendix A].

In the case of second-order arithmetic there are partial truth definitions for classes $\Pi ^1_n(\Pi ^0_m)$ , $\Sigma ^1_n(\Sigma ^0_m)$ , $\Sigma ^1_n(\Pi ^0_m)$ , and $\Pi ^1_n(\Sigma ^0_m)$ , where $m\ge 1$ , over $\mathsf {RCA}_0$ . One could easily construct this partial truth definitions from the partial truth definitions for classes ${\Pi }_n$ and ${\Sigma }_n$ over $\mathsf {EA}(X)$ . However, over $\mathsf {ACA}_0$ it is possible to construct partial truth definitions for the classes $\Pi ^1_n$ and $\Sigma ^1_n$ , $n\ge 1$ . Let ${\Sigma }^1_1$ be the class of $\Sigma ^1_1$ -formulas with a set parameter X. It is easy to construct partial truth definitions for classes $\Pi ^1_n$ and $\Sigma ^1_n$ , $n\ge 1$ , from a partial truth definition for ${\Sigma }^1_1$ . Simpson [Reference Simpson24, Lemma V.1.4] proves that for each $\Sigma ^1_1$ formula $\varphi (X)$ there exists a $\Delta ^0_0$ formula $\theta (x,y)$ such that

$$\begin{align*}\mathsf{ACA}_0\vdash \forall X\big(\varphi(X)\mathrel{\leftrightarrow} (\exists f\colon \mathbb{N}\to\mathbb{N})\;\forall m\; \theta_{\varphi}(X\upharpoonright m,f \upharpoonright m)\big).\end{align*}$$

Here $X\upharpoonright m$ is the natural number encoding the finite set $X\cap \{0,\ldots ,m-1\}$ and $f\upharpoonright m$ is the code of the finite sequence $\langle f(0),\ldots ,f(m-1)\rangle $ . From Simpson’s proof it is easy to extract a Kalmar elementary algorithm for constructing the formula $\theta _{\varphi }$ from a formula $\varphi $ . And by the same argument as Simpson we show that the $\Sigma ^1_1$ -formula $(\exists f\colon \mathbb {N}\to \mathbb {N})\;\forall m\; \mathsf {Tr}_{\Pi ^0_1}(\theta _{x}(X\upharpoonright m,f \upharpoonright m))$ is a partial truth definition $\mathsf {Tr}_{{\Sigma }^1_1}(X,x)$ for the class $\mathbf {\Sigma }^1_1$ over $\mathsf {ACA}_0$ .

2.2 Ordinal notations

There are many ways of treating ordinal notations in arithmetic. We choose one specific method that will be suitable when we work in the theory $\mathsf {EA}^+$ (and its extensions). Our results will be valid for other natural choices of treatment of ordinal notations, but some of the proofs would have to be tweaked slightly.

Often we will use ordinal notation systems within formal theories that couldn’t prove (or even express) the well-foundedness of the notation systems. Also, most of our results are intensional in nature and don’t require the notation system to be well-founded from an external point of view. Due to this, our definition of an ordinal notation system does not require it to be well-founded.

Officially, an ordinal notation $\alpha $ is a tuple $\langle \varphi (x),\psi (x,y), p, n \rangle $ where $\varphi ,\psi \in \Delta _0$ , $\varphi (n)$ is true according to $\mathsf {Tr}_{\Sigma _1}$ , and p is an $\mathsf {EA}$ proof of the fact that on the set $\{x\mid \varphi (x)\}$ the order

$$\begin{align*}x\prec_{\alpha}y\stackrel{{\text{def}}}{\iff} \psi(x,y)\end{align*}$$

is a strict linear order. More formally p is an $\mathsf {EA}$ proof of the conjunction of the following sentences:

1. 1. $\forall x,y,z \big (\varphi (x)\land \varphi (y)\land \varphi (z)\land \psi (x,y)\land \psi (y,z)\to \psi (x,z)\big )$ (Transitivity);

2. 2. $\forall x \big (\varphi (x)\to \neg \psi (x,x)\big )$ (Irreflexivity);

3. 3. $\forall x,y \Big (\varphi (x)\land \varphi (y)\land x\ne y \to \big (\psi (x,y)\land \neg \psi (y,x)\big )\lor \big (\psi (y,x)\land \neg \psi (x,y)\big )\Big )$ (Antisymmetry).

We now define a partial order $\prec $ on the set of all notation systems. Any tuples $\alpha =\langle \varphi ,\psi ,p,n\rangle $ and $\alpha '=\langle \varphi ',\psi ',p',n\rangle $ are $\prec $ -incomparable if either $\varphi \ne \varphi '$ , or $\psi \ne \psi '$ , or $p\ne p'$ . If $\alpha ,\beta $ are of the form $\alpha =\langle \varphi ,\psi ,p,n\rangle $ and $\beta =\langle \varphi ,\psi ,p,m\rangle $ , we put $\alpha \prec \beta $ if $\mathsf {Tr}_{\Sigma _1} \big ( \psi (n,m) \big )$ but $\mathsf {Tr}_{\Sigma _1} \big (\neg \psi (m,n) \big )$ .

Clearly the relation $\prec $ and the property of being an ordinal notation system are expressible by $\Sigma _1$ -formulas. In $\mathsf {EA}^+$ we could expand the language by a definable superexponentiation function $2^{x}_y$ . Since the superexponentiation function is $\mathsf {EA}^+$ provably monotone, by a standard technique one could show that $\mathsf {EA}^+$ proves induction for the class $\Delta _0(2^x_y)$ of formulas with bounded quantifiers in the expanded language. It is easy to show that over $\mathsf {EA}^+$ the truth of $\Delta _0$ -formulas according to the $\Sigma _1$ -truth predicate could be expressed by a $\Delta _0(2^x_y)$ formula. Thus, the order $\prec $ and the property of being an ordinal notation system are expressible by $\Delta _0(2^x_y)$ formulas, which allows us to reason about them in $\mathsf {EA}^+$ is a straightforward manner.

Let us show that $\mathsf {EA}^+$ proves that $\prec $ is a disjoint union of linear orders. First we note that the theory $\mathsf {EA}^+$ proves the $\Pi _2$ soundness of $\mathsf {EA}$ (i.e. $\mathsf {RFN}_{\Pi _2}(\mathsf {EA})$ , see section below). And we note that for any $\alpha =\langle \varphi (x),\psi (x,y), p, n \rangle $ the conclusion of p (conjunction of sentences (1)–(3)) is $\mathsf {EA}$ -provably equivalent to a $\Pi _1$ sentence. Hence for any notation system $\alpha =\langle \varphi (x),\psi (x,y), p, n \rangle $ the theory $\mathsf {EA}^+$ proves that the corresponding conjunction of sentences (1)–(3) is true. Using this we easily prove in $\mathsf {EA}^+$ that $\prec $ is a linear ordering, when restricted to the tuples that share the same first three components.

For an ordinal notation $\alpha $ the value of $|\alpha |$ is either an ordinal or $\infty $ . If the lower cone $(\{\beta \mid \beta \prec \alpha \},\prec )$ is well-founded, then $|\alpha |$ is the ordinal isomorphic to the well-ordering $(\{\beta \mid \beta \prec \alpha \},\prec )$ . Otherwise, $|\alpha |=\infty $ . In other words, $|\alpha |$ is the well-founded rank of $\alpha $ in the $\prec $ -order.

An alternative (more standard) approach to treating ordinal notations in arithmetic is to fix an elementary ordinal notation up to some ordinal $\boldsymbol \alpha $ . This is a fixed linear order $\mathbf {L}=(\mathcal {D}_{\mathbf {L}},\prec _{\mathbf {L}})$ , where both $\mathcal {D}_{\mathbf {L}}\subseteq \mathbb {N}$ and $\prec _{\mathbf {L}} \subseteq \mathbb {N}\times \mathbb {N}$ are given by $\Delta _0$ formulas such that (i) $\mathbf {L}$ is provably linear in $\mathsf {EA}$ , (ii) $\mathbf {L}$ is well-founded, and (iii) the order type of $\mathbf {L}$ is $\boldsymbol \alpha $ . It has been empirically observed that the ordinal notation systems that arise in ordinal analysis results in proof theory are of this kind; see, e.g., [Reference Rathjen, Cooper and Truss21]. Note that from any $\mathbf {L}$ of this sort we could easily form an ordinal notation (in our sense) $\alpha $ such that there is a Kalmar elementary isomorphism f between $\mathbf {L}$ and $(\{\beta \mid \beta \prec \alpha \},\prec )$ ; moreover, the latter is provable in $\mathsf {EA}^+$ .

Further we will work with ordinal notation systems that are given by some combinatorially defined system of terms and order on them. The standard example of such a system is the Cantor ordinal notation system up to $\varepsilon _0$ . For the notations that we will consider it will be always possible to formalize in $\mathsf {EA}$ the definition and proof that the order is linear. Thus, as described above, we will be able to form an ordinal notation $\alpha $ such that there will be a natural isomorphism between $(\{\beta \mid \beta \prec \alpha \},\prec )$ and the initial combinatorially defined ordinal notation system. We will make transitions from combinatorial definitions of notation systems to ordinal notation systems in our sense without any further comments.

Moreover, we will use expressions like $\omega ^{\alpha }$ and $\varepsilon _{\alpha }$ , where $\alpha $ is some ordinal notation system. Let us consider a notation system $\alpha =\langle \varphi (x),\psi (x,y),p,n\rangle $ and define the notation system $\omega ^{\alpha }=\langle \varphi '(x),\psi '(x,y),p',n'\rangle $ . We want the order $\prec _{\omega ^\alpha }$ to be the order on the terms $\omega ^{a_1}+\cdots +\omega ^{a_k}$ , where $a_1\succeq _{\alpha }\cdots \succeq _{\alpha }a_k$ . And the order $\prec _{\omega ^\alpha }$ is defined as the usual order on Cantor normal forms, where we compare $a_i$ by the order $\prec _{\alpha }$ . By arithmetizing this definition of $\prec _{\omega ^{\alpha }}$ we get $\varphi '$ , $\psi '$ , and $p'$ . We put $n'$ to be the number encoding the term $\omega ^{n}$ . Note that, according to this definition, $\alpha $ and $\omega ^{\alpha }$ are $\prec $ -incomparable. However, if $\alpha \prec \beta $ , then $\omega ^{\alpha }\prec \omega ^{\beta }$ .

The definition of the notation system $\varepsilon _{\alpha }$ is similar to that of $\omega ^{\alpha }$ . The system of terms for $\varepsilon _{\alpha }$ consists of nested Cantor normal forms built up from $0$ and elements $\varepsilon _{a}$ , for $a\in \mathsf {dom}(\prec _{\alpha })$ . The comparision of nested Cantor normal forms is defined in the standard fashion, where we compare elements $\varepsilon _{a}$ and $\varepsilon _b$ as $a\prec _{\alpha } b$ .

2.3 Reflection principles

Suppose $\mathcal {C}$ is some class of formulas in one of the languages that we consider and T is a theory in the same language. The uniform $\mathcal {C}$ reflection principle $\mathsf {RFN}_{\mathcal {C}}(T)$ over T is the schema

$$\begin{align*}\forall\vec{x} \big( \mathsf{Pr}_T(\varphi(\vec{x})) \rightarrow \varphi(\vec{x}) \big)\end{align*}$$

for all $\varphi \in \mathcal {C}$ , where $\vec {x}$ are free number variables and $\varphi (\vec {x})$ contains no other variables.

In those cases for which we have a truth-definition for $\mathcal {C}$ in T the scheme $\mathsf {RFN}_{\mathcal {C}}(T)$ can be axiomatized by the single sentence

$$\begin{align*}\forall \varphi \in \mathcal{C} \big (\mathsf{Pr}_T (\varphi) \rightarrow \mathsf{Tr}_{\mathcal{C}}(\varphi)\big).\end{align*}$$

Given an ordinal notation system $\prec $ , we informally define the operation $\mathbf {R}_{\mathcal {C}}^{\cdot }(\cdot )$ of iterated $\mathcal {C}$ reflection along $\prec $ as follows.

$$ \begin{align*} \mathbf{R}^0_{\mathcal{C}}(T) &: = T, \\ \mathbf{R}^\alpha_{\mathcal{C}}(T) &: = T + \bigcup\limits_{\beta\prec\alpha}\mathsf{RFN}_{\mathcal{C}}\big(\mathbf{R}^\beta_{\mathcal{C}}(T)\big)\text{ for } \alpha\succ 0. \end{align*} $$

More formally, we appeal to Gödel’s fixed point lemma in $\mathsf {EA}$ . We fix a formula $\mathsf {RFN}\mbox {-}\mathsf {Inst}_{\mathcal {C}}(U,x)$ , where U and x are first-order variables, that formalizes the fact that x is an instance of the scheme $\mathsf {RFN}_{\mathcal {C}}(U)$ . We now want to define a $\Sigma _1$ formula $\mathsf {Ax}_{\mathbf {R}^\alpha _{\mathcal {C}}(T)}(x)$ (note that $\alpha $ , T, and x are arguments of the formula) that defines the set of axioms of the theories $\mathbf {R}^\alpha _{\mathcal {C}}(T)$ . We define the formula as a fixed point:

$$\begin{align*}\mathsf{EA}\vdash \mathsf{Ax}_{\mathbf{R}^\alpha_{\mathcal{C}}(T)}(x)\leftrightarrow \big( \mathsf{Ax}_{T}(x) \vee \exists \beta \prec \alpha \;\mathsf{RFN}\mbox{-}\mathsf{Inst}_{\mathcal{C}}(\mathbf{R}^\beta_{\mathcal{C}}(T),x)) \big)\end{align*}$$

note that when we substitute $\mathbf {R}^\beta _{\mathcal {C}}(T)$ in $\mathsf {RFN}\mbox {-}\mathsf {Inst}_{\mathcal {C}}$ we actually substitute (the Gödel number of) $\mathsf {Ax}_{\mathbf {R}^\beta _{\mathcal {C}}(T)}$ .

Beklemishev introduced this approach to defining progressions of iterated reflection in [Reference Beklemishev1]; the reader can find a more modern version of this approach in [Reference Beklemishev8]. It is easy to prove that this definition of progressions of iterated reflection provides a unique (up to $\mathsf {EA}$ provable deductive equivalence) definition of the theories $\mathbf {R}^\alpha _{\mathcal {C}}(T)$ .

2.4 Reflexive induction

We often employ Schmerl’s technique of reflexive induction. Reflexive induction is a way of simulating large amounts of transfinite induction in weak theories. The technique is facilitated by the following theorem; we include the proof of the theorem, which is very short.

Theorem 2.1 (Schmerl)

Let T be a recursively axiomatized theory (in one of the languages that we consider) that contains $\mathsf {EA}$ . Suppose

$$\begin{align*}T \vdash \forall\alpha \Big(\mathsf{Pr}_{T} \big(\forall\beta \prec \alpha \; \varphi(\beta) \big) \rightarrow \varphi(\alpha)\Big).\end{align*}$$

Then $T \vdash \forall \alpha \;\varphi (\alpha )$ .Footnote ²

Proof. Suppose that $T \vdash \forall \alpha \Big (\mathsf {Pr}_{T} \big (\forall \beta \prec \alpha \; \varphi (\beta ) \big ) \rightarrow \varphi (\alpha )\Big ).$ We infer that

$$\begin{align*}T \vdash \forall\alpha \mathsf{Pr}_T\big(\forall \beta \prec\alpha\; \varphi(\beta)\big) \rightarrow \forall\alpha\;\varphi(\alpha),\end{align*}$$

whence it follows that

$$\begin{align*}T\vdash \mathsf{Pr}_T\big(\forall\alpha \;\varphi(\alpha)\big) \rightarrow\forall\alpha \;\varphi(\alpha).\end{align*}$$

Löb’s theorem then yields $T\vdash \forall \alpha \;\varphi (\alpha )$ . ⊣

Accordingly, to prove claims of the form $T \vdash \forall \alpha \;\varphi (\alpha )$ , we often prove that $T \vdash \forall \alpha \Big (\mathsf {Pr}_{T} \big (\forall \beta \prec \alpha \; \varphi (\beta ) \big ) \rightarrow \varphi (\alpha )\Big )$ and infer the desired claim by Schmerl’s Theorem. While working inside T, we refer to the assumption $\mathsf {Pr}_{T} \big (\forall \beta \prec \alpha \; \varphi (\beta ) \big )$ as the reflexive induction hypothesis.

3.1 $\Pi ^1_1$ -Reflection

In this subsection we examine the ordering $\prec _{\Pi ^1_1}$ on r.e. extensions of $\mathsf {ACA}_0$ , where

$$\begin{align*}T\prec_{\Pi^1_1}U\stackrel{{\text{def}}}{\iff} U\vdash \mathsf{RFN}_{\Pi^1_1}(T).\end{align*}$$

We will show that there are no infinite $\prec _{\Pi ^1_1}$ descending sequences of $\Pi ^1_1$ sound extensions of $\mathsf {ACA}_0$ . We recall that, provably in $\mathsf {ACA}_0$ , a theory T is $\Pi ^1_1$ sound if and only if T is consistent with any true $\Sigma ^1_1$ statement.

Proof. In order to prove the result in $\mathsf {ACA}_0$ we show the inconsistency of the theory $\mathsf {ACA}_0$ plus the following statement $\mathsf {DS}$ , which says that there is a descending sequence of $\Pi ^1_1$ sound extensions of $\mathsf {ACA}_0$ in the $\prec _{\Pi ^1_1}$ ordering:

$$\begin{align*}\mathsf{DS}:=\exists E\colon \langle T_i\mid i\in \mathbb{N}\rangle (\mathsf{RFN}_{\Pi^1_1}(T_{0})\land \forall x \;\mathsf{Pr}_{T_x}(\mathsf{RFN}_{\Pi^1_1} (T_{x+1}))\wedge \forall x (T_x \sqsupseteq \mathsf{ACA}_0)).\end{align*}$$

Note that $E\colon \langle T_i\mid i\in \mathbb {N}\rangle $ is understood to mean that E is a set encoding a sequence $\langle T_0,T_1,T_2,\ldots \rangle $ of r.e. theories.

If we prove that $\mathsf {ACA}_0+\mathsf {DS}$ proves its own consistency, then the inconsistency of $\mathsf {ACA}_0+\mathsf {DS}$ follows from Gödel’s second incompleteness theorem. We reason in $\mathsf {ACA}_0+\mathsf {DS}$ to prove consistency of $\mathsf {ACA}_0+\mathsf {DS}$ .

Let $E\colon \langle T_i\mid i\in \mathbb {N}\rangle $ be a sequence of theories witnessing the truth of $\mathsf {DS}$ . Let us consider the sentence $\mathsf {F}$

$$\begin{align*}\exists U\colon \langle S_i\mid i\in \mathbb{N}\rangle (S_0=T_1\land \forall x \;\mathsf{Pr}_{S_x}(\mathsf{RFN}_{\Pi^1_1}(S_{x+1})) \wedge\forall x (S_x \sqsupseteq \mathsf{ACA}_0)).\end{align*}$$

The sentence $\mathsf {F}$ is true since we could take $\langle T_{i+1}:i\in \mathbb {N}\rangle $ as U. It is easy to observe that $\mathsf {F}$ is $\Sigma ^1_1$ .

From $\mathsf {RFN}_{\Pi ^1_1}(T_{0})$ we get that $T_{0}$ is consistent with any true $\Sigma ^1_1$ statement. Thus, we infer that

$$\begin{align*}\mathsf{Con}(T_{0} + \mathsf{F}).\end{align*}$$

Now using the fact that $\mathsf {Pr}_{T_0} \big (\mathsf {RFN}_{\Pi ^1_1}(T_{1})\big )$ and that $T_0\sqsupseteq \mathsf {ACA}_0$ we conclude,

$$\begin{align*}\mathsf{Con}( \mathsf{ACA}_0 + \mathsf{RFN}_{\Pi^1_1}(T_{1}) + \mathsf{F}).\end{align*}$$

But it is easy to see that $\mathsf {RFN}_{\Pi ^1_1}(T_{1}) + \mathsf {F}$ implies $\mathsf {DS}$ in $\mathsf {ACA}_0$ . In particular, we may take $\langle T_1, T_2, \ldots \rangle $ as our new witness to $\mathsf {DS}$ . Thus, we conclude that $\mathsf {Con}(\mathsf {ACA}_0+\mathsf {DS})$ . ⊣

We now observe that a similar result holds over $\mathsf {RCA}_0$ . To do so, we consider formulas from the complexity class $\Pi ^1_1(\Sigma ^0_2)$ (see Section 2.4). It is easy to see that the proof of Theorem 3.3 remains valid if we replace the theory $\mathsf {ACA}_0$ with $\mathsf {RCA}_0$ , the complexity class $\Pi ^1_1$ with $\Pi ^1_1(\Sigma ^0_2)$ , and the complexity class $\Sigma ^1_1$ with $\Sigma ^1_1(\Pi ^0_2)$ . Thus, we also infer the following.

3.2 $\Pi _3$ soundness

In this subsection we study the complexity of descending sequences of r.e. theories with respect to $\Pi _3$ soundness. We recall that (provably in $\mathsf {EA}$ ) a theory T is $\Pi _3$ sound just in case T is 2-consistent, i.e., just in case T is consistent with any true $\Pi _2$ sentence.

Proof. If the theorem fails, then the following sentence is true,

$$\begin{align*}\mathsf{DS}:= \exists e\colon\langle T_i \mid i\in \mathbb{N}\rangle \; \Big(\mathsf{RFN}_{\Pi_3}(T_0) \wedge \forall x \;\mathsf{Pr}_{T_x} \big(\mathsf{RFN}_{\Pi_3}(T_{x+1}) \big) \Big),\end{align*}$$

where $\exists e:\langle T_i : i\in \mathbb {N}\rangle $ is understood to mean that e is an index for a Turing machine enumerating the sequence $\langle T_0, T_1, \ldots \rangle $ .

We show that $\mathsf {EA}+\mathsf {DS}$ proves its own consistency, whence, by Gödel’s second incompleteness theorem, $\mathsf {EA}+\mathsf {DS}$ is inconsistent and hence $\mathsf {DS}$ is false.

Work in $\mathsf {EA}+\mathsf {DS}$ . Since $\mathsf {DS}$ is true, it has some witness $e\colon \langle T_i \mid i\in \mathbb {N}\rangle $ . We now consider the sequence $e'$ that results from omitting $T_0$ from e. More formally, we consider the sequence $e'\colon \langle T^{\prime }_i\mid i\in \mathbb {N}\rangle ,$ which is numerated by the Turing functional $\{e'\}:x\mapsto \{e\}(x+1)$ . That is, for each i, $T_i'=T_{i+1}$ .

From $\mathsf {DS}$ we infer that for all x, $T_{x+1} \vdash \mathsf {RFN}_{\Pi _3}(T_{x+2})$ . Thus, for every x, $T^{\prime }_x \vdash \mathsf {RFN}_{\Pi _3}(T^{\prime }_{x+1})$ by the definition of $e'$ .

From the first conjunct of $\mathsf {DS}$ we infer that $\mathsf {RFN}_{\Pi _3}(T_0)$ . That is, $T_0$ is consistent with any $\Pi _2$ truth. Thus, we infer that

$$\begin{align*}T_0+\forall x \;\mathsf{Pr}_{T^{\prime}_x} \big(\mathsf{RFN}_{\Pi_3}(T^{\prime}_{x+1})\big)\end{align*}$$

is consistent.

On the other hand, from $\mathsf {DS}$ we infer that $T_0$ proves the $\Pi _3$ soundness of $T^{\prime }_0$ . So it is consistent that $e'$ witnesses $\mathsf {DS}$ . ⊣

3.3 Consistency

In this subsection we provide a new proof of a theorem independently due to H. Friedman, Smorynski, and Solovay (see [Reference Lindström17, Reference Smorynski26]). Before stating the theorem we recall that, $\mathsf {EA}$ proves the equivalence of, the consistency sentences $\mathsf {Con}(T)$ and the $\Pi _1$ -reflection principle $\mathsf {RFN}_{\Pi _1}(T)$ .

Proof. Suppose, toward a contradiction, that there is a recursively enumerable sequence $(T_n)_{n<\omega }$ of r.e. extensions of $\mathsf {EA}$ such that $T_0$ is consistent and such that

$$\begin{align*}\mathsf{EA}\vdash \forall x \; \mathsf{Pr}_{T_x} \big( \mathsf{Con}(T_{x+1}) \big).\end{align*}$$

Since $\mathsf {EA}$ is sound, we also infer that for every n, $T_n \vdash \mathsf {Con}(T_{n+1})$ . Thus the following sentence is true.

$$\begin{align*}\mathsf{DS}:= \exists e\colon\kern-2pt\langle\kern-1pt T_i \kern-1.5pt\mid\kern-1.5pt i\kern-1.5pt\in\kern-1pt \mathbb{N}\rangle \Big(\kern-2pt\mathsf{Con}(T_0) \wedge \mathsf{Pr}_{\mathsf{EA}} \big( \forall x \; \mathsf{Pr}_{T_x} (\mathsf{Con}(T_{x+1})) \kern-1pt\big) \kern-1.5pt\wedge \kern-1.5pt\forall x \kern-1pt\;\mathsf{Pr}_{T_x} \kern-1pt\big(\mathsf{Con}(T_{x+1}) \kern-1pt\big) \kern-2pt\Big),\end{align*}$$

where $\exists e:\langle T_i : i\in \mathbb {N}\rangle $ is understood to mean that e is an index for a Turing machine enumerating the sequence $\langle T_0, T_1, \ldots \rangle $ .

We show that $\mathsf {EA}+\mathsf {DS}$ proves its own consistency, whence, by Gödel’s second incompleteness theorem, $\mathsf {EA}+\mathsf {DS}$ is inconsistent and hence $\mathsf {DS}$ is false.

Work in $\mathsf {EA}+\mathsf {DS}$ . Since $\mathsf {DS}$ is true, it has some witness $e\colon \langle T_i \mid i\in \mathbb {N}\rangle $ . We consider the sequence $e'\colon \langle T^{\prime }_i \mid i\in \mathbb {N}\rangle $ that results from dropping $T_0$ from the sequence produced by e. More formally, we consider the sequence $e'$ which is numerated by the Turing functional $\{e'\}:x\mapsto \{e\}(x+1)$ .

Claim. $e'$ is provably a witness to $\mathsf {DS}$ in $T_0$ .

To see that $e'$ provably witnesses the third conjunct of $\mathsf {DS}$ in $T_0$ , we reason as follows.

$$ \begin{align*} \mathsf{EA}\vdash&\forall x \; \mathsf{Pr}_{T_{x+1}} \mathsf{Con}(T_{x+2}) \text{ by } \mathsf{DS}.\\ \mathsf{EA}\vdash&\forall x \; \mathsf{Pr}_{T^{\prime}_x} \mathsf{Con}(T^{\prime}_{x+1}) \text{ since } T^{\prime}_x=T_{x+1} \text{ by definition of } e'. \\ T_0\vdash&\forall x \;\mathsf{Pr}_{T^{\prime}_x} \mathsf{Con}(T^{\prime}_{x+1}) \text{ since } T_0 \text{extends } \mathsf{EA}. \end{align*} $$

To see that $e'$ provably witnesses the second conjunct of $\mathsf {DS}$ in $T_0$ , we reason as follows.

$$ \begin{align*} \mathsf{EA}\vdash&\forall x \;\mathsf{Pr}_{T^{\prime}_x} \mathsf{Con}(T^{\prime}_{x+1}) \text{ as above.}\\ \mathsf{EA}\vdash&\mathsf{Pr}_{\mathsf{EA}} \big(\forall x \;\mathsf{Pr}_{T^{\prime}_x} \mathsf{Con}(T^{\prime}_{x+1})\big) \text{ by the } \Sigma_1 \text{ completeness of } \mathsf{EA}.\\ T_0\vdash&\mathsf{Pr}_{\mathsf{EA}} \big(\forall x \;\mathsf{Pr}_{T^{\prime}_x} \mathsf{Con}(T^{\prime}_{x+1})\big) \text{ since } T_0 \text{ extends } \mathsf{EA}. \end{align*} $$

We now show that $e'$ provably witnesses the first conjunct of $\mathsf {DS}$ in $T_0$ . From the first conjunct of $\mathsf {DS}$ we infer that $\mathsf {Con}(T_0)$ . It follows that $T_0$ is $\Pi _1$ sound. We reason as follows.

$$ \begin{align*} &T_{0} \vdash \mathsf{Con}(T_{1}) \text{ by } \mathsf{DS}.\\ &T_0 \vdash \mathsf{Con}(T^{\prime}_0) \text{ since provably } T^{\prime}_0=T_1. \end{align*} $$

We then infer that $\mathsf {Con}(T^{\prime }_0)$ by the $\Pi _1$ soundness of $T_0$ . So $e'$ is provably a witness to $\mathsf {DS}$ in a consistent theory. Therefore $\mathsf {EA}+\mathsf {DS}$ is consistent. ⊣

3.4 $\Pi _2$ soundness

We now know that there are no recursive descending sequences of $\Pi _3$ sound theories with respect to the $\Pi _3$ reflection order, but there are recursive descending sequences of consistent theories with respect to consistency strength. In this subsection we treat the remaining case, namely, $\Pi _2$ soundness. We prove that there is an infinite sequences $\langle T_0, T_1, \ldots \rangle $ of $\Pi _2$ sound extensions of $\mathsf {EA}$ such that for all n, $T_n \vdash \mathsf {RFN}_{\Pi _2}(T_{n+1})$ . In this sense, Theorem 3.4 is best possible.

In the section, for technical reasons it will be useful for us to impose some natural conditions on our proof predicate. We make sure that any proof in our proof system has only one conclusion, whence

$$\begin{align*}\mathsf{EA}\vdash \forall x,y_1,y_2 \Big( \big(\mathsf{Prf}_{T}(x,y_1)\land \mathsf{Prf}_{T}(x,y_2) \big) \to y_1=y_2 \Big).\end{align*}$$

Moreover, we arrange the proof system so that indices for statements are less than or equal to the indices for their proofs, i.e.,

(1) $$ \begin{align}\mathsf{EA}\vdash\forall x,y(\mathsf{Prf}_{T}(x,y)\to y\le x).\end{align} $$

Note that the conclusions of the theorems in our paper are not sensitive to the choice of proof predicate as long as the resulting provability predicates are $\mathsf {EA}$ -provably equivalent. And it is easy to see that even if our initial choice of $\mathsf {Prf}_{T}(x,\varphi )$ didn’t satisfy the mentioned conditions, it is easy to modify it to satisfy the conditions, while preserving the provability predicate $\mathsf {Pr}_{T}(\varphi )$ up to $\mathsf {EA}$ -provable equivalence.

Before proving the theorem we make a few more remarks preliminary remarks. We use the symbol to denote the truncated subtraction function, i.e., if $n>m$ and $0$ otherwise. We remind the reader that, provably in $\mathsf {EA}$ , a theory is $\Sigma _1$ sound if and only if it is $\Pi _2$ sound. We also pause to make the following remark, which will invoke in the proof of the theorem.

Remark 3.7. For any $\Pi _2$ sound extension T of $\mathsf {EA}$ , the theory $T+ \neg \mathsf {RFN}_{\Pi _2}(T)$ is $\Pi _2$ sound. This is actually an instance Gödel’s second incompleteness theorem that is applied to $1$ -provability rather than the ordinary provability. Recall that $1$ -provability predicate $1\mbox {-}\mathsf {Pr}_T(\varphi )$ for a theory T is

(2) $$ \begin{align} \exists \psi\in \Sigma_2\big(\mathsf{Tr}_{\Sigma_2}(\psi)\land \mathsf{Pr}_T(\psi\to\varphi)\big). \end{align} $$

The consistency notion that corresponds to $1$ -provability is precisely $\Pi _2$ -soundness:

(3) $$ \begin{align} \mathsf{EA}\vdash \forall \varphi\;\big(\lnot 1\mbox{-}\mathsf{Pr}_T(\lnot \varphi)\mathrel{\leftrightarrow}\mathsf{RFN}_{\Pi_2}(T+\varphi)\big). \end{align} $$

It is easy to see that $1$ -provability predicate for a theory T satisfies the usual Hilbrt-Bernays-Löb derivability conditions. Thus Gödel’s second incompleteness theorem for it states that if a theory $T\sqsupseteq \mathsf {EA}$ is $\Pi _2$ -sound, then $\mathsf {RFN}_{\Pi _2}(T)$ is not $1$ -provable in T. And the latter is equivalent to $\Pi _2$ -soundness of $T+\lnot \mathsf {RFN}_{\Pi _2}(T)$ .

We are now ready for the proof of the theorem.

Proof. For each $n\in \mathbb {N}$ , we define the sentence $\varphi _n$ as follows:

That is, $\varphi _n$ expresses “ $\mathsf {I}\Sigma _2$ proves a false $\Sigma _1$ sentence via a proof p, and $\Pi _2$ reflection for $\mathsf {EA}$ can be iterated up to

.”

The motivation for picking that individual formula is as follows: To find a descending sequence, we will iterate $\Pi _2$ reflection up to some nonstandard number. So we need to make sure that our formula forces a certain number to be nonstandard but without implying any false $\Pi _2$ sentences. The way we do that is by saying that $\mathsf {I}\Sigma _2$ proves a false $\Sigma _1$ sentence. This has (we will show) no false $\Pi _2$ consequences. However, (the code of) any proof witnessing a failure of $\Sigma _1$ soundness in $\mathsf {I}\Sigma _2$ must be nonstandard. We find our descending sequence by iterating $\Pi _2$ reflection up to this nonstandard number.

Now the formal details start. We need to check that $\varphi _n$ is $\Pi _2$ sound for each n, and that $\mathsf {EA}+ \varphi _n \vdash \mathsf {RFN}_{\Pi _2}(\mathsf {EA}+\varphi _{n+1})$ .

Claim. $\mathsf {EA} + \varphi _n$ is $\Pi _2$ sound for each n.

The first thing to note is that

(4) $$ \begin{align} \mathsf{I}\Sigma_2 \vdash \forall x \;\mathsf{RFN}_{\Pi_2}\big(\mathbf{R}_{\Pi_2}^x(\mathsf{EA})\big). \end{align} $$

Indeed, $\mathsf {I}\Sigma _2$ can prove the latter claim by induction on x. Recall that $\mathsf {I}\Sigma _2 \equiv I\Pi _2$ and $\forall x\; \mathsf {RFN}_{\Pi _2}\big (\mathbf {R}_{\Pi _2}^x(\mathsf {EA})\big )$ is a $\Pi _2$ -formula, hence $\mathsf {I}\Sigma _2$ could formalize the necessary induction. Also it is known that $\mathsf {I}\Sigma _2\sqsupseteq \mathsf {I}\Sigma _1\equiv \mathsf {EA}+\mathsf {RFN}_{\Pi _3}(\mathsf {EA})$ and that

$$\begin{align*}\mathsf{EA}+\mathsf{RFN}_{\Pi_3}(\mathsf{EA})\vdash \psi\to \mathsf{RFN}_{\Pi_2}(\mathsf{EA}+\psi),\end{align*}$$

for any $\Pi _2$ -formula $\psi $ . This allows us to verify the base and step of the induction in $\mathsf {I}\Sigma _2$ .

The second thing to note is that, since $\Pi _2$ reflection is provably equivalent (in $\mathsf {EA}$ ) to $\Sigma _1$ reflection, it follows that:

(5) $$ \begin{align} \mathsf{I}\Sigma_2 + \neg \mathsf{RFN}_{\Pi_2}(\mathsf{I}\Sigma_2) \vdash \exists \psi \in \Sigma_1 \exists p \big( \mathsf{Prf}_{\mathsf{I}\Sigma_2}(p,\psi) \wedge \neg \mathsf{True}_{\Sigma_1}(\psi) \big). \end{align} $$

Putting these two observations together, we infer that, for each standard $n\in \mathbb {N}$ ,

(6)

which is just to say that for each standard $n\in \mathbb {N}$ , $\mathsf {I}\Sigma _2 + \neg \mathsf {RFN}_{\Pi _2}(\mathsf {I}\Sigma _2) \vdash \varphi _n$ . Thus, to see that $\mathsf {EA}+\varphi _n$ is $\Pi _2$ sound, it suffices to observe that $\mathsf {I}\Sigma _2 + \neg \mathsf {RFN}_{\Pi _2}(\mathsf {I}\Sigma _2)$ is $\Pi _2$ sound. The latter claim follows immediately from Remark 3.7.

Before checking that $\mathsf {EA}+ \varphi _n \vdash \mathsf {RFN}_{\Pi _2}(\mathsf {EA}+\varphi _{n+1})$ , we will establish the following lemma:

Lemma 3.9. For all standard $n\in \mathbb {N}$ ,

$$\begin{align*}\mathsf{EA} \vdash \forall p \forall \psi\in\Sigma_1 \Big( \big( \mathsf{Prf}_{\mathsf{I}\Sigma_2}(p,\psi) \wedge \neg \mathsf{True}_{\Sigma_1}(\psi) \big) \rightarrow p>n \Big).\end{align*}$$

Proof. The first thing to note is that (by the $\Sigma _1$ soundness of $\mathsf {I}\Sigma _2$ and the $\Sigma _1$ completeness of $\mathsf {EA}$ ) for any $\psi \in \Sigma _1$ , if $\mathsf {I}\Sigma _2\vdash \psi $ then also $\mathsf {EA}\vdash \psi $ . Now, for any standard $p\in \mathbb {N}$ , $\mathsf {EA}$ can check whether p constitutes an $\mathsf {I}\Sigma _2$ proof of a $\Sigma _1$ sentence $\psi $ , and if p does constitute such a proof, then $\mathsf {EA}$ will prove $\psi $ as well. That is, for each standard $p\in \mathbb {N}$ :

$$\begin{align*}\mathsf{EA} \vdash \forall \psi \in \Sigma_1 \Big( \mathsf{Prf}_{\mathsf{I}\Sigma_2}(p,\psi) \rightarrow \mathsf{True}_{\Sigma_1}(\psi) \Big).\end{align*}$$

It follows that for each standard $n\in \mathbb {N}$ :

$$\begin{align*}\mathsf{EA} \vdash \forall p\leq n \forall \psi \in \Sigma_1 \Big( \mathsf{Prf}_{\mathsf{I}\Sigma_2}(p,\psi) \rightarrow \mathsf{True}_{\Sigma_1}(\psi) \Big).\end{align*}$$

Whence for each standard $n\in \mathbb {N}$ :

$$\begin{align*}\mathsf{EA} \vdash \forall p \forall \psi \in \Sigma_1 \Big( \big(\mathsf{Prf}_{\mathsf{I}\Sigma_2}(p,\psi) \wedge \neg \mathsf{True}_{\Sigma_1}(\psi) \big) \rightarrow p>n \Big).\end{align*}$$

This completes the proof of the lemma.  ⊣

With the lemma on board, we are now ready to verify the following claim:

Claim. For each $n\in \mathbb {N}$ ,

$$\begin{align*}\mathsf{EA}+ \varphi_n \vdash \mathsf{RFN}_{\Pi_2}(\mathsf{EA}+\varphi_{n+1}).\end{align*}$$

Let’s fix an $n\in \mathbb {N}$ and reason in $\mathsf {EA}+\varphi _n$ :

According to $\varphi _n$ , there is an $\mathsf {I}\Sigma _2$ proof p of a false $\Sigma _1$ sentence $\psi $ and

is $\Pi _2$ -sound. From Lemma 3.9 we infer that $p>n$ . It follows that

, whence

. Hence

(7)

Thus

Since $\mathsf {Prf}_{\mathsf {I}\Sigma _2}(p,\psi )$ is a true $\Sigma _1$ sentence and $\psi $ is a false $\Sigma _1$ sentence we infer that

Which straightforwardly implies $\mathsf {RFN}_{\Pi _2} ( \mathsf {EA} + \varphi _{n+1})$ . This completes the proof of the theorem.  ⊣

4.1 Iterated reflection and recursive comprehension

Recall that there are no descending chains in the $\mathsf {RFN}_{\Pi ^1_1(\Sigma ^0_2)}$ ordering of ${\Pi ^1_1(\Sigma ^0_2)}$ sound extensions of $\mathsf {RCA}_0$ (this is Theorem 3.3). In this subsection we investigate iterated $\Pi ^1_1(\Sigma ^0_2)$ reflection over the theory $\mathsf {RCA}_0$ . The main result of this subsection is that $\mathbf {R}^\alpha _{\Pi ^1_1(\Sigma ^0_2)}(\mathsf {RCA}_0)$ is $\Pi ^1_1$ conservative over $\mathbf {R}^{1+\alpha }_{\mathbf {\Pi }^0_3}(\mathsf {EA}^+(X))$ . This result will be used in the next section to calculate $\Pi ^1_1$ proof-theoretic ordinals of subsystems of second-order arithmetic.

Before proving the theorem we prove a few lemmas. These lemmas concern proof-theoretic properties of theories that are closed under an inference rule that we call the $ {\Delta }^0_1$ substitution rule.

Definition 4.4. We write $\mathsf {Subst}_{\mathbf {\Delta }^0_1}[\varphi ]$ to denote the formula

$$\begin{align*}\forall \theta_1(x)\forall\theta_2(x)\Big(\forall y \big(\mathsf{Tr}_{{\Pi}^0_1}(\theta_1(y))\leftrightarrow\mathsf{Tr}_{{\Sigma}^0_1}(\theta_2(y))\big) \rightarrow \varphi[\mathsf{Tr}_{{\Pi}^0_1}(\theta_1(x))]\Big).\end{align*}$$

A theory T is closed under the $\mathbf {\Delta }^0_1$ substitution rule if, for any formula $\psi (X)$ , whenever $T\vdash \psi (X)$ then $T\vdash \mathsf {Subst}_{\mathbf {\Delta }^0_1}[\psi ]$ .

Recall that there is a translation $\varphi (X)\longmapsto \forall X\;\varphi (X)$ from the set of $\boldsymbol \Pi ^0_{\infty }$ sentences to the set of sentences of the language of second order arithmetic. Recall also that we are regarding the pseudo- $\Pi ^1_1$ language as a sublanguage of the language of second order arithmetic by identifying each pseudo $\Pi ^1_1$ sentence with its translation.

Proof. Suppose that $\mathsf {EA}^+$ proves $``T\sqsupseteq \mathsf {I}{\Sigma }_1(X)$ is closed under the $\mathbf {\Delta }^0_1$ substitution rule.” Let us use the name U for the theory $\mathsf {EA}^+(X) + \mathsf {RFN}_{\mathbf {\Pi }^0_3}(T)$ . We want to show that U is closed under the $\mathbf {\Delta }^0_1$ substitution rule. Note that, by Remark 4.7, U contains $\mathsf {I}{\Sigma _1}(X)$ . That is, $U\equiv \mathsf {I}{\Sigma _1}(X)+\mathsf {RFN}_{{\Pi }^0_3}(T)$ . Over $\mathsf {EA}(X)$ , the reflection schema $\mathsf {RFN}_{\boldsymbol \Pi ^0_3}(T)$ is equivalent to

$$\begin{align*}\forall \varphi\in {\Pi}^0_3 \Big(\mathsf{Pr}_T\big(\mathsf{Tr}_{{\Pi}^0_3}(\varphi)\big)\rightarrow\mathsf{Tr}_{{\Pi}^0_3}(\varphi)\Big).\end{align*}$$

Thus, by Lemma 4.5, it suffices to show that U proves

$$\begin{align*}\mathsf{Subst}_{{\Delta}^0_1}\left[\forall \varphi\in {\Pi}^0_3 \Big(\mathsf{Pr}_T\big(\mathsf{Tr}_{{\Pi}^0_3}(\varphi)\big)\rightarrow\mathsf{Tr}_{{\Pi}^0_3}(\varphi)\Big)\right].\end{align*}$$

But since the formula $\mathsf {Pr}_T(\mathsf {Tr}_{{\Pi }^0_3}(\varphi ))$ doesn’t contain occurrences of X, we could push $\mathsf {Subst}_{{\Delta }^0_1}$ under the quantifier, i.e., it will be sufficient to show that

$$\begin{align*}U \vdash \forall \varphi\in {\Pi}^0_3 \Big(\mathsf{Pr}_T\big(\mathsf{Tr}_{{\Pi}^0_3}(\varphi)\big)\rightarrow\mathsf{Subst}_{\mathbf{\Delta}^0_1}[\mathsf{Tr}_{{\Pi}^0_3}(\varphi)]\Big).\end{align*}$$

Observe that $\mathsf {Subst}_{\mathbf {\Delta }^0_1}[\mathsf {Tr}_{{\Pi }^0_3}(\varphi )]$ is equivalent to a ${\Pi }^0_3$ formula over $\mathsf {EA}(X)$ . We reason as follows.

This concludes the proof of the lemma.  ⊣

With these lemmas on board we are ready for the proof of the main theorem of this subsection.

Theorem 4.9. $(\mathsf {EA}^+)$ For any ordinal notation $\alpha $ ,

$$\begin{align*}\mathbf{R}^\alpha_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0) \equiv_{\boldsymbol\Pi^0_\infty} \mathbf{R}^{1+\alpha}_{{\Pi}^0_3}(\mathsf{EA}^+(X)).\end{align*}$$

Proof. We prove the claim by reflexive induction. We reason in $\mathsf {EA}^+$ and assume the reflexive induction hypothesis: provably in $\mathsf {EA}^+$ , for any $\beta \prec \alpha $ ,

$$\begin{align*}\mathbf{R}^\beta_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0) \equiv_{\boldsymbol\Pi^0_\infty} \mathbf{R}^{1+\beta}_{{\Pi}^0_3}(\mathsf{EA}^+(X)).\end{align*}$$

Of course, since $\mathsf {RCA}_0$ contains $\mathsf {EA}^+$ , this also implies that,

$$\begin{align*}\mathsf{RCA}_0 \vdash \forall \beta\prec \alpha \Big( \mathbf{R}^\beta_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0) \equiv_{\boldsymbol\Pi^0_\infty} \mathbf{R}^{1+\beta}_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big) \Big).\end{align*}$$

If $\mathsf {RCA}_0$ proves mutual $\Gamma $ conservation of two theories T and U, then $\mathsf {RFN}_{\Gamma }(T)$ and $\mathsf {RFN}_{\Gamma }(U)$ are equivalent over $\mathsf {RCA}_0$ . Thus, we immediately infer

(8) $$ \begin{align} \mathsf{RCA}_0 \vdash \forall \beta\prec \alpha \Big( \mathsf{RFN}_{\boldsymbol\Pi^0_3} \big(\mathbf{R}^\beta_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0) \big) \leftrightarrow \mathsf{RFN}_{\boldsymbol\Pi^0_3} \big(\mathbf{R}^{1+\beta}_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big)\big) \Big). \end{align} $$

We now reason as follows.

$$ \begin{align*} \mathbf{R}^\alpha_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0) &\equiv \mathsf{RCA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}\big(\mathbf{R}^\beta_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0)\big) \text{ by definition.}\\ &\equiv_{\boldsymbol\Pi^0_\infty} \mathsf{RCA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{\boldsymbol\Pi^0_3}\big(\mathbf{R}^\beta_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0)\big)\\ & \equiv \mathsf{RCA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_3}\Big(\mathbf{R}^{1+\beta}_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big)\Big) \text{ by (8).} \end{align*} $$

Since $\mathbf {R}^1_{\mathbf {\Pi }^0_3}(\mathsf {EA}^+(X))\equiv \mathsf {I}{\Sigma }_1(X)$ , we are able to show that

$$\begin{align*}\mathbf{R}^{1+\alpha}_{\mathbf{\Pi^0_3}}\big(\mathsf{EA}^+(X)\big)\equiv \mathsf{I}{\Sigma}_1(X)+\bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_3}\Big(\mathbf{R}^{1+\beta}_{{\Pi^0_3}}\big(\mathsf{EA}^+(X)\big)\Big),\end{align*}$$

by the following argument:

$$ \begin{align*} \mathbf{R}^{1+\alpha}_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big) &\equiv \mathbf{R}^1_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big) + \mathbf{R}^{1+\alpha}_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big) \text{ since } 1\leq 1+\alpha.\\ &\equiv \mathsf{I}{\Sigma}_1(X) + \mathbf{R}^{1+\alpha}_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big) \text{ since } \mathbf{R}^1_{{\Pi}^0_3}\big(\mathsf{EA}^+(X)\big)\equiv\mathsf{I}{\Sigma}_1(X).\\ &\equiv \mathsf{I}{\Sigma}_1(X)+\bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_3}\Big(\mathbf{R}^{1+\beta}_{{\Pi^0_3}}\big(\mathsf{EA}^+(X)\big)\Big) \text{ by definition.} \end{align*} $$

Hence in order to finish the proof of the lemma it will be enough to show that

$$\begin{align*}\mathsf{I}{\Sigma}_1(X)+\bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_3}(\mathbf{R}^{1+\beta}_{{\Pi^0_3}}(\mathsf{EA}^+(X)))\equiv_{{\Pi}^0_\infty} \mathsf{RCA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_3}(\mathbf{R}^{1+\beta}_{{\Pi}^0_3}(\mathsf{EA}^+(X))),\end{align*}$$

which, by Lemma 4.5, can be achieved by proving that

$$\begin{align*}\mathsf{I}{\Sigma}_1(X)+\bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_3}(\mathbf{R}^{1+\beta}_{{\Pi^0_3}}(\mathsf{EA}^+(X)))\end{align*}$$

is closed under the $\mathbf {\Delta }^0_1$ substitution rule. We will prove this closedness in the rest of the proof.

By a usual compactness argument, it will be enough to show that $\mathsf {I}{\Sigma }_1(X)$ is closed under the $\mathbf {\Delta }^0_1$ substitution rule and that for each $\beta \prec \alpha $ the theories $\mathsf {I}{\Sigma }_1(X)+ \mathsf {RFN}_{{\Pi }^0_3}(\mathbf {R}^{1+\beta }_{{\Pi ^0_3}}(\mathsf {EA}^+(X)))$ are closed under the $\mathbf {\Delta }^0_1$ substitution rule. Closure of $\mathsf {I}{\Sigma }_1(X)$ under the $\mathbf {\Delta }^0_1$ substitution rule follows directly from Lemma 4.5.

By Lemma 4.5, we infer that, for each $\beta \prec \alpha $ , $\mathbf {R}^{1+\beta }_{\mathbf {\Pi ^0_3}}(\mathsf {EA}^+(X))$ is $\mathsf {EA}^+$ provably closed under the $\mathbf {\Delta }^0_1$ substitution rule. Thus, by Lemma 4.8, we infer that for each $\beta \prec \alpha $ ,

$$\begin{align*}\mathsf{EA}^+(X) + \mathsf{RFN}_{{\Pi}^0_3}(\mathbf{R}^{1+\beta}_{{\Pi^0_3}}(\mathsf{EA}^+(X)))\end{align*}$$

is closed under the ${\Delta }^0_1$ substitution rule. Since $\mathsf {EA}^+(X) + \mathsf {RFN}_{{\Pi }^0_3}(\mathbf {R}^{1+\beta }_{{\Pi ^0_3}}(\mathsf {EA}^+(X)))\sqsupseteq \mathsf {I}{\Sigma }_1(X)$ , the theory $\mathsf {I}{\Sigma }_1(X)+ \mathsf {RFN}_{{\Pi }^0_3}(\mathbf {R}^{1+\beta }_{{\Pi ^0_3}}(\mathsf {EA}^+(X)))$ is closed under the ${\Delta }^0_1$ substitution rule. This concludes the proof of the lemma.  ⊣

4.2 Iterated reflection and arithmetical comprehension

In this subsection we investigate the relationship between iterated $\Pi ^1_1$ reflection over $\mathsf {ACA}_0$ and iterated $\Pi ^1_1(\Sigma ^0_2)$ reflection over $\mathsf {RCA}_0$ . The main theorem of this subsection is that $\mathbf {R}^\alpha _{\Pi ^1_1}(\mathsf {ACA}_0)$ is $\Pi ^1_1(\Sigma ^0_2)$ conservative over $\mathbf {R}^{\varepsilon _\alpha }_{\Pi ^1_1(\Sigma ^0_2)}(\mathsf {RCA}_0)$ . The proof of the main theorem of this subsection is similar to the proof of Theorem 4.9. For our first step towards this result, we establish a conservation theorem relating extensions of $\mathsf {ACA}_0$ with extensions of $\mathsf {PA}(X)$ .

There is a standard semantic argument that $\mathsf {ACA}_0$ is conservative over $\mathsf {PA}$ (see, e.g., [Reference Simpson24, Section IX.1]). We will present a version of this argument for extensions of $\mathsf {ACA}_0$ by $\Pi ^1_1$ sentences. Moreover we ensure that this conservation result is provable in $\mathsf {ACA}_0$ . Before presenting the argument, we will say a bit about how we will formalize model theory within $\mathsf {ACA}_0$ for the purposes of our argument.

We will reason in $\mathsf {ACA}_0$ and use the formalization of model theory from [Reference Simpson24, Section II.8]. Recall that according to formalization from [Reference Simpson24, Section II.8] a model $\mathfrak {M}$ essentially is a set that encodes the domain of $\mathfrak {M}$ (which is by necessity a subset of $\mathbb {N}$ ) and the full satisfaction relation for $\mathfrak {M}$ (the latter essentially is the elementary diagram of the model $\mathfrak {M}$ ). Note that if one would require $\mathfrak {M}$ contain information only about the satisfaction of atomic formulas, rather than all formulas, the resulting notion of a model would be weaker. This is due to the fact that in $\mathsf {ACA}_0$ , unlike in stronger theories, it is not always possible to recover the elementary diagram of a model from its atomic diagram.

Due to this limitation, in $\mathsf {ACA}_0$ it is sometimes (including in our proof) useful to employ weak models [Reference Simpson24, Definition II.8.9]. A weak model $\mathfrak {M}$ of a theory T is a set that encodes the domain of $\mathfrak {M}$ and a partial satisfaction relation for $\mathfrak {M}$ that is defined only on Boolean combinations of subformulas of formulas used in axioms of T such that all the axioms of T are according to this satisfaction relation. The key fact that we use is that $\mathsf {ACA}_0$ proves that any theory that has a weak model is consistent [Reference Simpson24, Theorem II.8.10].

Proof. Suppose that T proves every substitution variant of its own axioms. Let $\theta $ be a $\boldsymbol \Pi ^0_{\infty }$ formula and let $\varphi (X)$ be a theorem of T. Since $\varphi (X)$ is a theorem of T, there is some finite conjunction $A_T(X)$ of axioms of T such that the sentence

$$\begin{align*}A_T(X) \rightarrow \varphi(X)\end{align*}$$

is a theorem of pure logic. Since pure logic is closed under substitution, the sentence

$$\begin{align*}A_T[\theta(x)] \rightarrow \varphi[\theta(x)]\end{align*}$$

is also a theorem of pure logic. Since T proves every substitution variant of its own axioms, T proves $A_T[\theta (x)]$ , whence T proves $\varphi [\theta (x)]$ . ⊣

Proof. We prove the claim by reflexive induction. We reason within $\mathsf {EA}^+$ and assume the reflexive induction hypothesis: provably in $\mathsf {EA}^+$ , for all $\beta \prec \alpha $ , $\mathsf {PA}(X) + \mathbf {R}^\beta _{{\Pi }^0_\infty }(\mathsf {PA}(X))$ is closed under substitution. First we note that

$$\begin{align*}\mathbf{R}^\alpha_{{\Pi}^0_\infty}\big(\mathsf{PA}(X)\big) \equiv \mathsf{PA}(X) + \bigcup\limits_{\beta\prec\alpha}\mathsf{RFN}_{{\Pi}^0_\infty}\Big(\mathbf{R}^\beta_{{\Pi}^0_\infty}\big(\mathsf{PA}(X)\big)\Big).\end{align*}$$

For $\beta \prec \alpha $ let us denote by $S_\beta $ the theory

$$\begin{align*}\mathsf{PA}(X) + \mathsf{RFN}_{{\Pi}^0_\infty}\Big(\mathbf{R}^\beta_{{\Pi}^0_\infty}\big(\mathsf{PA}(X)\big)\Big).\end{align*}$$

To prove that $\mathbf {R}^\alpha _{{\Pi }^0_\infty }\big (\mathsf {PA}(X)\big )$ is closed under substitution it suffices to prove that, for every $\beta \prec \alpha $ , $S_{\beta }$ is closed under substitution.

By Lemma 4.13, to prove that $S_\beta $ is closed under substitution, it suffices to show that $S_\beta $ proves every substitution-variant of its own axioms. Let us use the name $U_{\beta }$ to denote the theory $\mathbf {R}^\beta _{{\Pi }^0_\infty }\big (\mathsf {PA}(X)\big )$ . An axiom of the theory $S_\beta $ is either an axiom of $\mathsf {PA}(X)$ or is a sentence of the form $\forall \vec {y}\big (Pr_{U_{\beta }}\big (\varphi (X,\vec {y})\big )\rightarrow \varphi (X,\vec {y})\big )$ . Already the theory $\mathsf {PA}(X)$ proves every substitutional instance of its own axioms. By the reflexive induction hypothesis, $U_{\beta }$ is provably closed under substitution. So $S_\beta $ proves $\forall \vec {y}\big (Pr_{U_{\beta }}\big (\varphi (X,\vec {y})\big )\rightarrow \varphi (\theta ,\vec {y})\big )$ for any formula $\theta $ . This is to say that $S_\beta $ proves every substitution instance of its axioms.  ⊣

Most of the work towards proving the main theorem of this section is contained in the proof of the following key lemma.

Proof. We prove the claim by reflexive induction. We reason within $\mathsf {ACA}_0$ and assume the reflexive induction hypothesis: provably in $\mathsf {ACA}_0$ , for all $\beta \prec \alpha $ , $\mathbf {R}^\beta _{\Pi ^1_1}(\mathsf {ACA}_0)$ is $\boldsymbol \Pi ^0_\infty $ conservative over $\mathbf {R}^\beta _{{\Pi }^0_\infty }(\mathsf {PA}(X)).$ This means that, provably in $\mathsf {ACA}_0$ , for any $\beta \prec \alpha $ , $\boldsymbol \Pi ^0_\infty $ reflection over $\mathbf {R}^\beta _{\Pi ^1_1}(\mathsf {ACA}_0)$ is equivalent to $\boldsymbol \Pi ^0_\infty $ reflection over $\mathbf {R}^\beta _{ {\Pi }^0_\infty }(\mathsf {PA}(X))$ . That is:

(9) $$ \begin{align} \mathsf{ACA}_0 \vdash \forall \beta\prec\alpha \Big( \mathsf{RFN}_{\boldsymbol\Pi^0_\infty} \big(\mathbf{R}^\beta_{\Pi^1_1}(\mathsf{ACA}_0) \big) \leftrightarrow \mathsf{RFN}_{\boldsymbol\Pi^0_\infty} \big(\mathbf{R}^\beta_{\mathbf{\Pi}^0_\infty}(\mathsf{PA}(X)) \big) \Big). \end{align} $$

We reason as follows.

$$ \begin{align*} \mathbf{R}^\alpha_{\Pi^1_1}(\mathsf{ACA}_0) &\equiv \mathsf{ACA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{\Pi^1_1}\big(\mathbf{R}^\beta_{\Pi^1_1}(\mathsf{ACA}_0)\big) \text{ by definition.} \\ &\equiv_{{\Pi}^0_\infty} \mathsf{ACA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_\infty}\big(\mathbf{R}^\beta_{\Pi^1_1}(\mathsf{ACA}_0)\big) \\ & \equiv \mathsf{ACA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_\infty} \Big(\mathbf{R}^\beta_{{\Pi}^0_\infty}\big( \mathsf{PA}(X)\big) \Big) \text{ by (9).} \\ & \equiv \mathsf{ACA}_0 + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_\infty} \Big(\mathsf{PA}(X) + \mathbf{R}^\beta_{{\Pi}^0_\infty}\big( \mathsf{PA}(X)\big) \Big) \text{ by definition.} \\ & \equiv_{\boldsymbol\Pi^0_\infty} \mathsf{PA}(X) + \bigcup\limits_{\beta\prec\alpha\;\theta\in\boldsymbol \Pi^0_\infty} \mathsf{RFN}_{{\Pi}^0_\infty} \Big(\mathsf{PA}(X) + \mathbf{R}^\beta_{{\Pi}^0_\infty} \big(\mathsf{PA}(X)\big) \Big)[\theta]\\ &\qquad\text{ by Lemma 4.10.}\\ & \equiv_{\boldsymbol\Pi^0_\infty} \mathsf{PA}(X) + \bigcup\limits_{\beta\prec\alpha} \mathsf{RFN}_{{\Pi}^0_\infty} \Big(\mathsf{PA}(X) + \mathbf{R}^\beta_{{\Pi}^0_\infty} \big(\mathsf{PA}(X)\big) \Big) \text{ by Remark 4.15.}\\ & \equiv_{\boldsymbol\Pi^0_\infty} \mathbf{R}^\alpha_{{\Pi}^0_\infty}(\mathsf{PA}(X)) \text{ by definition.} \end{align*} $$

This concludes the proof.  ⊣

The proof of the main theorem of this section is now straightforward, given Theorem 4.9 and Lemma 4.16.

Proof. We reason as follows.

$$ \begin{align*} \mathbf{R}^\alpha_{\Pi^1_1}(\mathsf{ACA}_0) &\equiv_{\boldsymbol \Pi^0_\infty}\mathbf{R}^\alpha_{{\Pi}^0_\infty}(\mathsf{PA}(X)) \text{ by Lemma 4.16.} \\ &\equiv_{\boldsymbol \Pi^0_3}\mathbf{R}^{\varepsilon_\alpha}_{{\Pi}^0_3}(\mathsf{EA}^+(X)) \text{ by Theorem 4.2.} \\ &\equiv_{\boldsymbol \Pi^0_3}\mathbf{R}^{\varepsilon_\alpha}_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0) \text{ by Theorem 4.9.} \end{align*} $$

Note for each $\Pi ^1_1(\Sigma ^0_2)$ sentence $\varphi $ we could find a $\boldsymbol \Pi ^0_3$ sentence $\varphi '$ such that $\mathsf {RCA}_0$ proves the equivalence of $\varphi $ and (the translation into the second order language of) $\varphi '$ . Thus moreover we have

$$\begin{align*}\mathbf{R}^\alpha_{\Pi^1_1}(\mathsf{ACA}_0)\equiv_{\Pi^1_1(\Sigma^0_2)} \mathbf{R}^{\varepsilon_\alpha}_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0).\end{align*}$$

This completes the proof of the theorem.  ⊣

5.1 Reflection ranks

Recall that the reflection order $\prec _{\Pi ^1_1}$ on r.e. extensions of $\mathsf {ACA}_0$ is:

$$\begin{align*}{T}_1 \prec_{\Pi^1_1} {T}_2\stackrel{{\text{def}}}{\iff} {T}_2\vdash \mathsf{RFN}_{\Pi^1_1}({T}_1).\end{align*}$$

For a theory $ {T}\sqsupseteq \mathsf {ACA}_0$ we define the reflection rank $| {T}|_{\mathsf {ACA}_0}\in \mathbf {On}\cup \{\boldsymbol \infty \}$ as the rank of $ {T}$ in the order $\prec _{\Pi ^1_1}$ .

Recall that Theorem 3.2 states that $| {T}|_{\mathsf {ACA}_0}\in \mathbf {On}$ , for $\Pi ^1_1$ -sound $ {T}$ .

We will also consider the more general notion of reflection rank with respect to some other base theories. For second-order theories $ {U}\sqsupseteq \mathsf {RCA}_0$ we consider the reflection order $\prec _{\Pi ^1_1(\Sigma ^0_2)}$ :

$$\begin{align*}{U}_1 \prec_{\Pi^1_1(\Sigma^0_2)} {U}_2\stackrel{{\text{def}}}{\iff} {U}_2\vdash \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}({U}_1).\end{align*}$$

Let us consider some base theory $ {T}_0\sqsupseteq \mathsf {RCA}_0$ . We define the set $\mathcal {E}\mbox {-} {T}_0$ of all theories $ {U}$ such that $\mathsf {EA}$ proves that $ {U}\sqsupseteq {T}_0$ . For $ {U}\in \mathcal {E}\mbox {-} {T}_0$ we denote by $| {U}|_{ {T}_0}$ the rank of $ {U}$ in the order $(\mathcal {E}\mbox {-} {T}_0,\prec _{\Pi ^1_1(\Sigma ^0_2)})$ . Note that $\Pi ^1_1(\Sigma ^0_2)$ -sound extensions of $T_0$ have a well-founded rank in this ordering by Theorem 3.3.

Remark 5.3. The definition of the rank $| {T}|_{\mathsf {ACA}_0}$ given in the beginning of the section coincides with the more general definition of rank, since in $\mathsf {ACA}_0$ each $\Pi ^1_1$ formula is equivalent to a $\Pi ^1_1(\Sigma ^0_2)$ -formula and hence for any $ {T}\sqsupseteq \mathsf {ACA}_0$ ,

$$\begin{align*}\mathsf{ACA}_0\vdash \mathsf{RFN}_{\Pi^1_1}({T})\mathrel{\leftrightarrow}\mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}({T}).\end{align*}$$

Straightforwardly from Theorem 3.3 we get the following.

Remark 5.5. The converse of Corollary 5.4 is not true, there are $\Pi ^1_1(\Sigma ^0_2)$ unsound theories whose rank is an ordinal. In particular, for each consistent theory $T_0\sqsupseteq \mathsf {RCA}_0$ , we have $|T_0+\lnot \mathsf {Con}(T_0)|_{T_0}=0$ . Indeed, assume $T_0+\lnot \mathsf {Con}(T_0)\vdash \mathsf {RFN}_{\Pi ^1_1}(U)$ , for some $U\in \mathcal {E}\mbox {-}T_0$ . Then

$$\begin{align*}\begin{aligned}T_0+\lnot \mathsf{Con}(T_0) & \vdash \mathsf{RFN}_{\Pi^1_1}(T_0)\\ & \vdash \mathsf{Con}(T_0)\\ & \vdash \bot. \end{aligned}\end{align*}$$

But by Gödel’s Second Incompleteness Theorem $T_0+\lnot \mathsf {Con}(T_0) $ is consistent. This is to say that, though $T_0+\neg \mathsf {Con}(T_0)$ is not $\Pi ^1_1$ sound, $|T_0+\neg \mathsf {Con}(T_0)|_{T_0}\in \mathbf {On}$ .

Note that later we will introduce a notion of robust reflection rank that enjoys much better behavior and, in particular, satisfies the converse of Corollary 5.4.

Recall that for an ordinal notation $\alpha $ we denote by $|\alpha |\in \mathbf {On}\cup \{\boldsymbol \infty \}$ the rank of the ordinal notation $\alpha $ in the order $\prec $ .

The main proposition proved in this subsection is the following:

Proposition 5.6. For each $\Pi ^1_2(\Pi ^0_2)$ -sound theory $ {T}_0$ and ordinal notation $\alpha $ :

$$\begin{align*}|\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}({T}_0)|_{{T}_0}=|\alpha|.\end{align*}$$

In order to prove the proposition we first establish some lemmas. We state without proof the following two lemmas, the truth of which may easily be verified.

Before proving proposition 5.6, we prove the following lemma.

Lemma 5.9. If $|U|_{T_0}>|\alpha |$ then there is a true $\Sigma ^1_1(\Pi ^0_2)$ sentence $\varphi $ such that

(10) $$ \begin{align}U+\varphi\vdash \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}(\mathbf{R}^{\alpha}_{\Pi^1_1(\Sigma^0_2)}(T_0)).\end{align} $$

Proof. We prove the lemma by transfinite induction on $|\alpha |$ . Since $|U|_{T_0}>|\alpha |$ , there is a $V\in \mathcal {E}\mbox {-}T_0$ such that $U\vdash \mathsf {RFN}_{\Pi ^1_1(\Sigma ^0_2)}(V)$ and $|V|_{T_0}\ge |\alpha |$ . By the induction hypothesis there are true $\Sigma ^1_1(\Pi ^0_2)$ sentences $\varphi _{\beta }$ , for all $\beta \prec \alpha $ , such that

$$\begin{align*}V+\varphi_{\beta}\vdash \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}(\mathbf{R}^{\beta}_{\Pi^1_1(\Sigma^0_2)}(T_0)).\end{align*}$$

We now formalize the latter fact by a single $\Sigma ^1_1(\Pi ^0_2)$ sentence $\varphi $ , which states that there is a sequence of $\Pi ^0_2$ formulas $\langle \psi _{\beta }(Y)\mid \beta \prec \alpha \rangle $ without free variables other that Y and sequence of sets $\langle S_{\beta }\mid \beta \prec \alpha \rangle $ such that

• • for all $\beta $ , the formula $\psi _{\beta }(Y)$ holds on $Y=S_{\beta }$ ;

• • for all $\beta $ , we have $V +\exists Y\;\psi _{\beta }(Y)\vdash \mathsf {RFN}_{\Pi ^1_1(\Sigma ^0_2)}(\mathbf {R}^{\beta }_{\Pi ^1_1(\Sigma ^0_2)}(T_0))$ .

It is easy to see that indeed we could form a $\Sigma ^1_1(\Pi ^0_2)$ sentence $\varphi $ constituting the desired formalization.

Now let us show that $\varphi $ is true. Without loss of generality, we may assume that each $\varphi _{\beta }$ is of the form $\exists Y \theta _{\beta }(Y)$ , where all $\theta _{\beta }(Y)$ are $\Pi ^0_2$ -formulas. We put each $\psi _{\beta }$ to be $\theta _{\beta }$ and for each $\beta \prec \alpha $ we choose $S_{\beta }$ so that $\theta _{\beta }(Y)$ holds on $Y=S_{\beta }$ . Thus we see that $\varphi $ is true.

We establish (10) by reasoning in $U+\varphi $ and showing that the theory $\mathbf {R}^{\alpha }_{\Pi ^1_1(\Sigma ^0_2)}(T_0)$ is $\Pi ^1_1(\Sigma ^0_2)$ -sound. It is enough for us to establish the $\Pi ^1_1(\Sigma ^0_2)$ -soundness of each finite subtheory of $\mathbf {R}^{\alpha }_{\Pi ^1_1(\Sigma ^0_2)}(T_0)$ , i.e., each theory

$$\begin{align*}T_0+ \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}(\mathbf{R}^{\beta}_{\Pi^1_1(\Sigma^0_2)}(T_0)),\end{align*}$$

for $\beta \prec \alpha $ . We know (from U) that V is $\Pi ^1_1(\Sigma ^0_2)$ -sound. And also (from $\varphi $ ) we have a $\Pi ^0_2$ -formula $\psi _{\beta }(Y)$ such that

$$\begin{align*}V+\exists Y\; \psi_{\beta}(Y)\vdash \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}(\mathbf{R}^{\beta}_{\Pi^1_1(\Sigma^0_2)}(T_0))\end{align*}$$

and a set $S_{\beta }$ such that $\psi _{\beta }(S_{\beta })$ holds. From the $\Pi ^1_1(\Sigma ^0_2)$ -soundness of V we infer the $\Pi ^1_1(\Sigma ^0_2)$ -soundness of $V+\exists Y\; \psi _{\beta }(Y)$ . Therefore $T_0+ \mathsf {RFN}_{\Pi ^1_1(\Sigma ^0_2)}(\mathbf {R}^{\beta }_{\Pi ^1_1(\Sigma ^0_2)}(T_0))$ is $\Pi ^1_1(\Sigma ^0_2)$ -sound. ⊣

We are now in a position to prove Proposition 5.6.

Proof. First let us notice that $|\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }( {T}_0)|_{ {T}_0}\ge |\alpha |$ . Indeed this inequality holds since there is a homomorphism $\beta \mapsto \mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\beta }( {T}_0)$ of the low $\prec $ -cone of $\alpha $ (the order $(\{\beta \mid \beta \preceq \alpha \},\prec )$ ) to the low $\prec _{\Pi ^1_1(\Sigma ^0_2)}$ -cone of $\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }( {T}_0)$ in $\mathcal {E}\mbox {-} {T}_0$ .

Now assume for a contradiction that $|\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }( {T}_0)|_{ {T}_0}>|\alpha |$ . In this case by Lemma 5.9 we have

$$\begin{align*}\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}({T}_0)+\varphi\vdash \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}(\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}({T}_0)),\end{align*}$$

for some true $\Sigma ^1_1(\Pi ^0_2)$ sentence $\varphi $ . We derive

$$ \begin{align*} \mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}({T}_0)+\varphi&\vdash \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}(\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}({T}_0)+\varphi)\\ & \vdash \mathsf{Con}(\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}({T}_0)+\varphi). \end{align*} $$

So $\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }( {T}_0)+\varphi $ is inconsistent by Gödel’s Second Incompleteness Theorem. Yet by Lemma 5.7, since $T_0$ is $\Pi ^1_2(\Pi ^0_2)$ sound, $\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }( {T}_0)$ is $\Pi ^1_1(\Sigma ^0_2)$ sound. Thus, by Lemma 5.8, $\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }( {T}_0)+\varphi $ is consistent. This is a contradiction.  ⊣

5.2 Proof-theoretic ordinals

For a theory $T\sqsupseteq \mathsf {RCA}_0$ we write $|T|_{\mathsf {WO}}$ to denote the $\Pi ^1_1$ proof-theoretic ordinal of T, which we define as the supremum of the ranks $|\alpha |$ of ordinal notations $\alpha $ such that $T\vdash \mathsf {WO}(\alpha )$ . The formula $\mathsf {WO}(\alpha )$ is

$$\begin{align*}\forall X((\exists \beta\prec \alpha)\;\beta\in X\to (\exists \beta\prec\alpha)(\beta\in X\land (\forall \gamma\prec \beta)\gamma\not\in X)).\end{align*}$$

In order to prove the theorem we first establish the following lemma:

We will derive Lemma 5.12 from the more general Lemma 5.13.

We will follow Simpson’s formalization of countable coded models of the language of second-order arithmetic [Reference Simpson24, Definition VII.2.1]. Under this definition a countable coded $\omega $ -model $\mathfrak {M}$ is a code for a countable family $W_0,W_1,\ldots $ of subsets of $\mathbb {N}$ , where $\{W_0,W_1,\ldots \}$ is the $\mathfrak {M}$ -domain for sets of naturals. We note that the property $``\mathfrak{M}$ is a countable coded $\omega $ -model” is arithmetical. The expression $X\in \mathfrak {M}$ denotes the natural $\Sigma ^0_2$ formula that expresses the fact that the set X is coded in a model $\mathfrak {M}$ (i.e. it is one of $X=W_i$ , for some i). For each fixed second-order formula $\varphi (X_1,\ldots ,X_n,x_1,\ldots ,x_n)$ the expression $\mathfrak {M}\models \varphi (X_1,\ldots ,X_n,x_1,\ldots ,x_n)$ denotes the natural second-order formula that expresses that $\mathfrak {M}$ is a countable coded $\omega $ -model, sets $X_1,\ldots ,X_n$ are coded in $\mathfrak {M}$ , and $\varphi (X_1,\ldots ,X_n,x_1,\ldots ,x_n)$ is true in $\mathfrak {M}$ . We express the fact that that $\varphi (X_1,\ldots ,X_n,x_1,\ldots ,x_n)$ is true in $\mathfrak {M}$ by relativizing second-order quatifiers $\forall X$ and $\exists X$ to $\forall X\in \mathfrak {M}$ and $\exists X\in \mathfrak {M}$ . Note that the latter quantifiers are in fact just first-order quantifiers. Hence $\mathfrak {M}\models \varphi (\vec {X},\vec {x})$ is equivalent to a $\Pi ^0_m$ -formula, where m depends only on the depth of quantifier alternations in $\varphi $ . For a fixed theory T given by a finite list of axioms, by $\mathfrak {M}\models T$ we mean the formula $\mathfrak {M}\models \varphi $ , where $\varphi $ is the conjunction of all the axioms of T.

For each theory $T_0\sqsupseteq \mathsf {RCA}_0$ given by a finite list of axioms we denote by $T_0^{+}$ the theory We use this notation by analogy with $\mathsf {ACA}_0^+$ . We note that for $T_0=\mathsf {ACA}_0$ the theory $T_0^{+}$ is just $\mathsf {ACA}_0^+$ and for $T_0=\mathsf {RCA}_0$ the theory $T_0^{+}$ is just $\mathsf {ACA}_0$ .

Lemma 5.13. For each $T_0\sqsupseteq \mathsf {RCA}_0$ given by a finite list of axioms

$$\begin{align*}T_0^+\vdash\forall \alpha \; \Big( \mathsf{WO}(\alpha)\to \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}\big(\mathbf{R}^{\alpha}_{\Pi^1_1(\Sigma^0_2)}(T_0)\big)\Big).\end{align*}$$

Lemma 5.14.

$$\begin{align*}\mathsf{RCA}_0\vdash \forall \alpha\;\Big(\mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}\big(\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}(\mathsf{RCA}_0)\big)\to \mathsf{WO}(\alpha)\Big).\end{align*}$$

Proof. We prove the lemma by reflexive induction on $\alpha $ in $\mathsf {RCA}_0$ . We reason in $\mathsf {RCA}_0$ and assume the reflexive induction hypothesis

$$\begin{align*}\forall \beta\prec \alpha\; \mathsf{Pr}_{\mathsf{RCA}_0}\Big(\mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}\big(\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\beta}(\mathsf{RCA}_0)\big)\to \mathsf{WO}(\beta)\Big).\end{align*}$$

We need to show that:

(11) $$ \begin{align} \mathsf{RFN}_{\Pi^1_1(\Sigma^0_2)}\big(\mathbf{R}_{\Pi^1_1(\Sigma^0_2)}^{\alpha}(\mathsf{RCA}_0)\big)\to \mathsf{WO}(\alpha). \end{align} $$

So assume the antecedent of (11). From the reflexive induction hypothesis we see that for each individual $\beta \prec \alpha $ the theory $\mathbf {R}_{\Pi ^1_1(\Sigma ^0_2)}^{\alpha }(\mathsf {RCA}_0)$ proves $\mathsf {WO}(\beta )$ . Since $\mathsf {WO}(\beta )$ is a $\Pi ^1_1(\Sigma ^0_2)$ -formula, we infer from the antecedent of (11) that $\forall \beta \prec \alpha \; \mathsf {WO}(\beta )$ . Thus $\mathsf {WO}(\alpha )$ . ⊣

Now we are ready to prove Theorem 5.11.

Proof. From Theorem 4.17 we know that

$$\begin{align*}\mathbf{R}^{\alpha}_{\Pi^1_1}(\mathsf{ACA}_0)\equiv_{\Pi^1_1(\Sigma^0_2)} \mathbf{R}^{\varepsilon_{\alpha}}_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0).\end{align*}$$

From Lemma 5.14 we see that $\mathbf {R}^{\varepsilon _{\alpha }}_{\Pi ^1_1(\Sigma ^0_2)}(\mathsf {RCA}_0)$ proves $\mathsf {WO}(\beta )$ for each $\beta \prec \varepsilon _\alpha $ and thus $|\mathbf {R}^{\alpha }_{\Pi ^1_1}(\mathsf {ACA}_0)|_{\mathsf {WO}}\ge |\varepsilon _{\alpha }|$ .

In order to prove $|\mathbf {R}^{\alpha }_{\Pi ^1_1}(\mathsf {ACA}_0)|\le |\varepsilon _{\alpha }|$ let us assume that for some $\beta $ the theory $\mathbf {R}^{\alpha }_{\Pi ^1_1}(\mathsf {ACA}_0)$ proves $\mathsf {WO}(\beta )$ and then show that $|\beta |< |\varepsilon _{\alpha }|$ . Indeed, by Lemma 5.12 the theory $\mathbf {R}^{\alpha }_{\Pi ^1_1}(\mathsf {ACA}_0)$ proves $\mathsf {RFN}_{\Pi ^1_1(\Sigma ^0_2)}(\mathbf {R}^{\beta }_{\Pi ^1_1(\Sigma ^0_2)}(\mathsf {RCA}_0))$ . Hence

$$\begin{align*}|\beta|<|\mathbf{R}^{\alpha}_{\Pi^1_1}(\mathsf{ACA}_0)|_{\mathsf{RCA}_0}=|\mathbf{R}^{\varepsilon_{\alpha}}_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0)|_{\mathsf{RCA}_0}.\end{align*}$$

And Proposition 5.6 gives us

$$\begin{align*}|\varepsilon_{\alpha}|=|\mathbf{R}^{\varepsilon_{\alpha}}_{\Pi^1_1(\Sigma^0_2)}(\mathsf{RCA}_0)|_{\mathsf{RCA}_0}>|\beta|.\end{align*}$$

This completes the proof.  ⊣

5.3 Extensions of $\mathsf {ACA}_0^+$

It is usually attributed to Kreisel that for extensions $T\sqsupseteq \mathsf {ACA}_0$ the $\Pi ^1_1$ proof-theoretic ordinal $|T|_{\mathsf {WO}}=|T+\varphi |_{\mathsf {WO}}$ , for any true $\Sigma ^1_1$ -sentence $\varphi $ (see [Reference Pohlers20, Theorems 6.7.4 and 6.7.5]). We note that our notion of reflection rank $|T|_{\mathsf {ACA}_0}$ does not enjoy the same property.

Remark 5.15. Let us consider an ordinal notation system $\alpha $ for some large recursive ordinal, for example the Bachmann-Howard ordinal. Now we modify $\alpha $ to define pathological ordinal notation $\alpha '$ . The order $\prec _{\alpha '}$ is the restriction of $\prec _{\alpha }$ to numbers m such that $\forall x\le m\;\lnot \mathsf {Prf}_{\mathsf {ACA}_0}(x,0=1)$ . And $\alpha '$ corresponds to the same element of the domain of $\prec _{\alpha }$ as $\alpha $ (note that since $\mathsf {ACA}_0$ is consistent this element is in the domain of $\prec _{\alpha '}$ as well). We see externally that $\alpha '$ is isomorphic to $\alpha $ , since $\mathsf {ACA}_0$ is consistent. Let us denote by $\mathsf {Iso}$ the true $\Sigma ^1_1$ -sentence that expresses the fact that $\alpha $ and $\alpha '$ are isomorphic. Clearly,

$$\begin{align*}\mathsf{ACA}_0+\mathsf{WO}(\alpha')+\mathsf{Iso}\sqsupseteq \mathsf{ACA}_0+\mathsf{WO}(\alpha),\end{align*}$$

$$\begin{align*}|\mathsf{ACA}_0+\mathsf{WO}(\alpha')+\mathsf{Iso}|_{\mathsf{ACA}_0}\ge|\mathsf{ACA}_0+\mathsf{WO}(\alpha)|_{\mathsf{ACA}_0}\end{align*}$$

and under our choice of $\alpha $ the rank $|\mathsf {ACA}_0+\mathsf {WO}(\alpha )|_{\mathsf {ACA}_0}$ will be equal to the Bachmann-Howard ordinal. At the same time, the theory $\mathsf {ACA}_0+\lnot \mathsf {Con}(\mathsf {ACA}_0)$ proves that $\alpha '$ is isomorphic to some finite order and hence

$$\begin{align*}\mathsf{ACA}_0+\lnot\mathsf{Con}(\mathsf{ACA}_0)\vdash \mathsf{WO}(\alpha').\end{align*}$$

Hence

$$\begin{align*}|\mathsf{ACA}_0+\mathsf{WO}(\alpha')|_{\mathsf{ACA}_0}\le |\mathsf{ACA}_0+\lnot \mathsf{Con}(\mathsf{ACA}_0)|_{\mathsf{ACA}_0}=0,\end{align*}$$

the latter equality follows from Remark 5.5. And thus

$$\begin{align*}|\mathsf{ACA}_0+\mathsf{WO}(\alpha')|_{\mathsf{WO}}<|\mathsf{ACA}_0+\mathsf{WO}(\alpha')+\mathsf{Iso}|_{\mathsf{WO}}.\end{align*}$$

Accordingly, $\mathsf {Iso}$ is a true $\Sigma ^1_1$ sentence that alters the reflection rank of the theory $\mathsf {ACA}_0+\mathsf {WO}(\alpha ')$ .

We address this problem with two different results. First in Theorem 5.16 we show that for any extension $T\sqsupseteq \mathsf {ACA}_0^+$ , $|T|_{\mathsf {ACA}_0}=|T|_{\mathsf {WO}}$ . Second we introduce the notion of robust reflection rank $|\cdot |_{\mathsf {ACA}_0}^{\star }$ that enjoys a number of nice properties and at the same time coincides with reflection rank $|\cdot |_{\mathsf {ACA}_0}$ , for many natural theories T (in particular, for any T such that $T\equiv _{\Pi ^1_1}\mathbf {R}_{\Pi ^1_1}^{\alpha }(\mathsf {ACA}_0)$ , for some ordinal notation $\alpha $ ).

Theorem 5.16. Suppose $T\sqsupseteq \mathsf {ACA}_0^{+}$ then

$$\begin{align*}|T|_{\mathsf{WO}}=|T|_{\mathsf{ACA}_0}.\end{align*}$$

We prove the following general theorem.

Theorem 5.17. Suppose that a $\Pi ^1_2(\Pi ^0_2)$ -sound theory $T_0\sqsupseteq \mathsf {RCA}_0$ is given by a finite list of axioms. Then for each $U\sqsupseteq T_0^+$ we have

$$\begin{align*}|U|_{\mathsf{WO}}=|U|_{T_0}.\end{align*}$$