# Correspondence between proof-theoretic ordinals and fast growing functions?

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 ?

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.
• @Ł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 '18 at 2:35