Suppose $V\models ZFC$ and $P\in V$ is a poset of forcing conditions.

It is a basic theorem in forcing that $V[G]\models ZFC$ for any generic extension by a $V$-generic filter $G$.

It is also known that if $V\subseteq M\subseteq V[G]$, and $M\models ZFC$ then $M$ is a forcing extension of $V$ and $V[G]$ is a forcing extension of $M$.

Now, consider $V[G]$ to be some generic extension. We can define in $V[G]$ a transitive subclass which is a model of $ZF$, but often not of $AC$. This is done by considering some permutation group of the forcing conditions and taking only names which obey some condition. The interpretation of this class of special names is called a *symmetric extension* of $V$.

In most interesting cases the symmetric extension negates the axiom of choice one way or another. ~~This doesn't sit right with the two theorems mentioned above, since if $M$ is actually a generic extension of $V$ then the axiom of choice should hold in $M$, but it does not.~~ (This is nullified by the correction points by Andreas Blass and Amit Kumar Gupta in the comments).

*Edit:* Instead of the above, then, how much choice is needed to have the second theorem stated in $ZF$ alone? does that depend on the forcing $P$ at hand? If the answer is that the theorem is nontransferable?

The way I see it negative answers would mean at least one of two possible things:

We consider $V$ as a model of $ZF$ and by some forcing which preserves only $ZF$ we obtain $M$ as the generic extension, this is similar to the way we may violate the continuum hypothesis or collapse the continuum to be $\aleph_1$, and so change the truth value of an unprovable statement (very much like $AC$ is unprovable from $ZF$).

$M$ can be achieved by class forcing. I have very little intuition on that topic, so I cannot see any reason why this may be either true or false.

Is my intuition correct?

While we're on the topic, I do recall forcing is indeed possible without choice, but that should require extra assumptions or different methods to handle the genericity. Is there a good introduction to the topic available?

`$M = V \cup \{G\}$`

then not only is $M$ not a forcing extension of $V$, it fails spectularly to satisfy ZFC, for instance it fails to satisfy pairing, power set, and separation. – Amit Kumar Gupta Sep 1 '11 at 22:28