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

- Logic/Set theory

### Session Forcing

- Utils
- Forcing_Notions
- Pointed_DC
- Rasiowa_Sikorski
- Nat_Miscellanea
- Internalizations
- Recursion_Thms
- Relative_Univ
- Synthetic_Definition
- Interface
- Forcing_Data
- Internal_ZFC_Axioms
- Renaming
- Renaming_Auto
- Names
- FrecR
- Arities
- Forces_Definition
- Forcing_Theorems
- Separation_Rename
- Separation_Axiom
- Pairing_Axiom
- Union_Axiom
- Powerset_Axiom
- Extensionality_Axiom
- Foundation_Axiom
- Least
- Replacement_Axiom
- Infinity_Axiom
- Choice_Axiom
- Ordinals_In_MG
- Proper_Extension
- Succession_Poset
- Forcing_Main

## Cite

×

Forcing-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 7, 2020 : Isabelle2020
- May 6, 2020 : Isabelle2020