Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis

TL;DR

This paper formalizes an undecidable problem linked to the continuum hypothesis using Isabelle/HOL, illustrating the intersection of complex analysis, set theory, and formal proof systems.

Contribution

It provides a formal proof of Erdős's result connecting an undecidable problem to the continuum hypothesis within Isabelle/HOL.

Findings

Formal proof of Erdős's result in Isabelle/HOL

Demonstrates integration of set theory and higher-order logic

Highlights undecidability linked to the continuum hypothesis

Abstract

In 1964, Paul Erd\H{o}s published a paper settling a question about function spaces that he had seen in a problem book. Erd\H{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.