10.4 Classical well-orderings

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

Lemma 10.4.1.

Assuming excluded middle, every ordinal is trichotomous:

\\forall(a,b:A).\\,(a<b)\\vee(a=b)\\vee(b<a).

Proof.

By induction on $a$ , we may assume that for every $a^{\\prime}<a$ and every $b^{\\prime}:A$ , we have $(a^{\\prime}<b^{\\prime})\\vee(a^{\\prime}=b^{\\prime})\\vee(b^{\\prime}<a^{\\prime})$ .Now by induction on $b$ , we may assume that for every $b^{\\prime}<b$ , we have $(a<b^{\\prime})\\vee(a=b^{\\prime})\\vee(b^{\\prime}<a)$ .

By excluded middle, either there merely exists a $b^{\\prime}<b$ such that $a<b^{\\prime}$ , or there merely exists a $b^{\\prime}<b$ such that $a=b^{\\prime}$ , or for every $b^{\\prime}<b$ we have $b^{\\prime}<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 $\\forall(b^{\\prime}:A).\\,(b^{\\prime}<b)\\to(b^{\\prime}<a)$ .

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

Lemma 10.4.2.

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

\\forall(n:\\mathbb{N}).\\,\\forall(a:\\mathbb{N}_{n}\\to A).\\,\eg\\Big{(}(a_{0}<a_{%1})\\wedge\\dots\\wedge(a_{n-1}<a_{n})\\wedge(a_{n}<a_{0})\\Big{)}.

Proof.

We prove by induction on $a : A$ that there is no cycle containing $a$ .Thus, suppose by induction that for all $a^{\\prime}<a$ , there is no cycle containing $a^{\\prime}$ .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 irreflexive, i.e. $\eg(a<a)$ for all $a$ .

Theorem 10.4.3.

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

Proof.

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 $\\setof{a,b}:\\!\\!\\equiv\\setof{x:A|x=a\\lor x=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 $\\forall(c:A).\\,(c<a)\\Leftrightarrow(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 structure identity 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 choice.For any set $X$ , let $\\mathcal{P}_{+}(X)$ denote the type of merely inhabited subsets of $X$ :

\\mathcal{P}_{+}(X):\\!\\!\\equiv\\setof{Y:\\mathcal{P}(X)|\\exists(x:X).\\,x\\in Y}.

Assuming excluded middle, this is equivalently the type of nonempty subsets of $X$ , and we have $\\mathcal{P}(X)\\simeq(\\mathcal{P}_{+}(X))+\\mathbf{1}$ .

Theorem 10.4.4.

Assuming excluded middle, the following are equivalent.

1.
For every set $X$ , there merely exists a function $f:\\mathcal{P}_{+}(X)\\to X$ such that $f(Y)\\in Y$ for all $Y:\\mathcal{P}(X)$ .
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.

Proof.

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

\\bar{f}:\\mathcal{P}(X)\\simeq(\\mathcal{P}_{+}(X))+\\mathbf{1}\\longrightarrow X+%\\mathbf{1}

in the obvious way.Now for any ordinal $A$ , we can define $g_{A}:A\\to X+\\mathbf{1}$ by well-founded recursion:

g_{A}(a):\\!\\!\\equiv\\bar{f}\\Big{(}X\\setminus\\setof{g_{A}(b)|(b<a)\\wedge(g_{A}(b%)\\in X)}\\Big{)}

(regarding $X$ as a subset of $X+\\mathbf{1}$ in the obvious way).

Let $A^{\\prime}:\\!\\!\\equiv\\setof{a:A|g_{A}(a)\\in X}$ be the preimage of $X\\subseteq X+\\mathbf{1}$ ; then we claim the restriction $g_{A}^{\\prime}:A^{\\prime}\\to X$ is injective.For if $a,a^{\\prime}:A$ with $a\eq a^{\\prime}$ , then by trichotomy and without loss of generality, we may assume $a^{\\prime}<a$ .Thus $g_{A}(a^{\\prime})\\in\\setof{g_{A}(b)|b<a}$ , so since $f(Y)\\in Y$ for all $Y$ we have $g_{A}(a)\eq g_{A}(a^{\\prime})$ .

Moreover, $A^{\\prime}$ is an initial segment of $A$ .For $g_{A}(a)$ lies in $\\mathbf{1}$ if and only if $\\setof{g_{A}(b)|b<a}=X$ , and if this holds then it also holds for any $a^{\\prime}>a$ .Thus, $A^{\\prime}$ is itself an ordinal.

Finally, since $\\mathsf{Ord}$ is an ordinal, we can take $A:\\!\\!\\equiv\\mathsf{Ord}$ .Let $X^{\\prime}$ be the image of $g_{\\mathsf{Ord}}^{\\prime}:\\mathsf{Ord}^{\\prime}\\to X$ ; then the inverse of $g_{\\mathsf{Ord}}^{\\prime}$ yields an injection $H:X^{\\prime}\\to\\mathsf{Ord}$ .By \\autorefthm:ordunion, there is an ordinal $C$ such that $Hx\\leq C$ for all $x:X^{\\prime}$ .Then by \\autorefthm:ordsucc, there is a further ordinal $D$ such that $C<D$ , hence $Hx<D$ for all $x:X^{\\prime}$ .Now we have

	$\\displaystyle g_{\\mathsf{Ord}}(D)$	$\\displaystyle=\\bar{f}\\Big{(}X\\setminus\\setof{g_{\\mathsf{Ord}}(B)\|\\rule{0.0pt}{%10.0pt}B<D\\wedge(g_{\\mathsf{Ord}}(B)\\in X)}\\Big{)}$
		$\\displaystyle=\\bar{f}\\Big{(}X\\setminus\\setof{g_{\\mathsf{Ord}}(B)\|\\rule{0.0pt}{%10.0pt}g_{\\mathsf{Ord}}(B)\\in X}\\Big{)}$

since if $B:\\mathsf{Ord}$ and $(g_{\\mathsf{Ord}}(B)\\in X)$ , then $B=Hx$ for some $x:X^{\\prime}$ , hence $B<D$ .Now if

\\setof{g_{\\mathsf{Ord}}(B)|\\rule{0.0pt}{10.0pt}g_{\\mathsf{Ord}}(B)\\in X}

is not all of $X$ , then $g_{\\mathsf{Ord}}(D)$ would lie in $X$ but not in this subset, which would be a contradiction since $D$ is itself a potential value for $B$ .So this set must be all of $X$ , and hence $g_{\\mathsf{Ord}}^{\\prime}$ is surjective as well as injective.Thus, we can transport the ordinal structure on $\\mathsf{Ord}^{\\prime}$ 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 universe levels.As it is, we require propositional resizing (which follows from $\\mathsf{LEM}$ ) to ensure that $X^{\\prime}$ lives in the same universe as $X$ (up to equivalence).

Corollary 10.4.6.

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

Note that $\\mathsf{Ord}$ 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 $\\mathsf{AC}$ , $\\mathcal{S}et$ admits a weak equivalence functor from a strict category.

Proof.

Let $X_{0}:\\!\\!\\equiv\\mathsf{Ord}$ , and for $A,B:X_{0}$ let $\\hom_{X}(A,B):\\!\\!\\equiv(A\\to B)$ .Then $X$ is a strict category, since $\\mathsf{Ord}$ is a set, and the above surjection $X_{0}\\to\\set$ extends to a weak equivalence functor $X\\to\\mathcal{S}et$ .∎

Now recall from \\autorefsec:cardinals that we have a further surjection $\\mathopen{}\\left|\\mathord{\\hskip 1.0pt\\underline{\\hskip 4.3pt}\\hskip 1.0pt}%\\right|_{0}\\mathclose{}:\\set\\to\\mathsf{Card}$ , and hence a composite surjection $\\mathsf{Ord}\\to\\mathsf{Card}$ which sends each ordinal to its cardinality.

Theorem 10.4.8.

Assuming $\\mathsf{AC}$ , the surjection $\\mathsf{Ord}\\to\\mathsf{Card}$ has a section.

Proof.

There is an easy and wrong proof of this: since $\\mathsf{Ord}$ and $\\mathsf{Card}$ are both sets, $\\mathsf{AC}$ implies that any surjection between them merely has a section.However, we actually have a canonical specified section: because $\\mathsf{Ord}$ 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 theory to identify cardinals with their image in $\\mathsf{Ord}$ : the least ordinal having that cardinality.

It follows that $\\mathsf{Card}$ also canonically admits the structure of an ordinal: in fact, one isomorphic to $\\mathsf{Ord}$ .Specifically, we define by well-founded recursion a function $\\aleph:\\mathsf{Ord}\\to\\mathsf{Ord}$ , such that $\\aleph(A)$ is the least ordinal having cardinality greater than $\\aleph({{A}_{/a}})$ for all $a : A$ .Then (assuming $\\mathsf{AC}$ ) the image of $\\aleph$ is exactly the image of $\\mathsf{Card}$ .