10.4 Classical well-orderings

We now show the equivalence of our ordinalsMathworldPlanetmathPlanetmath with the more familiar classical well-orderings.

Lemma 10.4.1.

Assuming excluded middle, every ordinal is trichotomous:


By inductionMathworldPlanetmath on a, we may assume that for every a<a and every b:A, we have (a<b)(a=b)(b<a). Now by induction on b, we may assume that for every b<b, we have (a<b)(a=b)(b<a).

By excluded middle, either there merely exists a b<b such that a<b, or there merely exists a b<b such that a=b, or for every b<b we have b<a. In the first case, merely a<b by transitivity, hence a<b as it is a mere proposition. Similarly, in the second case, a<b by transport. Thus, suppose (b:A).(b<b)(b<a).

Now analogously, either there merely exists a<a such that b<a, or there merely exists a<a such that a=b, or for every a<a we have a<b. In the first and second cases, b<a, so we may suppose (a:A).(a<a)(a<b). However, by extensionality, our two suppositions now imply a=b. ∎

Lemma 10.4.2.

A well-founded relation contains no cycles, i.e.


We prove by induction on a:A that there is no cycle containing a. Thus, suppose by induction that for all a<a, there is no cycle containing a. But in any cycle containing a, there is some element less than a and contained in the same cycle. ∎

In particular, a well-founded relation must be irreflexiveMathworldPlanetmath, i.e. ¬(a<a) for all a.

Theorem 10.4.3.

Assuming excluded middle, (A,<) is an ordinal if and only if every nonempty subset BA has a least element.


If A is an ordinal, then by \autorefthm:wfmin every nonempty subset merely has a minimal element. But trichotomy implies that any minimal element is a least element. Moreover, least elements are unique when they exist, so merely having one is as good as having one.

Conversely, if every nonempty subset has a least element, then by \autorefthm:wfmin, A is well-founded. We also have trichotomy, since for any a,b the subset \setofa,b:\setofx:A|x=ax=b merely has a least element, which must be either a or b. This implies transitivity, since if a<b and b<c, then either a=c or c<a would produce a cycle. Similarly, it implies extensionality, for if (c:A).(c<a)(c<b), then a<b implies (letting c be a) that a<a, which is a cycle, and similarly if b<a; hence a=b. ∎

In classical mathematics, the characterization of \autorefthm:wellorder is taken as the definition of a well-ordering, with the ordinals being a canonical set of representatives of isomorphism classes for well-orderings. In our context, the structureMathworldPlanetmath identityPlanetmathPlanetmath principle means that there is no need to look for such representatives: any well-ordering is as good as any other.

We now move on to consider consequences of the axiom of choiceMathworldPlanetmath. For any set X, let 𝒫+(X) denote the type of merely inhabited subsets of X:


Assuming excluded middle, this is equivalently the type of nonempty subsets of X, and we have 𝒫(X)(𝒫+(X))+𝟏.

Theorem 10.4.4.

Assuming excluded middle, the following are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath.

  1. 1.

    For every set X, there merely exists a function f:𝒫+(X)X such that f(Y)Y for all Y:𝒫(X).

  2. 2.

    Every set merely admits the structure of an ordinal.

Of course, 1 is a standard classical version of the axiom of choice; see \autorefex:choice-function.


One direction is easy: suppose 2. Since we aim to prove the mere proposition 1, we may assume A is an ordinal. But then we can define f(B) to be the least element of B.

Now suppose 1. As before, since 2 is a mere proposition, we may assume given such an f. We extend f to a function


in the obvious way. Now for any ordinal A, we can define gA:AX+𝟏 by well-founded recursion:


(regarding X as a subset of X+𝟏 in the obvious way).

Let A:\setofa:A|gA(a)X be the preimageMathworldPlanetmath of XX+𝟏; then we claim the restrictionPlanetmathPlanetmathPlanetmath gA:AX is injectivePlanetmathPlanetmath. For if a,a:A with aa, then by trichotomy and without loss of generality, we may assume a<a. Thus gA(a)\setofgA(b)|b<a, so since f(Y)Y for all Y we have gA(a)gA(a).

Moreover, A is an initial segment of A. For gA(a) lies in 𝟏 if and only if \setofgA(b)|b<a=X, and if this holds then it also holds for any a>a. Thus, A is itself an ordinal.

Finally, since 𝖮𝗋𝖽 is an ordinal, we can take A:𝖮𝗋𝖽. Let X be the image of g𝖮𝗋𝖽:𝖮𝗋𝖽X; then the inversePlanetmathPlanetmath of g𝖮𝗋𝖽 yields an injection H:X𝖮𝗋𝖽. By \autorefthm:ordunion, there is an ordinal C such that HxC for all x:X. Then by \autorefthm:ordsucc, there is a further ordinal D such that C<D, hence Hx<D for all x:X. Now we have

g𝖮𝗋𝖽(D) =f¯(X\setofg𝖮𝗋𝖽(B)|B<D(g𝖮𝗋𝖽(B)X))

since if B:𝖮𝗋𝖽 and (g𝖮𝗋𝖽(B)X), then B=Hx for some x:X, hence B<D. Now if


is not all of X, then g𝖮𝗋𝖽(D) would lie in X but not in this subset, which would be a contradictionMathworldPlanetmathPlanetmath since D is itself a potential value for B. So this set must be all of X, and hence g𝖮𝗋𝖽 is surjective as well as injective. Thus, we can transport the ordinal structure on 𝖮𝗋𝖽 to X. ∎

Remark 10.4.5.

If we had given the wrong proof of \autorefthm:ordsucc or \autorefthm:ordunion, then the resulting proof of \autorefthm:wop would be invalid: there would be no way to consistently assign universePlanetmathPlanetmath levels. As it is, we require propositional resizing (which follows from LEM) to ensure that X lives in the same universe as X (up to equivalence).

Corollary 10.4.6.

Assuming the axiom of choice, the function Ord\set (which forgets the order structure) is a surjection.

Note that 𝖮𝗋𝖽 is a set, while \setis a 1-type. In general, there is no reason for a 1-type to admit any surjective function from a set. Even the axiom of choice does not appear to imply that every 1-type does so (although see \autorefex:acnm-surjset), but it readily implies that this is so for 1-types constructed out of \set, such as the types of objects of categories of structures as in \autorefsec:sip. The following corollary also applies to such categories.

Corollary 10.4.7.

Assuming AC, Set admits a weak equivalenceMathworldPlanetmath functor from a strict category.


Let X0:𝖮𝗋𝖽, and for A,B:X0 let homX(A,B):(AB). Then X is a strict category, since 𝖮𝗋𝖽 is a set, and the above surjection X0\set extends to a weak equivalence functor X𝒮et. ∎

Now recall from \autorefsec:cardinals that we have a further surjection |¯|0:\set𝖢𝖺𝗋𝖽, and hence a composite surjection 𝖮𝗋𝖽𝖢𝖺𝗋𝖽 which sends each ordinal to its cardinality.

Theorem 10.4.8.

Assuming AC, the surjection OrdCard has a sectionPlanetmathPlanetmathPlanetmathPlanetmath.


There is an easy and wrong proof of this: since 𝖮𝗋𝖽 and 𝖢𝖺𝗋𝖽 are both sets, 𝖠𝖢 implies that any surjection between them merely has a section. However, we actually have a canonical specified section: because 𝖮𝗋𝖽 is an ordinal, every nonempty subset of it has a uniquely specified least element. Thus, we can map each cardinal to the least element in the corresponding fiber. ∎

It is traditional in set theoryMathworldPlanetmath to identify cardinals with their image in 𝖮𝗋𝖽: the least ordinal having that cardinality.

It follows that 𝖢𝖺𝗋𝖽 also canonically admits the structure of an ordinal: in fact, one isomorphicPlanetmathPlanetmath to 𝖮𝗋𝖽. Specifically, we define by well-founded recursion a function :𝖮𝗋𝖽𝖮𝗋𝖽, such that (A) is the least ordinal having cardinality greater than (A/a) for all a:A. Then (assuming 𝖠𝖢) the image of is exactly the image of 𝖢𝖺𝗋𝖽.

Title 10.4 Classical well-orderings