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

Standard

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

Harvard

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

APA

Vancouver

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

Author

Adams, Robin ; Luo, Zhaohui. / A Pluralist Approach to the Formalisation of Mathematics. In: Mathematical Structures in Computer Science. 2011 ; Vol. 21, No. 4. pp. 913-942.

BibTeX

@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",

}

RIS

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 -