Are forcing techniques possible to automate for mechanized reasoning?

Looking at Cohen's success at proving independence of the Axiom of Choice and the Continuum Hypothesis, I was wondering if it was possible to mechanize forcing techniques for the purpose of proving independence (and hence undecidability) of conjectures. It would seem to be useful to test any sentence you're trying to prove or disprove with an automated theorem prover for independence. I'm imagining some automated forcing technique that constructs a model of ZFC plus the conjecture and its negation to prove it isn't a theorem of ZFC (or whatever foundation being used) rather than spinning forever on an undecidable statement, since the incompleteness theorems indicate that any statement in a sufficiently strong formal system can be undecidable.

Its not obvious to me how to automate such a method, as its probably quite a bit more complicated than just implementing resolution, but it would be nice to have automated reasoning go down three paths of searching for proof of a conjecture, proof of its negation, and proof of its independence.

• I'm not 100% clear on what you're asking here. – Asaf Karagila Aug 27 '13 at 1:14
• I was mostly interested in developing some algorithm for searching for independence of a sentence, and was familiar with forcing as the most mature technique for doing so, and wondered if it was applicable to automated theorem proving. The response seems to suggest even if it is, its quite difficult and isn't usually useful for most statements that aren't foundational from a question already asked link here. – dezakin Aug 27 '13 at 4:28

1 Answer

Forcing is not easy to automate. A typical forcing argument requires at the very least a clever choice of the sequence of dense sets that the generic filter will meet. Unless you program a special heuristic into the search, how would it know which dense sets to consider?

In many cases there is even more work to do. For example, in the modern treatment of Cohen's proof of the independence of CH there is the concept of a ccc forcing and the proof that ccc forcings do not collapse cardinals. It would not be straightforward to automate the discovery of that sort of proof - it is not obvious how to narrow the search space for the proof in the right way.

• With respect to the second paragraph, it should be added that sometime we don't know whether or not we want certain properties (sometimes we want to collapse cardinals, and sometimes we don't). Not to mention that sometimes one ends up starting with ultimately-unnecessary assumptions (e.g. Prikry forcing requires a measurable, but we can remove the normality of the measure from the original definition). – Asaf Karagila Aug 27 '13 at 2:33