### Abstract

We redeveloped our formalization 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 proper generic extensions that satisfy the Continuum Hypothesis and its negation.

### License

BSD License

### Topics

- Logic/Set theory

### Session Independence_CH

- Forcing_Notions
- Cohen_Posets_Relative
- Edrel
- FrecR
- FrecR_Arities
- Fm_Definitions
- Internal_ZFC_Axioms
- Interface
- Separation_Instances
- Replacement_Instances
- ZF_Trans_Interpretations
- Forcing_Data
- Forces_Definition
- Names
- Forcing_Theorems
- Ordinals_In_MG
- Separation_Rename
- Separation_Axiom
- Pairing_Axiom
- Union_Axiom
- Powerset_Axiom
- Extensionality_Axiom
- Foundation_Axiom
- Replacement_Axiom
- Infinity_Axiom
- Choice_Axiom
- Proper_Extension
- Succession_Poset
- Forcing_Main
- Cardinal_Preservation
- Not_CH
- Kappa_Closed_Notions
- CH
- Absolute_Versions
- Definitions_Main
- Demonstrations

### Depends on

- Transitive Models of Fragments of ZFC

### Auto-related entries

- Formalization of Forcing in Isabelle/ZF
- Cofinality and the Delta System Lemma

## Cite

×

Independence_CH-AFP

    @article{Independence_CH-AFP,
      author  = {Emmanuel Gunther and Miguel Pagano and Pedro Sánchez Terraf and Matías Steinberg},
      title   = {The Independence of the Continuum Hypothesis in Isabelle/ZF},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Independence_CH.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

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