How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Cardinal (initial ordinal) and cardinality
Definition
Write , and say and are equinumerous, when there is a bijection .
An ordinal (Ordinal (von Neumann)) is a cardinal, equivalently an initial ordinal, when
that is, is not equinumerous with any strictly smaller ordinal.
Cardinality, under the Axiom of Choice. Assume the Axiom of Choice (The Axiom of Choice) and let be a set. Then carries a well-order (The well-ordering theorem), which has an order type (Every well-order has a unique order type) and in particular . Now is an ordinal (Basic closure properties of ordinals, claim (c)) whose elements are ordinals (claim (a)) and which contains , so is a nonempty set of ordinals and has an -least element (Trichotomy and well-ordering of the ordinals). This is the cardinality of , written ; it is a cardinal, because with would lie in and contradict the minimality of .
Well-definedness: does not depend on the well-order or on . The recipe above instantiates a well-order of and an order type for it, and will in general carry many well-orders with many different order types, so the value has to be shown independent of both. It is, because is in fact the least ordinal equinumerous with outright, a description in which neither the well-order nor appears. Let be any ordinal with . By trichotomy for ordinals (Trichotomy and well-ordering of the ordinals) exactly one of , , holds. In the first case , so by minimality of . In the other two cases claim (f) of Basic closure properties of ordinals gives , and because , so and hence by claim (f) again; and , so by minimality, whence . In every case , that is . So is the least element of the collection of all ordinals equinumerous with , and any two runs of the recipe, from any two well-orders of , return the same .
Remarks
-
What the well-definedness argument does and does not need. The obligation is that depend on alone, and it is discharged in the definition itself, from two lemmas that are genuine prerequisites of this item and therefore sit in
depsrather than injustified_by: comparability and trichotomy of ordinals (Trichotomy and well-ordering of the ordinals) and the elementary closure facts (Basic closure properties of ordinals). Neither mentions cardinals, so neither points forward, and no separate discharging lemma is needed. The bound is a device for turning "the least ordinal equinumerous with " into a Separation instance over a set; the argument above is what shows that the device does not change the answer. -
The definition is choice-free; the cardinality assignment is not. Being a cardinal is a property of an ordinal and needs no axiom beyond ZF. Attaching a cardinality to an arbitrary set is a different matter: a set that carries no well-order is equinumerous with no ordinal at all, so simply does not exist for it. Without the Axiom of Choice there is no ordinal-valued notion of size for arbitrary sets, and what survives is Hartogs: an ordinal that does not inject into a given set: every set has a smallest ordinal that does not inject into it.
-
Most ordinals are not cardinals. The successor is equinumerous with , by the explicit bijection sending to and each natural number to , which is a bijection because is injective and its image is exactly the nonzero natural numbers. So is an ordinal and not a cardinal, and the same shift applies to the successor of any ordinal containing . Cardinals are sparse among ordinals, which is precisely why the least one equinumerous with a given set is a useful representative.
-
Which ordinals up to and including are cardinals. Every natural number is a cardinal, and so is . Both facts are counting facts rather than order facts, and both come from the pigeonhole principle (The pigeonhole principle on ), proved on the countability page. Every natural number is an ordinal, and so is ( is the least limit ordinal, claim (ii)); and if with a natural number then is itself a natural number, since is a transitive set (On the order is membership: ), with by claim (i) of is the least limit ordinal. So if some had , claim 3 of the pigeonhole principle would force and hence , which claim (b) of Basic closure properties of ordinals forbids; therefore is a cardinal. And if some had , then would be a natural number equinumerous with , which claim 4 of the pigeonhole principle forbids; therefore is a cardinal. Nothing else on this page depends on either fact, and the definition above is stated so that it does not.
-
Notation. The infinite cardinals are traditionally written , with . That last equation can now be stated outright rather than quoted: it says is the least ordinal equinumerous with , which is precisely the assertion that is a cardinal, established in the previous remark from claim 4 of The pigeonhole principle on . Nothing below rests on it. The notation for the Hartogs number of (Hartogs: an ordinal that does not inject into a given set) comes from the same source and is deliberately close: under the Axiom of Choice is the successor cardinal of .
-
Why initial ordinals rather than equivalence classes. For a nonempty set , the class of all sets equinumerous with is a proper class. Indeed, fix . For each set , the set is equinumerous with , by replacing with and fixing the other elements. If the equinumerosity class were a set , its union would therefore contain every set outside and also every member of , since . Thus would contain every ordinal, contrary to Burali-Forti: there is no set of all ordinals. The empty set is the exception: its equinumerosity class is the set . Choosing the least ordinal in an equinumerosity class is von Neumann's fix, and it works exactly when the class contains an ordinal, which is exactly when the set can be well ordered.
Depends on
Ordinal (von Neumann)
Basic closure properties of ordinals
Trichotomy and well-ordering of the ordinals
Every well-order has a unique order type
The well-ordering theorem
Hartogs: an ordinal that does not inject into a given set
The Axiom of Choice
is the least limit ordinal
On the order is membership:
The pigeonhole principle on
Burali-Forti: there is no set of all ordinals