[FOM] proof assistants and foundations of mathematics

[Frédéric Blanqui]

Hello.

Another such system is Dedukti (https://deducteam.github.io/). It is 
based on LF + a user-defined (decidable) congruence on objects and types 
given by rewrite rules. The point is to replace axioms by rewrite rules 
as much as possible. For instance, Peano arithmetic, HOL, some subset of 
ZF, functional pure type systems (PTS) including system F, Fw, CC, CIC, 
etc. can be encoded into a Dedukti theory with no axiom but rewrite 
rules. See http://www.lsv.fr/~dowek/Publi/expressing.pdf for more details.

But, currently, Dedukti is just a proof/type checker. It has very little 
support for interactive proof development. Instead, it comes with 
additional tools for translating proofs developed elsewhere to Dedukti, 
and from Dedukti to other provers. For instance, Krajono 
(http://deducteam.gforge.inria.fr/krajono/index.html) translates Matita 
(a clone of Coq) proofs into Dedukti proofs; Holide 
(http://deducteam.gforge.inria.fr/holide/index.html) translates 
OpenTheory proofs (from HOL, HOL-Light, etc.) into Dedukti proofs. 
François Thiré (http://www.lsv.fr/~fthire/) is developing tools for 
automatically translating Matita proofs into HOL. And an extension of 
Dedukti allowing the interactive development of proofs is under 
development (https://github.com/rlepigre/lambdapi).

Frédéric.


Le 14/08/2018 à 10:36, Till Mossakowski a écrit :
> Am 11.08.2018 um 21:39 schrieb Timothy Y. Chow:
>> What I think Jose implicitly desires is a proof assistant that has the
>> feature that it can verify "T is a theorem of S if your logic is L"
>> where S and L are arbitrary and *user-specified*.  Moreover, the
>> verification of such statements should assume as little as possible.
>> So if the next Ed Nelson comes along who doesn't even trust PRA, he
>> can still plug in his favorite set of axioms and proof calculus and
>> find out if his theorem is really a theorem by his own standards.  He
>> won't have to go off and write his own home-grown, bug-ridden proof
>> assistant.
>>
>>
> actually, one can formally specifcy a logic L and verify "T is a theorem
> of S if your logic is L" with any logical framework, e.g. LF. Also
> Isabelle/Pure is capable of doing this, although in practice, mostly
> L=HOL. A recent system that also covers model theory and soundness and
> completeness proofs is MMT, see https://uniformal.github.io/  MMT is not
> only logic-independent but even "foundation independent" in the sense
> that it works with different logical frameworks, although in practice,
> mostly LF is used.
>
> Till Mossakowski
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom