A Pluralist Approach to the Formalisation of Mathematics

Abstract

We present a programme of research for pluralist formalisations — formalisations that involve proving results in more than one foundation. A foundation consists of two parts: a logical part that provides a notion of inference, and a non-logical part that provides the entities to be reasoned about. A logic-enriched type theory (LTT) is a formal system composed of such two separate parts. We show how LTTs may be used as the basis for a pluralist formalisation. We show how different foundations may be formalised as LTTs, and also describe a new method for proof reuse. If we know that a translation Φ exists between logic-enriched type theories (LTTs) S and T , and we have formalised a proof of a theorem α in S, we may wish to make use of the fact that Φ(α) is a theorem of T . We show how this is sometimes possible by writing a proof script MΦ . For any proof script Mα that proves a theorem α in S, if we change Mα so it first imports MΦ , then the resulting proof script will still parse, and will be a proof of Φ(α) in T . In this paper, we focus on the logical part of an LTT-framework and show how the above method of proof reuse is done for four cases of Φ: inclusion, the double negation translation, the A-translation, and the Russell-Prawitz modality. This work has been carried out using the proof assistant Plastic.