[proofplan] We prove the statement by induction on formula complexity. The atomic base is the atomic truth lemma obtained from the simultaneous recursion defining forcing for equality and membership of names. For the logical steps, negation uses the dense set of conditions deciding the subformula, conjunction uses directedness of the filter, and the existential step uses the dense-witness clause in the recursive definition of forcing. These cases cover all formulas after rewriting disjunction, implication, and universal quantification in terms of negation, conjunction, and existential quantification. [/proofplan]

[step:Set up the induction] For every $\mathbb{P}$-name $\tau\in M$, its interpretation by $G$ is \begin{align*} \tau^G=\{\sigma^G:\text{there exists }p\in G\text{ such that }(\sigma,p)\in\tau\}. \end{align*} For conditions $q,r\in\mathbb{P}$, write $q\perp r$ to mean that no condition $s\in\mathbb{P}$ satisfies $s\leq q$ and $s\leq r$. For a name $\sigma$, write $\operatorname{rank}(\sigma)$ for its usual von Neumann rank as a set. We use the following recursive definition of forcing, all computed inside $M$. For names $\sigma,\tau$, the atomic clauses are: \begin{align*} p\Vdash_M\sigma\in\tau \end{align*} iff the set of all $q\leq p$ for which there are $(\rho,r)\in\tau$ with $q\leq r$ and $q\Vdash_M\sigma=\rho$ is dense below $p$; and \begin{align*} p\Vdash_M\sigma=\tau \end{align*} iff, for every $(\rho,r)\in\sigma$, the set of all $q\leq p$ such that $q\perp r$ or $q\Vdash_M\rho\in\tau$ is dense below $p$, and symmetrically for every $(\rho,r)\in\tau$ with $\sigma$ and $\tau$ interchanged. The logical clauses are: \begin{align*} p\Vdash_M\neg\psi \end{align*} iff no $q\leq p$ forces $\psi$; \begin{align*} p\Vdash_M\psi\wedge\theta \end{align*} iff $p\Vdash_M\psi$ and $p\Vdash_M\theta$; and \begin{align*} p\Vdash_M\exists v\,\psi(v,\vec\tau) \end{align*} iff the set of all $q\leq p$ for which some $\mathbb{P}$-name $\sigma\in M$ satisfies $q\Vdash_M\psi(\sigma,\vec\tau)$ is dense below $p$. The recursion is well-founded as follows. For atomic formulas, order pairs of name-ranks by the componentwise well-founded order: \begin{align*} (\alpha',\beta')\prec(\alpha,\beta) \end{align*} when $\alpha'\leq\alpha$, $\beta'\leq\beta$, and at least one inequality is strict. If $(\rho,r)\in\tau$, then $\operatorname{rank}(\rho)<\operatorname{rank}(\tau)$; hence the membership clause for $\sigma\in\tau$ refers only to equality for $(\sigma,\rho)$, and the equality clause for $\sigma=\tau$ refers only to membership for $(\rho,\tau)$ or $(\rho,\sigma)$, all of which are lower in this order. The logical clauses then recurse on formula complexity. We shall use monotonicity: if $p\Vdash_M\chi$ and $q\leq p$, then $q\Vdash_M\chi$. This is proved by the same induction. In dense clauses, a set dense below $p$ is dense below every $q\leq p$; in the negation clause, an extension of $q$ is also an extension of $p$; in the conjunction clause the claim is immediate; and in the existential clause the same witness-dense set remains dense below $q$. We prove, by induction on the complexity of $\varphi$, that \begin{align*} M[G]\models\varphi(\tau_1^G,\dots,\tau_n^G) \end{align*} if and only if there is $p\in G$ such that \begin{align*} p\Vdash_M\varphi(\tau_1,\dots,\tau_n). \end{align*} The definition is formalized in $M$ by recursion on formula complexity together with the well-founded rank recursion on names. At each stage, the predicates just displayed are first-order definable over $M$ from the relevant names, formula codes, and earlier stages of the recursion. Separation in $M$ forms the displayed sets of conditions, and Replacement in $M$ supports the rank-recursive construction of the forcing relation. Since $M$ is transitive and $\mathbb{P}\in M$, the names and dense sets used in these recursive clauses belong to $M$ whenever their defining parameters do. [/step]

[step:Use the atomic truth lemma as the base case]The base case is the following atomic truth lemma. For all $\mathbb{P}$-names $\sigma,\tau\in M$, \begin{align*} \sigma^G\in\tau^G \iff \text{there exists }p\in G\text{ such that }p\Vdash_M\sigma\in\tau \end{align*} and \begin{align*} \sigma^G=\tau^G \iff \text{there exists }p\in G\text{ such that }p\Vdash_M\sigma=\tau. \end{align*} We prove the lemma by simultaneous induction on the componentwise rank pair \begin{align*} (\operatorname{rank}(\sigma),\operatorname{rank}(\tau)). \end{align*} For membership, suppose $p\in G$ and $p\Vdash_M\sigma\in\tau$. The recursive membership clause gives a dense set below $p$ of conditions $q$ for which there are $(\rho,r)\in\tau$ with $q\leq r$ and $q\Vdash_M\sigma=\rho$. Since $p\in G$ and the dense set is in $M$, genericity gives such a $q\in G$. Then $r\in G$ by upward closure of the filter, and the equality statement for the lower pair $(\sigma,\rho)$ gives $\sigma^G=\rho^G$. Hence $\sigma^G\in\tau^G$. Conversely, assume $\sigma^G\in\tau^G$. Choose $(\rho,r)\in\tau$ with $r\in G$ and $\sigma^G=\rho^G$. Since $(\sigma,\rho)\prec(\sigma,\tau)$, the lower-rank equality induction gives $q\in G$ such that $q\Vdash_M\sigma=\rho$. By directedness choose $p\in G$ with $p\leq q$ and $p\leq r$. If $u\leq p$, then $u\leq r$, and monotonicity gives $u\Vdash_M\sigma=\rho$. Thus every $u\leq p$ belongs to the dense set required by the membership clause, with the same tagged pair $(\rho,r)$. Therefore $p\Vdash_M\sigma\in\tau$. Now suppose $p\in G$ and $p\Vdash_M\sigma=\tau$. Let $(\rho,r)\in\sigma$ with $r\in G$. Directedness gives $p_0\in G$ with $p_0\leq p$ and $p_0\leq r$. The equality clause supplies a dense set below $p$ of conditions $q$ such that $q\perp r$ or $q\Vdash_M\rho\in\tau$. Applying genericity below $p_0$ gives $q\in G$ with $q\leq p_0$ in that set. The alternative $q\perp r$ is impossible because $q,r\in G$. Hence $q\Vdash_M\rho\in\tau$, and the lower membership induction for $(\rho,\tau)$ gives $\rho^G\in\tau^G$. This proves $\sigma^G\subseteq\tau^G$; the symmetric dense requirements prove $\tau^G\subseteq\sigma^G$. It remains to prove the converse for equality. Assume $\sigma^G=\tau^G$. Let $D$ be the set of all conditions $s$ such that one of the following three alternatives holds: \begin{align*} s\Vdash_M\sigma=\tau, \end{align*} or there is $(\rho,r)\in\sigma$ with $s\leq r$ and no extension of $s$ forces $\rho\in\tau$, or there is $(\rho,r)\in\tau$ with $s\leq r$ and no extension of $s$ forces $\rho\in\sigma$. The set $D$ is definable in $M$ from $\sigma,\tau$ and the lower-rank forcing relations. We verify that $D$ is dense. Fix $p_0\in\mathbb{P}$. If some $s\leq p_0$ forces $\sigma=\tau$, then $s\in D$. Otherwise no extension of $p_0$ forces equality. In particular, $p_0$ does not satisfy the recursive equality clause. Hence one of its dense requirements fails. Suppose, for example, that for some $(\rho,r)\in\sigma$, the set \begin{align*} A_{\rho,r}=\{q\leq p_0:q\perp r\text{ or }q\Vdash_M\rho\in\tau\} \end{align*} is not dense below $p_0$. Then there is $s_0\leq p_0$ such that no $q\leq s_0$ lies in $A_{\rho,r}$. Since no extension of $s_0$ is incompatible with $r$, the conditions $s_0$ and $r$ are compatible; choose $s\leq s_0,r$. For every $u\leq s$, also $u\leq s_0$, so $u$ cannot force $\rho\in\tau$. Thus $s\in D$ by the second alternative. The case where a symmetric dense requirement for a tag in $\tau$ fails is identical. Hence $D$ is dense. By $M$-genericity choose $p\in G\cap D$. The two failure alternatives cannot occur. For instance, if $(\rho,r)\in\sigma$, $p\leq r$, and no extension of $p$ forces $\rho\in\tau$, then $r\in G$, so $\rho^G\in\sigma^G=\tau^G$. The lower membership induction gives $q\in G$ such that $q\Vdash_M\rho\in\tau$. Directedness gives $u\in G$ with $u\leq p$ and $u\leq q$; by monotonicity $u\Vdash_M\rho\in\tau$, contradicting the failure alternative. The symmetric alternative is ruled out in the same way. Therefore the first alternative holds, so some $p\in G$ forces $\sigma=\tau$.[/step]

[guided]The atomic proof is a simultaneous induction on \begin{align*} (\operatorname{rank}(\sigma),\operatorname{rank}(\tau)). \end{align*} The order is \begin{align*} (\alpha',\beta')\prec(\alpha,\beta) \end{align*} when $\alpha'\leq\alpha$, $\beta'\leq\beta$, and at least one inequality is strict. Thus, if $(\rho,r)\in\tau$, then \begin{align*} (\operatorname{rank}(\sigma),\operatorname{rank}(\rho)) \prec (\operatorname{rank}(\sigma),\operatorname{rank}(\tau)), \end{align*} and if $(\rho,r)\in\sigma$, then \begin{align*} (\operatorname{rank}(\rho),\operatorname{rank}(\tau)) \prec (\operatorname{rank}(\sigma),\operatorname{rank}(\tau)). \end{align*} These are exactly the lower atomic cases used in the recursion. For membership, assume first that $p\in G$ and \begin{align*} p\Vdash_M\sigma\in\tau. \end{align*} The recursive clause says that below $p$ it is dense to find $q$ and a tag $(\rho,r)\in\tau$ such that \begin{align*} q\leq r \end{align*} and \begin{align*} q\Vdash_M\sigma=\rho. \end{align*} Since $G$ is $M$-generic and $p\in G$, choose such a $q\in G$. From $q\leq r$ and $q\in G$, upward closure gives $r\in G$. The equality case for the lower pair $(\sigma,\rho)$ gives \begin{align*} \sigma^G=\rho^G. \end{align*} Because $(\rho,r)\in\tau$ and $r\in G$, we have $\rho^G\in\tau^G$, and hence \begin{align*} \sigma^G\in\tau^G. \end{align*} Conversely, suppose \begin{align*} \sigma^G\in\tau^G. \end{align*} Choose $(\rho,r)\in\tau$ such that $r\in G$ and \begin{align*} \sigma^G=\rho^G. \end{align*} By the lower equality case, choose $q\in G$ with \begin{align*} q\Vdash_M\sigma=\rho. \end{align*} Directedness gives $p\in G$ such that \begin{align*} p\leq q \end{align*} and \begin{align*} p\leq r. \end{align*} For every $u\leq p$, monotonicity gives \begin{align*} u\Vdash_M\sigma=\rho, \end{align*} and also $u\leq r$. Therefore every $u\leq p$ belongs to the dense set required by the recursive clause for $p\Vdash_M\sigma\in\tau$, using the same tag $(\rho,r)$. Thus \begin{align*} p\Vdash_M\sigma\in\tau. \end{align*} For equality, first assume $p\in G$ and \begin{align*} p\Vdash_M\sigma=\tau. \end{align*} Let $(\rho,r)\in\sigma$ with $r\in G$. Choose $p_0\in G$ such that \begin{align*} p_0\leq p \end{align*} and \begin{align*} p_0\leq r. \end{align*} The recursive equality clause gives a dense set below $p$ of conditions $q$ such that either \begin{align*} q\perp r \end{align*} or \begin{align*} q\Vdash_M\rho\in\tau. \end{align*} Genericity below $p_0$ gives $q\in G$ in this dense set. Since $q,r\in G$, the alternative $q\perp r$ is impossible. Therefore \begin{align*} q\Vdash_M\rho\in\tau. \end{align*} The lower membership case for $(\rho,\tau)$ gives \begin{align*} \rho^G\in\tau^G. \end{align*} So every element contributed to $\sigma^G$ lies in $\tau^G$. The symmetric half of the equality clause gives \begin{align*} \tau^G\subseteq\sigma^G, \end{align*} and therefore \begin{align*} \sigma^G=\tau^G. \end{align*} For the converse equality direction, assume \begin{align*} \sigma^G=\tau^G. \end{align*} Define $D$ to consist of all conditions $s$ such that either \begin{align*} s\Vdash_M\sigma=\tau, \end{align*} or there is $(\rho,r)\in\sigma$ with \begin{align*} s\leq r \end{align*} and no extension of $s$ forces \begin{align*} \rho\in\tau, \end{align*} or there is $(\rho,r)\in\tau$ with \begin{align*} s\leq r \end{align*} and no extension of $s$ forces \begin{align*} \rho\in\sigma. \end{align*} This definition uses only $\sigma,\tau$ and lower-rank forcing relations, so $D\in M$. To see that $D$ is dense, fix $p_0\in\mathbb{P}$. If some $s\leq p_0$ satisfies \begin{align*} s\Vdash_M\sigma=\tau, \end{align*} then $s\in D$. Otherwise no extension of $p_0$ forces $\sigma=\tau$. Hence $p_0$ fails the recursive equality clause. For example, suppose the failed requirement is witnessed by $(\rho,r)\in\sigma$. Then \begin{align*} A_{\rho,r}=\{q\leq p_0:q\perp r\text{ or }q\Vdash_M\rho\in\tau\} \end{align*} is not dense below $p_0$. Choose $s_0\leq p_0$ such that no $q\leq s_0$ lies in $A_{\rho,r}$. Since no extension of $s_0$ is incompatible with $r$, the conditions $s_0$ and $r$ are compatible. Choose \begin{align*} s\leq s_0,r. \end{align*} Then every $u\leq s$ is also below $s_0$, so no such $u$ forces \begin{align*} \rho\in\tau. \end{align*} Thus $s\in D$ by the second alternative. The symmetric failed requirement for a tag in $\tau$ gives the third alternative. Therefore $D$ is dense. Choose $p\in G\cap D$. If $p$ is in the second alternative, then for some $(\rho,r)\in\sigma$ we have \begin{align*} p\leq r \end{align*} and no extension of $p$ forces $\rho\in\tau$. Since $p\in G$ and $p\leq r$, also $r\in G$, so \begin{align*} \rho^G\in\sigma^G. \end{align*} Using $\sigma^G=\tau^G$, this gives \begin{align*} \rho^G\in\tau^G. \end{align*} The lower membership case gives $q\in G$ such that \begin{align*} q\Vdash_M\rho\in\tau. \end{align*} Choose $u\in G$ with \begin{align*} u\leq p \end{align*} and \begin{align*} u\leq q. \end{align*} By monotonicity, \begin{align*} u\Vdash_M\rho\in\tau, \end{align*} contradicting the assertion that no extension of $p$ forces $\rho\in\tau$. The third alternative is symmetric. Thus the only possible alternative for $p\in D$ is \begin{align*} p\Vdash_M\sigma=\tau. \end{align*}[/guided]

[step:Pass the induction through negation] Assume the theorem has been proved for $\psi(\tau_1,\dots,\tau_n)$. We prove it for $\neg\psi(\tau_1,\dots,\tau_n)$. Suppose first that $p\in G$ and \begin{align*} p\Vdash_M\neg\psi(\tau_1,\dots,\tau_n). \end{align*} By the recursive negation clause, no condition $q\leq p$ forces $\psi(\tau_1,\dots,\tau_n)$. If $M[G]\models\psi(\tau_1^G,\dots,\tau_n^G)$, the induction hypothesis gives $q\in G$ with $q\Vdash_M\psi(\tau_1,\dots,\tau_n)$. Directedness of $G$ gives $r\in G$ with $r\leq p$ and $r\leq q$. Monotonicity of the recursively defined forcing relation gives $r\Vdash_M\psi(\tau_1,\dots,\tau_n)$, contradicting the negation clause. Therefore \begin{align*} M[G]\models\neg\psi(\tau_1^G,\dots,\tau_n^G). \end{align*} Conversely, suppose \begin{align*} M[G]\models\neg\psi(\tau_1^G,\dots,\tau_n^G). \end{align*} Let $D$ be the set of all $p\in\mathbb{P}$ such that either $p\Vdash_M\psi(\tau_1,\dots,\tau_n)$ or $p\Vdash_M\neg\psi(\tau_1,\dots,\tau_n)$. The set $D$ belongs to $M$ by definability of the forcing relation in $M$, and it is dense: below any $p_0$, either some $q\leq p_0$ forces $\psi$, or else $p_0$ itself forces $\neg\psi$ by the negation clause. Since $G$ is $M$-generic, choose $p\in G\cap D$. The first alternative is impossible by the induction hypothesis, so $p\Vdash_M\neg\psi(\tau_1,\dots,\tau_n)$. [/step]

[step:Pass the induction through conjunction] Assume the theorem has been proved for $\psi(\tau_1,\dots,\tau_n)$ and for $\theta(\tau_1,\dots,\tau_n)$. If $p\in G$ and $p\Vdash_M\psi\wedge\theta$, then the conjunction clause gives $p\Vdash_M\psi$ and $p\Vdash_M\theta$. The induction hypotheses give \begin{align*} M[G]\models\psi(\tau_1^G,\dots,\tau_n^G) \end{align*} and \begin{align*} M[G]\models\theta(\tau_1^G,\dots,\tau_n^G). \end{align*} Thus $M[G]\models(\psi\wedge\theta)(\tau_1^G,\dots,\tau_n^G)$. Conversely, suppose $M[G]\models(\psi\wedge\theta)(\tau_1^G,\dots,\tau_n^G)$. The induction hypotheses give $p_0,p_1\in G$ such that $p_0\Vdash_M\psi(\tau_1,\dots,\tau_n)$ and $p_1\Vdash_M\theta(\tau_1,\dots,\tau_n)$. Directedness of $G$ gives $p\in G$ with $p\leq p_0$ and $p\leq p_1$. By monotonicity, $p$ forces both conjuncts, so \begin{align*} p\Vdash_M(\psi\wedge\theta)(\tau_1,\dots,\tau_n). \end{align*} [/step]

[step:Pass the induction through existential quantification] Assume the theorem has been proved for $\psi(v,\tau_1,\dots,\tau_n)$. In the recursive definition, \begin{align*} p\Vdash_M\exists v\,\psi(v,\tau_1,\dots,\tau_n) \end{align*} means that the set \begin{align*} E_p=\{q\leq p:\text{there is a }\mathbb{P}\text{-name }\sigma\in M\text{ with }q\Vdash_M\psi(\sigma,\tau_1,\dots,\tau_n)\} \end{align*} is dense below $p$. Suppose $p\in G$ and $p\Vdash_M\exists v\,\psi(v,\tau_1,\dots,\tau_n)$. The set $E_p$ is definable in $M$ and dense below $p$, so genericity gives $q\in G\cap E_p$. Choose a name $\sigma\in M$ such that \begin{align*} q\Vdash_M\psi(\sigma,\tau_1,\dots,\tau_n). \end{align*} By the induction hypothesis, \begin{align*} M[G]\models\psi(\sigma^G,\tau_1^G,\dots,\tau_n^G), \end{align*} so $M[G]\models\exists v\,\psi(v,\tau_1^G,\dots,\tau_n^G)$. Conversely, suppose \begin{align*} M[G]\models\exists v\,\psi(v,\tau_1^G,\dots,\tau_n^G). \end{align*} Choose $a\in M[G]$ witnessing the existential statement. Since every element of $M[G]$ is the interpretation of a name from $M$, choose a $\mathbb{P}$-name $\sigma\in M$ with $a=\sigma^G$. The induction hypothesis gives $p\in G$ with \begin{align*} p\Vdash_M\psi(\sigma,\tau_1,\dots,\tau_n). \end{align*} If $u\leq p$, monotonicity gives \begin{align*} u\Vdash_M\psi(\sigma,\tau_1,\dots,\tau_n). \end{align*} Thus every $u\leq p$ belongs to $E_p$, with witness $\sigma$, so $E_p$ is dense below $p$. Therefore $p\Vdash_M\exists v\,\psi(v,\tau_1,\dots,\tau_n)$. [/step]

[step:Conclude for all formulas] Every first-order formula is built from atomic formulas by negation, conjunction, and existential quantification after using the standard abbreviations for the other connectives and universal quantifiers. The atomic step supplies the base case, and the preceding three steps supply the induction transitions. Therefore, for every formula $\varphi(v_1,\dots,v_n)$ and every tuple of $\mathbb{P}$-names $\tau_1,\dots,\tau_n\in M$, \begin{align*} M[G]\models\varphi(\tau_1^G,\dots,\tau_n^G) \end{align*} if and only if there exists $p\in G$ such that \begin{align*} p\Vdash_M\varphi(\tau_1,\dots,\tau_n). \end{align*} This proves the truth lemma. [/step]