Alphabeta Math
RemarkRemark: AI-adaptedProof: Not applicable
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: A≺P(A) there is a strict gap N≺P(N) (Equinumerous sets, A≈B and A⪯B). In particular P(N) is uncountable (Finite, countably infinite, countable, uncountable), since a surjection N→P(N) would exist if it were at most countable (A nonempty set is at most countable iff it is a surjective image of N) and the theorem forbids one; and so, by a completely different argument, is R (R 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 A with N≺A≺P(N).

Over ZFC this is equivalent to: every uncountable subset of P(N) is equinumerous with P(N) itself. The qualification matters. Passing from the displayed form to the subset form uses choice to well order an uncountable A⊆P(N) and obtain N≺A. 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 Con⁡(ZFC) implies consistency of both ZFC+CH and ZFC+GCH. 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 R: that every uncountable set of reals is equinumerous with R. That form is equivalent to the one above only once one knows R≈P(N), 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: P(N) is uncountable by the diagonal argument, and R 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 Q, uncountability of R 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 A and set B with A≺B≺P(A). It implies CH by its instance at A=N, since N is infinite by claim 4 of The pigeonhole principle on N. 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.

Depends on

Dependency tree · 2 levels

Sources