Forcing relation: names and check names

36 Views Asked by At

Let $P\in V$ be a forcing notion and let $\varphi(x,\sigma_1,\dots,\sigma_n)$ be a formula in the forcing language, where $\sigma_1,\dots,\sigma_n$ are $P$-names. Suppose there is a condition $p\in P$ such that $p\Vdash\exists x\in\check{V}\big(\varphi(x,\sigma_1,\dots,\sigma_n)\big)$. It is well know that if $q\leq p$, then there are $r\leq q$ and $\tau\in V^P$ such that $r\Vdash \varphi(\tau,\sigma_1,\dots,\sigma_n)\wedge \tau\in\check{V}$. Let $q\leq p$. Is it possible to prove that there are $r\leq q$ and $a\in V$ so that $r\Vdash \varphi(\check{a},\sigma_1,\dots,\sigma_n)$?