[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:



> 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