Editing Well-quasi-ordering (section)

==Formal definition==

A '''well-quasi-ordering''' on a set <math>X</math> is a [[quasi-ordering]] (i.e., a [[reflexive relation|reflexive]], [[transitive relation|transitive]] [[binary relation]]) such that any [[Infinity|infinite]] sequence of elements <math>x_0, x_1, x_2, \ldots</math> from <math>X</math> contains an increasing pair <math>x_i \le x_j</math> with <math>i< j</math>. The set <math>X</math> 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 relation|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 <math>x_0> x_1> x_2> \cdots</math>){{ref|a}} nor infinite sequences of ''pairwise incomparable'' elements. Hence a quasi-order (''X'', ≤) is wqo if and only if (''X'', <) is [[well-founded relation|well-founded]] and has no infinite [[antichain]]s.