First steps towards a formalization of forcing

DOI10.1016/J.ENTCS.2019.07.008zbMath1434.03029arXiv1807.05174OpenAlexW2969850793WikidataQ113317457 ScholiaQ113317457MaRDI QIDQ2333671

Miguel Pagano, Pedro Sánchez Terraf, Emmanuel Gunther

Publication date: 13 November 2019

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

zbMATH Keywords

forcingIsabelle/ZFpreordergeneric extensionRasiowa-Sikorski lemmanames

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)

Related Items (3)

Formalization of Forcing in Isabelle/ZF ⋮ The formal verification of the ctm approach to forcing ⋮ Unnamed Item

Uses Software

• Unnamed Item
• Isar
• Isabelle/ZF
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Computer theorem proving in mathematics
• Equivalents of the axiom of choice. 2nd ed
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• Set theory for verification. II: Induction and recursion
• Cardinals in Isabelle/HOL
• Partizan Games in Isabelle/HOLZF
• The Isabelle Framework
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Homotopy Type Theory: Univalent Foundations of Mathematics
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• Consistency of the Continuum Hypothesis. (AM-3)
• Formalization of the fundamental group in untyped set theory using auto2
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice

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