[FOM] proof assistants and foundations of mathematics
Till Mossakowski
till at iks.cs.ovgu.de
Tue Aug 14 04:36:58 EDT 2018
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
More information about the FOM
mailing list