[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

Petrus Abaelardus said: "The beginning of wisdom is found in doubting; by
doubting we come to the question, and by seeking we may come upon the
truth".

This year, I hear several times, from different people, the following
statements: "in community X we assume that proof assistant Y is consistent
and everything that we mechanize in this proof assistant is considered
true, if you don't believe in that, goodbye".

I like proof assistants for doing traditional mathematics (number theory,
algebraic geometry, partial differential equations, measure theory, etc.),
but I am not sure that some proof assistants could be used for foundations
of mathematics, because they required their own foundation and if someone
assume that "anything that my proof assistant verifies is true" the
foundations of mathematics thinking dies.

 I'm almost convinced that MetaMath can be used for the foundation of
mathematics, but I'm not so sure that Coq could be used for the same
purpose. So, I would like to recommend people interested in this subject to
read the following paper, from the point of view of the foundations of
mathematics, and to reply if they are convinced of this proof of the
"Essential Incompleteness of Arithmetic": https://arxiv.org/abs/cs/0505034

I'm not making a claim, I'm just sharing my doubts with people with more
experience than me in foundations of mathematics.

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180804/615974da/attachment-0001.html>