Document Open Access Logo

Mechanized HOL Reasoning in Set Theory

Authors Simon Guilloud , Sankalp Gambhir , Andrea Gilot , Viktor Kunčak

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2024.18.pdf
  • Filesize: 0.75 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Proof assistant
  • First Order Logic
  • Set Theory
  • Higher Order Logic

Metrics

Abstract

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assume traditional FOL syntax without notation for term-level binders. To embed λ-terms, we define a notion of context, defining the closure of all abstractions occuring inside a term. We implement the embedding in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory (presented at ITP 2023). We show how to implement type checking and the proof steps of HOL Light as proof-producing tactics in Lisa. The embedded HOL theorems and proofs are interoperable with the existing Lisa library. This yields a form of soft type system supporting top-level polymorphism and ADTs within set theory. The approach offers tools for Lisa users to carry HOL-style proofs within set theory. It also enables the import of HOL Light theorem statements into Lisa, as well as the replay of small HOL Light kernel proofs.

Cite As Get BibTex

Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak. Mechanized HOL Reasoning in Set Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.18

Author Details

Simon Guilloud
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland
Sankalp Gambhir
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland
Andrea Gilot
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland
Viktor Kunčak
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland

Funding

This work is supported in part by the Swiss National Science Foundation grant 219474 "Algebraic Reasoning in Adaptive Verifiers".

Supplementary Materials

References

  1. Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In DROPS-IDN/v2/Document/10.4230/LIPIcs.ITP.2022.3. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.3.
  2. Sten Agerholm and Mike Gordon. Experiments with zf set theory in hol and isabelle. In E. Thomas Schubert, Philip J. Windley, and James Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications, pages 32-45, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  3. Rob Arthan. HOL Constant Definition Done Right. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, Lecture Notes in Computer Science, pages 531-536, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_34.
  4. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, 2013. Google Scholar
  5. Chad Brown. The Egal Manual, 2014. Google Scholar
  6. Chad E. Brown. Combining type theory and untyped set theory. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, pages 205-219, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  7. Chad E. Brown, C. Kaliszyk, and Karol Pak. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In ITP, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.9.
  8. Mario M Carneiro. Conversion of hol light proofs into metamath. Journal of Formalized Reasoning, 9(1):187-200, January 2016. URL: https://doi.org/10.6092/issn.1972-5787/4596.
  9. G. Gentzen. Untersuchungen über das logische Schließen I. Mathematische Zeitschrift, 39:176-210, 1935. Google Scholar
  10. Mike Gordon. Set theory, higher order logic or both? In W. Brauer, D. Gries, J. Stoer, Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125, pages 191-201. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/BFb0105405.
  11. Simon Guilloud. LISA Reference Manual. EPFL-LARA, February 2023. Google Scholar
  12. Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak. epfl-lara/lisa. Software, version 0.1., (visited on 2024-08-21). URL: https://github.com/epfl-lara/lisa/tree/itp2024-archive
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.22517
  13. Simon Guilloud, Sankalp Gambhir, and Viktor Kuncak. LISA - A Modern Proof System. In 14th Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, pages 17:1-17:19, Bialystok, 2023. Daghstuhl. Google Scholar
  14. John Harrison. HOL Light: An Overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, volume 5674, pages 60-66. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  15. Thomas Jech. Set theory: The third millennium edition, revised and expanded. Springer, 2003. Google Scholar
  16. Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987. Google Scholar
  17. Cezary Kaliszyk and Karol Pąk. Combining higher-order logic with set theory formalizations. Journal of Automated Reasoning, 67(2):20, May 2023. URL: https://doi.org/10.1007/s10817-023-09663-5.
  18. Alexander Krauss and Andreas Schropp. A mechanized translation from higher-order logic to set theory. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, pages 323-338, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  19. Kenneth Kunen. Set Theory An Introduction To Independence Proofs. North Holland, Amsterdam Heidelberg, reprint edition edition, December 1983. Google Scholar
  20. Thomas F. Melham. Automating Recursive Type Definitions in Higher Order Logic, pages 341-386. Springer New York, New York, NY, 1989. URL: https://doi.org/10.1007/978-1-4612-3658-0_9.
  21. Elliott Mendelson. Introduction to Mathematical Logic. Springer US, Boston, MA, 1987. URL: https://doi.org/10.1007/978-1-4615-7288-6.
  22. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. Google Scholar
  23. Adam Naumowicz and Artur Kornilowicz. A Brief Overview of Mizar. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674, pages 67-72, August 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_5.
  24. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  25. Steven Obua. Partizan games in Isabelle/HOLZF. In Theoretical Aspects of Computing - ICTAC 2006, pages 272-286, November 2006. URL: https://doi.org/10.1007/11921240_19.
  26. Steven Obua, Jacques Fleuriot, Phil Scott, and David Aspinall. Type inference for zfh. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, pages 87-101, Cham, 2015. Springer International Publishing. Google Scholar
  27. Stanislas Polu. HOL Light / ProofTrace: Modern proof steps recording for hol light. https://github.com/jrh13/hol-light/tree/master/ProofTrace. Accessed: 2024-03-18.
  28. Konrad Slind and Michael Norrish. A Brief Overview of HOL4. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 28-32, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  29. The Coq Development Team. The coq proof assistant, July 2023. URL: https://doi.org/10.5281/zenodo.8161141.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact