Sorry if this sounds like a silly reference request, but I wasn't able to track down any. I'm looking for proof, via forcing, that axiom of choice can fail in a model of $ZF$. All of papers I found where either proving something more sophisticated or, if it was some introductory paper/book, it showed that $\neg CH$ is consistent relative to $ZFC$.


Again, sorry if this question sounds silly, but I would appreciate any help!


Thanks in advance!



Forcing $\neg AC$
This is difficult to prove using forcing, for one simple reason.


If $M\models\sf ZFC$, and $G$ is an $M$-generic filter (for some forcing notion), then $M[G]\models\sf ZFC$.


In other words, the only way to use forcing to have a model where the axiom of choice fails, is if the ground model was such that the axiom of choice failed. But it's worse than that, not only that you can't violate the axiom of choice with forcing, *sometimes* you can force it back. So sometimes, even if the axiom of choice failed in $M$, it might still hold in $M[G]$.




---


In order to use forcing to construct models where the axiom of choice fails you need to first use forcing, and then reduce to an inner model, either by relative constructibility arguments, or by a technique called symmetric extensions. The two have deep connections between them.


You can find both covered in Jech **Set Theory** (chapters 13 through 15 include the relevant information), and in his book **The Axiom of Choice** which covers symmetric extensions nicely with plenty of uses.


Other sources may also include Ioanna Dimitriou's Ph.D. thesis which has a very nice introduction to symmetric extensions.


