Document Open Access Logo

Dependently Sorted Theorem Proving for Mathematical Foundations

Authors Yiming Xu , Michael Norrish

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.33.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Author Details

Yiming Xu
  • Australian National University, Canberra, Australia
Michael Norrish
  • Australian National University, Canberra, Australia

Acknowledgements

We appreciate all the anonymous reviewers for their time and effort in pointing out typos and suggesting improvements to this paper. We would also like to thank James Borger for the name "DiaToM", which we feel beautifully encapsulates the aims and nature of our project.

Cite As Get BibTex

Yiming Xu and Michael Norrish. Dependently Sorted Theorem Proving for Mathematical Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ITP.2023.33

Abstract

We describe a new meta-logical system for mechanising foundations of mathematics. Using dependent sorts and first order logic, our system (implemented as an LCF-style theorem-prover) improves on the state-of-the-art by providing efficient type-checking, convenient automatic rewriting and interactive proof support. We assess our implementation by axiomatising Lawvere’s Elementary Theory of the Category of Sets (ETCS) [F. William Lawvere, 1964], and Shulman’s Sets, Elements and Relations (SEAR) [Michael Shulman, 2022]. We then demonstrate our system’s ability to perform some basic mathematical constructions such as quotienting, induction and coinduction by constructing integers, lists and colists. We also compare with some existing work on modal model theory done in HOL4 [Yiming Xu and Michael Norrish, 2020]. Using the analogue of type-quantification, we are able to prove a theorem that this earlier work could not. Finally, we show that SEAR can construct sets that are larger than any finite iteration of the power set operation. This shows that SEAR, unlike HOL, can construct sets beyond V_{ω+ω}.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • first order logic
  • sorts
  • structural set theory
  • mechanised mathematics
  • foundation of mathematics
  • category theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  2. Mario Cáccamo and Glynn Winskel. A higher-order calculus for categories. In Richard J. Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, pages 136-153, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  3. John Harrison. Inductive definitions: automation and application. In Phillip J. Windley, Thomas Schubert, and Jim Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Science, pages 200-213, Aspen Grove, Utah, 1995. Springer-Verlag. Google Scholar
  4. Peter V. Homeier. The HOL-Omega logic. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 244-259, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  5. F. William Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences, 52(6):1506-1511, 1964. URL: https://doi.org/10.1073/pnas.52.6.1506.
  6. F. William Lawvere. The category of categories as a foundation for mathematics. In S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl, editors, Proceedings of the Conference on Categorical Algebra, pages 1-20, Berlin, Heidelberg, 1966. Springer Berlin Heidelberg. Google Scholar
  7. Michael Makkai. First order logic with dependent sorts, with applications to category theory. Available from https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf, 1995.
  8. Colin McLarty. Axiomatizing a category of categories. The Journal of Symbolic Logic, 56(4):1243-1260, 1991. URL: http://www.jstor.org/stable/2275472.
  9. Colin McLarty and Andrei Rodin. A discussion between Colin McLarty and Andrei Rodin about structuralism and categorical foundations of mathematics, 2013. URL: http://philomatica.org/wp-content/uploads/2013/02/colin.pdf.
  10. Thomas F. Melham. The HOL logic extended with quantification over type variables. In Luc J. M. Claesen and Michael J. C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, IFIP Transactions A: Computer Science and Technology, pages 3-17. North-Holland, Amsterdam, 1993. URL: https://doi.org/10.1016/B978-0-444-89880-7.50007-3.
  11. Elliott Mendelson. Introduction to Mathematical Logic. Princeton: Van Nostrand, 1964. Google Scholar
  12. Max S. New and Daniel R. Licata. A formal logic for formal category theory, 2022. URL: https://doi.org/10.48550/ARXIV.2210.08663.
  13. Lawrence Charles Paulson. Isabelle: The next 700 theorem provers. ArXiv, cs.LO/9301106, 2000. Google Scholar
  14. W. V. Quine. New foundations for mathematical logic. The American Mathematical Monthly, 44(2):70-80, 1937. URL: http://www.jstor.org/stable/2300564.
  15. Florian Rabe. First-order logic with dependent types. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, pages 377-391, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  16. Michael Shulman. Comparing material and structural set theories. Annals of Pure and Applied Logic, 170(4):465-504, 2019. URL: https://doi.org/10.1016/j.apal.2018.11.002.
  17. Michael Shulman. SEAR, 2022. URL: https://ncatlab.org/nlab/show/SEAR.
  18. Andrzej Trybulec. Tarski-Grothendieck set theory, 1990. URL: http://mizar.uwb.edu.pl/JFM/Axiomatics/tarski.html.
  19. Freek Wiedijk. Formalizing 100 theorems, 2013. URL: https://www.cs.ru.nl/~freek/100/.
  20. Yiming Xu and Michael Norrish. Mechanised modal model theory. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, International Joint Conference on Automated Reasoning (IJCAR), Paris, France, volume 12166 of Lecture Notes in Computer Science, pages 518-533. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_30.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact