A Pluralist Approach to the Formalisation of Mathematics

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.