Symmetric extensions and class forcing

Question

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:

1. 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$).

2. $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?

Answer 1

These intermediate model questions were thoroughly investigated by Serge Grigorieff in Intermediate Submodels and Generic Extensions in Set Theory [Annals of Mathematics 101 (1975), 447-490].

The basic result of the kind you are looking for is due to Solovay (according to Grigorieff):

Let $P$ be a poset in $M$, a model of ZF, and let $G$ be $P$-generic over $M$. If $a \in M[G]$ contains only elements of $M$, then $M[a]$ is a generic extension of $M$ and $M[G]$ is a generic extension of $M[a]$.

This is similar to what you state, but note the special form of the intermediate model. In fact, the intermediate models of ZF between $M$ and $M[G]$ that are generic extensions of $M$ are precisely those of the form $M[a]$ as described above.

When $M$ satisfies ZFC, then any intermediate model of ZFC between $M$ and $M[G]$ is of the form $M[a]$ for some set of ordinals $a \in M[G]$. Thus, your stated result does hold provided that all models involved satisfy ZFC.

Since you mentioned symmetric models in the questions, note that Grigorieff goes on to classify all of those too:

The symmetric submodels of $M[G]$, are all intermediate models of the form $(HOD\ M[a])^{M[G]}$ as $a$ varies over $M[G]$.