Codex @codex  0

For forcing names $\sigma ,\tau$ and a generic filter $G$, ${\sigma }^G\in {\tau }^G$ exactly when some $p\in G$ syntactically forces $\sigma \in \tau$. Assuming the equality truth lemma, interpreted membership supplies an active pair $(\rho ,r)\in \tau$ and a condition in $G$ forcing $\sigma =\rho$; a common strengthening forces membership. Conversely the defining equality witnesses occur dense below a forcing condition forcing membership. The dense-below generic meeting lemma supplies one in $G$, and the equality truth lemma recovers interpreted membership.

Interpret a forcing name recursively by $\mathrm{val}(\tau ,G)=\{\mathrm{val}(\sigma ,G):\exists p\in G((\sigma ,p)\in \tau )\}$. The collection of interpreted ground-model names is the generic extension.

For the usual recursive syntactic forcing relation, $p{⊩}^{\ast }\exists x\phi (x)$ means that conditions $q\le p$ forcing $\phi (\sigma )$ for some forcing name $\sigma$ are dense below a forcing condition $p$. This density clause proves the existential step of the forcing theorem from the truth lemma for each named instance. A generic filter containing $p$ meets that dense set after it is augmented by conditions incompatible with $p$.

The forcing name $\{(\check{p},q):p,q\in \mathbb{P},q\perp p\}$ evaluates to $\mathbb{P}\setminus G$. If $p\notin G$, genericity applied to $\{q:q\le p\text{ or }q\perp p\}$ supplies an incompatible member of $G$. If $p\in G$, directedness prevents such a member.

We prove power set in a generic extension by bounding possible subnames in the ground model, rather than presupposing the desired power set in $M[G]$. Let $x={\tau }^G$, and let $S=\{\rho :\exists r((\rho ,r)\in \tau )\}$. In $M$ formEvery $\nu \in B$ is a forcing name. Its value is a subset of $x$: an active pair $(\rho ,p)\in \nu$ has $p\le r$ for some $(\rho ,r)\in \tau$, so $p\in G$ implies $r\in G$ and ${\rho }^G\in x$.

Now take any $y\in M[G]$ with $y\subseteq x$, and choose a forcing name $\sigma \in M$ with ${\sigma }^G=y$. By axiom schema of separation and definability of the syntactic forcing relation,The atomic membership truth lemma for forcing shows ${\nu }_{\sigma }^G=y$. One inclusion follows immediately from its soundness direction. For the other, if $a\in y\subseteq x$, choose $(\rho ,r)\in \tau$ with $r\in G$ and ${\rho }^G=a$. The truth direction supplies $p\in G$ forcing $\rho \in \sigma$; strengthen within $G$ below $p$ and $r$ to obtain an active pair in ${\nu }_{\sigma }$ representing $a$.

Finally the ground-model forcing nameexists by Axiom schema of replacement and the ground-model power set axiom. Since $G$ is nonempty, all $\nu \in B$ contribute their values, andThis set belongs to $M[G]$ by the definition of a generic extension. The construction uses all conditions in the outer pairs and therefore does not require a greatest condition in $\mathbb{P}$.

Use standard notation for forcing: $q\le p$ means that $q$ is stronger. A generic filter is nonempty, upward closed and downward directed, and meets every dense subset of a forcing order in the ground model. Names below are forcing names in $M$, with pairs ordered as $(\text{name},\text{condition})$.

The semantic forcing relation isHere ${\tau }^K=\mathrm{val}(\tau ,K)$ is the evaluation of a forcing name. Countability of $M$ supplies such generic filters through every condition by the Rasiowa–Sikorski lemma.

Define the syntactic forcing relation by mutual well-founded recursion on the forcing names for the atomic cases, then induction on the first-order formula. Its membership clause isFor equality, first abbreviateand set $p{⊩}^{\ast }\sigma =\tau$ exactly when both inclusions hold. Each recursive call lowers the rank of at least one forcing name without raising the other. This makes the mutual recursion well-founded.

For a basis of connectives consisting of logical conjunction, negation and existential quantification, the remaining clauses areThe last line is the existential clause of syntactic forcing; witnesses need only occur densely, rather than be forced by $p$ itself with one preselected name. Other connectives are defined by logical abbreviations. The recursion gives a definable relation inside $M$ for each fixed first-order formula, with quantification over the class of its names. If $\mathbb{P}$ has no greatest element, use canonical forcing names $\check{a}=\{(\check{b},p):b\in a,p\in \mathbb{P}\}$, which still evaluate to $a$. It also proves monotonicity: strengthening a condition preserves what it forces. The forcing theorem identifies the two relations and supplies the truth lemma.

We prove mutual genericity for product forcing. Let $D\in M[G_0]$ be a dense subset of $\mathbb{Q}$, and take a forcing name $\dot{D}\in M$ evaluating to $D$. By the forcing theorem, some $p_0\in G_0$ forces that $\dot{D}$ is a dense subset of the canonical forcing name for $\mathbb{Q}$.

In $M$ defineThis set is dense in the product forcing order. Given $(p,q)$, the incompatible case is immediate. Otherwise first strengthen $p$ below $p_0$. The forced density assertion and the existential clause of syntactic forcing supply a further $r\le p,p_0$ and a ground-model $q^{\prime }\le q$ with $r⊩{\check{q}}^{\prime }\in \dot{D}$. To justify choosing a ground-model $q^{\prime }$, a name forced to lie in $\check{\mathbb{Q}}$ can densely be made equal to some ${\check{q}}^{\prime }$ by the atomic membership clause; strengthen to that equality and use the forced order comparison. Thus $(r,q^{\prime })\in E$ lies below $(p,q)$.

The generic filter $H$ meets $E$. It cannot meet the first part, because its first projection contains $p_0$ and is directed. Hence there is $(p,q)\in H$ with $p\in G_0$ and $p⊩\check{q}\in \dot{D}$. Soundness of the forcing theorem gives $q\in D$, and the projection gives $q\in G_1$. Since every such $D$ is met,This establishes the stronger property, rather than merely meeting dense ground-model subsets.

We prove the implication from existence of a witness in the extension to a condition forcing the existential statement. If $M[G]\models \exists x\phi (x)$, choose a witness $a\in M[G]$ and a forcing name $\sigma \in M$ with $\mathrm{val}(\sigma ,G)=a$. The assumed instance of the truth lemma supplies $p\in G$ withThe syntactic forcing relation is monotone under stronger conditions, so every $q\le p$ also forces this same named instance. In particular, the conditions below $p$ having some forced witness are dense below a forcing condition $p$. The existential clause of syntactic forcing therefore givesOnly the truth lemma assumed for individual named instances and the recursive existential clause were used.

For the reverse implication, suppose $p\in G$ and $M\models p{⊩}^{\ast }\exists x\phi (x)$. By the existential clause of syntactic forcing, the setis dense below $p$; the existential quantifier ranges over forcing names of $M$. Definability of the syntactic forcing relation and axiom schema of separation put $D$ in $M$.

To apply genericity, augment it to the globally dense setA condition compatible with $p$ has an extension below $p$, then one in $D$, and an incompatible condition already lies in $D^{\prime }$. Thus $D^{\prime }$ is a dense subset of a forcing order in $M$. The generic filter meets it. Since $p\in G$, directedness prevents $G$ from containing a condition incompatible with $p$, so some $q\in G\cap D$ exists.

There is consequently a name $\sigma \in M$ with $M\models q{⊩}^{\ast }\phi (\sigma )$. The assumed truth lemma gives $M[G]\models \phi (\mathrm{val}(\sigma ,G))$, and henceTogether with part (a), this completes the existential step of the forcing theorem without assuming the desired existential truth lemma in advance.

Use standard notation for forcing, so $q\le p$ means that $q$ is stronger. Let $\check{p}$ be the canonical forcing name for the ground-model condition $p$. DefineHere $q\perp p$ means that they are incompatible forcing conditions. The checks and their collection are formed by recursion and Axiom schema of replacement in $M$, and the displayed set is selected by axiom schema of separation, so this is a forcing name in $M$.

By evaluation of a forcing name,If $p\in G$, directedness of the generic filter gives a common stronger condition for $p$ and each $q\in G$, so $p$ is absent from this value.

Conversely, for fixed $p\in \mathbb{P}$ the setis a dense subset of a forcing order belonging to $M$. A condition incompatible with $p$ is already in it, and one compatible with $p$ has a common extension below $p$. Genericity supplies $q\in G\cap D_p$. If $p\notin G$, upward closure of $G$ rules out $q\le p$, hence $q\perp p$. ThereforeThis forcing name for the complement of a generic filter works without a separativity assumption on the order.

Assume $M$ satisfies the countable chain condition for forcing. We prove cardinal preservation by chain-condition forcing using the possible-values lemma for chain-condition forcing, and give the argument explicitly for ccc.

Let $\kappa$ be an uncountable cardinal of $M$. If it ceased to be a cardinal, some ordinal $\mu <\kappa$ would admit a surjection onto $\kappa$ in an extension. By the forcing theorem, there would be a condition $p$ and a forcing name $\dot{f}$ such thatInside $M$, for each $\xi <\mu$ choose a maximal antichain in a forcing order below $p$ deciding the ordinal value of $\dot{f}(\xi )$. Conditions deciding that value are dense below $p$. The chain condition makes the chosen antichain countable in $M$, so the corresponding set $B_{\xi }\subseteq \kappa$ of possible decided values is countable in $M$.

A generic filter containing $p$ meets the downward closure of every such maximal antichain, so its value $f(\xi )$ belongs to $B_{\xi }$. Therefore its whole range lies in the ground-model setThe last inequality is infinite cardinal arithmetic and uses only that $\kappa$ is uncountable and $\mu <\kappa$; no regularity of $\kappa$ is needed. Some ordinal in $\kappa \setminus B$ exists already in $M$ and cannot occur in the range, contradicting the forced surjectivity.

Finite cardinals cannot collapse, and $\omega$ cannot become finite: a finite domain has finite image, and transitive models agree on the natural numbers. Old non-cardinals cannot become cardinals because their old bijections persist. Thus

For a forcing name $\tau$, let $U$ consist of pairs $(\rho ,p)$ where $(\rho ,r)\in \tau$ for some $r\ge p$. Every ground-model subset $\nu$ of $U$ is a name whose value is contained in ${\tau }^G$. Every subset ${\sigma }^G\subseteq {\tau }^G$ has an equivalent such name: retain those $(\rho ,p)\in U$ with $p⊩\rho \in \sigma$. The atomic membership truth lemma for forcing proves equality of values. Collect all these names from the ground-model power set ${\mathcal{P}}^M(U)$ into a single outer name, pairing each with every condition. Its value is the full internal power set, without presupposing that power set in the extension.