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!
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.
As Asaf wrote, the usual construction of models of $\neg AC$ consists of forcing followed by passing to an inner model. There is, however, an alternative construction that might be closer to what you're looking for. One can begin with a model of ZFC and first construct a model of ZFCA, a modification of ZFC that allows for atoms, which are not sets but can be elements of sets. With an infinite set of atoms, one can use the method of permutation models, pioneered by Fraenkel in 1922, to build submodels that satisfy ZFA but not the axiom of choice. (These are the permutation models described in Chapter 4 of Jech's "Axiom of Choice" book.) Then one can force over such a permutation model in such a way that the pure part of the resulting forcing extension (i.e., the submodel consisting of the sets that don't involve any atoms in their transitive closures) is a model of ZF (without atoms) violating choice.
In other words, one can do the symmetrization before forcing, rather than afterward. Then the symmetry involves just permutations of atoms rather than automorphisms of a complete Boolean algebra.
For a specific example: If you take the basic Fraenkel model (as defined in Jech's book) and force, in the usual way (finite partial functions), a family of mutually generic Cohen reals indexed by the atoms, then the pure part of the resulting forcing extension is the basic Cohen model (as defined in Chapter 5 of Jech's book).
This approach to the independence of AC from ZF is used, for example, in the book "Theory of Semisets" by Vopenka and Hajek. (Unfortunately, I think the only way to read that book is straight through from the beginning; if you try to look up a particular result in it, you'll find that it depends on so much prior notation that you'll have to read practically everything that precedes the result you want.)
