Combinatorics Planar graphs, embeddings, minors Theorem
Kruskal's tree theorem
Builds on Rooted tree
Statement
For finite rooted trees and , write for the nearest common ancestor of vertices of . Say that embeds in if some injective map from the vertices of to those of satisfies for all . Then the finite rooted trees are well-quasi-ordered by embedding. That is, for every infinite sequence of finite rooted trees, there are indices such that embeds in .
Remarks
The labelled form also holds. Let the vertices carry labels from a well-quasi-ordered set , and ask also that each label of is at most the label of its image. Then the trees are still well-quasi-ordered. Joseph Kruskal proved the theorem in 1960, and Crispin Nash-Williams gave a short proof by the minimal bad sequence argument. That argument takes a bad sequence whose trees are as small as possible at each step. It then applies Higman's lemma to the sets of subtrees at the roots to reach a contradiction. Harvey Friedman showed that a finite form of the theorem, although true, is not provable in the subsystem of second-order arithmetic. The Robertson–Seymour theorem on graph minors builds on its methods.
Going deeper
For a student
The theorem is a basic example of a well-quasi-order on structured objects, after Higman's lemma for finite words. It is used in term rewriting to prove that certain orderings, such as recursive path orderings, are well-founded. Its finite form grows so fast that it escapes strong formal systems, which makes it a standard example in proof theory.
Reading path
To understand this page from the ground up, read these 11 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Graph definition
- Walk definition
- Reachability definition
- Trail definition
- Connected graph definition
- Circuit definition
- Cycle definition
- Acyclic graph definition
- Tree definition
- Rooted tree definition
- Kruskal's tree theorem statement
Further reading
About this page
| Tag | XVHKCX4F5Y |
|---|---|
| URI | m2://XVHKCX4F5Y |
| Kind | statement, theorem |
| Writing | W0 stub |
| MSC | 05C05, 06A07 |
| Status | This copy of the site has no build data. Run m2 status XVHKCX4F5Y. |
| About | Rooted tree |
| Uses | Rooted tree |
| Same as | |
| Changed | 2 November 2026 |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- a source with a locator (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.
What links here
No page links to this page yet.