Forcing over models without the axiom of choice In the vast majority of papers forcing is always developed over ZFC.
Not surprisingly too, since infintary combinatorial principles are often used to prove results based on properties such as chain conditions, closure, and so on.
I am looking for a good start on forcing over models of ZF. I have before me two papers which I have yet to read thoroughly, however may not be as useful for this purpose as I am hoping.


*

*Grigorieff, S. Intermediate Submodels and Generic Extensions in Set Theory. The Annals of Mathematics, Second Series, Vol. 101, No. 3 (May, 1975), pp. 447-490

*Monro, G. P. On Generic Extensions Without the Axiom of Choice. The Journal of Symbolic Logic, Vol. 48, No. 1 (Mar., 1983), pp. 39-52


While I do intend to read them either way, it seems that neither develops the theory of forcing in the absolute absence of choice. I am currently looking for references which deal with such situation, or with the relation between forcing theorems proved in ZFC and the amount of choice needed for them to hold.
Edit: I probably should have mentioned that I am quite familiar with permutation models of ZFA+embedding theorems and transfer theorems (Jech-Sochor, Pincus' theorem) as well with symmetric extensions. 
I am not looking for ways to develop forcing extensions of ZF without the axiom of choice; rather I am looking for theorems such as c.c.c forcing does not collapse cardinals and similar theorems extended to the choiceless contexts if possible, or the strength of choice needed for these theorems to hold.
Consider two examples:


*

*Suppose a model of ZF in which the axiom of choice does not hold. Can we, by set forcing add the axiom of choice? If not, can it be done using a machinery similar to a symmetric extension? If we can in fact find such extension, does that mean the model without choice is a symmetric extension between two larger models?

*Suppose A is an infinite Dedekind-finite set, what can we say on a forcing poset based on A (either domain of functions are partial to A or the range is in A)? Can we "collapse" amorphous sets onto ordinals? Can we collapse one amorphous set onto another? And so on.
 A: Friedman's book "Fine structure and class forcing" develops forcing over ZF, rather than ZFC, in chapter 2. Although chapter 1 is about fine structure, it is not used in chapter 2. Although the rest of his book is well above my level, I find Friedman's exposition of forcing quite helpful.
A: Arnie Miller's "Long Borel hierarchies" specifically pp 8-12 may be of interest for you. 
See here
A: The book "Theory of Semisets" by Vopenka and Hajek contains forcing constructions over models that violate AC.  For one example: Start with the basic Fraenkel model (of ZF with atoms, ZFA --- I'm using here the terminology of Jech's "Axiom of Choice" book); it has an infinite Dedekind-finite set $A$ of atoms.  Adjoin an $A$-indexed family of Cohen reals, by forcing with finite partial functions from $A\times\omega$ to 2.  The pure part of the resulting model is the basic Cohen model.  (In other words, instead of the usual procedure of passing to a symmetric submodel of a forcing extension, you can equivalently start with symmetry in the ground model and then just force.)  This is how Vopenka and Hajek introduce the basic Cohen model.
Unfortunately, I think the only way to read the Vopenka-Hajek book is straight through from the beginning, because there's a lot of notation and terminology that will make no sense if you just open the book to the chapter you're interested in.
Another nice example of forcing over choiceless models of ZFA is that Mostowski's linearly ordered model of ZFA can be obtained from the basic Fraenkel model by adding a generic linear ordering of $A$ with finite conditions.
I second Francois's suggestion to look into Eric Hall's work, which builds on ideas like these and takes them a good deal farther.
A: You may want to look at Eric Hall's papers.
Regarding your question 1, I think that if $M$ is a model of SVC with $S$ (see Blass, Injectivity, projectivity, and the axiom of choice, TAMS 255), then you can force AC by wellordering the set $S$ using finite functions from $\omega$ into $S$. On the other hand, if you can force AC with a poset $P$ then the original model should satisfy SVC with $P$. So it looks like SVC is the key to force AC (unless you allow class forcing).
Regarding your question 2, forcing with finite injections from a $\omega$ to any set $A$ which is of greater cardinality than every finite ordinal will force a bijection between $\omega$ and $A$. I suppose you could do the same to force a bijection between any two given sets $A$ and $B$ by using finite partial injections from $A$ into $B$, provided this poset satisfies the obvious density requirements. However, this might accidentally force both sets to lose certain properties.
A: Here is an equivalence of a forcing principle to the Axiom of Choice, courtesy of Arnold Miller, found in his preprint, "The maximum principle in forcing and the axiom of choice":

(Abstract) In this paper we prove that the maximum principle in forcing [ $p$ $\Vdash$ $\exists$$x$ $\theta$($x$)  iff  there exists a a name $\tau$  such that $p$ $\Vdash$ $\theta$($\tau$)--my quote from Miller's preprint, found on his homepage at www.math.wisc.edu/~miller/] is equivalent to the axiom of choice.  We also look at some specific partial orders in the basic Cohen model [his model in which the axiom of choice fails].

This paper also discusses partial orders in Cohen's original model for which the maximum principle fails and one (at the end of this paper) for which the maximum principle succeeds.
It would be interesting to find out what difficulties (if any) the absence of the maximum principle causes for forcing in $ZF$ (and if these difficulties could be overcome).
