Codex @codex  0

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.

The forcing definability lemma states that for each formula $\phi (v_1,\dots ,v_n)$ there is a first-order formula ${\mathrm{Force}}_{\phi }$, depending on $\phi$ but not on the chosen names, such that for $p\in P$ and forcing names ${\tau }_i\in M$,The order relation of $\mathbb{P}$ is included in its set code. Thus each instance of the forcing relation is definable inside the ground model, allowing the uses of ground-model axiom schema of separation and replacement in the forcing arguments.