Prove2Me

Gödel: Con(ZF) ⇒\Rightarrow Con(ZFC + GCH)

Proved
ContinuumHypothesis.goedel_consistency_AC_GCH

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

constructible-universeindependenceset-theory

(Gödel, 1938/1940.) If ZF\mathrm{ZF} is consistent, then so is ZF\mathrm{ZF} together with the axiom of choice and the generalized continuum hypothesis:

Con(ZF) ⟹ Con(ZFC+GCH).\mathrm{Con}(\mathrm{ZF})\ \Longrightarrow\ \mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH}).

In particular CH (a consequence of GCH) cannot be disproved in ZFC.

Formalization Note Consistency is satisfiability of the first-order theory (equivalent by the completeness theorem).

Preamble
import Definitions.Def_CH_ZFC
open FirstOrder FirstOrder.Language
Formal statement
namespace ContinuumHypothesis

theorem goedel_consistency_AC_GCH (hZF : ZF.IsSatisfiable) :
    (ZFC ∪ {gchSentence}).IsSatisfiable := by sorry

end ContinuumHypothesis
Source
Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Independence from ZFC', paragraph 2 ('His proof shows that both CH and AC hold in the constructible universe L') and section 'Generalized continuum hypothesis' ('Kurt Gödel showed that GCH is a consequence of ZF + V=L … and is therefore consistent with ZFC'); Gödel 1938, 1940.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph