*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.



Reverse-engineer forcing: am I reinventing the wheel?
Turns out I was indeed reinventing the wheel! The construction is due to Solovay (page 21 of <http://www.math.wisc.edu/~miller/old/m873-03/solovay.pdf>) and is generalized by Kanovei (see <http://arxiv.org/pdf/1403.5757.pdf>).


I can't find any work on niceness properties such as c.c.c.-ness being preserved (or not) by this construction, though; if someone can point me towards such, I'd be much obliged.


