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).\,\neg\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. $\neg(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\neq 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)\neq 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}$ .

Title	10.4 Classical well-orderings
\metatable