A recent question (What is an example of model of ZF with a countable family of pairs whose union is uncountable?) has gotten me interested in permutation models again. It's been a while since I've done set theory and I'd like to read up on permutation models to refresh my understanding of the details.
I'm particularly interested if there's a direct way of going from relative consistency arguments with ZF+urelements to relative consistency arguments with ZF. It seems like there might be a compactness-like argument for this.
I'm currently working through Felgner's "Models of ZF-Set Theory", but are there any other sources I should be looking at?
The canonical answer is, of course, Jech "The Axiom of Choice", which also includes a fairly robust transfer theorem which lets you move some of the consistency results of $\sf ZF$. These are briefly covered in the "Set Theory" book as well, although not to the same level and with a lot less examples.
The Jech–Sochor theorem is good for moving results that are local, in the sense "There is some counterexample", but not so good at moving results which are global like Boolean Prime Ideal theorem, Dependent Choice, or even "Every set is the image of a Dedekind-finite set".
For these you need to get your hands dirty with Pincus' transfer theorem
This paper is quite hard to read, and it relies on a previous paper
whose MathSciNet review concludes with "{This paper can be read only by the most determined readers, partly because of the many misprints and inaccuracies in it.}"
There is another approach using forcing based on Blass–Scedrov, e.g. the following manuscript,
which was developed further by Blass' Ph.D. student, Eric Hall, for example
But now that I have your attention. I often felt that the correct approach to transferring the results from $\sf ZFA$ to $\sf ZF$ is to simply repeat the relevant proof using forcing. Most of the transfer theorems are kind of "fixed into their mechanism". For example, it was the observation of a great many set theorists that an infinite set of Cohen reals (or Cohen subsets of some $\kappa$) is somewhat like an atom, in that any two such sets are going to satisfy the same statements.
This allows you to view symmetric extensions, the methods by which we construct models of $\sf ZF$ without choice, in their own right. This also lets you control small things like the rank in which choice fails, the degree of failure of Kinna–Wagner Principles, etc.
Some technical work is still missing there, of course. Preservation theorems for the Boolean Prime Ideal Theorem, for example, or for weak choice principles like countable choice, etc. But that's why this is exciting, there's so much left to do!