INVESTIGADORES
SANCHEZ TERRAF Pedro Octavio
artículos
Título:
The formal verification of the ctm approach to forcing
Autor/es:
GUNTHER, EMMANUEL; PAGANO, MIGUEL; SÁNCHEZ TERRAF, PEDRO; MATÍAS STEINBERG
Revista:
ANNALS OF PURE AND APPLIED LOGIC
Editorial:
ELSEVIER SCIENCE BV
Referencias:
Lugar: Amsterdam; Año: 2024
ISSN:
0168-0072
Resumen:
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model M of ZFC , of generic extensions satisfying ZFC + ¬CH and ZFC + CH . Moreover, let R be the set of instances of the Axiom of Replacement. We isolated a 21-element subset Ω ⊆ R and defined F : R → R such that for every Φ ⊆ R and M -generic G, M |= ZC ∪ FΦ ∪ Ω implies M [G] |= ZC ∪ Φ ∪ {¬CH }, where ZC is Zermelo set theory with Choice.To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others.
