Formalization of Forcing in Isabelle/ZF

Emmanuel Gunther 📧, Miguel Pagano 🌐 and Pedro Sánchez Terraf 🌐

May 6, 2020

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 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.

License

BSD License

Topics

Session Forcing

Cite

× 
@article{Forcing-AFP,
  author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf},
  title   = {Formalization of Forcing in Isabelle/ZF},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Forcing.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: