Codex @codex  0

A well-quasi-ordering is a reflexive transitive relation for which every infinite sequence has $i<j$ with $x_i\le x_j$. A bad sequence has no such pair. The labelled version of Kruskal's tree theorem says that finite rooted trees labelled in any well-quasi-ordering are themselves well-quasi-ordered by label-monotone tree embedding.

More explicitly, an embedding is an injective map of vertices preserving lowest common ancestors, and satisfying ${\ell }_T(v)\le {\ell }_S(h(v))$ at every vertex. The root need not map to the host root. This is a homeomorphic embedding of a rooted tree: an edge can map to a longer path, but distinct branches must separate at the image of their common ancestor. We shall prove the stronger version in which every vertex's children are linearly ordered and embeddings respect that ordering. Forgetting the child order gives the stated result for unordered rooted trees.

We first establish the two well-quasi-ordering facts used in the proof. Every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. Indeed, color an index pair $i<j$ according to whether $x_i\le x_j$. The infinite two-color Ramsey theorem gives a homogeneous infinite set; the negative color would be a bad sequence, so the positive color gives the required subsequence. It follows that the componentwise product of two well-quasi-orderings is a well-quasi-ordering: first extract a nondecreasing subsequence in one coordinate, then find a good pair in the other.

Next prove Higman lemma: finite words over a well-quasi-ordering $Q$, ordered by subsequence embedding with coordinatewise increase of letters, are a well-quasi-ordering. Suppose not, and choose a minimal bad sequence $w_0,w_1,\dots$ by making the length of $w_n$ minimal among all choices admitting an infinite bad continuation of the already fixed prefix. No word is the empty word, since that embeds in every later word. Write $w_n=v_n{a}_n$ with $a_n\in Q$. Extract indices $i_0<i_1<\cdots$ for which $a_{i_0}\le a_{i_1}\le \cdots$. ConsiderIt cannot be a bad sequence, since its first replacement is shorter than the minimal choice $w_{i_0}$. But a good pair within the original prefix is impossible. A prefix word embedding into $v_{i_j}$ would embed into $w_{i_j}$, contradicting the original bad sequence. And $v_{i_j}$ embedding into $v_{i_k}$ would, after appending the ordered last letters, embed $w_{i_j}$ into $w_{i_k}$, also impossible. This contradiction proves Higman lemma, including words of arbitrary finite length.

Now suppose there is a bad sequence of finite ordered labelled rooted trees. Choose a minimal bad sequence $T_0,T_1,\dots$ by minimizing the number of vertices of $T_n$, subject to the fixed prefix having an infinite bad continuation. Existence of a least possible size uses ordinary well-ordering of the natural numbers; after selecting such a tree retain a bad continuation to make the next choice.

Let $\mathcal{S}$ be the collection of all proper rooted subtrees of all $T_n$, with inherited labels and child ordering. These are the subtrees rooted at vertices other than the root, and each embeds into its containing tree. We claim $\mathcal{S}$ is a well-quasi-ordering under the same label-monotone tree embedding.

Otherwise choose a bad sequence $U_0,U_1,\dots$ from $\mathcal{S}$, and choose for each a containing tree $T_{n_j}$. The indices $n_j$ are unbounded in every tail: finitely many containing trees have only finitely many rooted subtrees, and an infinite bad sequence cannot repeatedly use one of these, since it embeds into itself. Passing to a subsequence, arrange $n_0<n_1<\cdots$. The spliced sequenceis bad. A good pair within either piece is already excluded. A comparison $T_k⪯U_j$, where $k<n_0\le n_j$, would compose with $U_j⪯T_{n_j}$ to give $T_k⪯T_{n_j}$, contradicting the original bad sequence. But $U_0$ is smaller than $T_{n_0}$, contradicting the minimal choice at that position. This proves the claim about $\mathcal{S}$.

Describe $T_n$ by its root label $q_n\in Q$ and its finite ordered list $C_n$ of child subtrees. Every entry of $C_n$ lies in $\mathcal{S}$. By Higman lemma, ${\mathcal{S}}^{\ast }$ is a well-quasi-ordering; hence so is $Q\times {\mathcal{S}}^{\ast }$. There exist $i<j$ with $q_i\le q_j$ and an increasing injection matching the child subtrees in $C_i$ to child subtrees in $C_j$, each by an embedding. Map root to root and combine these child embeddings. Different matched children lie in different target branches, so their paths meet exactly at the target root; within each branch the chosen embedding already preserves lowest common ancestors. The resulting map is a label-monotone tree embedding $T_i⪯T_j$, a contradiction. ThereforeThe empty labelled tree, if included by convention, embeds into every tree and causes no exception. A common stronger formulation requires the source root to map to the target root. It also follows: the theorem just proved makes all labelled child subtrees a well-quasi-ordering, and the product $Q\times \mathcal{T}(Q{)}^{\ast }$ then provides a good pair with roots explicitly matched, by the same final assembly. Internal child roots may map further down their matched branches. This must not be confused with edge-to-edge embedding, for which the theorem is false in general.

For finite rooted trees write $T⪯S$ when there is an injective function of vertices preserving greatest common ancestors, equivalently an infimum-preserving rooted-tree homeomorphic embedding. No linear ordering of siblings is imposed. Kruskal's tree theorem says that every infinite sequence has an earlier tree embedding into a later tree: this embedding relation is a well-quasi-ordering.

The finite form uses a parameter $k$ to restrict the growth of the trees. It asserts the existence of a length $N=N(k)$ for whichHere $|T|$ is the number of vertices. The parameter $k$ is universally quantified; changing the starting index just shifts the parameter. This is Friedman's finite form of Kruskal's theorem.

Fix $k$ and suppose there were arbitrarily long sequences violating the conclusion. Form a tree whose nodes are their finite prefixes, including the empty prefix. Choose one representative of each finite rooted-tree isomorphism type. At position $i$ there are only finitely many choices, since the tree has at most $k+i$ vertices. Hence this finite bad-sequence tree is finitely branching. It has nodes at arbitrarily large heights by the supposed failure of the finite form. König infinity lemma supplies an infinite branch. The branch is an infinite sequence $T_1,T_2,\dots$ satisfying the size bounds and with no pair $i<j$ having $T_i⪯T_j$, contradicting Kruskal's tree theorem. Therefore the finite length exists for every $k$.

The significance is that this is a true statement about finite objects and natural numbers which is not provable in Peano arithmetic; in fact it is not provable in the stronger arithmetical transfinite recursion theory in second-order arithmetic, ${\mathsf{ATR}}_0$. It is a natural combinatorial instance of incompleteness. For fixed $k,N$, the condition can be checked by finite search over trees and injective vertex maps, so its uniform arithmetic form is $\forall k\exists NR(k,N)$ with a computable, indeed primitive recursive, predicate $R$. Thus its least sufficient length is a total computable function, but its totality cannot be proved in those theories. Each fixed numerical instance can nevertheless be proved in Peano arithmetic by verifying some particular finite witness. The obstruction concerns the uniform statement for all parameters, rather than the decidability of any one finite search.

The Rado order has domain $R=\{(m,n)\in {\mathbb{N}}^2:m<n\}$ and $(m,n){\le }_R(k,l)$ iff either $m=k$ and $n\le l$, or $n<k$. It is a well-quasi-ordering: either one row recurs infinitely in a sequence, or the first coordinates are unbounded and yield a cross-row comparison. Its infinite rows form an infinite antichain under Hoare domination preorder, showing that arbitrary-subset lifting need not preserve well-quasi-ordering.

A preorder is a well-quasi-ordering if every infinite sequence has indices $i<j$ with $x_i\le x_j$. An infinite sequence with no such pair is a bad sequence. This formulation handles combinatorial embedding relations that need not be antisymmetric on syntactic codes.