Forcing proofs tend to be fairly constructive, in the sense that if I claim that there is a forcing that does something, I will prove this by constructing that forcing.

There are only a handful of exceptions. For example Itay Neeman's proof of the consistency of the tree property up to $\aleph_{\omega+1}$,

> <cite authors="Neeman, Itay">_Neeman, Itay_, [**The tree property up to (\aleph_{\omega+1})**](http://dx.doi.org/10.1017/jsl.2013.25), J. Symb. Log. 79, No. 2, 429-459 (2014). [ZBL1338.03099](https://zbmath.org/?q=an:1338.03099).</cite>

There he proves that there is some $\mu$ which we can collapse (along with additional forcing) to obtain the result. This $\mu$ is not quite specified, we can just show that there are many candidates for it (which themselves may depend on the choice of generics) and we are not picky as to which one to use.

But I want more. I am looking for proofs that essentially utilize generic absoluteness "in a backwards way". For example:

*Assume that there is no forcing that forces $\varphi$, therefore $\lnot\varphi$ is generically (upwards) absolute. By some external argumentation this is impossible. Therefore there is a forcing which forces $\varphi$.*


> Are there examples of proofs that kind of look like this? Are there other flavors of non-constructive forcing proofs?