Forcing with Nontransitive Models 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.
 A: 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$.
A: Let me augment Victoria's nice answer with a few additional
remarks.
What I'd like to point out is that, contrary to what has been
stated, one doesn't actually need to assume that $G$ is
$M$-generic in order to conclude $M[G]\prec H_\theta[G]$; having
$G\subset\mathbb{P}\in M$ being $H_\theta$-generic (that is,
$V$-generic) is sufficient.
Let's begin by correcting, as Victoria does, your definition of
what it means for $G\subset\mathbb{P}$ to be $M$-generic, in the
case where $M\prec H_\theta$ is a possibly non-transitive
elementary submodel of some $H_\theta$. You said to be generic
means to meet every dense subset $D\subset \mathbb{P}$ with $D\in M$, but this
is not the right definition. You want to say instead that $G$
meets every such dense set $D$ inside $M$. That is, that $G\cap D\cap M\neq\emptyset$. If we only have $G\cap D\neq\emptyset$, then $M$ will not have access to the conditions $p\in G\cap D$ that are useful when a filter meets a dense set. So it is the corrected definition that treats $\langle M,{\in^M}\rangle$ as a model of set theory in its own right, insisting that for every dense set in this structure, the filter meets it. 
Proper forcing is of course concerned all about this, since we
seek a condition $p\in\mathbb{P}$ forcing that whenever
$G\subset\mathbb{P}$ is $V$-generic, then it is also $M$-generic
in this sense.
But we may still form the extension $M[G]$ whether or not $G$ is
$M$-generic in this sense, defining $M[G]=\{\tau_G\mid\tau\in M^{\mathbb{P}}\}$
to be the interpretation of all names in $M$ by the filter $G$.
Now, it turns out that for $V$-generic filters $G$, we have that
$G$ is $M$-generic just in case
$M[G]\cap\text{Ord}=M\cap\text{Ord}$, which holds just in case
$M[G]\cap V=M$. This is easy to see, since any name $\dot\alpha$
for an ordinal in $M$ gives rise to an antichain of possibilities
in $M$, and so if $G$ is $M$-generic, then it will force
$\dot\alpha$ to be an ordinal already in $M$. And for the other
direction, given any maximal antichain in $M$, we may construct by
the mixing lemma a name $\dot\alpha$ for an ordinal, which will be
a new ordinal just in case $G$ does not meet $A\cap M$.
Assume $H_\theta$ satisfies a sufficiently large fragment of ZFC.
Theorem. If $M\prec H_\theta$ and $G\subset\mathbb{P}\in M$ is
$H_\theta$-generic, then $M[G]\prec H_\theta[G]$.
Proof. Suppose that $M\prec H_\theta$ and $G\subset\mathbb{P}\in
M$ is $H_\theta$-generic. We may still form $M[G]=\{\tau_G\mid
\tau\in M^{\mathbb{P}}\}$ as the set of interpretations of names in $M$ using the
filter $G$. Let $\bar M=M[G]\cap V$. This is larger than $M$,
precisely when $G$ is not $M$-generic. I claim that $\bar M\prec
H_\theta$, by verifying the Tarski-Vaught criterion, since if
$H_\theta$ has a witness, then we may find a name in $M$ for such
a ground-model object, and so we will find a witness in $\bar M$.
And since $\bar M\subset \bar M[G]\cap V\subset M[G]\cap
V=\bar M$, it follows that $\bar M[G]\cap V=\bar M$, and so $G$ is
actually $\bar M$-generic. So $M[G]=\bar M[G]\prec H_\theta[G]$ by
reducing to the case where we do have the extra genericity. QED
In regard to question 2, of course we want $G$ to be
$H_\theta$-generic, since without this it is easy to make
counterexamples to $M[G]\prec H_\theta[G]$. For example, if $M$ is
countable we can easily find $M$-generic filters $G$ with $G\in
H_\theta$, and in this case, if the forcing is nontrivial then
$M[G]$ is definitely not an elementary substructure of
$H_\theta[G]=H_\theta$. This is the argument of your last paragraph, and that is totally right; so the conclusion is that for this question we want to assume $G$ is $V$-generic. 
Lastly, let me point out that one doesn't need countable models in order to undertake the forcing construction, and one can speak of the forcing extensions of any model of set theory, whether it is countable, transitive, uncountable, nonstandard, whatever. The most illuminating way to do this is via Boolean-valued models, and by taking the quotient, one arrives at the Boolean ultrapower construction. The basic situation is the if $V$ is a model of set theory containing a complete Boolean algebra $\mathbb{B}$, and $U\subset\mathbb{B}$ is an ultrafilter ($U\in V$ is completely fine), then one may form the quotient $V^{\mathbb{B}}/U$ of the $\mathbb{B}$-valued structure, and this is realized as a forcing extension of its ground model $\check V_U$, and furthermore there is an elementary embedding of $V$ into $\check V_U$, called the Boolean ultrapower map. So the entire composition $$V\overset{\prec}{\scriptsize\sim} \check V_U\subset \check V_U[G]=V^{\mathbb{B}}/U$$ lives inside $V$. There is no need for $V$ to be countable and no need for $U$ to be generic in any sense, yet $G$, which is the equivalence class of the name $\dot G$ by $U$, is still nevertheless $\check V_U$-generic. You can find fuller details in my paper with D. Seabold, Boolean ultrapowers as large cardinal embeddings. 
A: To summarize Joel's comments. 
Suppose that $M$ is a possibly nontransitive model of a sufficient fragment of ZFC like Zermelo with Choice and some Replacement. (Needs it to be an elementary submodel of some $H_\kappa$?) Let $P\in M$ be a forcing notion. In parallel to the usual inductive interpretation 
$$
t[G]=\{s[G]:\exists p\in G(\langle s,p\rangle\in t)\}
$$
and $M[G]=\{t[G]:t\in M\}$, we define the modified interpretation 
$$
t^M[G]=\{s^M[G]:\exists p\in G(\langle s,p\rangle\in t\cap M)\}
$$
and $M[G]^{\text{mod}}=\{t^M[G]:t\in M\}$. 
Note that $M[G]^{\text{mod}}$ is a transitive set and not necessarily an extension of $M$.
A filter $G\subseteq P$ is strongly $P$-generic over $M$ iff $G\cap D\cap M\ne\emptyset$ whenever a set $D\in M$, $D\subseteq P$ is dense in $P$.  Note: $G$ is not necessarily an ultrafilter in $P$ in this case!
Let $\pi=\pi_M:M\to M'$ be the Mostowski collapse, $\pi(x)=\{\pi(y):y\in x\cap M\}$, so $M'$ is a transitive set $\in$-isomorphic to $M$ by $\pi$. 
Let $P'=\pi(P)=\{\pi(p):p\in P\cap M\}$, a forcing in $M'$.
Theorem.
In these assumptions, let $G\subseteq P$ be strongly $P$-generic over $M$. Then 
(1) the set $G'=\{\pi(p):p\in G\cap M\}$ is $P'$-generic over $M'$ in the usual sense, and 
(2) $M'[G']=M[G]^{\text{mod}}$, in fact $t_M[G]=\pi(t)[G']$ for each $t\in M$.
Moreover if $A(x_1,\dots,x_n)$ is any formula and $t_1,\dots,t_n\in M$ then $A(t_1^M[G],\dots,t_n^M[G])$ is true in $M[G]^{\text{mod}}$ iff there is a condition $p\in G\cap M$ which $P$-forces $A(t_1,\dots,t_n)$ in $M$. 
$\Box$
TODO list. 


*

*Prove the theorem carefully.

*Study the relations between $M[G]$ and $M[G]^{\text{mod}}$. Still $M[G]$ is of a separate interest, albeit it is not only nontransitive but also not necessarily even an extensional model. (See an example in one of my comments.)

*Possible applications. For instance in the case $M\prec H_\kappa$, $M$ countable, one can consider sets $G\subseteq P$ in $H_\kappa$, strongly $P$-generic over $M$ (but not over $H_\kappa$, of course) as in my arXiv paper on countable OD sets in Cohen's extensions.
