Abstract

In this talk, we start with a picture of current existing theorem-proving systems. Then we describe our new meta-logical system 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. We assess our implementation by axiomatising 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 suitable choice of axioms, our system is sufficient to perform some basic mathematical constructions such as quotienting, induction and coinduction by constructing integers, lists and colists. 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.