The Independence of the Continuum Hypothesis in Isabelle/ZF

Emmanuel Gunther 📧, Miguel Pagano 🌐, Pedro Sánchez Terraf 🌐 and Matías Steinberg 📧

March 6, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Independence_CH