= Solution
For finite <rooted trees> write $T\preceq 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 which
$$
\boxed{|T_i|\leq k+i\ (1\leq i\leq N)\quad\Longrightarrow\quad(\exists i<j\leq N)\,T_i\preceq T_j.}
$$
Here $|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,\ldots$ satisfying the size bounds and with no pair $i<j$ having $T_i\preceq 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 N\,R(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.
Back to article page
