# Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?

As discussed in Noah Schweber's answer to What is the proof-theoretic ordinal of true arithmetic?, it is somewhat ambiguous what “the proof-theoretic ordinal of True Arithmetic” might mean. In one sense, it is $$\omega_1^\text{CK}$$, because e.g. True Arithmetic satisfies $$\Sigma^0_1$$ induction for every notation for a recursive ordinal. But of course $$\Sigma^0_1$$ transfinite induction is not the same as full transfinite induction, which can’t even be expressed in the language of first-order arithmetic, so I’d like to ask about a second-order version of this notion.

My question is, which ordinals $$\alpha$$ can $$\text{ACA}_0$$ + True Arithmetic prove are well-founded, in the sense that there exists some arithmetically definable well-ordering $$R$$ with order type $$\alpha$$ such that $$\text{ACA}_0$$ + True Arithmetic proves $$\operatorname{WO}(R)$$? Where $$\operatorname{WO}(R)$$ is the $$\Pi^1_1$$ sentence asserting $$R$$ is well-ordered, i.e. $$R$$ satisfies transfinite induction for all sets, not merely for e.g. $$\Sigma^0_1$$ sets.

Is the answer all recursive ordinals? If so, how does that square with the work of Feferman and Schutte, who made infinitary deductive systems for ramified second-order arithmetic containing $$\text{ACA}_0$$, the omega rule, and various comprehension schemes, and found that the proof-theoretic ordinal of the resultant systems is $$\Gamma_0$$, the Feferman–Schutte ordinal which is recursive?

There is a result of Kreisel (see [1, Theorem 6.7.4,6.7.5]) that for extensions of $$\mathsf{ACA}_0$$ the $$\Pi^1_1$$ proof-theoretic ordinal (suprema of the order types of provable recursive well-orderings) doesn't change after additions of true $$\Sigma^1_1$$-sentences. Also note that for infinitely axiomatized theory $$T$$ its $$\Pi^1_1$$ proof-theoretic ordinal is the suprema of proof-theoretic ordinals of its finite subtheories. Thus the $$\Pi^1_1$$ proof-theoretic ordinal of $$\mathsf{ACA}_0+\mathsf{Th}(\mathbb{N};0,1,+,\times)$$ is $$\varepsilon_0$$.
• Hmm, does $ACA_0$ + the omega rule have a higher $\Pi^1_1$ proof-theoretic ordinal? Dec 23, 2022 at 14:17
• Sure, the closure of $\mathsf{ACA}_0$ under $\omega$-rule will have $\omega_1^{\mathit{CK}}$ as its $\Pi^1_1$-ordinal. The point is that unlike all first-order truths, when applied to second-order formulas, $\omega$ rule isn't restricted to $\Sigma^1_1$ conclusions. Dec 23, 2022 at 14:31
• How do you prove that $ACA_0$ + the omega rule can prove that every recursive ordinal is well-founded? Dec 23, 2022 at 17:42
• @Keshav Simply by virtue of the fact that $\omega$-logic proves all true $\Pi^1_1$-sentences (for example, you could read about this in Pohlers textbook that I referred to in the answer). Dec 23, 2022 at 18:37