The continuum hypothesis is independent of ZFC

Identifier: F:continuum-hypothesis-independent
Proof route: Not assigned
External status: proved
Axiom footprint: Empty

Recorded description

If ZFC is consistent, then ZFC neither proves nor refutes the statement that every infinite set of real numbers is in bijection either with the natural numbers or with the reals.

Formal statement

; NOT EXPRESSIBLE, on two independent counts. The statement quantifies over subsets of the reals, which is second order and outside any SMT-LIB logic; and the independence claim is about derivability in ZFC, which needs the same reflection machinery F:godel-first-incompleteness names. axeyum's Real sort is a first-order ordered field with no set-of-reals sort and no cardinality apparatus.

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

Provenance

{
  "date": "2026-08-14",
  "established_by": "not established in this ledger",
  "source": "authored from the S:logic-and-proof strand of the math-education concept graph; statement written here, not copied",
  "prior_art": [
    {
      "citation": "Godel 1940 (consistency of CH); Cohen 1963 (consistency of not-CH)",
      "establishes": "the independence, long settled"
    }
  ]
}