nLab well-order




A well-order on a set SS is a relation \prec that allows one to interpret SS as an ordinal number α\alpha and \prec as the relation <\lt on the ordinal numbers less than α\alpha. In particular, one can do induction on SS over \prec (although the more general well-founded relations also allow this).

The well-ordering theorem states precisely that every set may be equipped with a well-order. This theorem follows from the axiom of choice, and is equivalent to it in the presence of excluded middle.


A binary relation \prec on a set SS is a well-order if it is transitive, extensional, and well-founded. A set equipped with a well-order is called a well-ordered set, or (following ‘poset’) a woset. Actually, the term ‘well-ordered’ came first; ‘well-order’ is a back formation, which explains the strange grammar.

Other definitions of a well-order may be found in the literature; they are equivalent given excluded middle, but the definition above seems to be the most powerful in constructive mathematics. Specifically:

  • a well-order is precisely a well-founded pseudo-order \prec;
  • a well-order is precisely a total order \preceq whose strict version \prec (defined by xyx \prec y iff xyx \preceq y and xyx \ne y) is well-founded;
  • (assuming also dependent choice) a well-order is precisely a pseudo-order \prec with no infinite descending sequence x 2x 1x 0\cdots \prec x_2 \prec x_1 \prec x_0;
  • (assuming also dependent choice) a well-order is precisely a total order \preceq such that every infinite descending sequence x 2x 1x 0\cdots \preceq x_2 \preceq x_1 \preceq x_0 has x i=x i +x_i = x_{i^+} for some ii (and hence for infinitely many ii);
  • a well-order on SS is precisely a pseudo-order \prec with the property that every inhabited subset UU of SS has a least element (an element U\bot_U such that no xUx \in U satisfies x Ux \prec \bot_U;
  • a well-order on SS is precisely a total order \preceq with the property that every inhabited subset UU of SS has a least element (an element U\bot_U such that every xUx \in U satisfies Ux\bot_U \preceq x.

The really interesting thing here is that every well-order is a pseudo-order; it is a constructive theorem that every pseudo-order is weakly extensional (and so extensional if well-founded) and transitive. (For a weak counterexample, take the set of truth values with xyx \prec y iff yy is true and xx is false; this is a well-order that's a pseudo-order iff excluded middle holds.) For the other equivalences, we're simply using well-known classical equivalents for well-foundedness and the classical correspondence between a pseudo-order \prec and its reflexive closure? \preceq.

For reference, a classical well-order is any order satisfying the last definition (a total order that is classically well-founded). A classically well-ordered set is a choice set, and so if any set with at least 22 unequal elements has a classical well-order, then excluded middle follows. (But there are still interesting examples of classically well-ordered sets in constructive mathematics, such as the Higgs set?.)

Well-orders are pseudo-orders

As stated above, well-founded extensional transitive relations \prec on a set XX are pseudo-orders, assuming classical logic.


Order X×XX \times X lexicographically: (a,b)(a,b)(a, b) \prec (a', b') if either aaa \prec a' in XX or a=aa = a' and bbb \prec b in XX. It is not hard to see that the lexicographic order is well-founded (and in fact a well-order, although we do not need this). Now let AX×XA \subset X \times X be the set of pairs (x,y)(x, y) of non-equal elements xx and yy that are incomparable in XX, and suppose AA is inhabited. Then AA has a minimal element (a,b)(a, b) (using excluded middle). Then, for every xbx \prec b, either axa \preceq x or xax \preceq a. If the former holds for some xx, then aba \prec b follows by transitivity, contradiction. Hence xax \prec a for every xbx \prec b. Now let aa' be minimal such that xaax \prec a' \preceq a for every xbx \prec b.


{x:xa}={x:xb}. \{x: x \prec a'\} = \{x: x \prec b\}.

We know already the right side is contained in the left. In the other direction, suppose xax \prec a'. Since xax \prec a and (a,b)(a, b) was chosen minimal in the lexicographic order, xx and bb are comparable. If bxab \preceq x \prec a', this contradicts minimality of aa'. Thus xbx \prec b, i.e., the left side is contained in the right.

But now, by extensionality, a=ba' = b, whence bab \preceq a, contradiction. Therefore AA was empty, so that XX is connected and therefore (being already transitive and irreflexive and using excluded middle again) a pseudo-order.


  • Any finite pseudo-ordered set {x 1<<x n}\{x_1 \lt \cdots \lt x_n\} is well-ordered.

  • The set of natural numbers is well-ordered under the usual order <\lt.

  • More generally, any set of ordinal numbers (or even the proper class of all ordinal numbers) is well-ordered under the usual order <\lt (which, constructively, may not be a pseudo-order).

  • The cardinal numbers of well-orderable sets (the well-orderable cardinals), forming a retract of the ordinals, are well-ordered. So by the well-ordering theorem, the class of all cardinal numbers is well-ordered.

  • A special case of the well-ordering theorem is the existence of a well-order on the set of real numbers; this is enough for many applications of the axiom of choice to analysis.

Interpretation as an ordinal number

Any well-ordered set SS defines an ordinal number α\alpha and an order isomorphism rr between SS and the set of ordinal numbers less than α\alpha; as such, SS may be identified (up to isomorphism of wosets) with the von Neumann ordinal α\alpha. The idea is that the minimal element \bot of SS itself (if any) is mapped to the ordinal number 00, the minimal element of S{}S \setminus \{\bot\} (if any) is mapped to 11, and so on; after which the next element of SS (if any) is mapped to ω\omega, and so on; and so on.

This may be defined immediately (and constructively) as a recursively defined function from SS to the class of all ordinal numbers:

r(x)=sup txr(t) +; r(x) = \sup_{t \prec x} r(t)^+ ;

the validity of this sort of recursive definition is precisely what the well-foundedness of \prec allows. Here, β +\beta^+ is the successor of the ordinal number β\beta, and sup\sup is the supremum operation on ordinal numbers (which is the union of von Neumann ordinals).

Since SS is a set, the image of rr in the class of all ordinals is also a set (by the axiom of replacement), and one can now prove that rr is an order isomorphism between SS and the set of ordinals less than the next ordinal, α(imr) +\alpha \coloneqq (\im r)^+.


Given two well-ordered sets SS and TT, a function f:STf\colon S \to T is a simulation of SS in TT if

  • f(x)f(y)f(x) \prec f(y) whenever xyx \prec y and
  • given tf(x)t \prec f(x), there exists yxy \prec x with t=f(y)t = f(y).

Note that any simulation of SS in TT must be unique. Thus, well-ordered sets and simulations form a category that is in fact a (large) preorder, whose reflection in the category of posets is in fact the poset of ordinal numbers.


A well-ordered set SS comes equipped with a successor, which is a partial map succ:SS succ\colon S \to S \, that sends aSa \in S to the lowest element of the subset S a:={sS,as}S_a := \{ s \in S, a \prec s\}, whenever this set is inhabited.


A limit well-order is a well-order SS whose successor map is a total function.

Similarly, one may define a successor functor on the category of well-ordered sets, taking SS to the well-order obtained by freely adjoining a (new) top element to SS. Since this category (which is thin) can be regarded as itself a well-ordered proper class, this is a special case of the successor operation above. (Hence the ordinal of all ordinals is a limit ordinal.)

Last revised on December 26, 2023 at 04:44:58. See the history of this page for a list of all contributions to it.