Well-quasi-ordering explained
In mathematics, specifically order theory, a well-quasi-ordering or wqo on a set
is a
quasi-ordering of
for which every
infinite sequence of elements
from
contains an increasing pair
with
Motivation
Well-founded induction can be used on any set with a well-founded relation, thus one is interested in when a quasi-order is well-founded. (Here, by abuse of terminology, a quasiorder
is said to be well-founded if the corresponding strict order
is a well-founded relation.) However the class of well-founded quasiorders is not closed under certain operations—that is, when a quasi-order is used to obtain a new quasi-order on a set of structures derived from our original set, this quasiorder is found to be not well-founded. By placing stronger restrictions on the original well-founded quasiordering one can hope to ensure that our derived quasiorderings are still well-founded.
An example of this is the power set operation. Given a quasiordering
for a set
one can define a quasiorder
on
's power set
by setting
if and only if for each element of
one can find some element of
that is larger than it with respect to
. One can show that this quasiordering on
needn't be well-founded, but if one takes the original quasi-ordering to be a well-quasi-ordering, then it is.
Formal definition
A well-quasi-ordering on a set
is a
quasi-ordering (i.e., a
reflexive,
transitive binary relation) such that any
infinite sequence of elements
from
contains an increasing pair
with
. The set
is said to be
well-quasi-ordered, or shortly
wqo.
A well partial order, or a wpo, is a wqo that is a proper ordering relation, i.e., it is antisymmetric.
Among other ways of defining wqo's, one is to say that they are quasi-orderings which do not contain infinite strictly decreasing sequences (of the form
) nor infinite sequences of
pairwise incomparable elements. Hence a quasi-order (
X, ≤) is wqo if and only if (
X, <) is
well-founded and has no infinite
antichains.
Ordinal type
Let
be well partially ordered. A (necessarily finite) sequence
of elements of
that contains no pair
with
is usually called a
bad sequence. The
tree of bad sequences
is the tree that contains a vertex for each bad sequence, and an edge joining each nonempty bad sequence
to its parent
. The root of
corresponds to the empty sequence. Since
contains no infinite bad sequence, the tree
contains no infinite path starting at the root. Therefore, each vertex
of
has an ordinal height
, which is defined by transfinite induction as
. The
ordinal type of
, denoted
, is the ordinal height of the root of
.
A linearization of
is an extension of the partial order into a total order. It is easy to verify that
is an upper bound on the ordinal type of every linearization of
. De Jongh and Parikh
[1] proved that in fact there always exists a linearization of
that achieves the maximal ordinal type
.
Examples
, the set of natural numbers with standard ordering, is a well partial order (in fact, a
well-order). However,
, the set of positive and negative integers, is
not a well-quasi-order, because it is not well-founded (see Pic.1).
, the set of natural numbers ordered by divisibility, is
not a well-quasi-order: the prime numbers are an infinite antichain (see Pic.2).
, the set of vectors of
natural numbers (where
is finite) with
component-wise ordering, is a well partial order (
Dickson's lemma; see Pic.3). More generally, if
is well-quasi-order, then
is also a well-quasi-order for all
.
be an arbitrary finite set with at least two elements. The set
of words over
ordered
lexicographically (as in a dictionary) is
not a well-quasi-order because it contains the infinite decreasing sequence
. Similarly,
ordered by the prefix relation is
not a well-quasi-order, because the previous sequence is an infinite antichain of this partial order. However,
ordered by the
subsequence relation is a well partial order.
[2] (If
has only one element, these three partial orders are identical.)
, the set of finite
-sequences ordered by
embedding is a well-quasi-order if and only if
is a well-quasi-order (
Higman's lemma). Recall that one embeds a sequence
into a sequence
by finding a subsequence of
that has the same length as
and that dominates it term by term. When
is an unordered set,
if and only if
is a subsequence of
.
, the set of infinite sequences over a well-quasi-order
, ordered by embedding, is
not a well-quasi-order in general. That is, Higman's lemma does not carry over to infinite sequences.
Better-quasi-orderings have been introduced to generalize Higman's lemma to sequences of arbitrary lengths.
- Embedding between finite trees with nodes labeled by elements of a wqo
is a wqo (
Kruskal's tree theorem).
- Embedding between infinite trees with nodes labeled by elements of a wqo
is a wqo (
Nash-Williams' theorem).
Constructing new wpo's from given ones
Let
and
be two disjoint wpo sets. Let
, and define a partial order on
by letting
if and only if
for the same
and
. Then
is wpo, and
, where
denotes
natural sum of ordinals.
Given wpo sets
and
, define a partial order on the Cartesian product
, by letting
if and only if
and
. Then
is wpo (this is a generalization of
Dickson's lemma), and
, where
denotes
natural product of ordinals.
Given a wpo set
, let
be the set of finite sequences of elements of
, partially ordered by the subsequence relation. Meaning, let
(x1,\ldots,xn)\le
(y1,\ldots,ym)
if and only if there exist indices
such that
for each
. By
Higman's lemma,
is wpo. The ordinal type of
is
[5] Given a wpo set
, let
be the set of all finite rooted trees whose vertices are labeled by elements of
. Partially order
by the
tree embedding relation. By
Kruskal's tree theorem,
is wpo. This result is nontrivial even for the case
(which corresponds to unlabeled trees), in which case
equals the
small Veblen ordinal. In general, for
countable, we have the upper bound
o(T(X))\le\vartheta(\Omega\omegao(X))
in terms of the
ordinal collapsing function. (The small Veblen ordinal equals
in this ordinal notation.)
[6] Wqo's versus well partial orders
In practice, the wqo's one manipulates are quite often not orderings (see examples above), and the theory is technically smoother if we do not require antisymmetry, so it is built with wqo's as the basic notion. On the other hand, according to Milner 1985, no real gain in generality is obtained by considering quasi-orders rather than partial orders... it is simply more convenient to do so.
Observe that a wpo is a wqo, and that a wqo gives rise to a wpo between equivalence classes induced by the kernel of the wqo. For example, if we order
by divisibility, we end up with
if and only if
, so that
.
Infinite increasing subsequences
If
is wqo then every infinite sequence
contains an
infinite increasing subsequence
(with
). Such a subsequence is sometimes called
perfect.This can be proved by a
Ramsey argument: given some sequence
, consider the set
of indexes
such that
has no larger or equal
to its right, i.e., with
. If
is infinite, then the
-extracted subsequence contradicts the assumption that
is wqo. So
is finite, and any
with
larger than any index in
can be used as the starting point of an infinite increasing subsequence.
The existence of such infinite increasing subsequences is sometimes taken as a definition for well-quasi-ordering, leading to an equivalent notion.
Properties of wqos
the quasiordering
defined by
A\le+B\iff\foralla\inA,\existsb\inB,a\leb
is well-founded if and only if
is a wqo.
- A quasiordering is a wqo if and only if the corresponding partial order (obtained by quotienting by
x\simy\iffx\ley\landy\lex
) has no infinite descending sequences or
antichains. (This can be proved using a
Ramsey argument as above.)
- Given a well-quasi-ordering
, any sequence of upward-closed subsets
S0\subseteqS1\subseteq … \subseteqX
eventually stabilises (meaning there exists
such that
; a subset
is called
upward-closed if
\forallx,y\inX,x\ley\wedgex\inS ⇒ y\inS
): assuming the contrary
\foralli\in\N,\existsj\in\N,j>i,\existsx\inSj\setminusSi
, a contradiction is reached by extracting an infinite non-ascending subsequence.
- Given a well-quasi-ordering
, any subset
of
has a finite number of minimal elements with respect to
, for otherwise the minimal elements of
would constitute an infinite antichain.
Notes
Here x < y means:
and
References
- Dickson . L. E. . Leonard Dickson . Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors . . 1913 . 35 . 413 - 422 . 10.2307/2370405 . 2370405 . 4 .
- Higman . G. . Graham Higman . Ordering by divisibility in abstract algebras . Proceedings of the London Mathematical Society . 1952 . 2 . 326 - 336 . 10.1112/plms/s3-2.1.326.
- Joseph Kruskal . Kruskal . J. B. . The theory of well-quasi-ordering: A frequently discovered concept . . Series A . 1972 . 13 . 297 - 305 . 10.1016/0097-3165(72)90063-5 . 3. free .
- Ketonen . Jussi . The structure of countable Boolean algebras . . 108 . 41–89 . 1978 . 10.2307/1970929 . 1970929 . 1.
- Book: Milner, E. C. . Eric Charles Milner
. Eric Charles Milner . 1985 . Basic WQO- and BQO-theory . I.. Rival. Ivan Rival . Graphs and Order. The Role of Graphs in the Theory of Ordered Sets and Its Applications . 487 - 502 . D. Reidel Publishing Co. . 90-277-1943-8.
- Gallier . Jean H. . Jean Gallier . What's so special about Kruskal's theorem and the ordinal Γo? A survey of some results in proof theory . Annals of Pure and Applied Logic . 1991 . 53 . 199–260 . 10.1016/0168-0072(91)90022-E . 3.
Notes and References
- de Jongh . Dick H. G. . Parikh . Rohit . Well-partial orderings and hierarchies . Indagationes Mathematicae (Proceedings) . 1977 . 80 . 3 . 195-207 . 10.1016/1385-7258(77)90067-1. free .
- . See in particular page 1160.
- .
- .
- Schmidt . Diana . Habilitationsschrift . 1979 . Well-partial orderings and their maximal order types . Heidelberg. Republished in: Book: Schmidt, Diana . 2020 . Well-partial orderings and their maximal order types . Well-Quasi Orders in Computation, Logic, Language and Reasoning . Springer . 351-391 . Schuster . Peter M. . Seisenberger . Monika . Weiermann . Andreas . Trends in Logic . 53 . 10.1007/978-3-030-30229-0_13.
- Rathjen . Michael . Weiermann . Andreas . Proof-theoretic investigations on Kruskal's theorem . Annals of Pure and Applied Logic . 1993 . 60 . 49-88 . 10.1016/0168-0072(93)90192-G. free .