Prove2Me

Sierpiński: ZF + GCH ⊢\vdash AC

Open
ContinuumHypothesis.sierpinski_gch_implies_ac

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

axiom-of-choicemodel-theoryset-theory

(Sierpiński, 1947.) The generalized continuum hypothesis implies the axiom of choice over ZF: every model of

ZF+GCH\mathrm{ZF}+\mathrm{GCH}

satisfies AC\mathrm{AC}. Here GCH is the choice-free form: for every infinite SS, every TT with ∣S∣≤∣T∣≤∣P(S)∣|S|\le|T|\le|\mathcal P(S)| is equinumerous with SS or with P(S)\mathcal P(S).

So there are no models of ZF in which GCH holds and AC fails.

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

theorem sierpinski_gch_implies_ac : (ZF ∪ {gchSentence}) ⊨ᵇ acSentence := 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', paragraph 3 ('Sierpiński proved that ZF + GCH implies the axiom of choice (AC)'); Gillman, Amer. Math. Monthly 109 (2002).
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