2026-07-24T01:58:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18408 2024-03-06T11:01:49Z ddc:004 open_access

Dependently Sorted Theorem Proving for Mathematical Foundations Xu, Yiming Norrish, Michael first order logic sorts structural set theory mechanised mathematics foundation of mathematics category theory 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_{ω+ω}. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yiming Xu and Michael Norrish 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.33 urn:nbn:de:0030-drops-184085 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.33 eng https://creativecommons.org/licenses/by/4.0/legalcode