A well-quasi-ordering is a reflexive transitive relation such that every infinite sequence contains with . 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 is a family of nonempty finite increasing sequences whose underlying sets are inclusion-incomparable, such that every infinite subset of has an initial segment in . Write if both are initial segments of some increasing sequence and its first-term deletion, respectively. BQO means that every has with . 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 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 according to whether and use Ramsey's theorem; the all-bad homogeneous possibility is excluded by WQO. Suppose finite words over had a bad sequence. Choose a minimal bad sequence , minimizing length at each stage among choices admitting a bad continuation. No word is empty. Write and choose with for . The sequencecannot be bad by minimality, since its new word at position is shorter. A good pair within the old prefix was already forbidden. A prefix word embedding in some embeds in , also forbidden. A good pair extends by the ordered last letters to , again forbidden. This proves the Higman lemma.
Assume next that labelled trees have a bad sequence. Choose minimally by number of vertices, again among choices admitting a bad continuation. Let be the collection of all immediate child subtrees of all . We claim it is WQO. If were a bad sequence in , attach to each a parent index with a proper child subtree of . 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 . Thenis bad. Indeed a prefix tree embedding into also embeds into its host , contrary to the original bad sequence, and the other possible good pairs were excluded already. But is smaller than , 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 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 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 , 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 . Consider bad finite sequences of unlabelled tree isomorphism types satisfying , 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.
Articles by others on the same topic
There are currently no matching articles.