Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] The Undecidability of the Continuum Hypothesis


view this post on Zulip Email Gateway (Dec 06 2021 at 20:07):

From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
​Dear colleagues,

We would like to share with you that we have completed a formalization
of the independence of CH in Isabelle/ZF. We plan to submit this library
to the AFP once we finish the review of the formalization.

For those who are interested, it is based on the ctm approach to
forcing. You can find more information at
https://cs.famaf.unc.edu.ar/~pedro/forcing/
<https://cs.famaf.unc.edu.ar/~pedro/forcing/>, including links to the
repository and slides from a recent presentation on the consistency of ¬CH.

This project was done by Emmanuel Gunther, Miguel Pagano, Matías
Steinberg, and myself.

Best regards,

On behalf of the team,

Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
cs.famaf.unc.edu.ar/~pedro <https://cs.famaf.unc.edu.ar/~pedro>

view this post on Zulip Email Gateway (Dec 06 2021 at 20:17):

From: Manuel Eberl <manuel@pruvisto.org>
Hello Pedro,

that is amazing news! Let me be the first to congratulate you and your
team on this.

I don't know anything about set theory, but even I know what a cool
result this is and I'm very happy that we will soon have it in the AFP.
I'm sure I speak for all of us when I say that we are looking forward to
your AFP submission and your paper and presentation at whatever venue
you will publish this!

Also note that this is one of Freek Wiedijk's 100 problems [1], so as
soon as your material is all in the AFP, we can notify him to update his
list. With this, Isabelle will finally pull into a well-deserved first
place ahead of HOL Light. Not that it matters very much, but I can't
resist engaging in some silly pointless competitiveness every once in a
while. :)

Cheers,

Manuel

[1]: https://www.cs.ru.nl/~freek/100/

view this post on Zulip Email Gateway (Dec 07 2021 at 08:57):

From: Lawrence Paulson <lp15@cam.ac.uk>
Absolutely terrific news! This was surely hard, and one of the rare applications of Isabelle/ZF.

Larry Paulson


Last updated: Jul 15 2022 at 23:21 UTC