The forcing theorem for Gitik's expanded proper-class language

A $P_3$-name is a set whose transitive closure contains only set many conditions. By F1, the union of their finite coordinate supports is bounded by a regular $\theta$, so rank induction makes the name a $P_{\theta }$-name. A finite tuple has a common regular bound, as does that tuple together with any one witness name or condition.

For names $\tau ,\sigma$ and a condition $p$, define $p{⊩}_3\tau \in \sigma$ iff some regular $\theta$ satisfies: for every regular $\eta \ge \theta$, $p\in P_{\eta }$, $\tau ,\sigma$ are $P_{\eta }$-names, and $p{⊩}_{P_{\eta }}\tau \in \sigma$; define equality identically. F1 gives a starting bound. If $\theta \le \eta$, completeness of $P_{\theta }\subseteq P_{\eta }$ preserves the set-forcing value of atomic formulas on $P_{\theta }$-names: a maximal antichain deciding the atomic statement in $P_{\theta }$ remains maximal in $P_{\eta }$. Thus the eventual value exists, is independent of the starting bound, and is first-order definable by F3.

Using the atomic equality relation from step 1.2, define the three new atoms by density below $p$: $p{⊩}_{3}B(\tau )$ iff $\{q\le p:(\mathrm{\exists }x\in M)q{⊩}_3\tau =\check{x}\}$ is dense below $p$; $p{⊩}_{3}A(\tau ,\sigma )$ iff $\{q\le p:(\mathrm{\exists }(a,b)\in P_3)q\le (a,b),q{⊩}_3\tau =\check{a},q{⊩}_3\sigma =\check{b}\}$ is dense below $p$; and $p{⊩}_3{W}_O(\tau ,\sigma )$ iff $\{q\le p:(\mathrm{\exists }x,y\in M)W_O(x,y),q{⊩}_3\tau =\check{x},q{⊩}_3\sigma =\check{y}\}$ is dense below $p$. All quantifiers range over sets satisfying definable class predicates, so these are first-order formulas rather than quantification over a set of all conditions or names.

Suppose $p\in G$ and $\tau ,\sigma$ have a common bound $\theta$. The restriction $G_{\theta }$ is $P_{\theta }$-generic by F1. The set-forcing truth lemma F3 identifies the eventual atomic relations from step 1.2 with ${\tau }_G\in {\sigma }_G$ and ${\tau }_G={\sigma }_G$: evaluation of bounded names by $G$ equals evaluation by every sufficiently large $G_{\eta }$. Conversely, when one of these atomic statements is true, F3 supplies a condition in some $G_{\eta }$ forcing it, and that condition forces the same eventual value.

For every fixed expanded formula, recurse externally through its finite syntax. Use conjunction in the usual way, let $p{⊩}_3\mathrm{\neg }\psi$ iff no $q\le p$ forces $\psi$, and let $p{⊩}_3\mathrm{\exists }x\psi (x,\vec{\tau })$ iff $\{q\le p:(\mathrm{\exists }\text{ set name }\sigma )q{⊩}_3\psi (\sigma ,\vec{\tau })\}$ is dense below $p$. Namehood and $P_3$ are definable classes, so each fixed recursion clause is first order. This is a scheme indexed externally by formulas, not a uniform satisfaction predicate. Induction also gives persistence under strengthening.

The dense clauses have the intended truth values. If $p\in G$ forces $B(\tau )$, genericity meets the dense class below $p$, giving $q\in G$ and $x\in M$ with $q{⊩}_3\tau =\check{x}$; hence ${\tau }_G=x\in M$. Conversely, if ${\tau }_G=x\in M$, atomic set-stage truth gives $q\in G$ forcing $\tau =\check{x}$, and persistence makes every extension of $q$ a witness to the $B$-clause. The $W_O$ proof is identical. For $A$, a forward witness has $q\le (a,b)$ with $q\in G$, so upward closure puts $(a,b)\in G$ and atomic truth gives $({\tau }_G,{\sigma }_G)=(a,b)$. Conversely, if this pair is a condition in $G$, directedness combines it with conditions forcing the two equalities; their common refinement makes the witnesses dense below it.

Induct on formula complexity. Conjunction follows immediately. For negation, if $p\in G$ forces $\mathrm{\neg }\psi$, no member of $G$ below $p$ forces $\psi$, so induction makes $\psi$ false. Conversely, if $\mathrm{\neg }\psi$ is true, no condition in $G$ forces $\psi$; the defining negation clause makes the conditions deciding $\psi$ dense, so $G$ contains one forcing $\mathrm{\neg }\psi$. If $p\in G$ forces an existential, genericity meets its dense witness class; a resulting $q\in G$ and set name $\sigma$ satisfy $q{⊩}_3\psi (\sigma ,\vec{\tau })$, and induction makes ${\sigma }_G$ a witness. Conversely, a true existential has a set witness $y\in M[G]$; F1 supplies a bounded name $\sigma$ for $y$, induction supplies $q\in G$ forcing $\psi (\sigma ,\vec{\tau })$, and persistence makes $q$ force the existential clause.

Steps 2.2–4.1 prove both implications of the truth lemma for every fixed expanded formula, and steps 1.2–3.1 prove definability. Step 1.1 bounds every parameter tuple and each actual witness; step 1.2 gives the stronger eventual-stage invariance exactly for membership and equality. The $A$-predicate remains a predicate for the full generic class, so no unsupported uniform stage bound for arbitrary expanded formulas has been inferred. The only choice principle present is the declared ground AC/global-well-order hypothesis F5.