# What is proof-theoretic ordinal of weak first-order arithmetic?

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.

• 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|$. Dec 6, 2019 at 17:28
• 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$ ? Dec 7, 2019 at 0:16
• @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}$. Dec 7, 2019 at 9:15
• @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$. Dec 7, 2019 at 9:21
• @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$). Dec 7, 2019 at 9:27