License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.33
URN: urn:nbn:de:0030-drops-184085
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18408/
Xu, Yiming ;
Norrish, Michael
Dependently Sorted Theorem Proving for Mathematical Foundations
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_{ω+ω}.
BibTeX - Entry
@InProceedings{xu_et_al:LIPIcs.ITP.2023.33,
author = {Xu, Yiming and Norrish, Michael},
title = {{Dependently Sorted Theorem Proving for Mathematical Foundations}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {33:1--33:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18408},
URN = {urn:nbn:de:0030-drops-184085},
doi = {10.4230/LIPIcs.ITP.2023.33},
annote = {Keywords: first order logic, sorts, structural set theory, mechanised mathematics, foundation of mathematics, category theory}
}
