First steps towards a formalization of forcing

DOI10.1016/J.ENTCS.2019.07.008MaRDI QIDQ2333671zbMATH OpenOpenAlexWikidataFDO

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

Publication date 13 November 2019

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

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)

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.

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

Cites work

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

Cited in

(12)

• scientific article; zbMATH DE number 4068858 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• kepler98
• Isabelle/ZF
• Isar
• Isabelle

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)