Small proof-theoretic ordinals

Where to find proofs of the following:

1) proof-theoretic ordinal of $I\Sigma_0$, which is Robinson's Q arithmetic with induction on $\Sigma_0$ formulas, is $\omega^2$?

2) proof-theoretic ordinal of $I\Sigma_0+\exp$, which is $I\Sigma_0$ augmented with the fact that exponentiation is total, is $\omega^3$?

3) proof-theoretic ordinal of $I\Sigma_1$, which is Robinson's Q arithmetic with induction on $\Sigma_1$ formulas, is $\omega^\omega$?

Is there any arithmetic (e.g. Robinson's $Q$ with induction on open formulas) with proof-theoretic ordinal less than $\omega^2$?

Solution 1:

While natural theories extending EFA (also called IΣ$_0$+exp or ERA or EA) appear well-ordered under $Π^0_2$ provability, the setting of exact $Π^0_2$ ordinal values for theories below PRA is a matter of convention. However, a reasonable convention is obtained using the Hardy hierarchy of functions:
Set $h_0(x) = x$
$h_{α+1}(x) = h_α(x+1)$
$h_{α}(x) = h_{α[x]}(x)$ for limit $α$ where $α[..]$ is a canonical fundamental sequence for $α$. The link defines a canonical choice below $Γ_0$, but basically we diagonalize over lower indices of $h$ in a reasonable way.

For a theory $T$ including basic arithmetic:
$|T|_{Π^0_2}$ = sup($α$: $T$ proves $h_α$ is total).

Note that $|T|_{Π^0_2}$ formally depends not only on the ordinal but also on the fundamental sequences (and on the formulas defining them). However, for canonical ordinal notation systems, different natural choices of fundamental sequences appear to be equivalent in that for $T$ extending EFA, they give the same $|T|_{Π^0_2}$. The reason is that different reasonable choices will give the same growth rate of $h_{α}(x)$ up to an elementary increase or decrease in the value of $x$.

The remarkable property is that for natural theories extending EFA, $Π^0_2$ provability is completely determined (and well-ordered) by $|T|_{Π^0_2}$. A caveat is that there are different notions of 'natural' (and counterexamples like EFA+Con(PA)), and also many natural theories are beyond known canonical ordinal notation systems.

Now, $h_{ωm+n}(x)=2^m (x+n)$, and for appropriate $α$ and $β$, $h_{α+β}(x) = h_α(h_β(x))$, and $h_{αω}(x)=h_α^x(x)$ (superscript indicates iteration). (The exact equality depends on the choice of fundamental sequences and that $α+β$ (resp. $αω$) does not truncate $α$.)
For every $m$, IΔ$_0$ (also called IΣ$_0$) proves that $2^m x$ is total, but it does not prove that $2^x x$ is total, so the ordinal is $ω^2$.
$h_{ω^2 n}$ approximately corresponds to a stack of $n$ exponentials, which is elementary for a particular $n$ but not as a function of $n$, hence the $ω^3$ ordinal.
$h_{ω^n}$ approximately corresponds to the $n$th level (or so) of the Ackermann function and thus provably total in PRA, but $h_{ω^ω}$ grows like the full Ackermann function, which is beyond PRA. $Σ^0_1$-PA (also called IΣ$_1$) is $Π^0_2$ conservative over PRA and thus has the same $Π^0_2$ ordinal.

A few notes:
* IΔ$_0$ is already interpretable in Robinson arithmetic Q, and there is no standard assignment of ordinals below that.
* Since total functions are closed under composition, every $|T|_{Π^0_2}$ is a power of $ω$.
* If we had set $h_{α+1}(x) = h_α(2^x)$, then $|\mathrm{EFA}|_{Π^0_2}$ would be $ω$, hence the caveat about convention.
* There also are other approaches to ordinals for weak theories, including by embedding the theory into a second order theory using a free second order variable $X$ and extending induction (and other axioms) to formulas using $X$ as a predicate, and getting the $Π^1_1$ ordinal of that theory. I think you would still get the $ω^2$ and $ω^3$ (and $ω^ω$) ordinals, but I have not seen the proof either.