I’m reading the chapter on Forcing of Kunen’s Set Theory, where he discusses the implications of the Definability Lemma on the Comprehension Axiom:
where the referenced equation is:
And the preceding discussion regarding the problem with comprehension is:
[…] say $\varphi(x,y)$ is a formula and $\sigma \in M^\mathbb{P}$. Why should the set $S=\{n\in\omega: (\varphi(n,\sigma_G))^{M[G]}\}$ be in $M[G]$?
As I understand it, the Definability Lemma implies that for some formula $\psi$ in the language of set theory $\{\in\}$ we have
$$\{(p,\mathbb{P},\le,\mathbb{1},\vartheta_1,\vartheta_2): (\mathbb{P},\le,\mathbb{1})\ \text{is a forcing poset}\wedge p\in\mathbb{P}\wedge \vartheta_1,\vartheta_2\in M^\mathbb{P} \wedge p \Vdash_{\mathbb{P},M}\varphi(\vartheta_1,\vartheta_2)\} $$ $$=\{x\in M:\psi(x)\}$$
so to see $\tau\in M$ it would suffice to show $\tau$ belongs to the first set. Is this correct? How would I go about proving it?
The set given in the lemma is not a set of names or a name itself, therefore you can't prove $\tau$ is an element of your first set. However, Your reasoning which says the first set is of the form $\{x\in M : \psi(x)\}$ is correct, so we can use it to specify names from a set of names.
For example, you can easily check that the set of names $\{(\check{n},p) : n<\omega\land p\in P\}$ is a member of $M$. By comprehension on $M$, the set $$\{(\check{n},p) : n<\omega\land p\in P\land \psi(p,\check{n})\}$$ is an element of $M$, where $\psi(p,\check{n})$ is a formula which is equivalent to $$p\in P\land \check{n}\in M^P\land p\Vdash_{P,M} \phi(\check{n},\sigma).$$
In fact, the form of $\psi$ is not exactly same to that of the formula in the theorem. However we know that $P$ is a forcing poset of $M$ so we can just join a formula that asserts "$P$ is a forcing poset" at a side of $\psi$ and we can make it to have that form.