A pluralist approach to the formalisation of mathematics
Robin Adams, Zhaohui Luo · Mathematical Structures in Computer Science · 2011
We present a programme of research forpluralist formalisations, that is, formalisations that involve proving results in more than one foundation. A foundation consists of two parts: a logical part, which provides a notion of inference, and a non-logical part, which provides the entities to be reasoned about. An LTT is a formal system composed of two such 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 two logic-enriched type theories (LTTs)SandT, and we have formalised a proof of a theorem α inS, we may wish to make use of the fact that Φ(α) is a theorem ofT. We show how this is sometimes possible by writing a proof scriptMΦ. For any proof scriptMαthat proves a theorem α inS, if we changeMαso it first importsMΦ, the resulting proof script will still parse, and will be a proof of Φ(α) inT. 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, theA-translation and the Russell–Prawitz modality. This work has been carried out using the proof assistant Plastic.