<p>Typically, fast growing hierarchies are characterized by <a href="https://en.wikipedia.org/wiki/Ordinal_notation" rel="nofollow noreferrer">ordinal notations</a>, which are really just ways to express fast-growing functions (but it's sometimes convenient to see them as ordinals in the mathematical sense).</p>

<p>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$.</p>

<p>So the question really is:</p>

<blockquote>
  <p>Is there an ordinal notation for $\mathrm{PA}_2$?</p>
</blockquote>

<p>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.</p>

<p>The following mathoverflow question explains this idea in more detail:</p>

<p><a href="https://mathoverflow.net/questions/144041/proof-theoretic-ordinal-of-zfc-or-consistent-zfc-extensions">https://mathoverflow.net/questions/144041/proof-theoretic-ordinal-of-zfc-or-consistent-zfc-extensions</a></p>

CC BY-SA 4.0
2018-06-08T18:01:29.780Z
Was the suspense "corresponds to the..." aimed for, or edit error?
Łukasz Lew
CC BY-SA 4.0
2018-06-08T18:06:23.880Z
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
CC BY-SA 4.0
2018-06-08T19:04:10.940Z
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
CC BY-SA 4.0
2018-06-08T19:14:54.130Z
@ŁukaszLew Oh and for some reason I forgot to finish that sentence. Fixed.
cody
CC BY-SA 4.0
2018-06-09T00:28:06.057Z
Thanks, the observation of correspondence between ordinal notations and fundamental sequence is useful.
Łukasz Lew
CC BY-SA 4.0
2018-06-08T17:51:47.257Z
2018-06-08T19:14:28.967Z
2018-06-08T19:14:28.967Z
cody
<p>Particular ordinals in slow-growing and fast growing hierarchies can capture the expressiveness of many predicative type systems.</p>

<p>Is there a hierarchy of function that could possibly capture impredicative System F?</p>

<type-systems><hierarchy-theorems><normalization>
Is there a 'very fast growing' hierarchy that would capture System F?
Łukasz Lew
# Is there a 'very fast growing' hierarchy that would capture System F?

(Asked by: username_0 on 2018-06-08)

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?

**Tags:** type-systems, hierarchy-theorems, normalization


---

## 1 answers

### Answer by username_1 on 2018-06-08. Score: 5 | Accepted answer

Typically, fast growing hierarchies are characterized by [ordinal notations](https://en.wikipedia.org/wiki/Ordinal_notation), 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>

> **Comments:**
> **username_0**: Was the suspense "corresponds to the..." aimed for, or edit error?  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_1**: @ŁukaszLew Oh and for some reason I forgot to finish that sentence. Fixed.  
> **username_0**: Thanks, the observation of correspondence between ordinal notations and fundamental sequence is useful.  

---

