If we take Peano Arithmetic and restrict induction to formulas over various fragments of the arithmetic hierarchy, say to the $\Sigma^0_n$ formulas for various $n$ or some other interesting fragments, how does the proof theoretic ordinal for the theory vary?
-
$\begingroup$ The ordinal of $I\Sigma^0_n$ ($n > 0$) is $\omega_{n+1}$, where one defines $\omega_1=\omega$, $\omega_{n+1}=\omega^{\omega_n}$. $\endgroup$– Emil JeřábekMar 10, 2011 at 17:00
-
$\begingroup$ @Emil: Why not post your comment as an answer? $\endgroup$– François G. DoraisMar 10, 2011 at 17:01
-
1$\begingroup$ OK, I just thought it was a bit cheap. $\endgroup$– Emil JeřábekMar 10, 2011 at 17:09
2 Answers
The proof-theoretic ordinal of $I\Sigma^0_n$ (for $n > 0$) is well-known to be $\omega_{n+1}$, where $\omega_1:=\omega$, $\omega_{n+1}:=\omega^{\omega_n}$. See e.g. Avigad & Sommer.
-
$\begingroup$ Thanks. Is $I\Pi^0_n$ equivalent to $I\Sigma^0_n$ and/or $I\Delta^0_n$? $\endgroup$ Mar 10, 2011 at 18:10
-
1$\begingroup$ $I\Pi^0_n=I\Sigma^0_n$. As for $I\Delta^0_n$, for $n>1$ it equals $B\Sigma^0_n$ (for $n=1$, this is only known in the presence of exponentiation), and it is a $\Pi^0_{n+1}$-conservative extension of $I\Sigma^0_{n-1}$. In particular, it has the same provably total computable functions as $I\Sigma^0_{n-1}$. $\endgroup$ Mar 10, 2011 at 18:34
Emil's answer gives you the ordinals you are asking for, but it may be worth to add a complementary remark: With restricted induction, one needs to be slightly careful about how the ordinals are computed.
For example, the provably recursive functions of $I\Sigma^0_1$ are precisely the primitive recursive functions.
However, these are precisely the $\omega^2$-recursive functions, i.e., those that can be proved total using the infinitary proof-system $\vdash^{\omega^2}_0$ of Tait "Normal derivability in classical logic", in "The syntax and semantics of infinitary languages", Lecture Notes in Mathematics 72, Springer, pp. 204-236.
Given $f:{\mathbb N}\to{\mathbb N}$, let $E(f)$ consist of all those functions "explicitly definable" using 0,1,$f$,$+$, restricted subtraction, and bounded sums and products.
There are several fast-growing hierarchies of recursive functions one uses to analyse fragments of arithmetic. The functions $B_\alpha$ are defined inductively: $B_0(n)=n+1$, $B_{\alpha+1}(n)=B_\alpha(B_\alpha(n))$, $B_\lambda(n)=B_{\lambda_n}(n)$ for $\lambda$ limit, where the $\lambda_n$ are the "natural" strictly increasing sequence of ordinals converging to $\lambda$.
The functions $F_\alpha$ are defined similarly, except that $F_{\alpha+1}(n)=F^{n+1}_\alpha(n)$, where the superindex denotes iterated composition ($n+1$ times). This is the sequence of functions most used in this context.
The functions of the Hardy hierarchy are defined by $H_0(n)=n$, $H_{\alpha+1}(n)=H_\alpha(n+1)$, and $H_\lambda(n)=H_{\lambda_n}(n)$.
Then the primitive recursive functions are precisely the functions in $$\bigcup_{\alpha\prec\omega^2}E(B_\alpha)=\bigcup_{\alpha\prec\omega}E(F_\alpha)=\bigcup_{\alpha\prec\omega^\omega}E(H_\alpha);$$ here, $\prec$ is a partial subordering of the ordinals, but at this level we may identify it with the usual $\lt$.
All this is discussed in great detail in the nice paper by Fairtlough and Wainer, "Hierarchies of provably recursive functions", in "Handbook of Proof Theory", Elsevier, pp. 149-207.