INVESTIGADORES
SANCHEZ TERRAF Pedro Octavio
artículos
Título:
Formalization of forcing in Isabelle/ZF
Autor/es:
GUNTHER, EMMANUEL; PAGANO, MIGUEL; PEDRO SÁNCHEZ TERRAF
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer
Referencias:
Lugar: Heidelberg; Año: 2020
ISSN:
0302-9743
Resumen:
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. In doing so, we remodularized Paulson´s ZF-Constructibility library.
