← All papers
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
cs.LO
Apr 23, 2019 · v1
TL;DR
Formalizes Cohen's forcing method in Lean 3 to prove the independence of the continuum hypothesis.
Abstract
The authors describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. They specialize the construction to the Boolean algebra of regular opens of the Cantor space and formally verify the failure of the continuum hypothesis in the resulting model.
Problem
The independence of the continuum hypothesis from ZFC is a central result in set theory, but forcing arguments had not been formalized in the Lean theorem prover.
Approach
The authors formalize forcing using Boolean-valued models in Lean 3. They implement a deep embedding of first-order logic with a Boolean-valued soundness theorem and prove the fundamental theorem of forcing. The construction is specialized to the Boolean algebra of regular opens of the Cantor space to produce the desired model.
Results
The formalization verifies the failure of the continuum hypothesis in the Boolean-valued model over regular opens of the Cantor space, establishing the unprovability of CH from ZFC within Lean 3's kernel.