[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

Tim wrote,

What I'm suggesting is that you carefully distinguish between:
> 1. worries that some particular system of axioms is consistent, and
> 2. worries that some particular proof assistant might erroneously declare
> that "X is a theorem of axiom system A" (e.g., because of a software or
> operating system or hardware bug, or because a cosmic ray zapped the
> crucial part of the hardware at the crucial moment and caused an
> irreproducible malfunction).


Yes, I implicitly identified Coq with CIC. So, I correct myself. My doubt
is: Does a proof of the incompleteness of Peano arithmetic in CIC is good
as a proof of the same result in Peter Andrews' Q0? Maybe this question is
trivial, but for someone like me, outside the world of foundations of
mathematics, it is a fundamental question. My intuition is that such a
proof in Q0 is better than the corresponding proof in CIC.

Also, when I said

"I am not sure that some proof assistants could be used for foundations of
mathematics, because they required their own foundation".

I meant that I'm not sure of the statement "for each deductive system X, we
have that X can be used for the foundation of mathematics", i.e., "maybe
there exists a deductive system X which is not good for the foundation of
mathematics". My reason for distrusting such a universal quantification
about deductive system is that if the foundations of X are as doubtful as
the foundations of traditional mathematics, then X is not a good candidate
for such a task. So, I rephrase my statement as follows, including the
implicit assumption "if the foundations of X are as doubtful as the
foundations of traditional mathematics, then X is not a good candidate for
such a task" :

"X could be used for foundations of mathematics if the foundations of X are
strictly less doubtful than the foundations of traditional mathematics"



Kind Regards
Jose M
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180808/00bbaf87/attachment.html>