# Well-quasi-ordering

## 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. 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.

## Formal definition

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 do not contain infinite strictly decreasing sequences (of the form $x_{0}$ >$x_{1}$ >$x_{2}$ >…) nor infinite sequences of pairwise incomparable elements. Hence a quasi-order ($X$ ,≤) is wqo if and only if it is well-founded and has no infinite antichains.

## 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.

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 $\mathbb {Z}$ by divisibility, we end up with $n\equiv m$ if and only if $n=\pm m$ , so that $(\mathbb {Z} ,\mid )\;\;\approx \;\;(\mathbb {N} ,\mid )$ .

## Infinite increasing subsequences

The existence of such infinite increasing subsequences is sometimes taken as a definition for well-quasi-ordering, leading to an equivalent notion.