[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

>
> Tim said:
> If you are right, and Jose trusts set theory to some degree, then maybe
> the following references will be relevant.


Following the so-called post-moderns, I would like to avoid the statement:
I trust X. I rather prefer to use the statement: I trust X more than Y. In
my case: I trust Q0 more than CIC. So, a proof of the incompleteness of
Peano arithmetic in Q0 is better than such a proof in CIC, that is my whole
point. Hence, the foundations of mathematics, like this incompleteness
result, should be done in Q0 rather than in CIC.

There are some people doing foundations of mathematics in Coq (I will no
mention names) and it would be a shame if their work will be dismissed in
the future because of some problem with the foundations of mathematics. In
my case, I have not personal interests in this question, because my own
mathematical results (published in Journal of Number Theory) are rather
classical and they can be formalized in any practical proof assistant.

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