6
$\begingroup$

According to Wikipedia(https://en.wikipedia.org/wiki/Ordinal_analysis) and nlab(https://ncatlab.org/nlab/show/ordinal+analysis), a proof-theoretic ordinal of $\mathsf{PRA}$ is $\omega^\omega$.

However, according to Beckmann's doctoral thesis, Separating fragments of bounded arithmetic, a proof-theoretic ordinal of $\mathsf{I}\Sigma^0_0$ that includes primitive recursive function symbols and their defining axioms is $\omega^2$.

I think this is contradicted by the fact that $\mathsf{I}\Sigma^0_0$ that includes primitive recursive function symbols and its defining axioms is a conservative extension of $\mathsf{PRA}$. I wonder whether the proof-theoretic ordinal of weak first-order arithmetic written in wikipedia, for example $|\mathsf{EFA}|=\omega^3, |\mathsf{PRA}|=\omega^\omega$, is actually correct.

Improve this question
$\endgroup$
8
  • 5
    $\begingroup$ Proof-theoretic ordinals are very nice measure of strength for natural strong theories (e.g. $\mathsf{PA},\Pi^1_1\text{-}\mathsf{CA}_0$) since 1. we have the same ordinal for various definitions of proof-theoretic ordinal that in general doesn't have to agree and 2. theories of different strength are differentiated by the proof-theoretic ordinals. However in the case of weak theories like $\mathsf{EFA}$ or systems of bounded arithmetic neither is the case. And if one for some reasons anyway wants to assign ordinals to weak systems, it is important to specify the definition of $|T|$. $\endgroup$
    – Fedor Pakhomov
    Dec 6, 2019 at 17:28
  • 2
    $\begingroup$ I'm not an expert, but is there any reasonable definition of proof theoretical ordinals for which the ordinal of PRA is not $\omega^\omega$ ? $\endgroup$
    – Simon Henry
    Dec 7, 2019 at 0:16
  • 2
    $\begingroup$ @Wojowu In fact the limit of provable transfinite induction for $\Delta_0$-formulas in $\mathsf{PRA}$ is $\omega^2$. The reason for this is that the axiom of transfinite induction on $\omega^2$ for $\Delta_0$-formulas is equivalent to the axiom of $\Pi_1$-induction (on $\omega$). And $\mathsf{I}\Pi_1=\mathsf{I}\Sigma_1\supsetneq \mathsf{PRA}$. $\endgroup$
    – Fedor Pakhomov
    Dec 7, 2019 at 9:15
  • 3
    $\begingroup$ @SimonHenry Actually one should be careful in order to get to $\omega^\omega$ as the ordinal of $\mathsf{PRA}$; I list the ways that I know. 1. The least $\alpha$ (from a canonical ordinal notation system) s.t. $\mathsf{EA}+\Delta_0\text{-}\mathsf{TI}(\alpha)\vdash \mathsf{Con}(\mathsf{PRA})$. 2. The suprema of $\alpha$ s.t. $\mathsf{PRA}$ proves the totality of function $H_\alpha$ from Hardy's hierarchy. 3. The suprema of order types of primitive recursive well-orderings $\prec$ such that $\mathsf{PRA}(f)$ proves that free unary functional symbol $f$ isn't a descending sequence in $\prec$. $\endgroup$
    – Fedor Pakhomov
    Dec 7, 2019 at 9:21
  • 3
    $\begingroup$ @SimonHenry I already pointed out that the definition with the limit of provable transfinite induction doesn't give $\omega^\omega$. But also you wouldn't get it as the limit of $\alpha$ for which $\mathsf{PRA}$ proves totality of functions $F_\alpha$ from fast-growing hierarchy (the limit is $\omega$). And also if instead of free function symbol you would add to $\mathsf{PRA}$ free unary predicate $X$ and consider the limit of order types of primitive recursive $\prec$ for which $\mathsf{PRA}(X)$ proves that $X$ isn't downward unbounded in $\prec$ (this ordinal is $\omega^2$). $\endgroup$
    – Fedor Pakhomov
    Dec 7, 2019 at 9:27

0

Reset to default

Your Answer

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