Kruskal's tree theorem

Kruskal's tree theorem states that finite trees over a well-quasi-ordered label set are well-quasi-ordered by homeomorphic embedding. Thus every infinite sequence contains an earlier tree that embeds into a later one.

Connect

Well-quasi-order: A reflexive, transitive relation in which every infinite sequence contains an earlier element related to a later one. This is the sequence property that Kruskal's theorem establishes for finite trees.
Minimal bad sequence: A sequence with no increasing pair, chosen so each term is minimal among choices preserving that failure. The standard proof assumes a counterexample sequence and makes it minimal.
Joseph Kruskal: American mathematician and statistician known for work in graph theory, statistics, and the mathematics of trees. Kruskal published the tree theorem in 1960.
Goodstein's theorem: A theorem stating that every Goodstein sequence eventually reaches zero, despite its rapid initial growth. Like Kruskal's theorem, it is true but not provable in Peano arithmetic.
Homeomorphic embedding: An injective map between graph vertices that preserves adjacency through paths, allowing edges to subdivide. This is the comparison relation used to order trees in the theorem.
Tree decomposition: A representation of a graph by overlapping vertex sets arranged in a tree, subject to coverage and connectivity conditions. Proofs use tree structure to reduce comparisons to smaller pieces.
Andrew Vázsonyi: Hungarian-American mathematician whose work included an early formulation of the finite-tree ordering result. Vázsonyi independently posed the theorem's central tree-ordering problem.
Friedman's finite forms of Kruskal's theorem: Finite combinatorial statements derived from Kruskal-style tree principles that can exceed Peano arithmetic in proof strength. These sharpen the theorem's role in measuring the limits of familiar arithmetic.
Rooted tree: A tree with one distinguished vertex called its root, inducing parent and descendant relations. Rooted trees provide the standard setting for defining tree embeddings.
Higman's lemma: The theorem that finite words over a well-quasi-ordered alphabet are well-quasi-ordered by subsequence embedding. Its sequence argument is a key ingredient in the labeled-tree proof.