Prove2Me

GCH implies CH (over ZFC)

Proved
ContinuumHypothesis.gch_sentence_implies_ch_sentence

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

model-theoryset-theory

The continuum hypothesis is the special case S=ωS=\omega of the generalized continuum hypothesis: every model of

ZFC+GCH\mathrm{ZFC}+\mathrm{GCH}

satisfies CH\mathrm{CH}.

Together with Gödel's consistency theorem this gives Con(ZF)⇒Con(ZFC+CH)\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{CH}).

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

theorem gch_sentence_implies_ch_sentence : (ZFC ∪ {gchSentence}) ⊨ᵇ chSentence := by sorry

end ContinuumHypothesis
Source
Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Generalized continuum hypothesis' ('The continuum hypothesis is the special case for the ordinal α = 1', 'As GCH implies CH, …').
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