Proof that TREE(n) where n >= 3 is finite? Reading online, it generally seems accepted that TREE(n) where n >= 3 is a finite number, but large enough to be incomputable and only has extremely loose lower bounds today. TREE(n) is the function defined by Harvey Friedman, based on Joseph Kruskal's tree theorem. A simplified definition:
"TREE(n) = the maximum length of a set of rooted trees Tm with n possible vertex labels, where Tm has m or fewer vertices, and subsequent trees do not homeomorphically embed a preceding tree."
We can trivially show that TREE(1) = 1 and TREE(2) = 3.
My question is, how can it be known that for values of n greater than 2, the series of possible trees is finite? If we can't compute the solution, how do we know that it ends? If there is an existing write up online describing proof that these numbers are finite, please link me to it, I'm finding limited reading material on the TREE function. Thanks.
 A: The finiteness of $TREE(n)$ for each $n$ is a consequence of Kruskal's tree theorem. There are various proofs of Kruskal's theorem, including a particularly short one by Nash-Williams.
Ultimately, the proof - similarly to the proof of Goodstein's theorem - amounts to showing that an appropriate partial order is well-founded by assigning invariants to elements of the partial order; the proof then concludes by showing that these invariants are in fact ordinals, and so the theorem follows from an appropriate transfinite induction principle (e.g. Goodstein's theorem follows from, and is in fact equivalent to in an appropriate sense, the well-foundedness of $\epsilon_0$). There is also a connection between such arguments and consistency proofs, beginning with Gentzen's proof of the consistency of PA from an appropriate transfinite induction principle.

Incidentally, in the sense of reverse mathematics Kruskal's theorem is quite strong; it is not provable in the system ATR$_0$, or even in the stronger system $\Pi^1_1$-CA$_0$, making it quite rare amongst standard combinatorial facts. The proof of appropriate unprovability goes by showing that Kruskal's theorem implies that certain ordinals are well-founded; these ordinals are large enough that (a la Gentzen) induction along them implies the consistency of ATR$_0$ and of $\Pi^1_1$-CA$_0$, so by Godel's incompleteness theorem neither system can prove Kruskal's theorem. 
