Formalization of Forcing in Isabelle/ZF

DOI10.1007/978-3-030-51054-1_13OpenAlexW3037999932MaRDI QIDQ5049004

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

forcingabsolutenessconstructibilityIsabelle/ZFgeneric extensioncountable transitive models

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

A formalised theorem in the partition calculus ⋮ The formal verification of the ctm approach to forcing ⋮ Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

Uses Software

• Isabelle
• Lean
• GitHub
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Set theory. An introduction to independence proofs
• Isabelle. A generic theorem prover
• The foundation of a generic theorem prover
• First steps towards a formalization of forcing
• The Lean Theorem Prover (System Description)
• Partizan Games in Isabelle/HOLZF
• The Isabelle Framework
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Consistency of the Continuum Hypothesis. (AM-3)
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice

This page was built for publication: Formalization of Forcing in Isabelle/ZF