The Independence of the Continuum Hypothesis in Isabelle/ZF

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

6 March 2022


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

Depends On


Related Entries