Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
Lawrence Charles Paulson · Lecture notes in computer science · 2022
In 1964, Paul Erdős published a paper [ 5 ] settling a question about function spaces that he had seen in a problem book. Erdő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 [ 17 ] integrates set theory with higher-order logic.