Document Open Access Logo

A Formalization of Forcing and the Unprovability of the Continuum Hypothesis

Authors Jesse Michael Han, Floris van Doorn



PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.19.pdf
  • Filesize: 0.64 MB
  • 19 pages

Document Identifiers

Author Details

Jesse Michael Han
  • Department of Mathematics, University of Pittsburgh, PA, USA
Floris van Doorn
  • Department of Mathematics, University of Pittsburgh, PA, USA

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail