29
$\begingroup$

From the Wikipedia article on Proof Assistant it shows some Proof Assistants are based on Higher Order Logic, (HOL Light) and some are based on Dependent Types, (Coq).

Are there any other means upon which to build a Proof Assistant? (Thinking MetaMath and ACL2).

Improve this question
$\endgroup$
4
  • 4
    $\begingroup$ Although there are no rules for tags yet. I think this question is not about metamath or like that, it's about mathematical foundations. So the specific examples given in the question should not go into the tags. $\endgroup$
    – Trebor ♦
    Feb 8 at 18:48
  • 1
    $\begingroup$ I think MetaMath gets subtle. If I understand correctly, on one hand MetaMath is a meta system which can implement any base (logic) you like. On the other hand, the main library set.mm is based on some sort of set theory (maybe in FOL) but I don't know the details. $\endgroup$
    – Jason Rute
    Feb 9 at 4:35
  • $\begingroup$ ... This comment also sort of also applied to other theorem provers. For example, the base foundations of Lean are constructive, but as used, Lean is practically classical since the main library mathlib uses classical logic as do many of Lean's tactics. $\endgroup$
    – Jason Rute
    Feb 9 at 4:38
  • 1
    $\begingroup$ Someone can turn this into an answer, but Lean's foundation is DTT (similar to Coq's) but it readily uses the axiom of choice and excluded middle. The full details, including a proof of consistency, are spelled out in Mario's paper. $\endgroup$
    – Jason Rute
    Feb 9 at 4:42

3 Answers 3

Reset to default
29
$\begingroup$

There are a lot of bases, theories and techniques in proof assistants. Let me show you how deep the rabbit hole is (in suggested order of implementation):

(Fibrational) Dependent Type Theories

  1. CoC (Calculus of Constructions, PTS, Coquand)
  2. CiC (Calculus of Inductive Constructions, Paulin-Mohring)
  3. MLTT (Martin-Löf)
  4. HoTT-I (Isaev)
  5. Cubical (Cubical Type System, CCHM)
  6. HTS (Homotopy Type System with Two Equalities, 2LTT, Voevodsky, ACKS)
  7. de Rham (Infinitesimal Shape Modality, Cherubini, Groupoid)
  8. Cartesian Cubical (ABCFHL)
  9. Guarded Cubical (BBCGSV)
  10. Rezk (Synthetic Theory of $\infty$-categories, Riehl, Shulman, Kudasov)
  11. Equivariant Super HoTT (Schreiber)

These are what we basically call Type Theories in Martin-Löf sense with 5 inference rules, some of them are monadic modalities. But on the market there are present proof assistants based on different theories, like custom model checkers or direct term rewriting systems. They internalize upper MLTT type systems into itself, like Dedukti. So the full answer to this question could be a good survey type PhD! Systems 1-7 are implemented as examples and included as parts of cubical.systems.

Embeddable DSL in host language

Before fibrational provers, the logic of computable functions was built upon relying on STLC flavours. In that sense you can write a needed type-checking rules in ML language as in meta theory and embed programs as strings instead of direct internalizations in the style of synthetic dependent type theories. This technique is not unique to HOL series, but is known as embeddable DSL in host-language technique. In that sense ACL2 is embeddable DSL in ANSI Common Lisp.

Ad-hoc dedicated model checkers and other LF

Everything that is big enough or impractical to run in the main Proof Assistant environment usually is being rewritten into separate ad-hoc model checker for the sake of speed, simplicity, etc. This category could include all known models checking cores: Reference SMT solver Z3 by Leonardo de Moura, TLA+ by Leslie Lamport, even Metamath-like systems or set-theoretical systems like Mizar. I think if you built the basis only for Set theory but not all mathematics it is called ad-hoc. Logical Frameworks like Twelf or system with separate language for automation of inference rules like Andromeda are also could be treated as separate ad-hoc logical systems. Modern powerful ad-hoc term rewriting systems like Dedukti could eat 2LTT with less effort than HoTT in HOL by Josh Chen.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ OK you can read it: formal.uno/monography.pdf $\endgroup$
    – Namdak Tönpa
    Feb 8 at 23:07
  • 1
    $\begingroup$ Your answer reminds me of "Smilla's Sense of Snow"; we could say "Maksym's Sense of Type Theory". All kidding aside, your work is impressive. $\endgroup$
    – M. Lonardi
    Feb 10 at 1:06
  • $\begingroup$ I just watched this movie by your recomendation, it's fine :-) $\endgroup$
    – Namdak Tönpa
    Feb 10 at 22:22
  • 1
    $\begingroup$ I have in mind to order links into pairs: main intro paper and its best github implementation. $\endgroup$
    – Namdak Tönpa
    Feb 16 at 9:15
25
$\begingroup$

Here are some other points in the space:

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ TLA+ is a proof assistant based on temporal logic $\endgroup$
    – Mario Carneiro
    Feb 9 at 2:27
  • 1
    $\begingroup$ Feel free to add more links to mine. I'm happy for either one to receive the accept vote. $\endgroup$
    – Jason Gross
    Feb 13 at 3:54
  • $\begingroup$ Indeed the thing I like about Namdak's answer is that it lays out the landscape rather than just giving some points in it. I don't really have a structural sense of the landscape in a way that adds anything to Namdak's answer. $\endgroup$
    – Jason Gross
    Feb 13 at 3:56
12
$\begingroup$

ACL2 is based on the logic of Common Lisp. This means several things:

  • The universe (over which one quantifies and defines predicates) consists of the s-expressions.
  • Logically, it is equivalent to finite set theory (that is all sets are hereditarily finite)
  • equality is decidable on closed terms
  • operational semantics is derived from that of lisp
Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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