MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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}$. – Emil Jeřábek Mar 10 '11 at 17:00
@Emil: Why not post your comment as an answer? – François G. Dorais Mar 10 '11 at 17:01
OK, I just thought it was a bit cheap. – Emil Jeřábek Mar 10 '11 at 17:09
up vote 7 down vote accepted

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.

share|cite|improve this answer
Thanks. Is $I\Pi^0_n$ equivalent to $I\Sigma^0_n$ and/or $I\Delta^0_n$? – Russell O'Connor Mar 10 '11 at 18:10
$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}$. – Emil Jeřábek Mar 10 '11 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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.