### Abstract

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.

### License

BSD License

### Topics

- Logic/Set theory

### Session Transitive_Models

- Utils
- Nat_Miscellanea
- ZF_Miscellanea
- Renaming
- Renaming_Auto
- M_Basic_No_Repl
- Eclose_Absolute
- Recursion_Thms
- Datatype_absolute
- Internalize
- Rec_Separation
- Satisfies_absolute
- DPow_absolute
- Synthetic_Definition
- Internalizations
- Least
- Higher_Order_Constructs
- Relativization
- Discipline_Base
- Arities
- Discipline_Function
- Lambda_Replacement
- Discipline_Cardinal
- Univ_Relative
- Cardinal_Relative
- CardinalArith_Relative
- Aleph_Relative
- Cardinal_AC_Relative
- FiniteFun_Relative
- ZF_Library_Relative
- Replacement_Lepoll
- Cardinal_Library_Relative
- Delta_System_Relative
- Pointed_DC_Relative
- Partial_Functions_Relative

### Depends on

- Cofinality and the Delta System Lemma

### Used by

- The Independence of the Continuum Hypothesis in Isabelle/ZF

### Auto-related entries

- The Independence of the Continuum Hypothesis in Isabelle/ZF

## Cite

×

Transitive_Models-AFP

    @article{Transitive_Models-AFP,
      author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and Matías Steinberg},
      title   = {Transitive Models of Fragments of ZFC},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Transitive_Models.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Mar 4, 2022 : Isabelle2021-1