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 Crispin Nash-Williams (1963).
It has since become a prominent example in reverse mathematics as a statement that cannot be proved in ATR0 (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
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[1] The version given here is that proven by Nash-Williams; Kruskal's formulation is somewhat stronger.
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 T1, T2 are rooted trees with vertices labeled in X, we say that T1 is inf-embeddable in T2 and write
if there is an injective map F from the vertices of T1 to the vertices of T2 such that: 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 T1, T2, … of rooted trees labeled in X, there is some
)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 ATR0,[2] thus giving the first example of a predicative result with a provably impredicative proof.
[3] This case of the theorem is still provable by Π11-CA0, but by adding a "gap condition"[4] to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system.
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).
are true as a consequence of Kruskal's theorem and Kőnig's lemma.
is true, but Peano arithmetic cannot prove the statement "
[8] Moreover, the length of the shortest proof of
in Peano arithmetic grows phenomenally fast as a function of n, far faster than any primitive recursive function or the Ackermann function, for example.
holds similarly grows extremely quickly with n. Define
, the weak tree function, as the largest m so that we have the following: It is known that
(where the argument specifies the number of labels; see below) is larger than
By incorporating labels, Friedman defined a far faster-growing function.
[a] to be the largest m so that we have the following: The TREE sequence begins
, and Graham's number,[b] are extremely small by comparison.
, and, hence, an extremely weak lower bound for
[c][10] Graham's number, for example, is much smaller than the lower bound
