= Friedman's finite form of Kruskal's theorem
{c}
{title2=$\forall k\ \exists N\ \forall(T_i)_{i\leq N}\ \exists i<j\ (T_i\preceq T_j)$}
= FFF
{c}
{synonym}
For every natural parameter $k$, there is a finite length $N$ such that every <sequence> of $N$ finite <rooted trees> satisfying $|T_i|\leq k+i$ has an earlier tree homeomorphically embedding into a later tree. It is a true finite-combinatorial principle unprovable in <Peano arithmetic> and in <arithmetical transfinite recursion theory>. Each fixed-parameter instance can still be verified by a sufficiently large finite search.
Back to article page
