[FOM] proof assistants and foundations of mathematics
doucetced at gmail.com
Sun Aug 5 15:28:37 EDT 2018
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
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM