10.4 Classical well-orderings
Assuming excluded middle, every ordinal is trichotomous:
By induction on , we may assume that for every and every , we have . Now by induction on , we may assume that for every , we have .
By excluded middle, either there merely exists a such that , or there merely exists a such that , or for every we have . In the first case, merely by transitivity, hence as it is a mere proposition. Similarly, in the second case, by transport. Thus, suppose .
Now analogously, either there merely exists such that , or there merely exists such that , or for every we have . In the first and second cases, , so we may suppose . However, by extensionality, our two suppositions now imply . ∎
A well-founded relation contains no cycles, i.e.
In particular, a well-founded relation must be irreflexive, i.e. for all .
Assuming excluded middle, is an ordinal if and only if every nonempty subset has a least element.
If 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, is well-founded. We also have trichotomy, since for any the subset merely has a least element, which must be either or . This implies transitivity, since if and , then either or would produce a cycle. Similarly, it implies extensionality, for if , then implies (letting be ) that , which is a cycle, and similarly if ; hence . ∎
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.
Assuming excluded middle, this is equivalently the type of nonempty subsets of , and we have .
Of course, 1 is a standard classical version of the axiom of choice; see \autorefex:choice-function.
in the obvious way. Now for any ordinal , we can define by well-founded recursion:
(regarding as a subset of in the obvious way).
Moreover, is an initial segment of . For lies in if and only if , and if this holds then it also holds for any . Thus, is itself an ordinal.
Finally, since is an ordinal, we can take . Let be the image of ; then the inverse of yields an injection . By \autorefthm:ordunion, there is an ordinal such that for all . Then by \autorefthm:ordsucc, there is a further ordinal such that , hence for all . Now we have
since if and , then for some , hence . Now if
is not all of , then would lie in but not in this subset, which would be a contradiction since is itself a potential value for . So this set must be all of , and hence is surjective as well as injective. Thus, we can transport the ordinal structure on to . ∎
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 ) to ensure that lives in the same universe as (up to equivalence).
Assuming the axiom of choice, the function (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.
Assuming , admits a weak equivalence functor from a strict category.
Let , and for let . Then is a strict category, since is a set, and the above surjection extends to a weak equivalence functor . ∎
Assuming , the surjection has a section.
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 theory 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 isomorphic to . Specifically, we define by well-founded recursion a function , such that is the least ordinal having cardinality greater than for all . Then (assuming ) the image of is exactly the image of .
|Title||10.4 Classical well-orderings|