## 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.

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 language | English |
---|---|

Pages (from-to) | 913-942 |

Number of pages | 29 |

Journal | Mathematical Structures in Computer Science |

Volume | 21 |

Issue number | 4 |

DOIs | |

Publication status | Published - 2 Jul 2011 |

## Keywords

- logical frameworks
- mathematical pluralism
- proof reuse