Transitive Models of Fragments of ZFC

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

March 3, 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.


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