[FOM] proof assistants and foundations of mathematics
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
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.
More information about the FOM