A Note on the Ordinal Analysis of $\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })$

Abstract

We fill an apparent gap in the literature by giving a short and self-contained proof that the ordinal of the theory $\mathbf {RCA}_0 + \mathrm {WO}(\sigma )$ is $\sigma ^\omega$, for any ordinal $\sigma$ satisfying $\omega \cdot \sigma = \sigma$ (e.g., $\omega ^\omega$, $\omega ^{\omega ^\omega }$, $\varepsilon _0$). Theories of the form $\mathbf {RCA}_0 + \mathrm {WO}(\sigma )$ are of interest in Proof Theory and Reverse Mathematics because of their connections to a number of well-investigated combinatorial principles related to various subsystems of arithmetic.

1 Introduction

Well-ordering statements are commonly used in Proof Theory and Reverse Mathematics as measures of strength of a theorem or a theory. For example a number of interesting theorems is known to be equivalent to $\mathrm {WO}(\omega ^\omega )$ or $\mathrm {WO}(\omega ^{\omega ^\omega })$ over the theory $\mathbf {RCA}_0$ (see, e.g., [3, 7, 9, 15]). It is then natural to ask what is the proof-theoretic ordinal of the theories $\mathbf {RCA}_0+\mathrm {WO}(\omega ^\omega )$, $\mathbf {RCA}_0+\mathrm {WO}(\omega ^{\omega ^\omega })$ and, in general, $\mathbf {RCA}_0+\mathrm {WO}(\alpha )$. While it is well-known that the ordinal of $\mathbf {RCA}_0$ is $\omega ^\omega$, the answer for the other theories is not so immediate and occasionally some confusion arises.¹ Even the standard argument for showing that $\omega ^\omega$ is an upper bound on the proof-theoretic ordinal of $\mathbf {RCA}_0$ is somewhat indirect in that it hinges on the characterization of the provably recursive functions of $\mathbf {RCA}_0$ rather than only on the computation of its proof-theoretical ordinal. A proper direct treatment approach to determining the proof-theoretic ordinal of theories of the form $\mathbf {RCA}_0 + \mathrm {WO}(\alpha )$ seems to be missing from the literature. The closest match is Sommer’s [17] model-theoretical treatment of first-order theories with transfinite induction restricted to various formula-classes and ordinals strictly below $\varepsilon _0$.

In this paper we show that, if $\sigma$ is an ordinal satisfying $\omega \cdot \mathbf {\sigma }=\mathbf {\sigma }$, the proof-theoretic ordinal of the theory $\mathbf {RCA}_0 + \mathrm {WO}(\sigma )$ is $\sigma ^\omega$. Examples of relevant $\sigma$s are $\omega ^\omega$, $\omega ^{\omega ^\omega }$ etc. and $\varepsilon _0$. This should be contrasted with the fact that the ordinal of $\mathbf {ACA}_0 + \mathrm {WO}(\varepsilon _0)$ is the much larger $\varepsilon _1$, as can be gleaned from the proof-theoretical analysis of transfinite induction over Peano Arithmetic (the original proof seems to be in [8]).

Essentially, we show that the first-order part of $\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })$ is the theory $\mathbf {I}\varSigma _1$ plus the scheme of transfinite induction up to $\mathbf {\sigma }$ restricted to $\varPi _1$ formulas, which we denote by $\mathrm {TI}(\mathbf {\sigma }, \varPi _1)$. We give an ordinal analysis of the latter theory augmented by a generic unary predicate symbol ${\mathsf U}$ and then show that the theories prove the same $\varPi ^1_1$-statements, where a $\varPi ^1_1$-sentence $\forall XF(X)$ with F(X) being arithmetic is identified with $F({\mathsf U})$ in the first-order context of $\mathrm {TI}(\mathbf {\sigma }, \varPi _1)$.

For the remainder of the paper, we fix an ordinal $\mathbf {\sigma }$ such that $\omega \cdot \mathbf {\sigma }=\mathbf {\sigma }$. The ordinal $\mathbf {\sigma }$ is assumed to be represented in a natural ordinal representation system. We denote by $\lhd$ the primitive recursive ordering on the ordinals smaller that $\mathbf {\sigma }$ to distinguish it from the usual ordering on the naturals.

2 Ordinal Analysis of $\mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$

The language of $\mathbf {T}_\mathbf {\sigma }:= \mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$ is the language of Primitive Recursive Arithmetic, $\mathbf {PRA}$, augmented by a unary predicate symbol ${\mathsf U}$. Especially we assume that there is a binary surjective coding function $\langle \, \cdot \, , \,\cdot \, \rangle$ with inverses $(\,\cdot \,)_0$, $(\,\cdot \,)_1$. The order relation for the ordering on $\mathbf {\sigma }$ will be denoted by the same symbol $\lhd$ used to denote the corresponding primitive recursive relation. Bounded quantifiers $\forall x\le t$ and $\exists x\le t$ will be treated as quantifiers in their own right. Formulas containing only bounded quantifiers are called $\varDelta _0$-formulas. For our proof-theoretic purposes, $\mathbf {T}_\mathbf {\sigma }$ will be formalized in a one-sided sequent calculus, using negation normal forms following [14] (this is also known as the Tait-calculus [18]). $\mathbf {T}_\mathbf {\sigma }$ has the usual axioms pertaining to primitive recursive functions and predicates. A noteworthy feature is that transfinite induction on $\mathbf {\sigma }$ for $\varPi _1$-formulas is expressed via the rule

$$\begin{aligned} \frac{\varTheta , \ \exists z \, ((z)_0 \lhd a \, \wedge \, \lnot F((z)_1, (z)_0)), \ \forall x F(x,a)}{\varTheta , \ F(t,s)} \end{aligned}$$

(1)

where a is an eigenvariable, F(x, a) is $\varDelta _0$, t, s are arbitrary terms, and $\varTheta$ is an arbitrary finite set of formulas.

Observe that we do not need $\varSigma _1$-induction as an extra induction principle as it follows from $\mathrm {TI}(\mathbf {\sigma },\varPi _1)$, since $\mathbf {I}\varPi _1$ entails $\mathbf {I}\varSigma _1$.

In order to perform partial cut eliminations, we define the degree, |A|, of a formula A as follows:

• $|A| = |\lnot A| = 0$ if A is $\varDelta _0$.

If A is not $\varDelta _0$ and of one of the forms below, then:

• $|A_0 \wedge A_1| = |A_0 \vee A_1| = \max (|A_0|,|A_1|) + 1$;

• $|\forall x F(x)| = |\exists x F(x)| = |F(0)| + 1$;

• $|\forall x\le t\, F(x)| = |\exists x\le t\, F(x)|= |F(0)| + 2$.

As the rule (1) introduces a $\varDelta _0$-formula and the main formulas of axioms are $\varDelta _0$ as well, we can easily eliminate cuts of degree greater than 0. We use the notation to convey that $\varGamma$ is deducible in $\mathbf {T}_\mathbf {\sigma }$ by a deduction of length at most m such that all cuts occurring in this deduction are with cut formulas of a degree $<k$. Thus means that there is deduction in which all cut formulas (if any) are $\varDelta _0$-formulas.

Theorem 1

.

Proof

By the usual cut elimination method of Gentzen’s Hauptsatz.

2.1 Embedding $\mathbf {T}_\mathbf {\sigma }$ in an Infinitary System

Next we embed $\mathbf {T}_\mathbf {\sigma }$ into an infinitary system, called $\mathbf {PA}_{\omega }$, with $\omega$-rule (basically the same as the system $Z_{\infty }$ in [14]; a definition of $\mathbf {PA}_{\omega }$ in a two-sided Gentzen calculus can be found in [10]). The formulas of $\mathbf {PA}_{\omega }$ are the closed formulas of $\mathbf {T}_\mathbf {\sigma }$, i.e. formulas without free variables. We shall assign a rank, $|A|_{\varDelta _0}$ to a formula A of $\mathbf {PA}_{\omega }$ as follows:

• (i) $|A|_{\varDelta _0}=0$ if A is atomic or a negated atom.

• (ii) $|A_0\wedge A_1|_{\varDelta _0}=|A_0\vee A_1|_{\varDelta _0}=\max (|A_0|_{\varDelta _0},|A_1|_{\varDelta _0})+1$.

• (iii) $|\exists x\le t\,F(x)|_{\varDelta _0}=|\forall x\le t\,F(x)|_{\varDelta _0}=|F(0)|_{\varDelta _0}+1$.

• (iv) $|\exists x\,F(x)|_{\varDelta _0}=|\forall x\,F(x)|_{\varDelta _0}=\max (\omega ,|F(0)|_{\varDelta _0}+1)$.

Note that $|A|_{\varDelta _0}<\omega$ exactly when A is $\varDelta _0$, and $|\exists x\,F(x)|_{\varDelta _0}=|\forall x\,F(x)|_{\varDelta _0}=\omega$ when F(0) is $\varDelta _0$.

Definition 1

For a natural number n we use $\bar{n}$ to denote the nth numeral, that is the term obtained from the term $\bar{0}$ for zero by adding the successor function symbol n-times in front of it. The terms of $\mathbf {PA}_{\omega }$ are closed and thus can be evaluated to a number. For a term t let $t^{\mathbb N}$ be the number n such that t evaluates to n (in the following we occasionally refer to $t^\mathbb {N}$ by t).

The axioms of $\mathbf {PA}_{\omega }$ are sequents of two kinds. Let $\varGamma$ be a finite set of formulas of $\mathbf {PA}_{\omega }$.

• (i) Let $R(t_1,\ldots ,t_r)$ be an atomic formula, where R is a relation symbol for a primitive recursive relation $R^{\mathbb N}$. If $R^{\mathbb N}(t_1^{\mathbb N},\ldots ,t_r^{\mathbb N})$ is true, then

  $$\varGamma , R(t_1,\ldots ,t_r)$$

  is an axiom. If $R^{\mathbb N}(t_1^{\mathbb N},\ldots ,t_r^{\mathbb N})$ is false, then

  $$\varGamma , \lnot R(t_1,\ldots ,t_r)$$

  is an axiom.

• (ii) If $s^{\mathbb N}=t^{\mathbb N}$ holds for terms s and t, then

  $$\varGamma , {\mathsf U}(s),\lnot {\mathsf U}(t)$$

  is an axiom.

The $\omega$-rule is the following rule: If $\varGamma ,F(\bar{n})$ is deducible for all n, then $\varGamma ,\forall x\,F(x)$ is the conclusion.

Similarly to derivations in $\mathbf {T}_\mathbf {\sigma }$, we will use the notation to convey that $\varGamma$ is deducible in $\mathbf {PA}_{\omega }$ by a deduction of height at most $\alpha$ such that all cuts occurring in this deduction are with cut formulas of $|\cdot |_{\varDelta _0}$-rank $<\beta$.

Lemma 1

(Reduction Lemma). If $|B|_{\varDelta _0}=\omega$, and , then

where $\alpha \#\beta$ denotes the natural or Hessenberg sum of $\alpha$ and $\beta$.

Proof

Standard.

Theorem 2

(Embedding Theorem). If , then , where $\varGamma ^*$ is the result of assigning closed terms to all free variables in $\varGamma$ (the same term to the same variable).

Proof

We proceed by induction on m. We only need to pay attention to the case where the last inference is an instance of the rule (1). So let $\varGamma = \varTheta , F(t,s)$ and assume with $m_0<m$ and $\varLambda = \varTheta , \exists z \; ((z)_0 \lhd a \wedge \lnot F((z)_1, (z)_0)), \forall x \; F(x,a)$.

Let * be an assignment. Inductively we have for all closed terms q that

(2)

We use transfinite induction on $\alpha$ for $\alpha$ in the field of $\lhd$ to show that:

(3)

By the induction hypothesis, we have:

for every $\eta \lhd \alpha$ and arbitrary closed term $s'$, yielding

via an inference $(\vee )$. If r is a closed term such that $r^{\mathbb N}$ is different from all $\eta$ preceding $\alpha$, then $\lnot r\lhd \bar{\alpha }$ is an axiom, and thus, via an inference $(\vee )$, we arrive at . Thus from the above we conclude that

holds for all k, so that, via an application of the $\omega$-rule, we get:

(4)

Applying the Reduction Lemma 1 to (2) and (4) yields:

(5)

From (5) we finally get:

confirming (3).

If a term q has the property that $q^{\mathbb N}$ is not in the field of $\lhd$ then one can directly infer from (2) that

(6)

The reason for this is that if the formula $\exists z \, ((z)_0 \lhd q \wedge \lnot F^*((z)_1, (z)_0))$ figures as the main formula of an inference in this derivation its minor formula is of the form $(p)_0\lhd q \wedge \lnot F^*((p)_1,(p)_0)$. The latter formula conjunctively contains a false atomic formula. Such a formula can always be erased from the derivation. Formally, of course, this has to be proved by a separate induction on the ordinal of the derivation.

(3) and (6) now yield

for all closed terms t and s, since $\omega \cdot (\alpha + 1)\lhd \mathbf {\sigma }$ on account of $\omega \cdot \mathbf {\sigma }=\mathbf {\sigma }$.

2.2 Eliminating Cuts with $\varDelta _0$-Formulas

The next step is to eliminate cuts with $\varDelta _0$-formulas that are not atomic.

Lemma 2

Let $0<n<\omega$ and suppose . Then .

Proof

We proceed by induction on $\alpha$. The crucial case is when the last inference was a cut of rank n with cut formulas $A,\lnot A$. Note that A is not an atomic formula. We then have and for some $\alpha _0<\alpha$. The induction hypotheses furnishes us with

(7)

Let A be of the form $\exists x\le t\,F(x)$. Then $\lnot A$ is the formula $\forall x\le t\,\lnot F(x)$. From (7) we obtain

(8)

for all $k\le p$, where p is the numerical value of t. As the formulas $F(\bar{k}),\lnot F(\bar{k})$ have rank $<n$, we can employ ($p+1$)-many cuts to (8) to arrive at . Thus we have as $\omega \cdot \alpha _0 +p+1<\omega \cdot \alpha$. A similar argument works when A is of either form $A_0\wedge A_1$ or $A_0\vee A_1$.

Corollary 1

If then .

Proof

We use induction on $\alpha$. The only interesting case arises when the last inference is a cut with a formula A of rank $k>0$. Then we have and for some $\alpha _0<\alpha$. The induction hypothesis yields and . Hence . Applying Lemma 2 k times we arrive at . As $\omega ^k\cdot (\omega ^{\omega }\cdot \alpha _0+1)=\omega ^{\omega }\cdot \alpha _0 +\omega ^k\le \omega ^{\omega }\cdot \alpha$ we also have as desired.

Note that $\mathbf {\sigma }\ge \omega ^{\omega }$ since $\omega \cdot \mathbf {\sigma }=\mathbf {\sigma }$.

Corollary 2

Let $m>0$. If then .

Proof

Corollary 1 yields . Thus the desired conclusion follows as $\omega ^{\omega }\cdot \mathbf {\sigma }^m\le \mathbf {\sigma }\cdot \mathbf {\sigma }^m=\mathbf {\sigma }^{m+1}$.

3 Upper Bounds for the Provable Well-Orderings of $\mathbf {T}_\mathbf {\sigma }$

The results of the previous section can be utilized to determine the ordinal rank of provable well-orderings of $\mathbf {T}_\mathbf {\sigma }$. Let $\prec$ be a primitive recursive ordering. $\prec$ is said to be a provable well-ordering of $\mathbf {T}_\mathbf {\sigma }$ if $\mathbf {T}_\mathbf {\sigma }$ proves that $\prec$ is a total linear ordering and

$$\mathbf {T}_\mathbf {\sigma }\vdash \mathrm {WO}(\prec )$$

where $\mathrm {WO}(\prec )$ stands for the formula

$$\forall v[\forall u\prec v {{\mathsf U}}(u)\,\rightarrow \,{{\mathsf U}}(v)]\,\rightarrow \,\forall v{{\mathsf U}}(v).$$

Assuming $\mathbf {T}_\mathbf {\sigma }\vdash \mathrm {WO}(\prec )$, as a consequence of Theorems 1, 2 and Corollary 2 we then have

(9)

for some $m>0$. There are several ways of obtaining an upper bound for the order-type of $\prec$ in terms of the length of a cut-free deduction of $\mathrm {WO}(\prec )$ (see e.g. [13, Theorem 23.1], [19, Theorem 3.6], [6, Theorem 2.27]) which ultimately go back to Gentzen. Schütte [13, Theorem 23.1] obtains particularly sharp bounds. He shows that the length $\alpha$ of a cut-free derivation of transfinite induction along an ordering $\prec$ provides an upper bound for the ordinal rank of $\prec$ if $\omega \cdot \alpha =\alpha$. For our purpose, however, we need to extract bounds from deductions that still have cuts with formulas ${\mathsf U}(s),\lnot {\mathsf U}(s)$.² We could first eliminate these remaining cuts, however, we would get bounds of the form $2^{\mathbf {\sigma }^{m}}$, and these are too high for our purpose of showing that $\mathbf {\sigma }^{\omega }$ is the proof-theoretic ordinal of $\mathbf {T}_\mathbf {\sigma }$. To overcome this obstacle we shall draw on a technique that the third author has used for many years. To this end we extend $\mathbf {PA}_{\omega }$ by yet another infinitary rule $\mathrm {Prog}_{\prec }$ due to Schütte [11, p. 384] called Progressionsregel ($\mathrm {Prog}_{\prec }$ was also used in [12, p. 214] and in [14]):

$$\begin{aligned} \frac{\displaystyle \varGamma , {\mathsf U}(\bar{m})\;\;\text{ for } \text{ all } m\prec n}{\displaystyle \varGamma , {\mathsf U}(s)}\end{aligned}$$

(10)

whenever s is a closed term with value n.

Let $\mathrm {PROG}_{\prec }$ be an abbreviation for $\forall v[\forall u\prec v {{\mathsf U}}(u)\,\rightarrow \,{{\mathsf U}}(v)]$. The rule $\mathrm {Prog}_{\prec }$ has the effect of making $\mathrm {PROG}_{\prec }$ provable. We shall refer by $\mathbf {PA}_{\infty }^*$ to the extension of $\mathbf {PA}_{\omega }$ by the rule $\mathrm {Prog}_{\prec }$.

Lemma 3

(11)

Proof

We proceed by induction on $\alpha$. If $\lnot \mathrm {PROG}_{\prec }$ was not the main formula of the last inference then the desired result follows immediately by applying the inductive assumption to its premisses and subsequently reapplying the same inference. Thus suppose that $\lnot \mathrm {PROG}_{\prec }$ was the main formula of the last inference. Then

(12)

for some $\alpha _0\lhd \alpha$. The induction hypothesis yields

(13)

for some s. Using inversion for $(\wedge )$, $(\forall )$ and $(\vee )$ we arrive at

(14)

for all n, and

(15)

Since holds for all n with $n\prec s^\mathbb {N}$, we can apply cuts and the rule $\mathrm {Prog}_{\prec }$ to (14) to arrive at

(16)

Applying Cut to (16) and (15) yields

(17)

and hence

(18)

Corollary 3

for all n.

Proof

Follows from (9) and Lemma 3. Note that $m>0$.

For a closed numerical term s we denote by $|s|_{\prec }$ the ordinal $\{|\bar{n}|_{\prec }\mid \bar{n}\prec s\,{\text {is}}\,{\text {true}}\}$.

Proposition 1

Assume that the sequent $\lnot {\mathsf U}(t_1),\ldots ,\lnot {\mathsf U}(t_r),{\mathsf U}(s_1),\ldots ,{\mathsf U}(s_q)$ is not an axiom and $s_1\preceq \ldots \preceq s_q$ holds. Then

implies

$$\begin{aligned} |s_1|_{\prec }< & {} \omega \cdot \alpha .\end{aligned}$$

(19)

Proof

Let $\lnot {\mathsf U}(\varvec{t}\,)$ be an abbreviation for $\lnot {\mathsf U}(t_1),\ldots ,\lnot {\mathsf U}(t_r)$. In the above we allow $r=0$ in which case $\lnot {\mathsf U}(\varvec{t}\,)$ is the empty sequent.

We proceed by induction on $\alpha$. As the sequent is not an axiom it must have been inferred. The only two possibilities are applications of $\mathrm {Prog}_{\prec }$ or cuts with atomic formulas.

Case 1: The last inference was $\mathrm {Prog}_{\prec }$. Then there is a term $s_j$ and $\alpha _0\lhd \alpha$ such that for all $\bar{n}\prec s_j$. As $s_1\preceq s_j$ this also holds for all $\bar{n}\prec s_1$. The induction hypothesis yields that

$$|\bar{n}|_{\prec }< \omega \cdot \alpha _0$$

holds for those $\bar{n}\prec s_1$ for which the sequent is not an axiom. Since by Definition 1 (ii)

$$\begin{aligned} \lnot {\mathsf U}(\varvec{t}\,),{\mathsf U}(s_1),\ldots ,{\mathsf U}(s_q),{\mathsf U}(\bar{n}) \end{aligned}$$

(20)

is an axiom only if $\bar{n}$ has the same value as some $t_1,\ldots ,t_r$, then there are only finitely many n for which (20) is an axiom. Thus $|s_1|_{\prec }<\omega \cdot \alpha _0+\omega$, whence $|s_1|_{\prec }<\omega \cdot \alpha$.

Case 2: The last inference was a cut with cut formulas ${\mathsf U}(p),\lnot {\mathsf U}(p)$, i.e., we have

(21)

(22)

for some $\alpha _0<\alpha$ and closed term p. If the sequent from (22) is not an axiom, the induction hypothesis applied to that derivation yields $|s_1|_{\prec }<\omega \cdot \alpha _0$. If it is an axiom, there is an $s_j$ such that p and $s_j$ evaluate to the same numeral, and hence $s_1\preceq p$. So in this case the induction hypothesis applied to (21) yields $|s_1|_{\prec }<\omega \cdot \alpha _0$.

Case 3: The last inference was a cut with cut formulas $R(u_1,\dots ,u_p),\lnot R(u_1,\dots ,u_p)$ for a symbol R for a primitive recursive relation. Then we have

(23)

(24)

for some $\alpha _0<\alpha$. If $R(u_1,\dots ,u_p)$ is true it follows from (24) that we also have

and hence the induction hypothesis yields $|s_1|_{\prec }<\omega \cdot \alpha _0$.

Likewise, if $R(u_1,\dots ,u_p)$ is false it follows from (23) that we also have

and hence the induction hypothesis yields $|s_1|_{\prec }<\omega \cdot \alpha _0$.

Corollary 4

 

• (i)
  
• (ii)
  

  where $|\prec |$ stands for the ordinal rank of $\prec$.

Proof

(i) is an immediate consequence of Proposition 1.

(ii) follows from (i) and Lemma 3.

In sum, it follows that the ordinal rank of $\prec$ is not bigger than $\mathbf {\sigma }^{m}$, and hence $\mathbf {\sigma }^{\omega }$ is an upper bound for the proof-theoretic ordinal of $\mathbf {T}_\mathbf {\sigma }$.

Proposition 1 can also be shown via techniques in A. Beckmann’s dissertation, notably his [1, 5.2.5 Boundedness Theorem] that also features in [2].

Turning to lower bounds, one can easily show, using external induction on n, that $\mathbf {T}_\mathbf {\sigma }\vdash \mathrm {WO}(\mathbf {\sigma }^n)$. This is a folklore result; details can be found in [17, Lemma 4.3]. As a consequence of the results gathered so far we have

Theorem 3

The proof-theoretic ordinal of $\mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$ is $\mathbf {\sigma }^{\omega }$.

It remains to transfer this result to our target theory $\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })$.

4 $\varPi ^1_1$-Conservativity

We here prove that $\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })$ is $\varPi ^1_1$-conservative over $\mathbf {T}_\mathbf {\sigma }$. More precisely, a $\varPi ^1_1$-sentence $\forall X F(X)$ (with F(X) being arithmetic) is identified with $F({\mathsf U})$ in the first-order context of $\mathrm {TI}(\mathbf {\sigma }, \varPi _1)$. This is enough to apply our results from the previous section to conclude that the ordinal of $\mathbf {RCA}_0 + \mathrm {WO}(\sigma )$ is $\sigma ^\omega$.

To prove the conservativity result, we proceed as follows. We start by showing that any model of $\mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$ can be extended to a model of $\mathrm {\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })}$. The argument is essentially contained in Simpson [16], IX.1. By writing that $\mathbf {M}_1$ is an $\omega$-submodel of $\mathbf {M}_2$ we mean that $\mathbf {M}_1=(M_1,\mathcal {S}_1)$ and $\mathbf {M}_2=(M_1, \mathcal {S}_2)$ where $\mathcal {S}_1\subseteq \mathcal {S}_2$. In other words, the two models share the same first-order part $M_1$.

Lemma 4

Let $\mathbf {M}$ be an $L_2$-structure which satisfies the axioms of $\mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$. Then $\mathbf {M}$ is an $\omega$-submodel of some model of $\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })$.

Proof

We first show that $\mathbf {M}$ can be extended to a model $\mathbf {M}'$ satisfying $\mathbf {RCA}_0$ and $\mathrm {TI}(\mathbf {\sigma },\varDelta ^0_0)$ with the same first-order domain as $\mathbf {M}$. Then we show that such an extension also satisfies $\mathrm {WO}(\mathbf {\sigma })$.

The $\omega$-extension $\mathbf {M}'$ is defined exactly as in Simpson [16] Lemma IX.1.8, i.e., the second-order part is given by the $\varDelta ^0_1$-definable sets of the base model $\mathbf {M}$. By Lemma IX.1.8 of [16] we have that $\mathbf {M}'$ satisfies $\mathbf {RCA}_0$.

Then, in order to check that $\mathrm {TI}(\mathbf {\sigma },\varDelta ^0_0)$ is also satisfied, we use the first claim in Simpson’s Lemma IX.1.8. Let $\varphi$ be a $\varSigma ^0_0$ formula with no free set variables and parameters in $M'$. Then, there exists a $\varPi ^0_1$-formula $\varphi _{\varPi }$ with the same free variables and parameters only in M such that $\varphi$ and $\varphi _{\varPi }$ are equivalent over $M'$. Thus, $\mathrm {TI}(\mathbf {\sigma },\varPi ^0_1)$ in $\mathbf {M}$ implies $\mathrm {TI}(\mathbf {\sigma },\varDelta ^0_0)$ in $\mathbf {M}'$.

Finally, we show that $M'$ also satisfies $\mathrm {WO}(\mathbf {\sigma })$. If this were not the case, letting S be a set witnessing $\lnot \mathrm {WO}(\mathbf {\sigma })$, we would have that $\bar{S}$, i.e. the complement of S, witnesses the failure of an instance of $\mathrm {TI}(\mathbf {\sigma },\varDelta ^0_0)$. More precisely: suppose that S is non-empty and has no $\lhd$-minimal element. Then $\exists x (x \in S)$. On the other hand, $\bar{S}$ is in $M'$ (since any model of $\mathbf {RCA}_0$ is closed under Turing reducibility hence under complement) and $\forall x (\forall y (y \lhd x \rightarrow y \in \bar{S})\rightarrow x \in \bar{S})$. Suppose in fact that for some x, $\forall y (y \lhd x \rightarrow y\in \bar{S})$ but $x\in S$. Then all $y\lhd x$ are not in S but x is in S and thus x is the minimum of S, contra our hypothesis.    $\square$

Remark 1

The proof of Lemma 4 above shows that if $\mathbf {RCA}_0+\mathrm {WO}(\sigma )$ proves $\forall X F(X)$ with F(X) arithmetic, then $\mathbf {T}_\mathbf {\sigma }$ proves the formula $F'({\mathsf U})$ obtained from F(X) by replacing expressions of the form ‘$t\in X$’ by ‘${\mathsf U}(t)$’.

Then, we proceed by showing that Lemma 4 gives a sufficient condition for $\varPi ^1_1$-conservativity.

Lemma 5

If $T_1$ and $T_2$ are theories in the language of second order arithmetic and every model of $T_1$ is an $\omega$-submodel of a model of $T_2$ then $T_2$ is $\varPi ^1_1$-conservative over $T_1$.

Proof

If $\psi$ is $\varPi ^1_1$ and $T_1$ does not prove $\psi$, let $\mathbf {M}_1$ be a model of $T_1 + \lnot \psi$. Then $\mathbf {M}_1$ is an $\omega$-submodel of a model $\mathbf {M}_2$ of $T_2$. Then $\mathbf {M}_2$ is a model of $T_2 + \lnot \psi$ and thus $T_2$ does not prove $\psi$.    $\square$

Theorem 4

$\mathrm {\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })}$ is $\varPi ^1_1$-conservative over $\mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$.

Proof

Follows immediately from Lemmas 4 and 5.

Theorem 5

The proof-theoretic ordinal of $\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })$ is $\mathbf {\sigma }^{\omega }$.

Proof

The upper bound follows from Theorems 3 and 4. The lower bound follows from the observation that for each n $\mathbf {RCA}_0 + \mathrm {WO}(\sigma )\vdash \mathrm {WO}(\sigma ^n)$. The proof, which we omit, is analogous to the proof that $\mathbf {RCA}_0 \vdash \mathrm {WO}(\omega ^n)$, for each n.

   $\square$

Remark 2

The $\varPi ^1_1$-conservativity of $\mathbf {I}\varSigma _1 + \mathrm {TI}(\mathbf {\sigma }, \varPi _1)$ over $\mathrm {\mathbf {RCA}_0 + \mathrm {WO}(\mathbf {\sigma })}$ also holds and can be established by standard arguments. In particular one can prove that if $A({\mathsf U})$ is provable in $\mathbf {T}_\mathbf {\sigma }$ then $\forall X A^*(X)$ is provable in $\mathbf {RCA}_0+\mathrm {WO}(\sigma )$, where $A^*(X)$ is the result of first replacing ‘${\mathsf U}(t)$’ by ‘$t\in X$’ and then translating the primitive recursive function and predicate symbols not belonging to the language of $\mathbf {RCA}_0$ as in [16], Definition IX.3.4.