Dependently Sorted Theorem Proving for Mathematical Foundations

Abstract

In this thesis, we start with a picture of current existing theorem-proving systems. Then we describe our new meta-logical system (named DiaToM) for mechanizing 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. By formalizing the proof theory of the DiaToM logic, we verified that the most suspicious design, namely the "formula variable", does not break the first-orderness of our logic. We assess our implementation by axiomatizing Lawvere's Elementary Theory of the Category of Sets(ETCS), Shulman's Sets, Elements and Relations(SEAR), and McLarty's Categories of Categories as a Foundation of mathematics(CCAF). With a suitable choice of axioms, our system is sufficient to perform some basic mathematical constructions such as quotients, induction, and coinduction by constructing integers, lists, and co-lists. More interestingly, we can provide concrete examples of some constructions that are not possible to be carried out in simpler systems as HOL can be carried out with SEAR in our system. This demonstrates that our system is in a sweet spot of simplicity and expressiveness. Show more