[FOM] proof assistants and foundations of mathematics

[Cédric Doucet]

If I read well, you claim that X can/could be used for foundations of
mathematics if X does not require its own foundation.
Does such X exist?

2018-08-05 0:59 GMT+02:00 José Manuel Rodriguez Caballero <
josephcmac at gmail.com>:

> 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.
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180805/5b440af2/attachment.html>