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?
Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)
|
7
2
|
||||||||||
|
|
6
|
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. |
||||||||
|
You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.
|
5
|
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. |
|||
|
|

