# Kruskal's tree theorem

In mathematics, **Kruskal's tree theorem** states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered under homeomorphic embedding. The theorem was conjectured by Andrew Vázsonyi and proved by Joseph Kruskal (1960); a short proof was given by Nash-Williams (1963). It has since become a prominent example in reverse mathematics as a statement that cannot be proved within ATR_{0} (a form of Arithmetical transfinite recursion), and a finitary application of the theorem gives the existence of the notoriously fast-growing TREE function.

In 2004, the result was generalized from trees to graphs as the Robertson–Seymour theorem, a result that has also proved important in reverse mathematics and leads to the even-faster-growing SSCG function.

## Statement[edit]

We give the version proved by Nash-Williams; Kruskal's formulation is somewhat stronger. Given a tree with a root, and given vertices , , call a successor of if the unique path from the root to contains , and call an immediate successor of if additionally the path from to contains no other vertex. Take to be a partially ordered set. Taking to be rooted trees with vertices labeled in , we say that is inf-embeddable in and write if there is a map from the vertices of to the vertices of such that

- For all vertices of , the label of precedes the label of ,
- If is any successor of in , then is a successor of , and
- If are any pair of distinct immediate successors of , then the path from to in contains .

Then result states that, if is well-quasi-ordered, it follows that the set of rooted trees with labels in is well-quasi-ordered under the order defined above. That is to say, given any infinite sequence of rooted trees labeled in , there is some so that .

## Friedman's work[edit]

For a countable label set , Kruskal's tree theorem can be expressed and proven using second-order arithmetic. However, like Goodstein's theorem or the Paris–Harrington theorem, some special cases and variants of the theorem can be expressed in subsystems of second-order arithmetic much weaker than the subsystems where they can be proved. This was first observed by Harvey Friedman in the early 1980's, an early success of the then-nascent field of reverse mathematics; in the case where the trees above are taken to be unlabeled (that is, in the case where has order one), Friedman found that the result was unprovable in ATR_{0},^{[1]} thus giving the first example of a predicative result with a provably impredicative proof.^{[2]} This case of the theorem is still provable in Π^{1}

_{1}-CA_{0}, but by adding a "gap condition" ^{[3]} to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system.^{[4]}^{[5]} Much later, the Robertson-Seymour theorem would give another theorem unprovable inside Π^{1}

_{1}-CA_{0}.

Ordinal analysis confirms the strength of Kruskal's theorem, with the proof-theoretic ordinal of the theorem equaling the small Veblen ordinal (sometimes confused with the smaller Ackermann ordinal).

### TREE(3)[edit]

Suppose that *P*(*n*) is the statement

- There is some
*m*such that if*T*_{1},...,*T*_{m}is a finite sequence of unlabeled rooted trees where*T*_{k}has*n*+*k*vertices, then*T*_{i}≤*T*_{j}for some*i*<*j*.

This statement is a simple application of Kruskal's theorem, for each *n*, Peano arithmetic can prove that *P*(*n*) is true, but Peano arithmetic cannot prove the statement "*P*(*n*) is true for all *n*".^{[6]} Moreover the shortest proof of *P*(*n*) in Peano arithmetic grows phenomenally fast as a function of *n*; far faster than any primitive recursive function or the Ackermann function for example. The least *m* for which *P*(*n*) holds similarly grows extremely quickly with *n*.

By incorporating labels, Friedman defined a far-faster growing function,^{[7]} for a positive integer *n*, take *TREE*(*n*)^{[*]} to be the largest *m* so that we have the following:

- There is a sequence
*T*_{1},...,*T*_{m}of rooted trees labelled from a set of*n*labels, where each*T*_{i}has at most*i*vertices, such that*T*_{i}≤*T*_{j}does not hold for any*i*<*j*≤*m*.

The *TREE* sequence begins *TREE*(1) = 1, *TREE*(2) = 3, then suddenly *TREE*(3) explodes to a value so enormously large that many other "large" combinatorial constants, such as Friedman's *n*(4),^{[*]} are extremely small by comparison. A lower bound for *n*(4), and hence an *extremely* weak lower bound for *TREE*(3), is *A*(*A*(...*A*(1)...)), where the number of *A*s is *A*(187196),^{[8]} and *A*() is a version of Ackermann's function: *A*(*x*) = 2 [*x*+1] *x* in hyperoperation. Graham's number, for example, is approximately *A*^{64}(4) which is much smaller than the lower bound *A*^{A(187196)}(1). It can be shown that the growth-rate of the function TREE is at least in the fast-growing hierarchy.

## See also[edit]

## Notes[edit]

Friedman originally denoted this function by^{^ *}*TR*[*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 x_{j},...,x_{2j}.^{[9]}*n*(1) = 3,*n*(2) = 11 and*n*(3) > 2 [7199] 158386.

## References[edit]

- Citations

**^**Simpson 1985, Theorem 1.8**^**Friedman 2002, p. 60**^**Simpson 1985, Definition 4.1**^**Simpson 1985, Theorem 5.14**^**Marcone 2001, p. 8–9**^**Smith 1985, p. 120**^**Friedman, Harvey (28 March 2006). "273:Sigma01/optimal/size".*Ohio State University Department of Maths*. Retrieved 8 August 2017.**^**Friedman, Harvey M. (1 June 2000). "Enormous Integers In Real Life" (PDF).*Ohio State University*. Retrieved 8 August 2017.**^**Friedman, Harvey M. (8 October 1998). "Long Finite Sequences" (PDF).*Ohio State University Department of Mathematics*. pp. 5, 48 (Thm.6.8). Retrieved 8 August 2017.

- Bibliography

- Friedman, Harvey M. (2002),
*Internal finite tree embeddings. Reflections on the foundations of mathematics (Stanford, CA, 1998)*, Lect. Notes Log.,**15**, Urbana, IL: Assoc. Symbol. Logic, pp. 60–91, MR 1943303 - Gallier, Jean H. (1991), "What's so special about Kruskal's theorem and the ordinal Γ
_{0}? A survey of some results in proof theory" (PDF),*Ann. Pure Appl. Logic*,**53**(3): 199–260, doi:10.1016/0168-0072(91)90022-E, MR 1129778 - Kruskal, J. B. (May 1960), "Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture" (PDF),
*Transactions of the American Mathematical Society*, American Mathematical Society,**95**(2): 210–225, doi:10.2307/1993287, JSTOR 1993287, MR 0111704 - Marcone, Alberto (2001). "Wqo and bqo theory in subsystems of second order arithmetic" (PDF).
*Reverse mathematics*.**21**: 303–330. - Nash-Williams, C. St.J. A. (1963), "On well-quasi-ordering finite trees",
*Proc. Camb. Phil. Soc.*,**59**(04): 833–835, doi:10.1017/S0305004100003844, MR 0153601 - Rathjen, Michael; Weiermann, Andreas (1993). "Proof-theoretic investigations on Kruskal's theorem".
*Annals of Pure and Applied Logic*.**60**(1): 49–88. doi:10.1016/0168-0072(93)90192-g. - Simpson, Stephen G. (1985), "Nonprovability of certain combinatorial properties of finite trees", in Harrington, L. A.; Morley, M.; Scedrov, A.; et al.,
*Harvey Friedman's Research on the Foundations of Mathematics*, Studies in Logic and the Foundations of Mathematics, North-Holland, pp. 87–117 - Smith, Rick L. (1985), "The consistency strengths of some finite forms of the Higman and Kruskal theorems", in Harrington, L. A.; Morley, M.; Scedrov, A.; et al.,
*Harvey Friedman's Research on the Foundations of Mathematics*, Studies in Logic and the Foundations of Mathematics, North-Holland, pp. 119–136