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 continuum hypothesis and the later local consistency results
Remark
By Cantor's theorem: there is a strict gap (Equinumerous sets, and ). In particular is uncountable (Finite, countably infinite, countable, uncountable), since a surjection would exist if it were at most countable (A nonempty set is at most countable iff it is a surjective image of ) and the theorem forbids one; and so, by a completely different argument, is ( is uncountable (Cantor's nested intervals, 1874)). The obvious next question is whether anything sits strictly in between.
The continuum hypothesis (CH) asserts that nothing does:
there is no set with .
Over ZFC this is equivalent to: every uncountable subset of is equinumerous with itself. The qualification matters. Passing from the displayed form to the subset form uses choice to well order an uncountable and obtain . Nothing here asserts that this passage is available in ZF; only the displayed form is used below. Determining the exact choiceless relationship between the formulations belongs to the later symmetric-model development.
Later local consistency results. Positive relative consistency of CH and GCH ↗ proves that implies consistency of both and . Externally fixed-fragment relative consistency of not CH and not GCH ↗ proves, as an external metatheorem using a separate construction for each fixed finite fragment, the corresponding consistency implications for not CH and not GCH. Its contract claims no PA proof of a uniform refutation transformer. Together these imply that, if ZFC is consistent, it decides neither CH nor GCH: a proof of either sentence would contradict consistency of the extension by its negation.
What this page has not proved. CH is usually stated about : that every uncountable set of reals is equinumerous with . That form is equivalent to the one above only once one knows , which this library now proves, in ZF, on a later page. At this point in the reading order, though, the two uncountability results on this page are still genuinely separate facts: is uncountable by the diagonal argument, and is uncountable by nested intervals, and the bridge between them is not available here — it needs binary expansions, which are developed much later, on the same later page. Nothing on this page depends on that bridge.
The countability results have their own proofs. Countability of , uncountability of and of the irrationals, and Cantor's theorem on this page are proved without a choice axiom. The later consistency comparisons are not premises of those arguments.
The generalised continuum hypothesis (GCH) asserts that there are no infinite and set with . It implies CH by its instance at , since is infinite by claim 4 of The pigeonhole principle on . The later Sierpiński: arbitrary-set GCH implies AC in ZF ↗ proves in ZF that this arbitrary-set formulation of GCH implies AC. This implication uses no consistency assumption and is distinct from the two consistency comparisons.