A common approach to forcing is to use countable transitive model $M \in V$ with $\mathbb{P} \in M$ and take a $G \in M$ (which always exists) to form a countable transitive model $M[G]$. Another approach takes $M$ to be countable such that $M \prec H_\theta$ for sufficiently large $\theta$ (and hence may not be transitive). For example, a definition of proper forcing considers such models.
Forcing with transitive models are quite convenient since many absoluteness results can be used to transfer properties of $x \in M[G]$ which hold in $M[G]$ up to $V$. If $M \prec H_\theta$ is not transitive, then it is not clear what type of property that $M[G]$ can prove about $x$ transfer to $V$. For instance, if $M[G] \models x \in {}^\omega\omega$, is $x \in {}^\omega\omega$ in $V$? Of course, one remedy could be to Mostowski collapse everything and then use the familiar absoluteness for transitive models. For $x \in {}^\omega\omega$, one could use the fact that $M \prec H_\theta$ implies $\omega \subseteq M$ and hence the Mostowski collapse of $M[G]$ would maps each real to itself and then use absoluteness to prove that $V \models x \in {}^\omega\omega$ as well. Is there a more direct way to prove these type of result rather than collapsing the forcing extension, which seem to suggest one should have started by collapse $M$ before starting the forcing construction.
So my questions are
1 First, if one chooses to work with countable $M \prec H_\theta$ are there any changes that need to made to the forcing construction and the forcing theorem as they appear in Kunen or Jech? Of course, the definition of a generic filter should be changed to meeting those dense sets that appear in $M$.
2 I am aware that if $G$ has master conditions, then $M[G] \prec H_\theta[G]$? Is $H_\theta[G]$ just the forcing construction applied to $H_\theta$? As $G$ is not necessarily generic over $H_\theta$, it is not clear to me that the forcing theorem need to apply to $H_\theta[G]$ (or a priori $H_\Theta[G]$ models any particular amount of $\text{ZF}- \text{P}$, but since $M[G] \prec H_\theta[G]$, actually $H_\Theta[G]$ would model as much as $M[G]$.) In general without addition assumption like master conditions, does the relation $M[G] \prec H_\Theta[G]$ still hold.
Also perhaps I am misunderstanding something, but since $\mathbb{P} \in M$, it appears that if $\theta$ is large enough, every $G \subseteq \mathbb{P}$ which is $\mathbb{P}$-generic over $M$ is already in $H_\Theta$. Would this not imply that $H_\theta[G] = H_\theta$ and hence $M[G] \prec H_\Theta$. Since $M \prec H_\theta$, $M$ and $M[G]$ models the exact same sentences. This surely can not happen.
Thanks for any help and clarification that can be provided.
Best Answer
All standard forcing machinery works when forcing over such $M$ because they satisfy a large enough fragment of $ZFC$, namely $ZFC$ without the powerset axiom. The purpose of forcing over such models is rarely to transfer results to $V$, although something like this can be done in the following way. Suppose that $M\prec H_\theta$ is countable with $\mathbb P\in M$ and for every $M$-generic $G$ in $V$, we have that $M[G]\models\varphi$. Then $M$ satisfies that $\varphi$ is forced by $\mathbb P$. But then by elementarity, $H_\theta$ satisfies that $\varphi$ is forced by $\mathbb P$ as well. Thus, $H_\theta[G]\models\varphi$ in every forcing extension $V[G]$. So in a way, we have transfered a property from $M[G]$ to $V[G]$. I recently encountered many such arguments when working with Schindler's remarkable cardinals and I have some notes written up here. In the case of remarkable cardinals, you use some properties of the transitive collapse of $M$ to argue that certain generic embeddings exist in its forcing extension by $Coll(\omega,<\kappa)$. Using the argument above you then conclude that such generic embeddings must exist in $H_\theta[G]$ where $G\subseteq Coll(\omega,<\kappa)$ is $V$-generic.
The argument that $M[G]\prec H_\theta[G]$ works only in the case that $G$ is both fully $H_\theta$-generic and also $M$-generic (meets every dense set of $M$ in $M$ itself). Indeed, in most situations where forcing over $M\prec H_\theta$ is used, as in say proper forcing, the arguments usually involve fully generic $G$. It seems that generally the purpose of such arguments is to use $M[G]$ to conclude that some property holds in $V[G]$ by reflecting down to countable objects. This is for instance how one can use the definition of proper posets, in terms of the existence of $M$-generic filters for countable $M\prec H_\theta$, to argue that they don't collapse $\omega_1$.