Particular ordinals in slow-growing and fast growing hierarchies can capture the expressiveness of many predicative type systems.

Is there a hierarchy of function that could possibly capture impredicative System F?


1 Answer 1


Typically, fast growing hierarchies are characterized by ordinal notations, which are really just ways to express fast-growing functions (but it's sometimes convenient to see them as ordinals in the mathematical sense).

There is a somewhat generic way of assigning an ordinal (notation) to a consistent theory, though it is very non-constructive. For various technical reasons, the ordinal for $\mathrm{PA}_2$ corresponds to the fast growing functions expressible in system $F$.

So the question really is:

Is there an ordinal notation for $\mathrm{PA}_2$?

As far as I am aware, we do not know the answer to this question, and it is a very important open question in proof theory/ordinal analysis.

The following mathoverflow question explains this idea in more detail:


  • $\begingroup$ Was the suspense "corresponds to the..." aimed for, or edit error? $\endgroup$ Commented Jun 8, 2018 at 18:01
  • $\begingroup$ Your answer seems to suggest that all the ordinals smaller than the proof ordinal of a theory correspond to indexes of provably fast-growing functions. Is that the case? If yes, how the fact that the choice of fundamental sequence affects the hierarchy is taken into account? Perhaps it is somehow related to a particular ordinal notation? $\endgroup$ Commented Jun 8, 2018 at 18:06
  • 1
    $\begingroup$ Yes, ordinal notations are essentially ways of constructively choosing a fundamental sequence. "Raw" ordinals are, as I understand it, mostly useless for measuring the strength of a theory. $\endgroup$
    – cody
    Commented Jun 8, 2018 at 19:04
  • $\begingroup$ @ŁukaszLew Oh and for some reason I forgot to finish that sentence. Fixed. $\endgroup$
    – cody
    Commented Jun 8, 2018 at 19:14
  • $\begingroup$ Thanks, the observation of correspondence between ordinal notations and fundamental sequence is useful. $\endgroup$ Commented Jun 9, 2018 at 0:28

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.