Formalization of Forcing in Isabelle/ZF

DOI10.1007/978-3-030-51054-1_13MaRDI QIDQ5049004zbMATH OpenOpenAlexFDO

Authors 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

absolutenessconstructibilitycountable transitive modelsforcinggeneric extensionIsabelle/ZF

Mathematics Subject Classification ID

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

Cites work

• Consistency of the Continuum Hypothesis. (AM-3)
• First steps towards a formalization of forcing
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Partizan Games in Isabelle/HOLZF
• Set theory.
• Set theory. An introduction to independence proofs
• The foundation of a generic theorem prover
• The Isabelle Framework
• The Lean theorem prover (system description)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf

Cited in

(7)

• 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
• Transitive Models of Fragments of ZFC
• The Independence of the Continuum Hypothesis in Isabelle/ZF
• Formalization of Forcing in Isabelle/ZF
• Cofinality and the Delta System Lemma

Describes a project that uses

Uses Software

• Lean
• Archive of Formal Proofs
• Isabelle
• GitHub

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

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