Formalization of Forcing in Set Theory

Emmanuel Gunther¹, Miguel Pagano¹, Pedro Sánchez Terraf^1,2, and Matías Steinberg¹

The Relative Consistency of CH in Isabelle/ZF (2022)

We developed relative versions of the Axiom of Dependent choices in order to formalize (ω+1)-closed forcing notions. Using this we are able to construct, given a countable transitive model M of ZFC, a generic extension satisfying ZFC plus the Continuum Hypothesis.

You can download the paper and look at the development for Isabelle2021-1 (with the AFP component enabled) at our Bitbucket repository, download the sources and generated documents, and browse the generated HTML. Sources for our treatment of relativization are also available. This project also appears as an AFP entry and in Wiedijk's 100 Theorems list.

The Unprovability of CH in Isabelle/ZF (2021)

We finished our formalization of the construction, given a countable transitive model M of ZFC, of a generic extension satisfying ZFC plus the negation of the Continuum Hypothesis.

You can look at the development at our Bitbucket repository and browse the cross-linked session as generated by Isabelle2021. Also slides from the virtual talk at the Set Theory and its Interactions session at CLAM2021 are available.

Formalization of Forcing in Isabelle/ZF (2020)

We formalize the theory 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 a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library.

You can download the paper (accepted at IJCAR 2020; arXiv:2001.09715; video of the talk) and the whole Isabelle 2019 development. You can also browse the session as generated by Isabelle. [New: cross-linked session for Isabelle 2020]

Mechanization of Separation in Generic Extensions (2019)

We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson’s library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened of the hypotheses in his development of relativization and absoluteness.

The manuscript is available at arXiv:1901.03313.

Previous stages of our project were announced here.