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

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?

-

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.

-

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.

-
But unless you involve forcing, the pure sets remain choicey. Which I think is what the question was coming from. – Asaf Karagila Jan 10 '13 at 9:27
@Asaf: I think we might have deciphered the question differently. I interpreted it as "Sure, AC might fail here, but this is such a special case! How do we know that AC is really really independent of ZF(A)?" – arjafi Jan 10 '13 at 9:31
Oh, that is how I understood is as well at first (see my first two lines). But then I saw it asked about passing from atoms to ZF. So I added another line. – Asaf Karagila Jan 10 '13 at 9:34