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.

Abstract

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.

License

BSD License

Topics

Session Independence_CH

Depends on

Auto-related entries

Cite

× 
@article{Independence_CH-AFP,
  author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and Matías Steinberg},
  title   = {The Independence of the Continuum Hypothesis in Isabelle/ZF},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Independence_CH.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: