I believe I can state with some confidence that TREE(3) is larger than $f_{\vartheta (\Omega^{\omega}, 0)} (n(4))$, given a natural definition of $f$ up to $\vartheta (\Omega^{\omega}, 0)$. I can state with certainty that TREE(3) is larger than $H_{\vartheta (\Omega^{\omega}, 0)} (n(4))$, where H is a certain version of the Hardy hierarchy.

To obtain this result, I will first define a version of TREE(n) for unlabeled trees:

Let tree(n) be the length of the longest sequence of unlabeled rooted trees $T_1, T_2, \ldots, T_m$ such that $T_i$ has less than or equal to $n+i$ vertices and for no $i, j$ with $i < j$ do we have $T_i$ homeomorphically embeddable into $T_j$. (Note the term "embeddable" rather than "subtree"; the terms are different, and I believe using "subtree" would lead to infinite sequences.)

In order to obtain a long sequence of trees, we will define a well-order on unlabeled rooted trees. This definition will be by induction on the sum of the heights of the two trees being compared.

Define an immediate subtree of a rooted tree $T$ to be a full subtree starting at one of its children.

Given two rooted trees $S, T$, we define $S = T$ if the two trees are identical. We define $S \leq T$ if $S = T$ or $S < T$.

Given two rooted trees $S, T$, we define $ < $ as follows. Say $S < T$ if $S \leq T_i$, where $T_i$ is an immediate subtree of $T$. Similarly, say $T < S$ if $T \leq S_i$, where $S_i$ is an immediate subtree of $S$.

Otherwise, compare the number of children of $S$ and $T$. If $S$ has more children than $T$, then $S > T$, and vice versa.

Otherwise, suppose $S$ and $T$ both have $n$ children. Let $S_1, S_2, \ldots, S_n$ and $T_1, T_2, \ldots T_n$ be the immediate subtrees of $S$ and $T$ respectively, ordered from smallest to largest. Compare $S_1$ to $T_1$, then $S_2$ to $T_2$, etc., until we get a pair of unequal trees $S_i$ and $T_i$. If $S_i > T_i$ then $S > T$, and vice versa. Of course, of all pairs of immediate subtrees are equal, then $S$ and $T$ will be equal.

This gives a linear order on unlabeled rooted trees, and one can prove that this is a well-order. Further, this well-ordering has order type $\vartheta(\Omega^\omega,0)$. This definition is a modification of a well-ordering of ordered rooted trees due to Levitz, and expounded on in papers by Jervell.

From this well-ordering we can define fundamental sequences for ordinals up to $\vartheta (\Omega^{\omega}, 0)$. Simply put, given an ordinal $\alpha$, let $\alpha[n]$ be the largest ordinal less than $\alpha$ corresponding to a tree of $n$ vertices or less.

From this, we can define our version of the Hardy hierarchy:

$H_0(n) = n$

$H_{\alpha + 1}( n) = H_{\alpha}( n+1)$

For $\alpha$ a limit ordinal, $H_{\alpha}( n) = H_{\alpha[n+1]}( n+1)$

Note the $n+1$'s in the last line - this differs from the usual values of $n$. Of course, this will only make the functions larger.

$H_{\alpha}( n)$ for $\alpha < \vartheta (\Omega^{\omega}, 0)$ is the final index $m$ in the sequence of trees $T_n, T_{n+1}, \ldots, T_m$ where $T_n$ corresponds to $\alpha$ and $T_i$ is the largest tree with at most $i$ vertices that is smaller than $T_{i-1}$, and $T_m$ is the tree with one vertex. Thus $H_{\vartheta (\Omega^{\omega}, 0)}( n)$ will be the final index $m$ in the sequence of trees $T_{n+1}, T_{n+2}, \ldots, T_m$ where $T_{n+1}$ is arbitrary.

Thus tree(n) $\geq H_{\vartheta (\Omega^{\omega}, 0)}( n) - n$.

So where does TREE(3) come in? Harvey Friedman himself explains in a post to the Foundations of Mathematics message boards:

http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html

In the post he explains why a proof of the theorem "TREE(3) exists" in the theory $ACA_0 + \Pi^1_2\text{-}BI$ must have more than $2\uparrow\uparrow 1000$ symbols. He does this by showing that TREE(3) must be very large - specifically, he constructs a sequence of more than $n(4)$ rooted trees labeled from {1,2,3} such that $T_i$ has at most $i$ vertices, for no $i, j$ with $i < j$ do we have $T_i$ homeomorphically embeddable into $T_j$, and each tree contains either a 2 label or a 3 label. We can obviously continue this with tree($n(4)$) trees with all labels 1. Thus we have

TREE(3) $\geq$ tree$(n(4)) + n(4) \geq H_{\vartheta (\Omega^{\omega}, 0)}(n(4))$

In fact, we can do somewhat better than this; we can replace the $n(4)$ above by $F(4)$, where $F(4)$ is defined as the length of the longest sequence of sequences $x_1, x_2, \ldots x_n$ from {1,2,3,4} such that $x_i$ has length $i+1$ and for no $i,j$ with $i < j$ do we have $x_i$ a subsequence of $x_j$. I can prove much better bounds for $F(4)$ than Friedman's lower bound for $n(4)$; specifically,

$F(4) > f_{\omega^2 + \omega + 1}f_{\omega^2 + \omega + 1}f_{\omega^2 + \omega}f_{\omega^2 + 1}f_{\omega^2 + 1}f_{\omega^2}f_{ \omega + 1}f_{ \omega + 1}f_{\omega}(30)$

But such specificity is perhaps unwarranted given how far from TREE(3) it may be.

canprove that $\mathsf{TREE}(3)$ exists, and indeed for each $n$ $\mathsf{PA}$ can prove that $\mathsf{TREE}(n)$ exists. This is because the definition of the $\mathsf{TREE}$ function is sufficiently simple that $\mathsf{PA}$ (or indeed vastly less) can verify each instance of it. What $\mathsf{PA}$ can't prove is "$\forall n$, $\mathsf{TREE}(n)$ exists." Note that the same situation holds re: consistency (for each $n$ $\mathsf{PA}$ proves "there is no contradiction in $\mathsf{PA}$ of length $<n$," Godel's second notwithstanding). $\endgroup$6more comments