[FOM] proof assistants and foundations of mathematics
Lawrence Paulson
lp15 at cam.ac.uk
Tue Aug 7 04:34:36 EDT 2018
You might like to read my paper on such topics:
https://arxiv.org/abs/1804.07860
Larry
> On 6 Aug 2018, at 20:04, José Manuel Rodriguez Caballero <josephcmac at gmail.com> wrote:
>
> My formation is mainly in pure mathematics (number theory), not in foundations of mathematics. So, I'm rather curious of some results that could be not interested at all for people with a solid formation in foundations of mathematics: I'm just learning from the answers in FOM and MetaMath groups and I'm understanding better the proof assistants from the point of view of foundations of mathematics. I'm not claiming any inconsistency in Coq, I'm just comparing this possibility with the possibility of inconsistency of Q0. For me the inconsistency of Coq is a rather theological claim.
More information about the FOM
mailing list