Set-stage names and the forcing truth lemma for the Easton class product

Set stages. For every infinite regular $\lambda$, $P^{\le \lambda }\in M$ by [F2]. If $D\in M$ is dense in that head, the class $D^{\ast }=\{p\in P:p^{\le \lambda }\in D\}$ belongs to $\mathcal{C}$ by [F1] and is dense in $P$: below $p$, choose $q\le p^{\le \lambda }$ in $D$ and take $q\cup p^{>\lambda }$. Thus $G$ meets $D^{\ast }$. Because restriction of a member of $G$ is weaker and hence also belongs to $G$, $G^{\le \lambda }=G\cap P^{\le \lambda }$ meets $D$. Restrictions of common extensions show that $G^{\le \lambda }$ is directed; it is upward closed in the head, so it is $M$-generic. For $\lambda \le \mu$, $P^{\le \lambda }\subseteq P^{\le \mu }$ and $G^{\le \lambda }=G^{\le \mu }\cap P^{\le \lambda }$.

Names. Every $p\in P$ has a set of first coordinates, bounded by some infinite regular $\lambda$, and therefore belongs to $P^{\le \lambda }$. For a set $\tau \in M$, the assertion that there is a regular $\lambda$ for which $\tau$ is a $P^{\le \lambda }$-name is a first-order assertion over $M$ with parameter $F$: the order $P^{\le \lambda }$ is a set uniformly defined from $F$, and the set-name predicate is uniform by [F3]. Comprehension [F1] makes the $P$-names a class in $\mathcal{C}$. Each such name is individually a set of $M$; for each fixed $\lambda$, the collection $M^{P^{\le \lambda }}$ of all names is internally a proper class of $M$ (it includes $\check{x}$ for every $x\in M$). No element of $M$ containing all names is used.

Atomic reduction to a set head. Suppose $\lambda \le \mu$ are infinite regular, $\sigma ,\tau$ are $P^{\le \lambda }$-names, and $p\in P^{\le \mu }$. In the factorization $P^{\le \mu }\cong P^{\le \lambda }\times P^{(\lambda ,\mu ]}$, the set-forcing atomic clauses give $p{⊩}_{P^{\le \mu }}\sigma R\tau ⟺p^{\le \lambda }{⊩}_{P^{\le \lambda }}\sigma R\tau$ for $R\in \{=,\in \}$. To verify this, induct simultaneously on the sorted pair of name ranks used in [F5]. Every coefficient of $\sigma ,\tau$ lies in the smaller head. A condition below $p$ projects to a condition below $p^{\le \lambda }$, and every head condition below $p^{\le \lambda }$ lifts by union with $p^{(\lambda ,\mu ]}$. The same projection and lifting work below any head coefficient and for the stronger witnesses in the dense membership and subset clauses. The recursive equality calls involve strictly smaller name-rank pairs, so the induction hypothesis makes their truth invariant under the projection. This proves the equivalence for equality and membership, including both directions of every density clause.

Meeting a dense class below a condition. If $p\in G$ and $D\in \mathcal{C}$ is dense below $p$, then $D\cup \{r\in P:r\perp p\}$ is a dense class in $\mathcal{C}$: a condition incompatible with $p$ is already in it, while a compatible one has a common extension with $p$ and then an extension in $D$. Genericity makes $G$ meet this union. Directedness prevents any member of $G$ from being incompatible with $p$, so $G\cap D\mathrm{\ne }\mathrm{\varnothing }$. The cone $\{r:r\le p\}$ itself is not claimed dense in all of $P$.

Valuation. The name classes increase with the heads: a $P^{\le \lambda }$-name remains a $P^{\le \mu }$-name when $\lambda \le \mu$, by induction on name rank and inclusion of the orders. If $\tau$ is a name from the smaller head, every coefficient and subname of $\tau$ also comes from that head. The equality $G^{\le \lambda }=G^{\le \mu }\cap P^{\le \lambda }$ from step 1.1 and induction in the valuation recursion [F4] yield ${\mathrm{val}}_{G^{\le \lambda }}(\tau )={\mathrm{val}}_{G^{\le \mu }}(\tau )$. Hence ${\tau }_G$ is independent of stage, the set extensions are nested, and $M[G]={\bigcup }_{\lambda }M[G^{\le \lambda }]$ is precisely the class of values of $P$-names.

The same rank induction works with the full class product in place of $P^{\le \mu }$. For $p\in P$, choose a regular $\lambda$ containing $p,\sigma ,\tau$; every class condition $q\le p$ projects to $q^{\le \lambda }\le p^{\le \lambda }$, and every head condition below $p^{\le \lambda }$ lifts by union with $p^{>\lambda }$. A witness below an arbitrary $q$ lifts with $q^{>\lambda }$. Thus the atomic clauses read with the class $P$ define exactly $p{⊩}_P\sigma R\tau ⟺p^{\le \lambda }{⊩}_{P^{\le \lambda }}\sigma R\tau$. Step 1.3 makes the right side independent of the sufficiently large stage. Since the set-forcing atomic relation is uniformly definable by [F5], this is a first-order definition over $M$ with class parameter $F$, so its extension belongs to $\mathcal{C}$ by [F1]. It uses a set-head recursion and no class-sized Boolean join or class-valued rank recursion. This is the atomic set-stage interface used by Jech on printed pp.235–236.

Formula forcing. Starting from step 2.2, define the forcing predicate for each fixed formula by the clauses of [F5]. At a conjunction or negation substitute the already defined subformula predicates. At an existential, quantify over set conditions and over sets satisfying the $P$-name predicate of step 1.2. All these are set quantifiers with class parameter $P$, so finite induction on the fixed formula and comprehension [F1] give one defining class in $\mathcal{C}$ for that formula. The clauses also give monotonicity by induction: strengthening preserves atomic forcing by step 2.2 and [F7], preserves conjunction and negation immediately, and preserves the dense-witness existential clause because every condition below a stronger condition was already below the original.

Atomic truth. Fix atomic $\phi (\vec{\tau })$ and a regular $\lambda$ containing all its names. Their values in $M[G]$ equal their values in $M[G^{\le \lambda }]$ by step 2.1. If $\phi$ is true there, the set-forcing truth lemma [F6] supplies $q\in G^{\le \lambda }$ forcing it in the head; step 2.2 makes $q{⊩}_P\phi$. Conversely if $p\in G$ forces the atom in $P$, enlarge $\lambda$ to include $p$; then $p^{\le \lambda }\in G^{\le \lambda }$ forces it in the set head by step 2.2, so [F6] gives its truth in the head and hence in $M[G]$.

Connectives. Induct on a fixed formula, the atomic case being step 3.2. For conjunction, if both conjuncts are true, their induction witnesses $p,q\in G$ have a common stronger member $r\in G$, which forces both by monotonicity from step 3.1. The converse follows from the two induction soundness directions. For negation, the class $D_{\psi }=\{p:p⊩\psi \text{ or }p⊩\mathrm{\neg }\psi \}$ is definable by step 3.1 and dense: below any condition either some extension forces $\psi$, or that condition itself forces $\mathrm{\neg }\psi$ by the negation clause. Therefore $G$ meets $D_{\psi }$. If $\psi$ is false in $M[G]$, the induction soundness direction excludes the positive side of this meeting, leaving some $p\in G$ that forces $\mathrm{\neg }\psi$. Conversely if $p\in G$ forces $\mathrm{\neg }\psi$ but $\psi$ were true, induction would give $q\in G$ forcing $\psi$; a common extension of $p,q$ in $G$ would force $\psi$, contrary to the negation clause.

Existential quantifier. If $M[G]\models \mathrm{\exists }x\psi (x,{\vec{\tau }}_G)$, choose a witness $a={\sigma }_G$ by step 2.1. Induction gives $p\in G$ forcing $\psi (\sigma ,\vec{\tau })$; monotonicity makes the matrix hold below every $q\le p$, so the existential forcing clause gives $p⊩\mathrm{\exists }x\psi (x,\vec{\tau })$. Conversely suppose $p\in G$ forces the existential. The class $D=\{r:\mathrm{\exists }P\text{-name }\sigma (r⊩\psi (\sigma ,\vec{\tau }))\}$ belongs to $\mathcal{C}$ by step 3.1 and is dense below $p$ by the existential clause. Step 1.4 gives $r\in G\cap D$ and a witnessing name $\sigma$; induction yields $M[G]\models \psi ({\sigma }_G,{\vec{\tau }}_G)$ and hence the existential.

Steps 1.1–2.1 prove stages, names and valuation. Steps 1.3–3.1 prove the class relation is well defined and definable for every fixed formula, and steps 3.2–4.2 prove its truth lemma by formula induction. All choices of head antichains or names in this proof occur inside a set-forcing truth lemma or as one existential witness; the class comprehension and class genericity uses are explicit in steps 1.1, 2.2–3.1 and 1.4–4.2. This proves (a)–(d). ∎