Higman's lemma


In mathematics, Higman's lemma states that the set of finite sequences over a finite alphabet, as partially ordered by the subsequence relation, is a well partial order. That is, if is an infinite sequence of words over a finite alphabet, then there exist indices such that can be obtained from by deleting some symbols. More generally the set of sequences is well-quasi-ordered even when is not necessarily finite, but is itself well-quasi-ordered, and the subsequence ordering is generalized into an "embedding" quasi-order that allows the replacement of symbols by earlier symbols in the well-quasi-ordering of. This is a special case of the later Kruskal's tree theorem. It is named after Graham Higman, who published it in 1952.

Proof

Let be a well-quasi-ordered alphabet of symbols. Suppose for a contradiction that there exist infinite bad sequences, i.e. infinite sequences of words such that no embeds into a later. Then there exists an infinite bad sequence of words that is minimal in the following sense: is a word of minimum length from among all words that start infinite bad sequences; is a word of minimum length from among all infinite bad sequences that start with ; is a word of minimum length from among all infinite bad sequences that start with ; and so on. In general, is a word of minimum length from among all infinite bad sequences that start with.
Since no can be the empty word, we can write for and. Since is well-quasi-ordered, the sequence of leading symbols must contain an infinite increasing sequence with.
Now consider the sequence of words
Because is shorter than,
this sequence is "more minimal" than, and so it must contain a word that embeds into a later word. But and cannot both be 's, because then the original sequence would not be bad. Similarly, it cannot be that is a and is a, because then would also embed into. And similarly, it cannot be that and,, because then would embed into. In every case we arrive at a contradiction.

Ordinal type

The ordinal type of is related to the ordinal type of as follows:

Reverse-mathematical calibration

Higman's lemma has been reverse mathematically calibrated as equivalent to over the base theory.