Formalization of Forcing in Isabelle/ZF (Q7361870)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Forcing
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formalization of Forcing in Isabelle/ZF |
AFP entry Forcing |
Statements
6 May 2020
0 references
Emmanuel Gunther
0 references
Miguel Pagano
0 references
Pedro Sánchez Terraf
0 references
Formalization of Forcing in Isabelle/ZF (English)
0 references
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.
0 references
