Transitive Models of Fragments of ZFC

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

March 3, 2022


We extend the ZF-Constructibility library by relativizing theories of the Isabelle/ZF and Delta System Lemma sessions to a transitive class. We also relativize Paulson's work on Aleph and our former treatment of the Axiom of Dependent Choices. This work is a prerrequisite to our formalization of the independence of the Continuum Hypothesis.


BSD License


Session Transitive_Models