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.
The first uncountable ordinal
Definition
The first uncountable ordinal is
the Hartogs number of (Hartogs: an ordinal that does not inject into a given set, The natural numbers (von Neumann)): the least ordinal (Ordinal (von Neumann)) that admits no injective function into . Equivalently, by that theorem, is the set of order types of the well-ordered subsets of .
Existence is a theorem of ZF. Hartogs: an ordinal that does not inject into a given set is choice free, so is available without any choice principle, and its defining property needs none either.
"Uncountable" is Finite, countably infinite, countable, uncountable's word, meaning "not at most countable", and it is not redefined here. That deserves the name — that it is uncountable, that every ordinal below it is at most countable, that it is a cardinal and a limit ordinal — is proved in is uncountable, every ordinal below it is at most countable, it is a cardinal and a limit ordinal, and its existence is a theorem of ZF ↗, which is what discharges the naming obligation of this definition.
Remarks
-
Why the Hartogs number and not "the least uncountable ordinal" outright. Taking the least element of the collection of uncountable ordinals presumes that collection is nonempty, which is precisely the content of Hartogs: an ordinal that does not inject into a given set; and that collection is a proper class, so the least element has to be produced by the argument of that theorem rather than by Trichotomy and well-ordering of the ordinals applied to a set. Defining as makes the existence explicit and keeps the definition inside ZF.
-
. injects into by the identity, so ; and would make inject into , which Hartogs: an ordinal that does not inject into a given set forbids. So by Trichotomy and well-ordering of the ordinals, and in particular is strictly above the least limit ordinal ( is the least limit ordinal).
-
Notation and reading order. The cardinal notation is not used on this page or in the ordinal development because the aleph hierarchy is not available at this point in the reading order; every statement here is written with . The later The successor cardinal , the alephs , the beths , successor and limit cardinals, and the identifications and ↗ constructs the hierarchy and proves . Nothing on the present page needs that later notation.
-
Without a choice principle can behave strangely, and it still exists. Its existence never fails, but statements about its cofinal structure do need countable choice; the accounting is in Choice ledger for this page: exists in ZF, and the boundedness theorem does not.