Truth lemma

First induct on the sorted pair of name ranks to prove the equivalence for equality. Suppose $p\in G$ forces $\sigma \subseteq \tau$, and $u_G\in {\sigma }_G$ comes from $⟨u,s⟩\in \sigma$ with $s\in G$. Directedness gives $q\in G$ with $q\le p,s$. The set of $r\le q$ admitting $⟨v,t⟩\in \tau$ with $r\le t$ and $r⊩u=v$ is in M by atomic definability and is dense below q by the subset clause. F1 gives such r in G; then t is in G, and equality induction on the two proper subnames gives $u_G=v_G\in {\tau }_G$. Applying this to both subset clauses proves the forward semantic implication from forced equality.

For the converse define $K_{\sigma ,\tau }$ to consist of r for which some $⟨u,s⟩\in \sigma$ satisfies $r\le s$ and there are no $a\le r$ and $⟨v,t⟩\in \tau$ with $a\le t$ and $a⊩u=v$. The union of $K_{\sigma ,\tau }$, $K_{\tau ,\sigma }$ and the equality-forcing conditions is dense. Indeed, if p fails equality, one subset clause fails; its negation supplies an entry and $q\le p,s$ with no such further witness, putting q in the corresponding K. All these sets belong to M by Separation and atomic definability.

If ${\sigma }_G={\tau }_G$, neither K meets G. For otherwise its witness u satisfies $u_G\in {\sigma }_G={\tau }_G$, so some $⟨v,t⟩\in \tau$ has $t\in G$ and $u_G=v_G$. Equality induction gives $b\in G$ forcing $u=v$. A common refinement in G of r,t,b still forces that equality by F1, contradicting r's K-condition. The reverse K is excluded identically with the names exchanged. Genericity applied to the dense union in step 1.2 therefore gives a condition in G forcing equality. The induction is legitimate in both equality directions because both names in each equality appeal are proper subnames. This establishes equality in both directions, including the empty-name base.

If $p\in G$ forces $\sigma \in \tau$, its dense set of coefficient/equality witnesses is in M; F1 gives $r\in G$ and $⟨v,t⟩\in \tau$ with $r\le t$ and $r⊩\sigma =v$. Equality gives ${\sigma }_G=v_G\in {\tau }_G$. Conversely if ${\sigma }_G\in {\tau }_G$, choose such an entry with $t\in G$ and ${\sigma }_G=v_G$ by F2. Equality gives $b\in G$ forcing $\sigma =v$. A common refinement p of b and t lies in G; every extension of p is a membership witness by persistence. Thus p forces membership.

Induct on formula complexity. Conjunction forced by a member of G makes both conjuncts true by induction. Conversely, truth of both conjuncts gives two forcing conditions in G; their common refinement forces both. If $p\in G$ forces $\mathrm{\neg }\psi$, truth of $\psi$ would give $b\in G$ forcing $\psi$ by induction, and a common refinement would contradict the negation clause. Conversely, if $\psi$ is false in M[G], G meets the ground decision set for $\psi$; its chosen condition cannot force $\psi$ by induction, hence forces $\mathrm{\neg }\psi$.

If $p\in G$ forces $\mathrm{\exists }x\psi (x,\vec{\tau })$, its ground set of witness-forcing conditions is dense below p. F1 supplies r in G and a name $\sigma \in M$ with $r⊩\psi (\sigma ,\vec{\tau })$. Induction gives a witness ${\sigma }_G$ in M[G]. Conversely a true existential has a witness $x={\sigma }_G$ by F2; induction gives r in G forcing its matrix. Every stronger condition forces the same matrix by persistence, so r forces the existential by F4. Together with step 4.1 this finishes the formula induction and both directions of the assertion. Only finitely many refinements and existential witnesses were used at each argument, so no AC enters.