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.
Depends on
Used by
- Refuted, assuming countable choice: every Hausdorff space built from ordinal spaces is normal. The deleted Tychonoff plank ((ω₁ + 1) × (ω + 1)) ∖ {(ω₁, ω)} is Hausdorff and not normal Counterexample
- Refuted: every limit ordinal has an at most countable cofinal subset — ω₁ has none, assuming countable choice Counterexample
- The closed long ray ω₁ × [0,1) under the lexicographic order, and the long line, with the order topology Definition
- The successor cardinal κ⁺, the alephs ℵ_α, the beths ℶ_α, successor and limit cardinals, and the identifications ℵ₀ = ω and ℵ₁ = ω₁ Definition
- Assuming countable choice, a strictly increasing ω-sequence of countable ordinals has a countable supremum, which is a countable limit ordinal below ω₁; the instance supₙ ω·(n+1) = ω² needs no choice Example
- Assuming countable choice, cf(ℵ_ω₁) = ℵ₁, so singular does not mean of countable cofinality Example
- The long ray is connected and locally connected, every proper initial segment is order-convex and connected, and, assuming countable choice, no at most countable subset is cofinal Example
- ω + 1 as a convergent sequence together with its limit, and, assuming countable choice, [0, ω₁), in which every sequence lies inside an at most countable initial segment Example
- ℵ₁ ≤ 2^ℵ₀ under the Axiom of Choice, because 2^ℵ₀ is a cardinal strictly above ℵ₀ and ℵ₁ is the least such; so ω₁ injects into ℝ Example
- FALSE: every countably compact space is compact False statement
- FALSE: every sequentially compact space is compact False statement
- Choice ledger for this page: ω₁ exists in ZF, and the boundedness theorem does not Remark
- Assuming countable choice: every at most countable subset of ω₁ is bounded below ω₁, so no at most countable subset of ω₁ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable Theorem
- Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, ω₁ is countably compact and sequentially compact while ω₁ + 1 is compact Theorem
- The long ray is a linear continuum, hence connected; every one of its at most countable subsets is bounded above, assuming countable choice Theorem
- ω₁ 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 Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 51 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- First uncountable ordinal (Wikipedia) (standard reference, not scraped)
- Hartogs number (Wikipedia) (standard reference, not scraped)
- T. Jech, Set Theory, 3rd millennium ed., Ch. 3 (Cardinal numbers) (standard reference, not scraped)