For theories with well known proof-theoretic-ordinals, (what) is there a correspondence between their proof-theoretic-ordinal and (ordinal indexed families of?) fast growing functions provable total in a given theory ?

up vote 10 down vote accepted

Yes: for many theories, $\alpha$ is the proof-theoretic ordinal of T exactly when T proves that $f_\beta$ is total for all $\beta<\alpha$, but does not prove $f_\alpha$ is total. (Where $f_\alpha$ is the $\alpha$-th function in the fast-growing hierarchy.)

Avigad has argued that the correct definition of proof-theoretic ordinals is in terms of provably total functions - specifically, that the proof theoretic ordinal of T is $\geq\alpha$ exactly when T proves the totality of all functions which are "$\prec\alpha$-recursive" functions, where $\prec\alpha$-recursive means that the function is given by a program together with a timer which uses ordinal notations $\prec\alpha$.

With some care about the encoding, there's a tight connection between proving fast-growing functions total and proving all $\prec\alpha$-recursive functions total, so in some sense one can take proving the totality of fast-growing functions to be the definition of the proof-theoretic ordinal.

As usual with proof-theoretic ordinals, all reasonable definitions are going to be equivalent for nice theories (which includes all strong enough theories which have appeared naturally elsewhere in logic), but there are artificial theories that make the various definitions no longer equivalent.

  • How come the correspondence you and Avigad are pointing out is not affected by the arbitrariness of choice of fundamental sequences? – Łukasz Lew Jun 12 at 0:58
  • 1
    @ŁukaszLew: I think it is somewhat affected by the arbitrariness of choice of fundamental sequences; the fast-growing hierarchy is less sensitive than the slow-growing one, but the claim I made is still only going to be for conventional choices of fundamental sequences. (This is one reason Avigad's notion of $\prec$-recursive is better as a definition, because some constraints on the encoding are built into the definition, and you can figure out from those which functions grow at the right rates to be provably total.) – Henry Towsner Jun 12 at 2:35

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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