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.



Forcing with Nontransitive Models
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](http://boolesrings.org/victoriagitman/2014/03/01/introduction-to-remarkable-cardinals/). 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$.


