The formal verification of the ctm approach to forcing

DOI10.1016/j.apal.2024.103413arXiv2210.15609OpenAlexW4391344760WikidataQ126471355 ScholiaQ126471355MaRDI QIDQ6151819

Matías Steinberg, Pedro Sánchez Terraf, Emmanuel Gunther, Miguel Pagano

Publication date: 11 March 2024

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

continuum hypothesisIsabelle/ZFproof assistantsgeneric extensioninteractive theorem proverscountable transitive models

Mathematics Subject Classification ID

Consistency and independence results (03E35) Axiomatics of classical set theory and its fragments (03E30) Ordered sets and their cofinalities; pcf theory (03E04) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Isabelle. A generic theorem prover
• The discovery of forcing.
• Edinburgh LCF. A mechanized logic of computation
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• The foundation of a generic theorem prover
• Set theory for verification. II: Induction and recursion
• Isabelle's metalogic: formalization and proof checker
• The Lean 4 theorem prover and programming language
• A modular first formalisation of combinatorial design theory
• Beautiful formalizations in Isabelle/Naproche
• First steps towards a formalization of forcing
• Rudimentary recursion, gentle functions and provident sets
• Mathias and set theory
• Partizan Games in Isabelle/HOLZF
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Provident sets and rudimentary set forcing
• Formalization of Forcing in Isabelle/ZF
• Formalizing Ordinal Partition Relations Using Isabelle/HOL
• Pollack-inconsistency
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• A Machine-Checked Proof of the Odd Order Theorem
• Inductively defined types in the Calculus of Constructions
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• A formalised theorem in the partition calculus
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

This page was built for publication: The formal verification of the ctm approach to forcing