Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

DOI10.1007/978-3-031-16681-5_6MaRDI QIDQ6159370zbMATH OpenOpenAlexFDO

Authors Lawrence C. Paulson

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

formalisation of mathematicsIsabelleset theorycomplex analysiscontinuum hypothesisErdős

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Abstract: In 1964, Paul ErdH{o}s published a paper settling a question about function spaces that he had seen in a problem book. ErdH{o}s proved that the answer was yes if and only if the continuum hypothesis was false: an innocent-looking question turned out to be undecidable in the axioms of ZFC. The formalisation of these proofs in Isabelle/HOL demonstrate the combined use of complex analysis and set theory, and in particular how the Isabelle/HOL library for ZFC integrates set theory with higher-order logic.

Recommendations

• Formalizing ordinal partition relations using Isabelle/HOL
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• scientific article; zbMATH DE number 4106832
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• “Gödel’s Modernism: On Set-Theoretic Incompleteness,” Revisited

Cites work

• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 2090314 (Why is no real title available?)
• An interpolation problem associated with the continuum hypothesis
• An introduction to Conway's games and numbers
• Formalization of Forcing in Isabelle/ZF
• Formalizing ordinal partition relations using Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Partizan Games in Isabelle/HOLZF
• Proofs from THE BOOK. Including illustrations by Karl H. Hofmann
• Set theory. An introduction to independence proofs
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• The foundation of a generic theorem prover

Cited in

(2)

• The formal verification of the ctm approach to forcing
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

This page was built for publication: Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

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