1\newcommand{\eqo}{\mbox{$=\!\!o$}} 2\newcommand{\leqo}{\mbox{$\leq\!\!o$}} 3\newcommand{\lesso}{\mbox{$<\!\!o$}} 4 5 6\begin{abstract} 7We develop a basic theory of ordinals and cardinals in Isabelle/HOL, up to the 8point where some cardinality facts relevant for the ``working mathematician" become available. 9Unlike in set theory, here we do not have at hand canonical notions of ordinal and cardinal. 10Therefore, here an ordinal is merely a well-order relation and a cardinal is an 11ordinal minim w.r.t. order embedding on its field. 12\end{abstract} 13 14 15 16\section{Introduction} 17 18In set theory (under formalizations such as Zermelo-Fraenkel or Von Neumann-Bernays-G\"{o}del), an 19{\em ordinal} is a special kind of well-order, namely one 20whose strict version is the restriction of the membership relation to a set. In particular, 21the field of a set-theoretic ordinal is a transitive set, and the non-strict version 22of an ordinal relation is set inclusion. Set-theoretic ordinals enjoy the nice properties 23of membership on transitive sets, while at the same time forming a complete class of 24representatives for well-orders (since any well-order turns out isomorphic to an ordinal). 25Moreover, the class of ordinals is itself transitive and well-ordered by membership as the strict relation 26and inclusion as the non-strict relation. 27Also knowing that any set can be well-ordered (in the presence of the axiom of choice), one then defines 28the {\em cardinal} of a set to be the smallest ordinal isomorphic to a well-order on that set. 29This makes the class of cardinals a complete set of representatives for the intuitive notion 30of set cardinality.\footnote{The ``intuitive" cardinality of a set $A$ is the class of all 31sets equipollent to $A$, i.e., being in bijection with $A$.} 32The ability to produce {\em canonical well-orders} from the membership relation (having the aforementioned 33convenient properties) 34allows for a harmonious development of the theory of cardinals in set-theoretic settings. 35Non-trivial cardinality results, such as $A$ being equipollent to $A \times A$ for any infinite $A$, 36follow rather quickly within this theory. 37 38However, a canonical notion of well-order is {\em not} available in HOL. 39Here, one has to do with well-order ``as is", but otherwise has all the necessary infrastructure 40(including Hilbert choice) to ``climb" well-orders recursively and to well-oder arbitrary sets. 41 42The current work, formalized in Isabelle/HOL, develops the basic theory of ordinals and cardinals 43up to the point where there are inferred a collection of non-trivial cardinality facts useful 44for the ``working mathematician", among which: 45\begin{itemize} 46\item Given any two sets (on any two given types)\footnote{Recall that, in HOL, a set 47on a type $\alpha$ is modeled, just like a predicate, as a function from $\alpha$ to \textsf{bool}.}, 48one is injectable in the other. 49\item If at least one of two sets is infinite, then their sum and their Cartesian product are equipollent 50to the larger of the two. 51\item The set of lists (and also the set of finite sets) with element from an 52infinite set is equipollent with that set. 53\end{itemize} 54 55Our development emulates the standard one from set-theory, but keeps everything 56{\em up to order isomorphism}. 57An (HOL) ordinal is merely a well-order. An {\em ordinal embedding} is an 58injective and order-compatible function which maps its source into an initial segment 59(i.e., order filter) of its target. Now, a {\em cardinal} (called in this work a {\em cardinal order}) 60is an ordinal minim w.r.t. the existence of embeddings among all 61well-orders on its field. After showing the existence of cardinals on any given set, 62we define the cardinal of a set $A$, denoted $|A|$, to be {\em some} cardinal order 63on $A$. This concept is unique only up to order isomorphism (denoted $\eqo$), but meets 64its purpose: any two sets $A$ and $B$ (laying at potentially distinct types) 65are in bijection if and only if $|A|\;\eqo\;|B|$. Moreover, we also show that numeric cardinals 66assigned to finite sets\footnote{Numeric cardinals of finite sets are already formalized in 67Isabelle/HOL.} 68are {\em conservatively extended} by our general (order-theoretic) notion of 69cardinal. We study the interaction of cardinals with standard set-theoretic 70constructions such as powersets, products, sums and lists. These constructions are shown 71to preserve the ``cardinal identity" $\eqo$ and also to be monotonic w.r.t. $\leqo$, the ordinal 72embedding relation. By studying the interaction between these constructions, infinite sets and 73cardinals, we obtain the 74aforementioned results for ``working mathematicians". 75 76For this development, we did not follow closely any particular textbook, and in fact are not 77aware of such basic theory of cardinals previously 78developed in HOL.\footnote{After writing this formalization, we became aware of 79Paul Taylor's membership-free development of the theory of ordinals \cite{taylor-ordinals}.} On 80the other hand, 81the set-theoretic versions of the facts proved here are folklore in set theory, and can be found, 82e.g., in the textbook \cite{card-book}. Beyond taking care of some locality aspects 83concerning the spreading of our concepts throughout types, we have not departed 84much from the techniques used in set theory for establishing these facts -- for instance, 85in the proof of one of our major theorems, 86\textit{Card-order-Times-same-infinite} from Section 8.4,\footnote{This theorem states that, for any 87infinite cardinal $r$ on a set $A$, $|A\times A|$ is not larger than $r$.} 88we have essentially applied the technique described, e.g., in the proof of 89theorem 1.5.11 from \cite{card-book}, page 47. 90 91Here is the structure of the rest of this document. 92 93The next three sections, 2-4, develop some 94mathematical prerequisites. 95In Section 2, a large collection of simple facts about 96injections, bijections, inverses, (in)finite sets and numeric cardinals are proved, 97making life easier 98for later, when proving less trivial facts. 99Section 3 introduces upper and lower 100bounds operators for order-like relations and studies their basic properties. 101Section 4 states some useful variations of well-founded recursion and induction principles. 102 103Then come the major sections, 5-8. 104Section 5 defines and studies, in the context of a well-order relation, 105the notions of minimum (of a set), maximum (of two elements), supremum, successor (of a set), 106and order filter (i.e., initial segment, i.e., downward-closed set). 107Section 6 defines and studies (well-order) embeddings, strict embeddings, isomorphisms, and 108compatible functions. 109Section 7 deals with various constructions on well-orders, and with the relations 110$\leqo$, $\lesso$ and $\eqo$ of well-order embedding, strict embedding, and isomorphism, respectively. 111Section 8 defines and studies cardinal order relations, the cardinal of a set, the connection 112of cardinals with set-theoretic constructs, 113the canonical cardinal of natural numbers and finite cardinals, the successor 114of a cardinal, as well as regular cardinals. (The latter play a crucial role in the development of 115a new (co)datatype package in HOL.) 116 117Finally, section 9 provides an abstraction of the previous developments on 118cardinals, to provide a simpler user interface to cardinals, which in most of 119the cases allows to forget that cardinals are represented by orders and use them 120through defined arithmetic operators. 121 122More informal details are provided at the beginning of each section, and also at the 123beginning of some of the subsections. 124