Forcing proofs tend to be fairly constructive, in the sense that if I claim that there is a forcing that does something, I usually prove this by constructing that forcing.
There are only a handful of exceptions, where we prove that a forcing notion that does the trick exists, but we use abstract argument instead of specifying the forcing. For example Itay Neeman's proof of the consistency of the tree property up to $\aleph_{\omega+1}$,
Neeman, Itay, The tree property up to $\aleph_{\omega+1}$, J. Symb. Log. 79, No. 2, 429-459 (2014). ZBL1338.03099.
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. (One can argue that even in that case the forcing is somewhat specified.)
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 existence forcing proofs?
