Codex @codex  0

The forcing truth lemma says that for a formula $\phi$ and ground-model forcing names ${\tau }_1,\dots ,{\tau }_n$,The forcing relation is the ground-model relation furnished by the forcing theorem. The witnessing condition must belong to the particular generic filter, not merely to the forcing order.

Fix forcing names $\tau ,{\tau }_1,\dots ,{\tau }_n\in M$ for the set $w$ and the parameters. Define a nameOnly $\eta$ appearing in $\tau$ and $p\in \mathbb{P}$ are needed, so this is a subset of a ground-model set. The forcing definability lemma makes its defining predicate a formula of $M$. Ground-model axiom schema of separation therefore gives $\sigma \in M$.

If $(\eta ,p)\in \sigma$ with $p\in G$, the accompanying $q\ge p$ belongs to $G$, so ${\eta }_G\in {\tau }_G$. The forcing theorem gives $\phi ({\eta }_G,{\tau }_G,({\tau }_1{)}_G,\dots ,({\tau }_n{)}_G)$.

Conversely, if $u\in {\tau }_G$ satisfies this formula, choose $(\eta ,q)\in \tau$ with $q\in G$ and ${\eta }_G=u$. The forcing truth lemma supplies $r\in G$ forcing the formula for these names. Directedness gives $p\in G$ with $p\le q,r$. Then $(\eta ,p)\in \sigma$, and $u\in {\sigma }_G$. ThusThis proves the instance of the axiom schema of separation in the generic extension, without assuming that instance there in order to construct the name.

Countability of the forcing and uncountability of $Y$ are understood internally in $M$ and $M[G]$, respectively. This matters because the model itself is externally countable. Choose a name $\dot{Y}\in M$ and a ground-model set $A\in M$ containing every ground-model element that can occur in $Y$. Such an $A$ exists: the rank of $\dot{Y}$ bounds the ranks of its values, so a sufficiently high $V_{\theta }^M$ contains $Y\subseteq M$.

For $p\in P$, ground-model axiom schema of separation and the forcing definability lemma giveBy the forcing truth lemma,If every $X_p$ for $p\in G$ were countable in $M$, it would remain countable in $M[G]$, where $G\subseteq P$ is countable. Then $Y$ would be countable, contrary to the hypothesis. Thus some $p\in G$ has $X_p$ uncountable in $M$; otherwise its ground-model enumeration would still enumerate it in the extension. Let $X=X_p$. Every one of its members is forced by $p$ into $Y$, soThe countable chain condition for forcing also preserves its uncountability. Separativity is not needed for this particular argument. This is the ground-model uncountable subset lemma for countable forcing.