A Pluralist Approach to the Formalisation of Mathematics

My latest project has been to play with a method of proof reuse suitable for pluralist formalisations in Plastic.

Let's say a theorem α is provable in a classical LTT. Then we know that its double-negation translation α∼∼ is provable in a constructive LTT. Can we take a proof script alpha.lf that proves α, and use it as if it were a proof script that proves α∼∼?

I don't want to write a script that translates alpha.lf into a new script. I don't want to prove a lemma that I'm going to end up applying 100 times. I want to be able to say import alpha.lf while working in a constructive LTT, and get a proof of α∼∼ put into the context.

It's possible, and it's all described in the paper A Pluralist Approach to the Formalisation of Mathematics, co-authored with Zhaohui Luo. A preprint is available here.

Plastic can be downloaded here.

Note

In the paper above, we describe a keyword Topkind. The command Topkind PropI PrfI, for example, introduces the kind PropI and, for every object P : PropI, the kind PrfI P. We are in the process of implementing this command in Plastic.

In the meantime, the proof scripts below use the following hack. Where we want to put Topkind PropI PrfI, we instead write:

[PropI : Type];
[PrfI : PropI -> Type];

The LTTs used

The Translations

The Translations in Use