In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence of the continumm hypothesis (abbr. CH).

I have read the article mentioned above, and I know that he does not provide a full metatheory, but only some instantiations required to achieve his goal; for example, he does not prove the fact that every $\Delta_0$-formula is absolute w.r.t. transitive models. Instead, he only proves the absoluteness of some useful concepts.

In the entire article, the author avoids metatheoretic arguments as much as possible. I didn't understand the reason why he did that, though it was very difficult in that time. We cannot hope, however, to formalize forcing arguments because it heavily relies on metatheory. For example, a forcing relation $p\Vdash \phi$ is defined for every formula $\phi$, so the definition of a forcing relation is in fact a metadefinition for each formula $\phi$.

Is the difficulty to handle metatheory the reason why nobody has tried to formalize the forcing arguments and the independence proof of the continuum hypothesis? 15 years have passed from when that article appeared, so I hope someone has found a way to formalize meta-arguments.

In short, my question is:

  1. Is there any attempt to mechanize an independence proof of CH?

  2. If not, what makes it so difficult? I guess handling metamathematics causes a problem. Is that right?

  • 6
    $\begingroup$ There is no obstacle to formalizing forcing in principle. It's just that nobody has done it for set theory. It's not more difficult that any other comparable proof in logic. There are formalizations of presheaf models of type theory, for instance, and that is half-way to having forcing, see for instance github.com/ppedrot/coq-forcing $\endgroup$ Feb 12, 2017 at 13:03
  • $\begingroup$ I have found that J. Han and F. van Doorn published a formalized proof of the independence of the continuum hypothesis by formalizing Boolean-valued models into Lean 3 theorem prover. $\endgroup$
    – Hanul Jeon
    Nov 27, 2019 at 17:53


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.