LIPIcs.ITP.2019.19.pdf
- Filesize: 0.64 MB
- 19 pages
Document
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Acknowledgements
We thank the members of the Pitt-CMU Lean group, particularly Simon Hudon, Jeremy Avigad, Mario Carneiro, and Tom Hales for their feedback and suggestions; we are also grateful to Dana Scott and John Bell for their advice and correspondence.
Cite AsGet BibTex
Jesse Michael Han and Floris van Doorn. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 19:1-19:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.19
https://doi.org/10.4230/LIPIcs.ITP.2019.19
Abstract
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
- Theory of computation → Type theory
- Software and its engineering → Formal methods
Keywords
- Interactive theorem proving
- formal verification
- set theory
- forcing
- independence proofs
- continuum hypothesis
- Boolean-valued models
- Lean
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads