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

Research output: Contribution to journal › Article

Published

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

Research output: Contribution to journal › Article

Adams, R & Luo, Z 2011, 'A Pluralist Approach to the Formalisation of Mathematics', *Mathematical Structures in Computer Science*, vol. 21, no. 4, pp. 913-942. https://doi.org/10.1017/S0960129511000156

Adams, R., & Luo, Z. (2011). A Pluralist Approach to the Formalisation of Mathematics. *Mathematical Structures in Computer Science*, *21*(4), 913-942. https://doi.org/10.1017/S0960129511000156

Adams R, Luo Z. A Pluralist Approach to the Formalisation of Mathematics. Mathematical Structures in Computer Science. 2011 Jul 2;21(4):913-942. https://doi.org/10.1017/S0960129511000156

@article{364ca1b56548483ea84cd17a731dc5d0,

title = "A Pluralist Approach to the Formalisation of Mathematics",

abstract = "We present a programme of research for pluralist formalisations — formalisations thatinvolve proving results in more than one foundation.A foundation consists of two parts: a logical part that provides a notion of inference, anda non-logical part that provides the entities to be reasoned about. A logic-enriched typetheory (LTT) is a formal system composed of such two separate parts. We show howLTTs may be used as the basis for a pluralist formalisation.We show how different foundations may be formalised as LTTs, and also describe a newmethod for proof reuse. If we know that a translation Φ exists between logic-enrichedtype theories (LTTs) S and T , and we have formalised a proof of a theorem α in S, wemay wish to make use of the fact that Φ(α) is a theorem of T . We show how this issometimes possible by writing a proof script MΦ . For any proof script Mα that proves atheorem α in S, if we change Mα so it first imports MΦ , then the resulting proof scriptwill 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 abovemethod of proof reuse is done for four cases of Φ: inclusion, the double negationtranslation, the A-translation, and the Russell-Prawitz modality. This work has beencarried out using the proof assistant Plastic.",

keywords = "logical frameworks, mathematical pluralism, proof reuse",

author = "Robin Adams and Zhaohui Luo",

year = "2011",

month = jul,

day = "2",

doi = "10.1017/S0960129511000156",

language = "English",

volume = "21",

pages = "913--942",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

number = "4",

}

TY - JOUR

T1 - A Pluralist Approach to the Formalisation of Mathematics

AU - Adams, Robin

AU - Luo, Zhaohui

PY - 2011/7/2

Y1 - 2011/7/2

N2 - We present a programme of research for pluralist formalisations — formalisations thatinvolve proving results in more than one foundation.A foundation consists of two parts: a logical part that provides a notion of inference, anda non-logical part that provides the entities to be reasoned about. A logic-enriched typetheory (LTT) is a formal system composed of such two separate parts. We show howLTTs may be used as the basis for a pluralist formalisation.We show how different foundations may be formalised as LTTs, and also describe a newmethod for proof reuse. If we know that a translation Φ exists between logic-enrichedtype theories (LTTs) S and T , and we have formalised a proof of a theorem α in S, wemay wish to make use of the fact that Φ(α) is a theorem of T . We show how this issometimes possible by writing a proof script MΦ . For any proof script Mα that proves atheorem α in S, if we change Mα so it first imports MΦ , then the resulting proof scriptwill 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 abovemethod of proof reuse is done for four cases of Φ: inclusion, the double negationtranslation, the A-translation, and the Russell-Prawitz modality. This work has beencarried out using the proof assistant Plastic.

AB - We present a programme of research for pluralist formalisations — formalisations thatinvolve proving results in more than one foundation.A foundation consists of two parts: a logical part that provides a notion of inference, anda non-logical part that provides the entities to be reasoned about. A logic-enriched typetheory (LTT) is a formal system composed of such two separate parts. We show howLTTs may be used as the basis for a pluralist formalisation.We show how different foundations may be formalised as LTTs, and also describe a newmethod for proof reuse. If we know that a translation Φ exists between logic-enrichedtype theories (LTTs) S and T , and we have formalised a proof of a theorem α in S, wemay wish to make use of the fact that Φ(α) is a theorem of T . We show how this issometimes possible by writing a proof script MΦ . For any proof script Mα that proves atheorem α in S, if we change Mα so it first imports MΦ , then the resulting proof scriptwill 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 abovemethod of proof reuse is done for four cases of Φ: inclusion, the double negationtranslation, the A-translation, and the Russell-Prawitz modality. This work has beencarried out using the proof assistant Plastic.

KW - logical frameworks

KW - mathematical pluralism

KW - proof reuse

U2 - 10.1017/S0960129511000156

DO - 10.1017/S0960129511000156

M3 - Article

VL - 21

SP - 913

EP - 942

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 4

ER -