First steps towards a formalization of forcing

DOI10.1016/J.ENTCS.2019.07.008zbMATH Open1434.03029arXiv1807.05174OpenAlexW2969850793WikidataQ113317457 ScholiaQ113317457MaRDI QIDQ2333671FDOQ2333671

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf 

Publication date: 13 November 2019

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 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 $M[G]$ is transitive.

Full work available at URL: https://arxiv.org/abs/1807.05174

Recommendations

• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• An axiomatic approach to forcing and generic extensions
• Forcing in Proof Theory
• The discovery of forcing.
• A beginner's guide to forcing

zbMATH Keywords

forcingpreordergeneric extensionRasiowa-Sikorski lemmanamesIsabelle/ZF

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Consistency and independence results (03E35) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• The Isabelle Framework
• Homotopy type theory. Univalent foundations of mathematics
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• Consistency of the Continuum Hypothesis. (AM-3)
• Partizan Games in Isabelle/HOLZF
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Formal proof - the four color theorem
• Set theory.
• Equivalents of the axiom of choice. 2nd ed
• Computer theorem proving in mathematics
• Title not available (Why is that?)
• A formal proof of the Kepler conjecture
• Set theory for verification. II: Induction and recursion
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• Cardinals in Isabelle/HOL
• Tutorial to locales and locale interpretation

Cited In (12)

• Formalizing ordinal partition relations using Isabelle/HOL
• The formal verification of the ctm approach to forcing
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Title not available (Why is that?)
• Forcing with propositional Lindenbaum algebras
• Forcing in Proof Theory
• Provident sets and rudimentary set forcing
• Forcing for first-order languages from the perspective of Rasiowa-Sikorski lemma
• Rasiowa-Sikorski sets and forcing
• An axiomatic approach to forcing and generic extensions
• Formalization of Forcing in Isabelle/ZF
• Title not available (Why is that?)

Uses Software

• Isabelle
• Isar
• Isabelle/ZF
• kepler98

This page was built for publication: First steps towards a formalization of forcing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2333671)