DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2023.33

Dependently Sorted Theorem Proving for Mathematical Foundations

Authors: Yiming Xu and Michael Norrish

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

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_{ω+ω}.

Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2023.33},
  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}
}

Search Results

Documents authored by Xu, Yiming

Dependently Sorted Theorem Proving for Mathematical Foundations

Abstract

Cite as

Thanks for your feedback!

Could not send message