# Is there a 'very fast growing' hierarchy that would capture System F?

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:

https://mathoverflow.net/questions/144041/proof-theoretic-ordinal-of-zfc-or-consistent-zfc-extensions

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