8
$\begingroup$

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?

$\endgroup$
3
  • $\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$ Mar 10, 2011 at 17:00
  • $\begingroup$ @Emil: Why not post your comment as an answer? $\endgroup$ Mar 10, 2011 at 17:01
  • 1
    $\begingroup$ OK, I just thought it was a bit cheap. $\endgroup$ Mar 10, 2011 at 17:09

2 Answers 2

7
$\begingroup$

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.

$\endgroup$
2
  • $\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
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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