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

DOI10.1007/978-3-031-16681-5_6arXiv2205.03159OpenAlexW4296118504MaRDI QIDQ6159370FDOQ6159370

Authors: Lawrence C. Paulson 

Publication date: 2 June 2023

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

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.

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

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

zbMATH Keywords

formalisation of mathematicsIsabelleset theorycomplex analysiscontinuum hypothesisErdős

Mathematics Subject Classification ID

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

Cites Work

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

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)