Email Gateway (Mar 07 2022 at 14:11): Email Gateway (Mar 07 2022 at 14:11):From: Lawrence Paulson <lp15@cam.ac.uk>
Sooner than I expected (and remarkable at any time), we have another contribution using Isabelle/ZF: The Independence of the Continuum Hypothesis. It is again by Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf and and Matías Steinberg:
We redeveloped our formalization of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct proper generic extensions that satisfy the Continuum Hypothesis and its negation.
A remark for the confused: Isabelle/ZF is a separate instance of Isabelle, which extends Isabelle/FOL (first-order logic) with the Zermelo Frankel axioms, so it is a reasonably orthodox implementation of ZF (and ZFC). It is independent from Isabelle/HOL, with a lot less automation: basic data types, auto, blast but no arithmetic decision procedures, sledgehammer or counterexample finders. So it is a much tougher world to work in than, say, Isabelle/HOL plus the AFP entry ZFC_in_HOL.
It’s online at https://www.isa-afp.org/entries/Independence_CH.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC