TREE(2)：Kruskal's tree theorem

Well-quasi-ordering of finite trees

In mathematics, Kruskals 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 TREE(3){\displaystyle {\text{TREE}}(3)}. A finitary application of the theorem gives the existence of the fast-growing TREE function.

The version given here is that proven by Nash-Williams; Kruskals fo...