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 linear order;
  • a well-order is precisely a well-founded total order;
  • (assuming also dependent choice) a well-order is precisely a linear 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 linear 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 linear; it is a constructive theorem that every linear 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 linear 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 linear relation \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 elements has a classical well-order, excluded middle follows.

Well-orders are linear

As stated above, well-founded extensional transitive relations \prec on a set XX are linear, 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 linear order.


  • Any finite linearly 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 linear).

  • 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 January 26, 2023 at 13:20:16. See the history of this page for a list of all contributions to it.