# 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