[FOM] proof assistants and foundations of mathematics

[Till Mossakowski]

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