10.4 Classical well-orderings

Lemma 10.4.1.

Assuming excluded middle, every ordinal is trichotomous:

 $\forall(a,b:A).\,(a
Proof.

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

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

Now analogously, either there merely exists $a^{\prime} such that $b, or there merely exists $a^{\prime} such that $a^{\prime}=b$, or for every $a^{\prime} we have $a^{\prime}. In the first and second cases, $b, so we may suppose $\forall(a^{\prime}:A).\,(a^{\prime}. 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}
Proof.

We prove by induction on $a:A$ that there is no cycle containing $a$. Thus, suppose by induction that for all $a^{\prime}, 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 , i.e. $\neg(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 and $b, then either $a=c$ or $c would produce a cycle. Similarly, it implies extensionality, for if $\forall(c:A).\,(c, then $a implies (letting $c$ be $a$) that $a, which is a cycle, and similarly if $b; 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.

1. 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. 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

(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}. Thus $g_{A}(a^{\prime})\in\setof{g_{A}(b)|b, 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, 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, hence $Hx 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 $\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. 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.

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