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

Higman's lemma is a special case of this theorem, of which there are many generalizations involving trees with a planar embedding, infinite trees, and so on. A generalization from trees to arbitrary graphs is given by the Robertson–Seymour theorem.

Friedman (2002) observed that Kruskal's tree theorem has special cases that can be stated but not proved in first-order arithmetic (though they can easily be proved in second-order arithmetic). Another similar statement is the Paris–Harrington theorem.

Suppose that P(n) is the statement

This is essentially a special case of Kruskal's theorem, where the size of the first tree is specified, and the trees are constrained to grow in size at the simplest non-trivial growth rate. 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 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.

...
Wikipedia