# What examples of existence forcing proofs are there?

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?

• How about "non-explicit" instead of "non-constructive"? – Andrej Bauer Jun 5 '19 at 10:36
• Andrej, I know that constructive has a specific meaning, but in order to prove that CH is false, I literally construct a forcing that does that. In order to prove that it is consistent from a measurable cardinal that there is a cardinal preserving forcing that changes its cofinality to $\omega$, I literally construct it. I'll be happy to amend my terminology, but the word "explicit" doesn't fit in my head to the situation. – Asaf Karagila Jun 5 '19 at 10:38
• I agree with you, except that the word "constructive" has acquired a different meaning (namely, that a proof is carried out in intuitionistic logic, possibly with some extra anti-classical principles). – Andrej Bauer Jun 5 '19 at 10:45
• @AndrejBauer Many mathematicians don't agree that the word "constructive" is owned by the intuitionistic logicians. This word is very commonly used in mathematics with a much looser meaning to mean something like "following a construction", even when that construction does not obey the rules of whatever constructive logic one might have in mind. In this sense, I find it over-reaching to claim that the word "constructive" has acquired another meaning in any absolute sense---it has only acquired that meaning in the contexts specifically about constructive logic, and not in mathematics generally. – Joel David Hamkins Jun 5 '19 at 14:50
• First thing that comes to mind is showing that the set of forcings fulfilling your goal is comeager in an appropriate Baire space of posets... – Pedro Sánchez Terraf Jun 5 '19 at 15:39