6
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

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$.

[1] Wolfram Pohlers. Proof theory: The first step into impredicativity. Springer Science, 2008.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Hmm, does $ACA_0$ + the omega rule have a higher $\Pi^1_1$ proof-theoretic ordinal? $\endgroup$
    – Keshav Srinivasan
    Dec 23, 2022 at 14:17
  • 2
    $\begingroup$ 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. $\endgroup$
    – Fedor Pakhomov
    Dec 23, 2022 at 14:31
  • $\begingroup$ By the way, there is a citation button in the editor. It's not supported on touch devices or I'd edit the answer myself. $\endgroup$
    – Calliope Ryan-Smith
    Dec 23, 2022 at 15:46
  • $\begingroup$ How do you prove that $ACA_0$ + the omega rule can prove that every recursive ordinal is well-founded? $\endgroup$
    – Keshav Srinivasan
    Dec 23, 2022 at 17:42
  • $\begingroup$ @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). $\endgroup$
    – Fedor Pakhomov
    Dec 23, 2022 at 18:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.