A well-order on a set is a relation that allows one to interpret as an ordinal number and as the relation on the ordinal numbers less than . In particular, one can do induction on over (although the more general well-founded relations also allow this).
A binary relation on a set 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:
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 iff is true and 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 and its reflexive closure? .
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 elements has a classical well-order, excluded middle follows.
As stated above, well-founded extensional transitive relations on a set are linear, assuming classical logic.
Order lexicographically: if either in or and in . 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 be the set of pairs of non-equal elements and that are incomparable in , and suppose is inhabited. Then has a minimal element (using excluded middle). Then, for every , either or . If the former holds for some , then follows by transitivity, contradiction. Hence for every . Now let be minimal such that for every .
We know already the right side is contained in the left. In the other direction, suppose . Since and was chosen minimal in the lexicographic order, and are comparable. If , this contradicts minimality of . Thus , i.e., the left side is contained in the right.
But now, by extensionality, , whence , contradiction. Therefore was empty, so that is connected and therefore (being already transitive and irreflexive and using excluded middle again) a linear order.
The set of natural numbers is well-ordered under the usual 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.
Any well-ordered set defines an ordinal number and an order isomorphism between and the set of ordinal numbers less than ; as such, may be identified (up to isomorphism of wosets) with the von Neumann ordinal . The idea is that the minimal element of itself (if any) is mapped to the ordinal number , the minimal element of (if any) is mapped to , and so on; after which the next element of (if any) is mapped to , and so on; and so on.
This may be defined immediately (and constructively) as a recursively defined function from to the class of all ordinal numbers:
the validity of this sort of recursive definition is precisely what the well-foundedness of allows. Here, is the successor of the ordinal number , and is the supremum operation on ordinal numbers (which is the union of von Neumann ordinals).
Since is a set, the image of in the class of all ordinals is also a set (by the axiom of replacement), and one can now prove that is an order isomorphism between and the set of ordinals less than the next ordinal, .
Note that any simulation of in 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 limit well-order is a well-order whose successor map is a total function.
Similarly, one may define a successor functor on the category of well-ordered sets, taking to the well-order obtained by freely adjoining a (new) top element to . 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.)