10
$\begingroup$

I've read that Isabelle and Metamath (and maybe Andromeda) are "generic" proof assistants in some sense that allows them to be used to implement different theories such as HOL, ZF and dependent type theory. I'm curious how generic these proof assistants can really be, especially if you can use them to implement linear and ordered logics and/or logics over restricted term languages.

In particular, Dan Licata and I have developed in recent work a domain-specific type theory for category theory (https://arxiv.org/abs/2210.08663) that is a kind of "proof-relevant ordered linear higher-order logic over a unary term language". A proof assistant based on this type theory would be somewhat similar to Isabelle/HOL since it is a kind of (weird) HOL. Are Isabelle or Metamath generic enough to handle such a bizarre system?

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ I do not know about the other ones, but I can answer for Andromeda: I don't think it will suit your needs. Indeed, its treatment of context is "hard-coded", to be what is "standard" in vanilla dependent type systems: you have a single context, with two operations (empty context and context extension), and the usual variable rule. So unless you somehow encode your more complicated contexts in a different way (which might be possible, but probably tedious), you will not be able to use Andromeda. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Mar 16, 2023 at 10:19
  • 1
    $\begingroup$ At first sight it looks like Metamath could be used to formalize VETT. A good inspiration might be the hol.mm database (github.com/metamath/set.mm/blob/develop/hol.mm). The syntactic forms defined in Fig. 2 would be formalized as syntactic axioms like hol.mm's kl. Connectives in Fig 3,4,5 would be encoded as further axioms, and if done correctly one should be able to derive the theorems. $\endgroup$
    – Thierry Arnoux
    Commented Mar 16, 2023 at 13:23
  • 1
    $\begingroup$ I concur with @MevenLennon-Bertrand, contexts in Andromeda are intuitionistic. $\endgroup$
    – Andrej Bauer
    Commented Mar 22, 2023 at 18:25

1 Answer 1

Reset to default
6
$\begingroup$

Isabelle/Sequents contains a formalisation of intuitionistic linear logic, so conceivably you have a chance of implementing your logic in Isabelle, following the techniques used there. Whether what you get meets your expectations is another matter. Provided the implemented inference system is acceptable to you, consider that you are getting a sophisticated user interface and structured proof language for free.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Cool I should definitely check it out. My more precise question then is maybe: is Isabelle generic in the term language and the logic over it or just the logic? $\endgroup$
    – Max New
    Commented Mar 20, 2023 at 16:44
  • 2
    $\begingroup$ The term language is essentially the typed lambda calculus. Many formalisms are easily expressed through that medium, though not all. $\endgroup$
    – Lawrence Paulson
    Commented Mar 22, 2023 at 14:20

Not the answer you're looking for? Browse other questions tagged or ask your own question.