9
$\begingroup$

One notable feature of Isabelle is that it allows for the definition and in-built integrated support of alternative object logics via the interface of Isabelle/Pure in combination with Isabelle/Isar. While Isabelle is primarily known for its implementation of Isabelle/HOL, it offers several alternative object logics, such as Isabelle/ZF and Isabelle/HoTT.

The important part to note here is that most of the main functionality and many proof methods implemented in Isabelle (Pure) are readily available for any newly implemented alternative object logic.

It seems to me that most of the other proof assistants are (rigidly) aimed at a specific object logic (usually some variant of a dependent type-theory and its various extensions). While new axioms can usually be added, the definition of alternative object logics is rarely supported out-of-the-box (that is, without a substantial modification of the code base that requires knowledge that goes well beyond that of an average user of the proof assistant and possibly non-backward compatible changes).

The question is whether Isabelle is the only modular proof assistant in the aforementioned sense? Are there any emerging proof assistants that aim to provide a similar level of modularity? Are there any ongoing projects to introduce similar features into the existing popular proof assistants, such as Agda/Coq/Lean?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ I think metamath (and metamath zero) would satisfy your definition of modular. $\endgroup$
    – Jason Rute
    Commented Feb 11, 2022 at 20:51
  • 1
    $\begingroup$ Logical frameworks like Automath and Twelf may satisfy your criteria for "modularity", as well. $\endgroup$
    – Alex Nelson
    Commented Feb 11, 2022 at 20:57
  • $\begingroup$ Indeed, it looks like they might. I am not very well familiar with metamath/automath/Twelf (I am an Isabelle user, but I played a little bit with Lean/Agda/Coq). If you know more about the technology behind metamath/automath/Twelf, I would appreciate it if you could spare a few minutes to describe them in an answer or several explicit answers (I think it would suffice to provide a high-level overview and compile links to the relevant sections of the documentation and papers, if any). $\endgroup$
    – user9716869 - supports Ukraine
    Commented Feb 11, 2022 at 21:01
  • 1
    $\begingroup$ I could be cheesy and pitch incredible.pm as a meta-logical theorem prover; you can instantiate it with differently logics. $\endgroup$
    – Joachim Breitner
    Commented Feb 11, 2022 at 22:18

3 Answers 3

Reset to default
4
$\begingroup$

It sounds like you're after a logical framework, i.e., a system which allows you to reason within a given foundations. Isabelle is a bit more than this, it's a so-called "meta-logical framework": it allows you to prove results about a foundations.

Automath (see, e.g., the Automath Archives) was one of the first proof assistants, dating back to 1968 (if not a few years earlier). For some examples of different foundations formalized within Automath, see:

  • Freek Wiedijk, "Is ZFC a Hack?" Journal of Applied Logic 4, no. 4 (2006): 622-645. Eprint and related code

It may look a little foreign to our modern eyes, because Automath uses lambda-typed lambda calculus rather than something belonging to the lambda cube or pure type systems.

Therefore, you may wish to examine a more modern cousin:

  • Robert Harper and Furio Honsell and Gordon Plotkin, "A Framework for Defining Logics". Journal of the ACM 40, no. 1 (1993): 143-184.Eprint

This works within the LF type theory (i.e., first-order dependently-typed lambda calculus). This served as the theoretical underpinning of Twelf, which has been used to formalize various foundations analogous to Wiedijk's paper in:

  • Mihnea Iancu and Florian Rabe, "Formalizing Foundations of Mathematics". Mathematical Structures in Computer Science 21 no.4 (2011) pp.883-911. Eprint
Improve this answer
$\endgroup$
2
$\begingroup$

I believe one "emerging proof assistant" along these lines is Andromeda. The theory of Andromeda is essentially an extensional dependent type theory with equality reflection, which can be used as a Logical Framework (as discussed in Alex's answer) to implement other type theories by asserting their type constructors as axioms and their computation rules as equalities. This allows arbitrarily poorly-behaved theories, and in particular requires giving the user the ability to control the application of definitional equalities; but there is a built-in equality-checker than can handle many of the "usual" sorts of type theories with equalities defined using beta- and eta-equalities.

Improve this answer
$\endgroup$
3
  • $\begingroup$ You're describing Andromeda 1. Andromeda 2 is not extensional. In fact, it's not anything, because it's empty when you start it up. Even things like $\Pi$ are user-definable, and so is equality reflection. Also, it's not usable at its current stage of development. $\endgroup$
    – Andrej Bauer
    Commented Feb 13, 2022 at 23:42
  • $\begingroup$ @AndrejBauer I thought the metatheory in which you define all of those things could be described as a kind of LF: the binding structure is essentially a framework-level $\Pi$-type, the judgmental equality is a framework-level equality type, etc. Is that not an okay way to think about it? (And I know it's not usable yet, but I thought that it would still count as "emerging".) $\endgroup$
    – Mike Shulman
    Commented Feb 14, 2022 at 2:22
  • $\begingroup$ I was just reacting to "the theory of Andromeda is essentially an extensional dependent type theory with equality reflection" and was not talking about what can be done in an extensional framework. That's a separate thing. $\endgroup$
    – Andrej Bauer
    Commented Feb 14, 2022 at 7:00
2
$\begingroup$

Both Metamath (and Metamath Zero) are naturally foundation generic.

Metamath

Like Isabelle, most of the active work done in Metamath is in just one theory (specifically set.mm uses ZFC). Nonetheless, there is support for other foundations and plenty of examples on the Metamath homepage. The way foundations are implemented through what they call substitution is quite simple and generic. Overall Metamath doesn't have any automation or fancy features, so this substitution mechanic is quite transparent and easy to follow in the proofs, e.g. the proof of 2 + 2 = 4.

Metamath Zero

Metamath Zero is a research project of Mario Carneiro. It aims to be a new proof assistant which proves its own correctness down to the x86 byte code. It borrows ideas from Metamath, including the ability to implement any foundation, as well as Lean. It is quite fast and I believe the author envisions it as both a way to double check the proofs of other theorem provers and as a sort of interchange language for theorem proving. He has already used it to translate all Metamath theorems into Lean. (However, this translation was mostly unaligned, so it was more of a research demo than a practical translation.) You can find a video tutorial on Youtube in which he implements propositional logic from scratch.

I believe he is going to use Peano Arithmetic as his foundation for proving the correctness of the x86 byte code. After that is verified, then for any foundation implemented in MM0, one can trust the checker assuming only they trust the human readable specification of the foundation. (...and that PA is consistent, and he actually implemented PA correctly, and the hardware is not faulty, etc. But one won't have to worry about the implementation of the kernel, just the logical rules currently used in the specification.)

P.S. I'm not a Metamath expert, and we really need to get one on this site. :)

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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