Cohen: Con(ZFC) $\Rightarrow$ Con(ZFC + $\neg$ CH)

Proved

ContinuumHypothesis.cohen_consistency_not_CH

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

forcingindependenceset-theory

(Cohen, 1963.) If $\mathrm{ZFC}$ is consistent, then so is $\mathrm{ZFC}$ together with the negation of the continuum hypothesis:

\mathrm{Con}(\mathrm{ZFC})\ \Longrightarrow\ \mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH}).

Hence CH cannot be proved 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 cohen_consistency_not_CH (hZFC : ZFC.IsSatisfiable) :
    (ZFC ∪ {∼chSentence}).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 3 ('Cohen showed that CH cannot be proven from the ZFC axioms … he developed the method of forcing'); Cohen, PNAS 50 (1963), 51 (1964).

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

Cohen: Con(ZFC) ⇒\Rightarrow⇒ Con(ZFC + ¬\neg¬CH)

Cohen: Con(ZFC) $\Rightarrow$ Con(ZFC + $\neg$ CH)