Gödel 1938: ZF does not refute the Axiom of Choice

If ZF is consistent, then ZF + AC + GCH is consistent. Here AC is the Axiom of Choice and GCH is the generalised continuum hypothesis.

Equivalently, and this is the form the library uses: if ZF is consistent, then ZF does not refute the Axiom of Choice, and ZFC does not refute GCH.

The witness is an inner model. Gödel (1938) defines the class $L$ of constructible sets by transfinite recursion along the ordinals, $L_0=\mathrm{\varnothing },L_{\alpha +1}=\mathrm{D}\mathrm{e}\mathrm{f}(L_{\alpha }),L_{\lambda }={\bigcup }_{\alpha <\lambda }{L}_{\alpha }\text{ for limit }\lambda ,L={\bigcup }_{\alpha \in \mathrm{O}\mathrm{r}\mathrm{d}}{L}_{\alpha },$ where $\mathrm{D}\mathrm{e}\mathrm{f}(X)$ is the set of subsets of $X$ definable over $(X,\in )$ with parameters from $X$. Working inside any model of ZF, one shows that $L$ satisfies every axiom of ZF, and in addition satisfies AC and GCH. Since a model of ZF yields a model of ZF + AC + GCH, the consistency of the second follows from the consistency of the first.

The conclusion is relative: it is an implication between consistency statements, not a proof that ZFC is consistent. If ZF is consistent, Gödel's second incompleteness theorem prevents ZF from proving its own consistency; a stronger metatheory may of course prove the antecedent.

• Not proved in this library. Nothing about $L$ is developed here. The definition above is recorded so the statement is precise, not as a construction this library carries out.

• What would prove it. The theory of the constructible universe: the definability operator $\mathrm{D}\mathrm{e}\mathrm{f}$, absoluteness of ${\mathrm{\Delta }}_0$ formulas, the reflection and Löwenheim-Skolem arguments behind the condensation lemma, and from condensation the two consequences that $L$ has a definable global well-ordering (giving AC) and that every constructible subset of $L_{{\omega }_{\alpha }}$ appears by stage ${\omega }_{\alpha +1}$ (giving GCH). That is an inner-model track, and this library has not built it.

• Why it matters here. This is the positive consistency half of the later independence theorem. Results proved from The Axiom of Choice ↗ do not use this metatheorem as a premise; the constructibility track must establish it from earlier local machinery before the catalogue can be retired. Its partner is Cohen 1963: ZF does not prove the Axiom of Choice ‡.

• Conditional discipline. The statement is never asserted unconditionally in this library. "ZF does not refute AC" is shorthand for the implication above, whose antecedent is the consistency of ZF.