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.


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.


BSD License


Session Forcing