eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
19:1
19:19
10.4230/LIPIcs.ITP.2019.19
article
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
Han, Jesse Michael
1
van Doorn, Floris
1
Department of Mathematics, University of Pittsburgh, PA, USA
We 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. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.19/LIPIcs.ITP.2019.19.pdf
Interactive theorem proving
formal verification
set theory
forcing
independence proofs
continuum hypothesis
Boolean-valued models
Lean