Authors
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg
Publication date
2022/3
Journal
Arch. Formal Proofs
Volume
2022
Description
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.
Total citations
Scholar articles
E Gunther, M Pagano, PS Terraf, M Steinberg - Arch. Formal Proofs, 2022