Document Open Access Logo

A Formalization of Forcing and the Unprovability of the Continuum Hypothesis

Authors Jesse Michael Han, Floris van Doorn

PDF

File

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

Document Identifiers

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
    0
    Metadata Views

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.

Cite As Get 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

Author Details

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

Funding

Both authors were supported by the Sloan Foundation, grant G-2018-10067.

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.

Supplementary Materials

References

  1. Peter Aczel. The type theoretic interpretation of constructive set theory. In Logic Colloquium, volume 77, pages 55-66, 1978. Google Scholar
  2. Peter Aczel. The type theoretic interpretation of constructive set theory: choice principles. In Studies in Logic and the Foundations of Mathematics, volume 110, pages 1-40. Elsevier, 1982. Google Scholar
  3. Peter Aczel. The type theoretic interpretation of constructive set theory: inductive definitions. In Studies in Logic and the Foundations of Mathematics, volume 114, pages 17-49. Elsevier, 1986. Google Scholar
  4. Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott. Boolean-valued semantics for the stochastic λ-calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 669-678. ACM, 2018. Google Scholar
  5. John L Bell. Set theory: Boolean-valued models and independence proofs, volume 47. Oxford University Press, 2011. Google Scholar
  6. Stefan Berghofer. First-Order Logic According to Fitting. Archive of Formal Proofs, August 2007. , Formal proof development. URL: http://isa-afp.org/entries/FOL-Fitting.html.
  7. Georg Cantor. Ein Beitrag zur Mannigfaltigkeitslehre. Journal für die reine und angewandte Mathematik, 84:242-258, 1878. Google Scholar
  8. Mario Carneiro. Natural deduction in the Metamath Proof Explorer. http://us.metamath.org/mpeuni/mmnatded.html, 2014. Slides (http://us.metamath.org/ocat/natded.pdf).
  9. Mario Carneiro. The type theory of Lean. In preparation (https://github.com/digama0/lean-type-theory/releases), 2019.
  10. Paul J Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences, 50(6):1143-1148, 1964. Google Scholar
  11. Paul J Cohen. The independence of the continuum hypothesis, II. Proceedings of the National Academy of Sciences, 51(1):105, 1964. Google Scholar
  12. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  13. Steven Givant and Paul Halmos. Introduction to Boolean algebras. Springer Science & Business Media, 2008. Google Scholar
  14. Kurt Gödel. The consistency of the axiom of choice and of the generalized continuum-hypothesis. Proceedings of the National Academy of Sciences, 24(12):556-557, 1938. Google Scholar
  15. Emmanuel Gunther, Miguel Pagano, and Pedro Sánchez Terraf. First steps towards a formalization of Forcing. CoRR, abs/1807.05174, 2018. URL: http://arxiv.org/abs/1807.05174.
  16. Emmanuel Gunther, Miguel Pagano, and Pedro Sánchez Terraf. Mechanization of Separation in Generic Extensions. CoRR, abs/1901.03313, 2019. URL: http://arxiv.org/abs/1901.03313.
  17. Joel David Hamkins and Daniel Evan Seabold. Well-founded Boolean ultrapowers as large cardinal embeddings. arXiv preprint arXiv:1206.6075, 2012. Google Scholar
  18. John Harrison. Formalizing Basic First Order Model Theory. In Jim Grundy and Malcolm C. Newey, editors, Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, volume 1479 of Lecture Notes in Computer Science, pages 153-170. Springer, 1998. URL: https://doi.org/10.1007/BFb0055135.
  19. John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. Google Scholar
  20. Simon Hudon. Temporal logic in Unit-B, 2018. URL: https://github.com/unitb/temporal-logic.
  21. Simon Hudon, Thai Son Hoang, and Jonathan S. Ostroff. The Unit-B method: refinement guided by progress concerns. Software & Systems Modeling, 15:1091-1116, 2015. Google Scholar
  22. Danko Ilik. Constructive completeness proofs and delimited control. PhD thesis, Ecole Polytechnique X, 2010. Google Scholar
  23. Thomas Jech. Set theory. Springer Science & Business Media, 2013. Google Scholar
  24. Akihiro Kanamori. The mathematical development of set theory from Cantor to Cohen. Bulletin of Symbolic Logic, 2(1):1-71, 1996. Google Scholar
  25. Akihiro Kanamori. The Higher Infinite: Large Cardinals in Set Theory from their beginnings. Springer Science & Business Media, 2008. Google Scholar
  26. Kenneth Kunen. Set theory, volume 102 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam-New York, 1980. Google Scholar
  27. Yu I Manin. A course in mathematical logic for mathematicians, volume 53. Springer Science & Business Media, 2009. Google Scholar
  28. Justin Tatch Moore. The method of forcing. arXiv preprint arXiv:1902.03235, 2019. Google Scholar
  29. Lawrence C. Paulson. Set Theory for Verification: I. From foundations to functions. J. Autom. Reasoning, 11(3):353-389, 1993. URL: https://doi.org/10.1007/BF00881873.
  30. Lawrence C. Paulson. The Reflection Theorem: A Study in Meta-theoretic Reasoning. In Andrei Voronkov, editor, Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, volume 2392 of Lecture Notes in Computer Science, pages 377-391. Springer, 2002. URL: https://doi.org/10.1007/3-540-45620-1_31.
  31. Lawrence C. Paulson. The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors, Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings, volume 5028 of Lecture Notes in Computer Science, pages 486-490. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-69407-6_52.
  32. Lawrence C. Paulson and Krzysztof Grabczewski. Mechanizing Set Theory. J. Autom. Reasoning, 17(3):291-323, 1996. URL: https://doi.org/10.1007/BF00283132.
  33. Tom Ridge and James Margetson. A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 294-309. Springer, 2005. URL: https://doi.org/10.1007/11541868_19.
  34. Anders Schlichtkrull. Formalization of logic in the Isabelle proof assistant. PhD thesis, Technical University of Denmark, 2018. Google Scholar
  35. Dana Scott. A Proof of the Independence of the Continuum Hypothesis. Theory of Computing Systems, 1(2):89-111, 1967. Google Scholar
  36. Dana Scott. The Algebraic Intepretation of Quantifiers: intuitionistic and classical. Andrzej Mostowski and Foundational Studies, pages 289-312, 2008. Google Scholar
  37. Dana Scott. Stochastic λ-calculi. Journal of Applied Logic, 12(3):369-376, 2014. Google Scholar
  38. Dana Scott and Robert Solovay. Boolean algebras and forcing. Unpublished manuscript, 1967. Google Scholar
  39. Natarajan Shankar. Metamathematics, machines and Gödel’s proof, volume 38. Cambridge University Press, 1997. Google Scholar
  40. Joseph R Shoenfield. Unramified forcing. In Axiomatic set theory, volume 13, pages 357-381. AMS Providence, RI, 1971. Google Scholar
  41. Sebastian Ullrich. Lean 4: A Guided Preview. https://leanprover.github.io/talks/vu2019.pdf. Slides.
  42. Benjamin Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software, pages 530-546. Springer, 1997. Google Scholar
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact