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.

A finitary application of the theorem gives the existence of a fast-growing TREE function. TREE(3) is one of the largest simply defined finite numbers, dwarfing other large numbers such as Graham's number and googolplex.¹

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₀ (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 TREE.

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 ${\displaystyle T}$ with a root, and given vertices ${\displaystyle v}$, ${\displaystyle w}$, call ${\displaystyle w}$ a descendant of ${\displaystyle v}$ if the unique path from the root to ${\displaystyle w}$ contains ${\displaystyle v}$, and call ${\displaystyle w}$ a child of ${\displaystyle v}$ if additionally the path from ${\displaystyle v}$ to ${\displaystyle w}$ contains no other vertex.

Take ${\displaystyle (X,\leq _{X})}$ to be a partially ordered set. If ${\displaystyle T_{1}}$, ${\displaystyle T_{2}}$ are rooted trees with vertices labeled in ${\displaystyle X}$, we say that ${\displaystyle T_{1}}$ is inf-embeddable in ${\displaystyle T_{2}}$ and write ${\displaystyle T_{1}\leq T_{2}}$ if there is an injective map ${\displaystyle F}$ from the vertices of ${\displaystyle T_{1}}$ to the vertices of ${\displaystyle T_{2}}$ such that:

• For all vertices ${\displaystyle v}$ of ${\displaystyle T_{1}}$, the label of ${\displaystyle v}$ is ${\displaystyle \leq _{X}}$ the label of ${\displaystyle F(v)}$;
• If ${\displaystyle w}$ is any descendant of ${\displaystyle v}$ in ${\displaystyle T_{1}}$, then ${\displaystyle F(w)}$ is a descendant of ${\displaystyle F(v)}$; and
• If ${\displaystyle w_{1}}$, ${\displaystyle w_{2}}$ are any two distinct children of ${\displaystyle v}$, then the path from ${\displaystyle F(w_{1})}$ to ${\displaystyle F(w_{2})}$ in ${\displaystyle T_{2}}$ contains ${\displaystyle F(v)}$ (equivalently, ${\displaystyle F(w_{1})}$ and ${\displaystyle F(w_{2})}$ lie in different subtrees of ${\displaystyle v}$).

Kruskal's tree theorem then states:

If ${\displaystyle X}$ is well-quasi-ordered, then the set of rooted trees with labels in ${\displaystyle X}$ is well-quasi-ordered under the inf-embeddable order defined above. That is to say, given any infinite sequence ${\displaystyle T_{1},T_{2},\ldots }$ of rooted trees labeled in ${\displaystyle X}$, there is some ${\displaystyle i<j}$ so that ${\displaystyle T_{i}\leq T_{j}}$.

For a countable label set ${\displaystyle 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 ${\displaystyle X}$ has size one), Friedman found that the result was unprovable in ATR₀,² thus giving the first example of a predicative result with a provably impredicative proof.³ This case of the theorem is still provable by Π¹
₁-CA₀, 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 Π¹
₁-CA₀.

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).⁷ Kruskal's tree theorem itself proves that ${\displaystyle \Gamma _{0}}$, the Feferman–Schütte ordinal, is well-founded; in particular, the inf-embeddable ordering on a countable label set contains a well-ordered chain of order type ${\displaystyle \Gamma _{0}}$.⁸

Suppose that ${\displaystyle P(n)}$ is the statement:

There is some ${\displaystyle m}$ such that if ${\displaystyle T_{1},\ldots ,T_{m}}$ is a finite sequence of unlabeled rooted trees where ${\displaystyle T_{i}}$ has ${\displaystyle i+n}$ vertices, then ${\displaystyle T_{i}\leq T_{j}}$ for some ${\displaystyle i<j}$.

All the statements ${\displaystyle P(n)}$ are true as a consequence of Kruskal's theorem and Kőnig's lemma. For each ${\displaystyle n}$, Peano arithmetic can prove that ${\displaystyle P(n)}$ is true, but Peano arithmetic cannot prove the statement "${\displaystyle P(n)}$ is true for all ${\displaystyle n}$".⁹ Moreover, the length of the shortest proof of ${\displaystyle P(n)}$ in Peano arithmetic grows phenomenally fast as a function of ${\displaystyle n}$, far faster than any primitive recursive function or the Ackermann function, for example. The least ${\displaystyle m}$ for which ${\displaystyle P(n)}$ holds similarly grows extremely quickly with ${\displaystyle n}$.

Friedman defined the following function, which is a weaker version of the TREE function below. For a positive integer ${\displaystyle n}$, take ${\displaystyle {\text{FFF}}(n)}$ to be the largest ${\displaystyle m}$ so that we have the following:

There is a sequence ${\displaystyle T_{1},\ldots ,T_{m}}$ of rooted trees, where each ${\displaystyle T_{i}}$ has ${\displaystyle i+n-1}$ vertices, such that ${\displaystyle T_{i}\leq T_{j}}$ does not hold for any ${\displaystyle i<j\leq m}$.

Friedman computes the first few terms of this sequence as ${\displaystyle {\text{FFF}}(1)=1}$, ${\displaystyle {\text{FFF}}(2)=2}$, and ${\displaystyle {\text{FFF}}(3)=5}$. He also estimates ${\displaystyle {\text{FFF}}(4)}$ to be less than 100, while ${\displaystyle {\text{FFF}}(5)}$ suddenly explodes to a very large value. Any proof that ${\displaystyle {\text{FFF}}(5)}$ exists in Peano arithmetic requires at least ${\displaystyle A(10)}$ symbols, where ${\displaystyle A(n)}$ is the unary version of the Ackermann function, but it can be proved to exist in ACA₀ with at most 10,000 symbols.¹⁰

By incorporating labels, Friedman defined a far faster-growing function.¹¹ For a positive integer ${\displaystyle n}$, take ${\displaystyle {\text{TREE}}(n)}$^[a] to be the largest ${\displaystyle m}$ so that we have the following:

There is a sequence ${\displaystyle T_{1},\ldots ,T_{m}}$ of rooted trees labelled from a set of ${\displaystyle n}$ labels, where each ${\displaystyle T_{i}}$ has at most ${\displaystyle i}$ vertices, such that ${\displaystyle T_{i}\leq T_{j}}$ does not hold for any ${\displaystyle i<j\leq m}$.

Kruskal's theorem asserts that ${\displaystyle {\text{TREE}}(n)}$ is finite for all ${\displaystyle n}$. The TREE function eventually dominates every provably recursive function of the system ACA₀ + Π¹
₂-BI.¹¹ It grows far faster than ${\displaystyle f_{\Gamma _{0}}(n)}$ on the fast-growing hierarchy; Friedman calculated the ordinal ${\displaystyle \alpha }$ where ${\displaystyle {\text{TREE}}(n)}$ and ${\displaystyle f_{\alpha }(n)}$ have similar growth rate (under affine transformation of input variables).¹²

The sequence begins ${\displaystyle {\text{TREE}}(1)=1}$, ${\displaystyle {\text{TREE}}(2)=3}$; before ${\displaystyle {\text{TREE}}(3)}$ suddenly explodes to a value so large that many other "large" combinatorial constants, such as Friedman's ${\displaystyle n(4)}$ and Graham's number,^[b] are extremely small by comparison. A lower bound for ${\displaystyle n(4)}$, and, hence, an extremely weak lower bound for ${\displaystyle {\text{TREE}}(3)}$, is ${\displaystyle A^{A(187196)}(1)}$,^[c] where ${\displaystyle A(x)}$ is the single-argument version of Ackermann's function, defined as ${\displaystyle A(x)=A(x,x)}$.¹¹¹³

Friedman showed that ${\displaystyle {\text{TREE}}(3)}$ is greater than the halting time of any Turing machine that can be proved to halt in ACA₀ + Π¹
₂-BI with at most ${\displaystyle 2\uparrow \uparrow 1000}$ symbols,^[d] where ${\displaystyle \uparrow \uparrow }$ denotes tetration.¹¹