A Pluralist Approach to the Formalisation of Mathematics. / Adams, Robin; Luo, Zhaohui.

In: Mathematical Structures in Computer Science, Vol. 21, No. 4, 02.07.2011, p. 913-942.

Research output: Contribution to journalArticle

Published

Documents

  • Plural

    Accepted author manuscript, 447 KB, PDF document

Links

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.
Original languageEnglish
Pages (from-to)913-942
Number of pages29
JournalMathematical Structures in Computer Science
Volume21
Issue number4
DOIs
Publication statusPublished - 2 Jul 2011
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 1445196