In the course of a project I’m working on, I’ve started playing around with a sort of “reverse-engineering” forcing. It seems interesting, but I have a sinking feeling I’m reinventing the wheel; does this construction already have a name?
(To me it feels in the same spirit as termspace forcing (https://mihahabic.wordpress.com/tag/termspace-forcing/), but not the same thing.)
Suppose $M\subset N$ are countable transitive models, $r\in N$ is a real (more generally, $r\in N$ is a subset of some $x\in M$ - but I’m only interested in the reals case for now), $\mathbb{P}$ is a forcing notion in $M$, and $\nu$ is a $\mathbb{P}$-name in $M$. Then - in $N$ - we can define a subforcing of $\mathbb{P}$, $\mathbb{P}_M[\nu=r]$, as follows:
$\mathbb{P}_M^0[\nu=r]$ is the set of $p\in\mathbb{P}$ such that there is no $n\in\omega$ such that $p\vdash$ "$\nu(n)=1-r(n)$".
$\mathbb{P}_M^\lambda[\nu=r]=\bigcap_{\alpha<\lambda}\mathbb{P}_M^\alpha[\nu=r]$.
$\mathbb{P}_M^{\alpha+1}[\nu=r]=\{p\in\mathbb{P}_M^\alpha[\nu=r]: \forall D\in\mathcal{P}_{do}^M(\mathbb{P})[\exists q\in D\cap \mathbb{P}_M^\alpha[\nu=r], q\le p]\}$. Here "$\mathcal{P}_{do}$" means "the set of dense open subsets of."
$\mathbb{P}_M[\nu=r]=\bigcap_{\alpha\in ON} \mathbb{P}_M^\alpha[\nu=r]$. Note that we can in fact just take the intersection up to $\vert\mathbb{P}\vert^+$, or $\aleph^*(\mathbb{P})^+$ in lieu of choice.
That is, we form $\mathbb{P}_M[\nu=r]$ by ``carving out” all the conditions of $\mathbb{P}$ which prevent a $\mathbb{P}$-generic filter $G$ over $M$ from satisfying $\nu[G]=r$.
We also obtain a rank function $\rho^M_{\nu=r}: \mathbb{P}\rightarrow\vert\mathbb{P}\vert^+\cup\{\infty\}$ given by $\rho^M_{\nu=r}(p)$ is the least $\alpha$ such that $p$ is not in $\mathbb{P}^\alpha_M[\nu=r]$ (and $\infty$ if $p\in\mathbb{P}_M[\nu=r]$).
It’s now easy to check a few basic properties of this construction:
If there is a $\mathbb{P}$-generic filter over $M$, $G$, such that $\nu[G]=r$, then $\mathbb{P}_M[\nu=r]\not=\emptyset$.
Moreover, in such a case we have: if $G$ is $\mathbb{P}_M[\nu=r]$-generic over $N$, then $G$ is $\mathbb{P}$-generic over $M$ and $\nu[G]=r$.
And if $N=M[r]\subseteq M[G]$ for $r$ a real with name $\nu$, $G$ is $\mathbb{P}_M[\nu=r]$-generic over $N$.
I’m interested in questions about the ranking function $\rho$, as well as the forcing $\mathbb{P}_M[\nu=r]$. For instance:
(For “nice” = “proper,” “c.c.c.,” etc.) Suppose $M\models$``$\mathbb{P}$ is nice” and $N$ is a forcing extension of $M$ by a nice forcing. Under what conditions is $\mathbb{P}_M[\nu=r]$ nice?
and
What is $\sup\{\rho_{\nu=r}^M(p): p\not\in\mathbb{P}_M[\nu=r]\}$? That is, how hard is it to tell that a condition is bad? (I’m tentatively thinking of this as analogous to Scott rank, but that might be a bad analogy.)
Note that the monotonic nature of the construction above is a byproduct of the assumption that $r$ is a subset of a set in the ground model. If we tried to replicate this for more general sets, things get messier. In particular, a kind of injury can occur: a condition may appear bad at some stage, and then later appear safe. I have some ideas for what to do, but I’m much less certain, so I’d also be interested in extensions to such sets if this has been looked at.
