7
$\begingroup$

The website Formalizing 100 Theorems by Freek Wiedijk contains a list of some theorems that were chosen at some point as good candidates for formalization (because of their complexity, their importance, etc.) This website seems to be updated very often.

Among the proofs not yet formalized is that of the independence of the Continuum Hypothesis from the axioms of set theory.

What is the current state of the formalization of the independence of $\mathit{CH}$ from $\mathit{ZFC}$?

I browsed this site for more information, and I found this recent question, as well as this one and this, and an answer in math.SE. But I couldn't find information directly concerned with my question.

EDIT. We finished our formalization of the countable transitive model approach to forcing and the independence of $\mathit{CH}$. The paper is available here and at the arXiv.

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ The [proof-theory] tag was suggested on this, but it seems to me that this is a little different: This one is just about implementing some of the usual proofs. But I'll be glad to hear some argument supporting the tag. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Mar 25, 2017 at 11:40
  • 3
    $\begingroup$ math.stackexchange.com/questions/2205154/… $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 27, 2017 at 13:25
  • 1
    $\begingroup$ This is great! But what is the exact theorem that you formalized? The countable transitive model approach to forcing, after all, does not achieve the strongest form of the result. Also, why did you choose that approach rather than the Boolean-valued model approach, which seems more direct and also more general and powerful? $\endgroup$
    – Joel David Hamkins
    Commented Mar 19 at 22:24
  • 1
    $\begingroup$ Thanks @JoelDavidHamkins! We (only) prove, in ZF, that given a ctm of ZFC, there exist models of ZFC+CH and ZFC+¬CH. We actually identify the always anonymous "sufficient amount of replacement" (though Matthias already knew about this). We chose ctms because that's the first approach we understood ;-). We discuss this for the comparison to the Lean formalization. BVM are indeed more elegant. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Mar 19 at 22:36
  • $\begingroup$ Isn't that version of the theorem provable even in PA or much less? One doesn't need ZF in the background once one has the countable transitive model. $\endgroup$
    – Joel David Hamkins
    Commented Mar 20 at 1:07

1 Answer 1

Reset to default
8
$\begingroup$

Jesse Michael Han and Floris van Doorn recently formalized the independence of the continuum hypothesis in the Lean theorem prover. See the Flypitch project webpage for their papers and code.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Thanks, I'm aware of their results. Actually, this surprised us in the middle of our development of the ctm approach to forcing in Isabelle/ZF (for instance see here). We'll soon upload some new material on that. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Jan 2, 2020 at 13:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .