How does Fraenkel's urelement proof show choice is independent of ZF?

Question

I understand the actual proof Fraenkel gives but I can't see how it proves choice independent of the full ZF because he works in a very restricted universe. Can anyone show how to connect one to the other?

Answer 1

The proof is that if ZFC+Atoms has a model then ZF+$\lnot$AC+Atoms is consistent.

Therefore we cannot prove the axiom of choice from the axioms of ZF+Atoms.

The removal of atoms did not occur for another 40 years until Cohen developed forcing, and Gödel proved that the axiom of choice does not add contradictions to ZF.

Answer 2

To show that AC is independent of ZF (or ZFA as was done in Fraenkel's model) you just need to construct of model of ZF(A) in which the Axiom of Choice fails. By Godel's Completeness Theorem, it follows that AC cannot be proven from ZF(A) (unless ZF(A) is inconsistent).

The exact structure of the model is unimportant: we don't need "all sets" to be present (whatever that means). All that matters is that the usual axioms of ZF(A) are satisfied within the model and that AC fails (using the usual model-theoretic notion of satisfaction).

Also, I do not think I say too much by asserting that Fraenkel's much less restrictive than Godel's Constructible Universe, which was used to show the relative consistency of AC to ZF.