# 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.

## History

The theorem was conjectured by Andrew Vázsonyi and proved by Joseph Kruskal (1960); a short proof was given by Crispin Nash-Williams (1963). It has since become a prominent example in reverse mathematics as a statement that cannot be proved in ATR$_0$ (a second-order arithmetic theory with a form of arithmetical transfinite recursion).
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, which dwarfs ${\text{TREE}}(3)$. A finitary application of the theorem gives the existence of the fast-growing TREE function. TREE(3) is largely accepted to be one of the large finite numbers, dwarfing other large numbers such as Graham's number and googolplex.

## Statement

The version given here is that proven by Nash-Williams; Kruskal's formulation is somewhat stronger. All trees we consider are finite.
Given a tree T with a root, and given vertices v, w, call w a successor of v if the unique path from the root to w contains v, and call w an immediate successor of v if additionally the path from v to w contains no other vertex.
Take X to be a partially ordered set. If T$_1$, T$_2$ are rooted trees with vertices labeled in X, we say that T$_1$ is inf-embeddable in T$_2$ and write $T_{1}\leq T_{2}$ if there is an injective map F from the vertices of T$_1$ to the vertices of T$_2$ such that:
* For all vertices v of T$_1$, the label of v precedes the label of $F(v)$;
* If w is any successor of v in T$_1$, then $F(w)$ is a successor of $F(v)$; and
* If w$_1$, w$_2$ are any two distinct immediate successors of v, then the path from $F(w_{1})$ to $F(w_{2})$ in T$_2$ contains $F(v)$.
Kruskal's tree theorem then states:
   If X is well-quasi-ordered, then the set of rooted trees with labels in X is well-quasi-ordered under the inf-embeddable order defined above. (That is to say, given any infinite sequence T$_1$, T$_2$, … of rooted trees labeled in X, there is some $i<j$ so that $T_{i}\leq T_{j}$.)

## Friedman's work

For a countable label set X, 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 1980s, 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 X has size one), Friedman found that the result was unprovable in ATR$_0$, thus giving the first example of a predicative result with a provably impredicative proof. This case of the theorem is still provable by Π$^1$ $_1$-CA$_0$, but by adding a "gap condition" to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system. Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π$^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).

## Weak tree function

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$_i$ has $i+n$ vertices, then $T_{i}\leq T_{j}$ for some $i<j$.
All the statements $P(n)$ are true as a consequence of Kruskal's theorem and Kőnig's lemma. 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". Moreover, the length of 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.
Define ${\text{tree}}(n)$, the weak tree function, as the largest m so that we have the following:
    There is a sequence T$_1$, ..., T$_m$ of unlabeled rooted trees, where each T$_i$ has at most $i+n$ vertices, such that $T_{i}\leq T_{j}$ does not hold for any $i<j\leq m$.
It is known that ${\text{tree}}(1)=2$, ${\text{tree}}(2)=5$, ${\text{tree}}(3)\geq 844,424,930,131,960$ (about 844 trillion), ${\text{tree}}(4)\gg g_{64}$ (where $g_{64}$ is Graham's number), and ${\text{TREE}}(3)$ (where the argument specifies the number of labels; see below) is larger than $\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{8}(7)}(7)}(7)}(7)}(7).$
To differentiate the two functions, "TREE" (with all caps) is the big TREE function, and "tree" (with all letters in lowercase) is the weak tree function.

## TREE function

By incorporating labels, Friedman defined a far faster-growing function. For a positive integer n, take ${\text{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}\leq T_{j}$ does not hold for any $i<j\leq m$.
The TREE sequence begins ${\text{TREE}}(1)=1$, ${\text{TREE}}(2)=3$, before ${\text{TREE}}(3)$ suddenly explodes to a value so large that many other "large" combinatorial constants, such as Friedman's $n(4)$, $n^{n(5)}(5)$, and Graham's number, are extremely small by comparison. A lower bound for $n(4)$, and, hence, an extremely weak lower bound for ${\text{TREE}}(3)$, is $A^{A(187196)}(1)$. Graham's number, for example, is much smaller than the lower bound $A^{A(187196)}(1)$, which is approximately $g_{3\uparrow ^{187196}3}$, where $g_{x}$ is Graham's function.