Mostrar el registro sencillo del ítem
dc.contributor.author
Gunther, Emmanuel
dc.contributor.author
Pagano, Miguel Maria
dc.contributor.author
Sanchez Terraf, Pedro Octavio
dc.date.available
2020-12-02T20:50:02Z
dc.date.issued
2019-08
dc.identifier.citation
Gunther, Emmanuel; Pagano, Miguel Maria; Sanchez Terraf, Pedro Octavio; First steps towards a formalization of forcing; Elsevier; Electronic Notes in Theoretical Computer Science; 344; 8-2019; 119-136
dc.identifier.issn
1571-0661
dc.identifier.uri
http://hdl.handle.net/11336/119677
dc.description.abstract
We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set M, we define its generic extension M[G], the canonical names for elements of M, and finally show that if M satisfies the axiom of pairing, then M[G] also does. We also prove that M[G] is transitive.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Elsevier
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
FORCING
dc.subject
GENERIC EXTENSION
dc.subject
ISABELLE/ZF
dc.subject
NAMES
dc.subject
PREORDER
dc.subject
RASIOWA-SIKORSKI LEMMA
dc.subject.classification
Matemática Pura
dc.subject.classification
Matemáticas
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
dc.subject.classification
Ciencias de la Computación
dc.subject.classification
Ciencias de la Computación e Información
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
dc.title
First steps towards a formalization of forcing
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2020-11-19T21:18:30Z
dc.journal.volume
344
dc.journal.pagination
119-136
dc.journal.pais
Países Bajos
dc.journal.ciudad
Amsterdam
dc.description.fil
Fil: Gunther, Emmanuel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.description.fil
Fil: Pagano, Miguel Maria. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina
dc.description.fil
Fil: Sanchez Terraf, Pedro Octavio. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Córdoba. Centro de Investigación y Estudios de Matemática. Universidad Nacional de Córdoba. Centro de Investigación y Estudios de Matemática; Argentina. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomia y Física. Sección Matemática; Argentina
dc.journal.title
Electronic Notes in Theoretical Computer Science
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://linkinghub.elsevier.com/retrieve/pii/S157106611930026X
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1016/j.entcs.2019.07.008
Archivos asociados