0

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)$?

Seba Thei
  • 236
  • Ignoring the issue that "$\check{V}$" doesn't actually make sense - which isn't fatal since we can get around this using Laver/Woodin - the answer is yes. It's easiest to see this semantically: Suppose $p$ is a condition and $\tau$ is a name such that for every generic $G\ni p$ we have $\tau[G]\in V$. Let $G$ be some generic filter containing $p$ and let $a\in V$ satisfy $\tau[G]=a$. Since forcing=truth, some condition $s\in G$ has $\Vdash\tau=\check{a}$; since $G$ is a filter $s$ and $p$ have a common extension $r$. ("Syntactifying" this fully will require fixing the $\check{V}$-issue.) – Noah Schweber May 09 '22 at 18:50
  • @Noah: We can also understand it as $\check V_\alpha$ for some large enough $\alpha$. – Asaf Karagila May 10 '22 at 05:31
  • @NoahSchweber thanks for the answer. For the $\check{V}$-issue, I'm using the fact that $V$ is a definable class (with parameter in $V$) in its set-forcing extension. Alternatively, as pointed out, one may write $\exists\alpha\tau\in\check{V}_\alpha$. – Seba Thei May 10 '22 at 08:06

0 Answers0