Ordinal interpretation of Friedman's $n$?
I heard that Kruskal's tree theorem can be turned into a finite form that creates an extremely fast growing function because ordinals could be encoded into trees.
On this wiki page it mentions that there is another very fast growing function (but it's not quite as fast) called $n$.
$n(k)$ is defined as the length of the longest possible sequence that can be constructed with a k-letter alphabet such that no block of letters $x_i$,...,$x_{2i}$ is a subsequence of any later block
I think that is related to Higman's lemma
so I was wondering what is the interpretation of this in terms of ordinals? I guess it must be related to an ordinal between $\epsilon_0$ and $\Gamma_0$.
How can I explain it better. The Ackermann and Goodstein function is fast growing and the TREE function is fast growing, because they are produced from ordinal notations (for up to omega^2 (or is it omega^omega of Primitive recursive arithmetic?), epsilon_0 and Gamma_0 respectively) that measure the proof strength of some theories.. so they are faster than any total function in those theories. I want to know what ordinal and theory is $n$ associated with.
If you understand my meaning please feel free to edit my question. I am only starting at logic so I don't know how to state it formally.
Solution 1:
There is indeed an ordinal interpretation of Friedman's block subsequence theorem; however, the associated ordinal is not between $\varepsilon_0$ and $\Gamma_0$; it is $\omega^{\omega^\omega}$. More precisely, k-labelled sequences have ordinal $\omega^{\omega^{k-1}}$. Friedman's block subsequence theorem is provable in the theory $I\Sigma_3$ but not the theory $I\Sigma_2$; the latter has poof theoretic ordinal $\omega^{\omega^\omega}$.
The ordering on sequences of order type $\omega^{\omega^\omega}$ is as follows:
1-labelled sequences are determined by their length, i.e. 1 < 11 < 111 ... .
Assume now that have ordered k-labelled sequences; we will now order k+1-labelled sequences. Let S and T be two k+1-labelled sequences. If one of S or T has more appearances of k+1 than the other, that sequence will be considered greater. Otherwise, suppose both S and T have n appearances of k+1; express S and T as
$S = S_0$ k+1 $S_1$ k+1 ... k+1 $S_n$
$T = T_0$ k+1 $T_1$ k+1 ... k+1 $T_n$
where the $S_i$ and $T_i$ are k-labelled sequences. Compare the $S_i$ and the $T_i$ lexicographically, i.e. first compare $S_0$ to $T_0$, then $S_1$ to $T_1$, etc. For the smallest $i$ for which $S_i$ and $T_i$ differ, if $S_i > T_i$, then $S > T$; if $S_i < T_i$, then $S < T$. This defines the ordering.
Now I will demostrate that k-labelled sequences have order type $\omega^{\omega^{k-1}}$. Clearly, 1-labelled sequences have order type $\omega = \omega^{\omega^{1-1}}$. Suppose that we have proven that k-labelled sequences have order type $\omega^{\omega^{k-1}}$. Let S be a k+1 labelled sequence, and express S as
$S = S_0$ k+1 $S_1$ k+1 ... k+1 $S_n$.
where the $S_i$ represent k-labelled sequences. Let $\alpha_i$ be the ordinals representing $S_i$. We have $\alpha_i < \omega^{\omega^{k-1}}$ for all $i$. Then $S$ will be associated with the ordinal
$\omega^{\omega^{k-1}n} (1+\alpha_0) + \omega^{\omega^{k-1}(n-1)} \alpha_1 + \ldots + \omega^{\omega^{k-1}} \alpha_{n-1} + \alpha_n$.
I leave it to the reader to show that this association will yield the same ordering as our previously defined ordering. This identifies k+1-labelled sequences with ordinals up to $\omega^{\omega^{k}}$, as desired.
Friedman's n(k) grows at a rate similar to that of $H_{\omega^{\omega^{\omega}}}(k)$ in the Hardy hierarchy, which is equal to $F_{\omega^{\omega}}(k)$ in the fast-growing hierarchy; you lose an $\omega$ when converting to the fast-growing hierarchy.
Solution 2:
According to the end of section 5 of Friedman's paper
http://www.math.osu.edu/~friedman.8/pdf/finiteseq10_8_98.pdf
$n(k)$ is situated at level $\omega^\omega$ of the extension of the hierarchy of primitive recursive functions past $\omega$. In computational terms he cites earlier papers showing that this level of the hierarchy contains (and is exhausted by) something called "nested multiple recursive functions". Based on this I would guess that the answer is along the following lines, and is far below $\epsilon_0$:
proving that $n(k)$ is finite for all $k$ is equivalent (over PRA) to proving ${\omega^\omega}$ is well ordered (or the same idea with a stack of $3$ or $4$ $\omega$'s)
there is a natural subsystem of PA (extending PRA) that can prove, for any nested multiple recursive function, that the function is total
the proof theoretic ordinal of this system is $\omega^{\omega^{\dots \omega}}$, where the exponential tower has between $2$ and $4$ $\omega$'s
there is a restriction of the $\epsilon_0$ ordinal notation, such as limiting the depth or width of some of the trees to a small value (such as $3$ or $4$ or $5$) that gives a natural graphic notation for the ordinals up to the one you want.