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?


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:


| cite | improve this answer | |
  • $\begingroup$ Was the suspense "corresponds to the..." aimed for, or edit error? $\endgroup$ – Łukasz Lew Jun 8 '18 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$ – Łukasz Lew Jun 8 '18 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 Jun 8 '18 at 19:04
  • $\begingroup$ @ŁukaszLew Oh and for some reason I forgot to finish that sentence. Fixed. $\endgroup$ – cody Jun 8 '18 at 19:14
  • $\begingroup$ Thanks, the observation of correspondence between ordinal notations and fundamental sequence is useful. $\endgroup$ – Łukasz Lew Jun 9 '18 at 0:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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