Cohen 1963: ZF does not prove the Axiom of Choice

If ZF is consistent, then ZF + (not AC) is consistent. Equivalently: if ZF is consistent, then ZF does not prove the Axiom of Choice.

Cohen (1963, 1964) proves this by inventing forcing. Starting from a countable transitive model $M$ of ZF, one adjoins a generic object, here a set of "Cohen reals" indexed by $\mathbb{N}$, and then passes to the symmetric submodel of the resulting extension: the sets kept are those whose names are invariant under a large group of permutations of the indices, in the sense of a fixed normal filter of subgroups. The symmetric model satisfies every axiom of ZF, and it contains the set $A$ of adjoined reals as a set with no well-ordering. In particular no choice function exists for the family of nonempty subsets of $A$, so AC fails there.

Together with Gödel 1938: ZF does not refute the Axiom of Choice ‡ this makes the Axiom of Choice independent of ZF, again relative to the consistency of ZF: neither AC nor its negation is a theorem of ZF, unless ZF is inconsistent, in which case it proves everything.

• Not proved in this library. Neither forcing nor the symmetric-model construction is developed here. The description above fixes what the statement says; it is not a proof and is not a sketch that could be completed with the material in this library.

• What would prove it. A forcing track: partial orders and dense sets, Boolean-valued models or names and the forcing relation, genericity and the truth lemma, then symmetric extensions and normal filters of subgroups. A second, older route reaches the same conclusion for ZF with atoms (Fraenkel-Mostowski permutation models) and transfers it to ZF by the Jech-Sochor embedding theorem. Neither route is in this library.

• Why it matters here. Zorn's lemma and the well-ordering theorem are each equivalent to the Axiom of Choice over ZF (The Axiom of Choice and Zorn's lemma are equivalent ↗), so the later forcing proof will transfer the same nonprovability conclusion to them. No Foundations proof uses that conclusion as a premise.

• Conditional discipline. "ZF does not prove AC" always abbreviates the implication above. Nothing in this library asserts the unconditional form, which is not available: by Gödel's second incompleteness theorem the consistency of ZF cannot be proved in ZF.