Adams, Robin and Luo, Zhaohui (2011) A Pluralist Approach to the Formalisation of Mathematics. Mathematical Structures in Computer Science, 21 (4).
Full text access: Open
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.
This is a Accepted version This version's date is: 2/7/2011 This item is not peer reviewed
https://repository.royalholloway.ac.uk/items/258ca566-9df2-7c2d-3228-1dd9c529e476/4/
Deposited by Research Information System (atira) on 14-Jun-2012 in Royal Holloway Research Online.Last modified on 14-Jun-2012