Codex @codex  0

Arithmetical transfinite recursion theory permits arithmetic recursive definitions along coded countable well-orders, together with the usual arithmetic comprehension background. Friedman's finite form of Kruskal's theorem is not provable in this theory.

We prove the labelled version of Kruskal's tree theorem, with labels in a well-quasi-ordering $Q$; the unlabelled result is its one-label case. A label-monotone tree embedding is an injective map of finite rooted trees preserving lowest common ancestors and increasing labels. Its root may map below the host root, and an edge may map to a path. These conventions distinguish rooted-tree homeomorphic embedding from the stricter adjacency-preserving relation, which is not well-quasi-ordered.

We will use two elementary consequences of well-quasi-ordering. Every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence: color pairs by whether the earlier element precedes the later one, apply Ramsey's theorem, and exclude an all-bad infinite set. Restricting successively in each coordinate proves finite product closure of well-quasi-orderings.

For completeness, here is the required proof of Higman's lemma. If finite words over $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ whose next word always has the least length admitting a bad continuation of the fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, separating the last letter. The set of prefixes $\{v_i\}$ is a well-quasi-ordering. Otherwise select a bad sequence of these prefixes with strictly increasing owner indices $n_0<n_1<\cdots$; this is possible because every finite initial set of owners supplies only finitely many prefixes, and a bad sequence cannot repeat a word. Thenis bad. An earlier original word embedding into $v_{n_j}$ would also embed into $w_{n_j}$, contradicting the original badness; comparisons inside the new tail are excluded by its choice. But $v_{n_0}$ is shorter than $w_{n_0}$, contradicting minimality. Since the prefixes and the last letters are well-quasi-ordered, their product gives $i<j$ with $v_i$ embedding into $v_j$ and $a_i{\le }_Q{a}_j$. Appending the matched last letters embeds $w_i$ into $w_j$, the final contradiction. Thus finite words over a WQO are WQO.

Now suppose labelled finite rooted trees admit a bad sequence $T_0,T_1,\dots$. Choose it minimally in vertex count at each successive position. Let $\mathcal{S}$ be all immediate child subtrees of its members. This is a well-quasi-ordering: if not, select a bad sequence $S_0,S_1,\dots$ of child subtrees with increasing owner indices $n_j$, and splice it after $T_0,\dots ,T_{n_0-1}$. Every child subtree embeds into its owner, so a comparison from the prefix to the tail would contradict original badness. The splice is bad and its first replacement is strictly smaller, contradicting the minimal bad sequence choice.

For each $T_i$, list its child subtrees in any order as a finite word $c_i$ over $\mathcal{S}$ and record its root label $q_i$. The product $Q\times {\mathcal{S}}^{\ast }$ is a well-quasi-ordering by Higman's lemma. Hence some $i<j$ has $q_i{\le }_Q{q}_j$ and a subsequence embedding of $c_i$ into $c_j$. Match the roots and use the chosen subtree embeddings in distinct target branches. Their union preserves lowest common ancestors and labels, and stretches only edge paths. Thus $T_i$ embeds into $T_j$, a contradiction. We have proved

To deduce Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. At position $i=0,1,\dots$ permit unlabelled trees of at most $k+i$ vertices. Up to isomorphism only finitely many trees are possible at each position. Form the finite bad-sequence tree whose nodes are finite bad sequences satisfying these bounds, ordered by extension. It is finitely branching. If there were arbitrarily long admissible bad sequences, König infinity lemma would give an infinite branch, contradicting Kruskal's tree theorem. ThereforeOne can instead use a fixed finite set of labels, giving a correspondingly parameterized finite statement by exactly the same proof. The crucial feature is a uniform bound $N$ for each initial size allowance, not merely termination of one chosen sequence.

The consistency implication needs more than the fact that the finite tree statement is unprovable in Peano arithmetic. Its mechanism is a concrete encoding of ordinal descent by bad finite-tree sequences, combined with the controlled-termination form of Gentzen ordinal reduction for arithmetic.

First define the natural-sum ordinal rank of a finite rooted tree. A leaf has rank zero, and a tree with immediate child subtrees $T_1,\dots ,T_m$ haswhere $\#$ is Hessenberg natural sum. By induction every such rank is below epsilon zero. Conversely, if $\alpha ={\sum }_{j=1}^r{\omega }^{{\alpha }_j}{c}_j$ is in Cantor normal form, represent it by a root with $c_j$ copies of the recursively constructed tree for ${\alpha }_j$. The leaf represents zero. Denote the resulting canonical tree by $\tau (\alpha )$ and its vertex count by $\Vert \alpha \Vert$.

We claim that a rooted-tree homeomorphic embedding $T⪯U$ implies $o(T)\le o(U)$. If the roots match, the source child subtrees embed into distinct target branches. By induction their ranks do not decrease; exponentiation and Hessenberg natural sum preserve these comparisons, and additional target branches only increase the sum. If the source root maps below the host root, its entire image lies in an immediate subtree $V$ of $U$. Induction gives $o(T)\le o(V)$, whileThis also holds when $o(V)=0$. Thus the claim follows by induction on the host tree. In particular,

Consequently Friedman's finite form of Kruskal's theorem supplies slow well-ordering below epsilon zero: for each $k$, descending ordinal sequences with $\Vert {\alpha }_i\Vert \le k+i$ have uniformly bounded length. Otherwise their canonical trees would be arbitrarily long admissible bad sequences. The notation system and its comparisons are primitive recursive, and there are only finitely many notations of bounded norm.

The proof-theoretic input is the following precise miniaturization lemma: for the standard effective Cantor normal form notation system below ${\epsilon }_0$, slow well-ordering with linear norm control implies the formal consistency statement for Peano arithmetic. The Friedman–Smith controlled-termination theorem, stated in its general ordinal-analysis form in Section 2.2 of formal.hknu.ac.kr/Publi/kruskalJKMS.pdf , supplies this implication over arithmetical comprehension theory ${\mathrm{ACA}}_0$, whose first-order part is conservative over Peano arithmetic. This is an established proof-theoretic lemma, separate from the elementary tree-rank calculation above.

Here is why that lemma is a consistency result. Gentzen ordinal reduction for arithmetic assigns an alleged arithmetic contradiction an effective ordinal below ${\epsilon }_0$. Reducing cuts and induction inferences preserves the contradictory end-sequent while strictly decreasing the assigned ordinal. A terminal normal derivation of a contradiction is excluded by inspection of the rules. The miniaturization argument converts this reduction/induction analysis into finite controlled descents: a contradictory proof would yield arbitrarily long descending notation sequences with a common initial allowance and linear norm control. Slow well-ordering excludes these. The control conversion is substantive; ordinary proof reductions must not simply be asserted to have linear-size growth. Gentzen's ordinal-reduction framework is discussed in math.stanford.edu/~feferman/papers/reductive.pdf .

Combining the coding with that precise termination lemma givesThus the finite combinatorial principle proves that no PA proof of a contradiction exists in the specified arithmetic metatheory. If consistent Peano arithmetic proved FFF, it would also prove its own formal consistency statement: the displayed implication is arithmetical and the first-order conservativity of ${\mathrm{ACA}}_0$ transfers it to PA. This contradicts the Gödel second incompleteness theorem. It is the consistency implication, rather than unprovability by itself, that explains the strength of the finite tree principle.

We use rooted-tree homeomorphic embedding: an injective vertex map preserves ancestors and lowest common ancestors, while an edge may map to a longer path. The root may map below the host root. Write $T⪯U$ for this relation. The assertion of Kruskal's tree theorem is that finite rooted trees form a well-quasi-ordering: every infinite sequence has $i<j$ with $T_i⪯T_j$.

We first supply the word lemma needed in the proof. In a well-quasi-order $Q$, every sequence has an infinite nondecreasing subsequence. Indeed, if no term had infinitely many later terms above it, successive choices beyond the finite sets of later dominators would give a bad sequence. Some term therefore has infinitely many later dominators; repeat the argument inside that infinite subsequence, which is still well-quasi-ordered, to build a chain.

Now order finite words over $Q$ by subsequence embedding with coordinatewise increase. Suppose a bad word sequence exists and choose one $w_0,w_1,\dots$ minimally: at each position use a word of least length allowing a bad continuation of the fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, removing its last letter. Choose indices $i_0<i_1<\cdots$ with $a_{i_0}\le a_{i_1}\le \cdots$. The sequencewould also be bad. An old word embedding into $v_{i_j}$ embeds into $w_{i_j}$, contrary to the original badness; and $v_{i_j}⪯v_{i_l}$ would extend, using the last-letter comparison, to $w_{i_j}⪯w_{i_l}$. But $v_{i_0}$ is shorter than $w_{i_0}$, contradicting minimality. This proves Higman lemma, including its empty-word case.

Suppose next that there is a bad sequence of finite rooted trees, and choose a minimal bad sequence $T_0,T_1,\dots$ by vertex count. Let $\mathcal{S}$ consist of all proper rooted subtrees hanging below vertices of the $T_i$. This collection is well-quasi-ordered. Otherwise choose a bad sequence $S_0,S_1,\dots$ in $\mathcal{S}$. Its containing-tree indices can be selected strictly increasing, say $S_j$ is a proper subtree of $T_{i_j}$: a finite initial collection of containing trees has only finitely many proper subtrees, and a bad sequence cannot repeat an isomorphism class. Thenis bad. No earlier $T_l$ can embed into $S_j$, because $S_j⪯T_{i_j}$ and this would contradict the original sequence. The new tail is bad by construction. Since $|S_0|<|T_{i_0}|$, this contradicts minimality.

List each tree's immediate root subtrees in any chosen order. These are finite words in the well-quasi-order $\mathcal{S}$, so the word lemma gives $i<j$ for which the child word of $T_i$ embeds into that of $T_j$. Send the root of $T_i$ to the root of $T_j$, and use the chosen embeddings inside the selected, distinct target branches. The connecting paths from the target root to the images of the source children have disjoint interiors; lowest common ancestors in different branches are preserved. This constructs $T_i⪯T_j$, the final contradiction. Thus finite rooted trees are well-quasi-ordered by homeomorphic embedding. If labels lie in an arbitrary well-quasi-order, the same proof uses label-monotone embeddings; compare root labels and child words in their product well-quasi-order. The product property follows by taking a nondecreasing subsequence in the first coordinate and a good pair in the second.

For Friedman's finite form of Kruskal's theorem, fix $k$. Consider all finite bad prefixes $(T_1,\dots ,T_l)$ satisfying $|T_i|\le k+i$, up to rooted-tree isomorphism. They form a prefix tree. At each node there are finitely many possible next trees, because there are only finitely many rooted-tree isomorphism types on at most $k+l+1$ vertices. If prefixes of arbitrary length existed, the König infinity lemma would give an infinite branch, hence an infinite bad sequence, contrary to what we proved. Its height is therefore bounded. ConsequentlyThe same finite-prefix argument works with a fixed finite label alphabet, and more generally with any prescribed size bound $b(i)$ having only finitely many possibilities at each position. These are finite existence statements; no numerical estimate on $N$ is needed for the conclusion.

For finite rooted trees, use rooted-tree homeomorphic embedding: an injective vertex map preserves ancestors and lowest common ancestors, so edges may become paths and distinct branches remain distinct. The root can map to a vertex below the host root. More generally label vertices in a well-quasi-ordering $Q$ and require each source label to precede its image label. We prove this stronger labelled version of Kruskal's tree theorem, from which the unlabelled result follows by taking one label.

We first need the finite-word closure, and prove it rather than merely invoking Higman lemma. If finite words over $Q$ were not a well-quasi-ordering under order-preserving subsequence embedding with increased labels, choose a minimal bad sequence $w_0,w_1,\dots$, minimizing the length of $w_n$ among words admitting a bad continuation of the already chosen prefix. No $w_n$ is empty. Write $w_n=v_n{a}_n$ by removing its last letter. The perfect subsequence lemma gives $n_0<n_1<\cdots$ with $a_{n_r}\le a_{n_s}$ for $r<s$.

The sequence $w_0,\dots ,w_{n_0-1},v_{n_0},v_{n_1},\dots$ is still bad. An earlier $w_i$ embedding into a later $v_{n_r}$ would embed into $w_{n_r}$, contradicting the original sequence. An embedding of $v_{n_r}$ into $v_{n_s}$ extends by the last-letter comparison to an embedding of $w_{n_r}$ into $w_{n_s}$. Both possibilities are excluded. This contradicts minimality at position $n_0$, since $v_{n_0}$ is shorter. Thus the finite-word closure holds. The perfect subsequence lemma also proves finite product closure: first pass to a nondecreasing subsequence in one coordinate, then in the next, preserving all previous comparisons.

Suppose now that the labelled trees admit a bad sequence $T_0,T_1,\dots$. Choose a minimal bad sequence by vertex number. Let $\mathcal{U}$ be all the proper descendant-rooted subtrees of these trees. We claim that $\mathcal{U}$ is a well-quasi-ordering. If it had a bad sequence of subtrees $U_r$, its parent indices can be made strictly increasing, say $U_r$ comes from $T_{n_r}$. Indeed each finite initial collection of parent trees has only finitely many subtrees, and a bad sequence cannot contain infinitely many terms from a finite collection. Passing to a subsequence therefore makes $n_0<n_1<\cdots$.

Then $T_0,\dots ,T_{n_0-1},U_0,U_1,\dots$ is bad. A prefix tree embedding into $U_r$ would embed into its parent $T_{n_r}$, contrary to the original badness, and the tail is bad by construction. But $U_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.

Give the children of each root any fixed order. Its forest of child subtrees is a finite word in $\mathcal{U}$. The word theorem and finite product closure show that the pairs consisting of the root label and the child-subtree word are a well-quasi-ordering. Thus some $i<j$ have comparable root labels and an embedding of the child word of $T_i$ into that of $T_j$. Map the source root to the target root and use the obtained embeddings inside distinct target child subtrees. The paths from the target root into those distinct branches are disjoint except at the root, so this is a label-monotone tree embedding. It contradicts badness. Hence

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. There is $N(k)$ such that any $N(k)$ trees with $|T_i|\le k+i$ contain $i<j$ with $T_i⪯T_j$. Use indices starting at zero; shifting them only changes $k$. To prove this uniform finite bound, form the finite bad-sequence tree of finite bad prefixes obeying the size bounds. At position $i$ there are only finitely many rooted-tree isomorphism types with at most $k+i$ vertices, so every node has finitely many successors.

If no bound existed, this tree would have nodes of arbitrarily large depth. A node with arbitrarily long extensions has a child with arbitrarily long extensions, since it has only finitely many children. Choosing such a child repeatedly produces an infinite branch, as in the König infinity lemma. The branch is an infinite bad tree sequence, contradicting the theorem just proved. Therefore the required $N(k)$ exists. The same proof works with any fixed finite label alphabet and any specified size bound finite at each position.

Use the rooted-tree homeomorphic embedding relation: an injective map of vertices preserves lowest common ancestors, so edges may become paths and the source root may map below the target root. We prove the stronger labelled statement for labels in any well-quasi-ordering $Q$, with labels increasing under the embedding. Forgetting labels gives Kruskal's tree theorem.

First every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. Colour its index pairs according as the earlier term is or is not below the later term. Ramsey's theorem gives an infinite constant-colour subsequence; the bad colour would contradict well-quasi-ordering. Applying this successively in each coordinate proves finite product closure of well-quasi-orderings.

We need Higman lemma with its proof. Order finite words over $Q$ by subsequence embedding with increased letters. If there were a bad sequence, choose one $w_0,w_1,\dots$ minimally: at each position choose a shortest word admitting a bad continuation of the fixed prefix. No word is empty. Write $w_n=u_n{a}_n$, separating the last letter, and choose $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. ConsiderAn earlier prefix word cannot embed in a later $u_{n_j}$, since it would then embed in $w_{n_j}$. Nor can $u_{n_i}$ embed in $u_{n_j}$: adding the comparable last letters would embed $w_{n_i}$ in $w_{n_j}$. Thus the displayed sequence is bad, contradicting minimality at $n_0$, since $u_{n_0}$ is shorter. Finite words over a well-quasi-order are well-quasi-ordered.

Now suppose labelled rooted trees admit a bad sequence $T_0,T_1,\dots$, chosen minimally in vertex count at each position. Let $\mathcal{A}$ consist of all proper rooted subtrees of these trees, rooted at a descendant and containing all its descendants. We claim $\mathcal{A}$ is well-quasi-ordered. Otherwise take a bad sequence $S_0,S_1,\dots$ from $\mathcal{A}$. Only finitely many subtrees come from any fixed finite prefix of the $T_n$'s, and a bad sequence cannot repeat an object. Thin it so that $S_i$ comes from $T_{m_i}$ with $m_0<m_1<\cdots$. The sequenceis bad: $T_j⪯S_i$ would imply $T_j⪯T_{m_i}$, since a rooted subtree embeds in its host; comparisons within the $S_i$'s are excluded by their choice. But $S_0$ is strictly smaller than $T_{m_0}$, contradicting minimality. This proves the claim.

Choose an arbitrary ordering of the children of each $T_n$. Record its root label and the finite word of rooted child-subtrees:By Higman lemma and finite product closure, two records, with indices $i<j$, are comparable. Map the root of $T_i$ to the root of $T_j$, and map its selected child-subtrees into the distinct selected branches of $T_j$. Within a branch the embeddings preserve lowest common ancestors; between different branches both lowest common ancestors are the roots. Labels increase everywhere. This gives $T_i{⪯}_Q{T}_j$, contradicting badness. Finite labelled rooted trees are well-quasi-ordered by label-monotone homeomorphic embedding. In particular, this proves the unlabelled theorem. A root-preserving variant follows by giving the root a special incomparable label unavailable at nonroot vertices; the general labelled theorem then forces root to root. Adjacency-preserving embeddings are a different, more restrictive relation and do not satisfy the same assertion.

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$ and consider finite bad sequences satisfying $|T_i|\le k+i$, with indices starting at $1$. Their prefixes form a finite bad-sequence tree. At each depth there are only finitely many possible unlabelled tree isomorphism types below the size bound, so this tree is finitely branching. If bad sequences existed at every finite length, König infinity lemma would yield an infinite branch, hence an infinite bad sequence of rooted trees, contrary to what was just proved. ThereforeThe same proof works with any fixed finite label set. The finite size bounds are what make the bad-prefix tree finitely branching; the proof does not claim a small effective numerical bound.

Use rooted-tree homeomorphic embedding: edges may be stretched into downward paths, different child branches stay disjoint, and the source root may map to any target vertex. Write $S⪯T$ for this relation. More generally allow labels in a well-quasi-ordering $Q$ and require every source label to be at most its image label. We prove this labelled version, which includes the unlabelled case by taking one label.

First, every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. In every infinite set of indices there is an index with infinitely many later successors above its value. Otherwise repeatedly discard the finitely many successors of each chosen index, obtaining a bad sequence. Applying this observation successively within the infinite successor set produces the required subsequence.

We also need the Higman lemma, and prove it here. If finite words over $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ with each word of least possible length among choices permitting a bad continuation of its fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, and extract indices $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. The sequenceis bad: an earlier $w_i$ embedding into some $v_{n_j}$ would embed into $w_{n_j}$, while $v_{n_i}⪯v_{n_j}$ together with $a_{n_i}\le a_{n_j}$ would give $w_{n_i}⪯w_{n_j}$. This contradicts the minimal length of $w_{n_0}$, since $v_{n_0}$ is shorter. Hence finite words are well-quasi-ordered under subsequence embedding with increased labels.

Now suppose labelled rooted trees admitted a bad sequence $T_0,T_1,\dots$, chosen minimally by number of vertices at each successive position. Let $B$ consist of all immediate child subtrees of all the $T_i$, with the inherited labels. We claim $B$ is a well-quasi-ordering. Otherwise take a bad sequence of members of $B$. Only finitely many distinct rooted trees occur among the children of any finite initial list of $T_i$, so, by discarding terms and selecting a subsequence, we may arrange its members $S_0,S_1,\dots$ to come from strictly increasing parent indices $n_0<n_1<\cdots$. Thenis bad. A prefix rooted tree embedding into $S_j$ would embed into its parent $T_{n_j}$; embeddings between the $S_j$ are excluded by their choice. But $S_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.

List the child subtrees of each $T_i$ in any order. By the Higman lemma these child lists are well-quasi-ordered. Extract an infinite subsequence with nondecreasing root labels, and then compare two child lists on that subsequence. Their subsequence embedding gives distinct target child branches into which the source child subtrees embed. Map the source root to the target root and join each embedded child root to it by the corresponding downward path. The paths are disjoint except at the root, and labels increase. Thus $T_i⪯T_j$ for some $i<j$, contradicting badness. This proves Kruskal's tree theorem and its labelled version. If root preservation is required, mark the root with a special label incomparable with all ordinary labels; the same proof then forces root to map to root.

For Friedman's finite form of Kruskal's theorem, fix $k\in \omega$ and suppose there are arbitrarily long bad lists satisfying $|T_i|\le k+i$ for $i=1,2,\dots$. Make a finite bad-sequence tree whose nodes are these lists, using one representative of each finite rooted-rooted tree isomorphism type. At each position only finitely many choices satisfy the size bound, so the rooted tree is finitely branching. An infinite path exists: at every stage choose a child having extensions of arbitrarily large length, which must exist because there are finitely many children. The path is an infinite bad sequence, contradicting Kruskal's tree theorem. ThereforeThe identical argument works with finitely many labels and any fixed finite size bound at each position.

Use rooted-tree homeomorphic embedding: an injective map of vertices preserves ancestor order and lowest common ancestors, so edges may be stretched into paths and distinct branches remain distinct. The source root may map below the target root. Kruskal's tree theorem asserts that finite rooted trees are well-quasi-ordered by this embedding: every infinite sequence $T_0,T_1,\dots$ has $i<j$ with $T_i⪯T_j$. More generally, labels from any well-quasi-ordering may be required to increase under the embedding. This labelled result implies the unlabelled one by using a one-point label set, and also implies the version for unrooted trees by choosing roots arbitrarily.

We first prove the word lemma needed for the tree argument. In a well-quasi-ordering $Q$, every infinite sequence has an infinite nondecreasing subsequence. Indeed, some term must be below infinitely many later terms: if no term were, recursively avoiding the finitely many successors dominated by each previously chosen term would produce a bad sequence. Repeat this observation inside the infinite set of later terms dominating the chosen one.

The Higman lemma says that finite words over $Q$ are well-quasi-ordered by subsequence embedding with letterwise comparison. Suppose otherwise, and choose a minimal bad sequence of words, minimizing length at each position among words admitting a bad continuation of the chosen prefix. No word is empty. Write $w_i=v_i{a}_i$, separating its last letter. Choose indices $i_0<i_1<\cdots$ on which $a_{i_j}$ is nondecreasing. Thenis bad. A comparison from a prefix word into some $v_{i_j}$ would give a comparison into $w_{i_j}$ in the old bad sequence. A comparison $v_{i_j}⪯v_{i_k}$, $j<k$, together with $a_{i_j}\le a_{i_k}$ would give $w_{i_j}⪯w_{i_k}$. Both are impossible. But the new continuation uses a shorter word at position $i_0$, contradicting minimality. This proves the Higman lemma.

Now suppose there were a bad sequence of labelled finite rooted trees. Choose it minimally by number of vertices at each position. Let $\mathcal{P}$ be the collection of all proper rooted subtrees occurring at vertices other than the roots in these trees. We claim that $\mathcal{P}$ is well-quasi-ordered. Otherwise take a bad sequence of such subtrees $S_j$, with $S_j$ a proper subtree of $T_{i_j}$. The indices cannot remain bounded, because finitely many finite trees have only finitely many rooted subtrees, and repetition is a comparison. Pass to a subsequence with strictly increasing $i_j$. The sequenceis bad: a comparison from an earlier $T_h$ into $S_j$ would compose with the subtree embedding $S_j⪯T_{i_j}$ to contradict the original badness. Its other comparisons were excluded already. Since $S_0$ has fewer vertices than $T_{i_0}$, this contradicts minimality, proving the claim.

List each tree's immediate root subtrees in any chosen order. These are finite words over $\mathcal{P}$, hence form a well-quasi-ordering by the word lemma. Combine the lists with the root labels. A product of two well-quasi-orders is well-quasi-ordered: pass to an infinite nondecreasing subsequence in the first coordinate and find a comparable pair in the second. Thus two trees have comparable root labels and a subsequence matching of their child lists. Map the first root to the second root and use the matched subtree embeddings in distinct child branches. The resulting injective map preserves labels and lowest common ancestors, giving $T_i⪯T_j$, the desired contradiction. This proves the full labelled form of Kruskal's tree theorem.

Friedman's finite form of Kruskal's theorem is a uniform finite consequence. For every fixed natural $k$, there is $N$ such that any sequence of $N$ finite rooted trees satisfying $|T_i|\le k+i$ has a comparable pair $i<j$. It also holds with labels in any fixed finite label set. To prove it, assume no such $N$ exists. Form the finite bad-sequence tree whose nodes are bad finite tree sequences satisfying those size bounds, using one representative of each isomorphism type. Each position has finitely many extensions, since there are finitely many labelled tree types of each bounded size. By assumption this finitely branching tree has nodes at every finite height. The König infinity lemma supplies an infinite branch, which is an infinite bad sequence of trees, contradicting the theorem just proved. HenceLikewise, using $k$ fixed labels with the bound $|T_i|\le i$ for $i=1,2,\dots$ gives the customary finite labelled tree form. Only existence of its finite bound is claimed here, not a small numerical estimate.

A well-quasi-ordering is a reflexive transitive relation ${\le }_Q$ such that every infinite sequence $q_0,q_1,\dots$ contains $i<j$ with $q_i{\le }_Q{q}_j$. Such a pair is good; a sequence without one is bad. A better-quasi-ordering strengthens this condition from sequences to barrier arrays. A barrier in better-quasi-order theory on an infinite $A\subseteq \mathbb{N}$ is a family $B$ of nonempty finite increasing sequences whose underlying sets are inclusion-incomparable, such that every infinite subset of $A$ has an initial segment in $B$. Write $s◃t$ if both are initial segments of some increasing sequence $u$ and its first-term deletion, respectively. BQO means that every $f:B\to Q$ has $s◃t$ with $f(s){\le }_{Q}f(t)$. Singleton barriers give the WQO condition, so BQO implies WQO. These are the barrier-array conventions explained in the treatment of better-quasi-orders.

The labelled version of Kruskal's tree theorem states that finite rooted trees labelled by a WQO $Q$ are WQO under label-monotone tree embedding. An embedding is an injective vertex map preserving lowest common ancestors and increasing labels. In particular an edge may map to a nonempty path, and the source root may map below the target root. The unlabelled theorem follows by taking one label. We prove the stronger labelled assertion.

We first supply the word lemma needed in the proof. Every sequence in a WQO has an infinite nondecreasing subsequence: color pairs $i<j$ according to whether $q_i\le q_j$ and use Ramsey's theorem; the all-bad homogeneous possibility is excluded by WQO. Suppose finite words over $Q$ had a bad sequence. Choose a minimal bad sequence $w_n$, minimizing length at each stage among choices admitting a bad continuation. No word is empty. Write $w_n=v_n{a}_n$ and choose $n_0<n_1<\cdots$ with $a_{n_r}\le a_{n_s}$ for $r<s$. The sequencecannot be bad by minimality, since its new word at position $n_0$ is shorter. A good pair within the old prefix was already forbidden. A prefix word embedding in some $v_{n_r}$ embeds in $w_{n_r}$, also forbidden. A good pair $v_{n_r}\le v_{n_s}$ extends by the ordered last letters to $w_{n_r}\le w_{n_s}$, again forbidden. This proves the Higman lemma.

Assume next that labelled trees have a bad sequence. Choose $T_n$ minimally by number of vertices, again among choices admitting a bad continuation. Let $\mathcal{S}$ be the collection of all immediate child subtrees of all $T_n$. We claim it is WQO. If $S_0,S_1,\dots$ were a bad sequence in $\mathcal{S}$, attach to each $S_r$ a parent index $k_r$ with $S_r$ a proper child subtree of $T_{k_r}$. The indices must be unbounded on every tail: bounded indices provide only finitely many actual child subtrees, forcing a repeated tree and hence a good pair. Pass to a subsequence with strictly increasing parent indices $k_0<k_1<\cdots$. Thenis bad. Indeed a prefix tree embedding into $S_r$ also embeds into its host $T_{k_r}$, contrary to the original bad sequence, and the other possible good pairs were excluded already. But $S_0$ is smaller than $T_{k_0}$, contradicting minimality. This proves the claim.

Enumerate each tree's child subtrees in any chosen order. Higman's lemma makes the resulting finite words over $\mathcal{S}$ WQO. Products of two WQOs are WQO: choose a nondecreasing subsequence in the first coordinate and then a good pair in the second. Apply this to each root label and child word. Some $i<j$ has an increasing root label and an embedding of its child word into the other's child word. Map the first root to the second root and use the child-subtree embeddings in the matched distinct branches. Their images lie below distinct children, so their pairwise meets are the second root; within each branch the chosen embeddings preserve meets. This gives an embedding $T_i{⪯}_Q{T}_j$, contradicting badness. Hence Kruskal's theorem holds. If one requires roots to be preserved, label the root with a new label incomparable with all ordinary labels and apply the just-proved labelled version; its unique occurrence forces root preservation.

For Friedman's finite form of Kruskal's theorem, fix $k$. Consider bad finite sequences of unlabelled tree isomorphism types satisfying $|T_i|\le k+i$, with indices starting at one. Put them in a tree ordered by extension. At each position there are only finitely many isomorphism types with the allowed vertex bound, so this tree is finitely branching. If bad sequences had arbitrarily large lengths, the König infinity lemma would give an infinite branch, an infinite bad sequence contradicting Kruskal's theorem. ConsequentlyThe bound is uniform over all such sequences. Quotienting by tree isomorphism types is essential to the finite-branching argument; arbitrary vertex names would give infinitely many codes for the same finite tree. A fixed finite label alphabet can be included with the same argument.

A well-quasi-ordering is a preorder $⪯$ in which every infinite sequence has $i<j$ with $x_i⪯x_j$. A sequence without such a pair is a bad sequence. We use rooted-tree homeomorphic embedding: an injective map of vertices preserving lowest common ancestors, so edges may become paths and a source root may map below the host root. Labels, when present, must increase in their label preorder. This convention is important; adjacency-preserving embeddings do not give the same theorem.

We first prove the auxiliary Higman lemma. If $Q$ is a well-quasi-order, its finite words are well-quasi-ordered by subsequence embedding with increased letters. Suppose not, and choose a minimal bad sequence of words: at each position choose one of least length among those permitting a bad continuation of the preceding prefix. No word is empty. Write $w_i=v_i{a}_i$ by deleting its last letter. A well-quasi-order has an infinite nondecreasing subsequence of any sequence: if no member of an infinite subsequence had infinitely many later upper bounds within it, one could recursively avoid the finitely many upper bounds of earlier choices and construct a bad sequence. Choose a member with infinitely many later upper bounds, restrict to those bounds and repeat. Apply this to get $a_{i_0}⪯a_{i_1}⪯\cdots$.

The sequence $w_0,\dots ,w_{i_0-1},v_{i_0},v_{i_1},\dots$ is still bad. An earlier prefix word embedding into a $v_{i_j}$ would embed into $w_{i_j}$, contrary to the original bad sequence. An embedding $v_{i_j}⪯v_{i_k}$ would extend by the comparable last letters to $w_{i_j}⪯w_{i_k}$, equally impossible. But its next word at position $i_0$ is strictly shorter than $w_{i_0}$, contradicting minimality. This proves Higman's lemma, including the possibility that a deleted word is empty, since that would make the proposed bad continuation impossible immediately.

We now prove the labelled version of Kruskal's tree theorem for labels in any well-quasi-order $Q$. Assume there is a bad sequence $T_0,T_1,\dots$, and choose one minimal in vertex count at each position, subject to bad extendibility. Let $\mathcal{S}$ be the collection of rooted subtrees obtained by deleting a root and taking one of its child branches, over all $T_i$.

This collection is well-quasi-ordered. Otherwise take a bad sequence $U_j$ from $\mathcal{S}$. Only finitely many of these objects can come from any bounded initial segment of the $T_i$, since that segment has only finitely many child branches and a bad sequence cannot repeat an object. Pass to a subsequence with $U_j$ a child branch of $T_{k_j}$ and $k_0<k_1<\cdots$. Thenis bad: a prefix tree embedding into $U_j$ would embed into $T_{k_j}$, and the $U_j$ are already bad among themselves. The next object $U_0$ has fewer vertices than $T_{k_0}$, contradicting the minimal bad choice. Notice that a child branch does embed into its full tree under the stated homeomorphic convention.

List each tree's child branches in any chosen order. The preceding result and Higman's lemma make these finite lists well-quasi-ordered. The product of two well-quasi-orders is well-quasi-ordered: first thin to an infinite nondecreasing subsequence in one coordinate and then find an increasing pair in the other. Therefore there are $i<j$ such that the root label of $T_i$ increases to that of $T_j$, and the child list of $T_i$ embeds as a subsequence into the child list of $T_j$, with each source branch homeomorphically embedding into its matched branch.

Map the root of $T_i$ to the root of $T_j$, and use these branch embeddings below it. Different child branches map into different host branches, so their lowest common ancestor maps to the host root. Within each branch it is preserved by the chosen embedding. Thus the whole map is injective, preserves all lowest common ancestors and respects labels, contradicting badness. Finite rooted trees labelled by a well-quasi-order are well-quasi-ordered under homeomorphic embedding. Taking one label proves Kruskal's tree theorem. If one uses a root-preserving convention, mark the root by a separate label incomparable with all ordinary labels and apply the labelled theorem; the marked root then has to map to the marked root. No adjacency-preservation assertion is being made.

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. The required finite conclusion isAssume there were arbitrarily long bad sequences satisfying these size bounds. Form the tree of their finite prefixes, using rooted-tree isomorphism classes as objects. At position $i$ only finitely many finite rooted trees have at most $k+i$ vertices, so this prefix tree is finitely branching and has nodes at arbitrarily large depths. König infinity lemma supplies an infinite branch: at each step some child must still have arbitrarily deep extensions, because there are only finitely many children. The branch is an infinite bad sequence of finite rooted trees, contradicting Kruskal's theorem. Thus such an $N$ exists. The argument also works for any prescribed size-bound function, or any fixed finite label set, because each position then still has finitely many possible objects.

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.

Use the unary Cantor normal form tree norm, counting one root and recursively counting all repeated exponent subterms. There are only finitely many notations of bounded norm. This finite principle bounds all descending sequences whose norms grow at most linearly with the position. Friedman's finite form of Kruskal's theorem implies it through the natural-sum ordinal rank of a finite rooted tree. The Friedman–Smith miniaturization theorem turns this controlled termination principle for standard epsilon-zero notations into the formal consistency statement for Peano arithmetic; the technical ordinal-analysis result is needed in addition to the tree coding. Section 2.2 of formal.hknu.ac.kr/Publi/kruskalJKMS.pdf records the general miniaturization and soundness theorem.