The formal verification of the ctm approach to forcing

DOI10.1016/J.APAL.2024.103413MaRDI QIDQ6151819zbMATH OpenOpenAlexWikidataFDO

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

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 hypothesiscountable transitive modelsgeneric extensioninteractive theorem proversIsabelle/ZFproof assistants

Mathematics Subject Classification ID

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

Abstract: We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $mathitZFC$, of generic extensions satisfying $mathitZFC+egmathitCH$ and $mathitZFC+mathitCH$. Moreover, let $mathcalR$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $OmegasubseteqmathcalR$ and defined $mathcalF:mathcalRomathcalR$ such that for every $PhisubseteqmathcalR$ and $M$-generic $G$, $$ implies $M[G]modelsmathitZCcupPhicupegmathitCH$, where $mathitZC$ is Zermelo set theory with Choice. To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others.

Cites work

• A formal proof of the Kepler conjecture
• A formalised theorem in the partition calculus
• A machine-checked proof of the odd order theorem
• A modular first formalisation of combinatorial design theory
• Beautiful formalizations in Isabelle/Naproche
• Edinburgh LCF. A mechanized logic of computation
• First steps towards a formalization of forcing
• Formal proof - the four color theorem
• Formalization of Forcing in Isabelle/ZF
• Formalizing ordinal partition relations using Isabelle/HOL
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 1302064 (Why is no real title available?)
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 7015112 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• Inductively defined types in the Calculus of Constructions
• Isabelle's metalogic: formalization and proof checker
• Isabelle. A generic theorem prover
• Mathias and set theory
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Partizan Games in Isabelle/HOLZF
• Pollack-inconsistency
• Provident sets and rudimentary set forcing
• Rudimentary recursion, gentle functions and provident sets
• Set forcing over models of Zermelo or Mac Lane
• Set theory for verification. II: Induction and recursion
• Set theory.
• The calculus of constructions
• The discovery of forcing.
• The foundation of a generic theorem prover
• The Lean 4 theorem prover and programming language
• 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
• 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

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