[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

O'Connor's formalisation of the first incompleteness theorem is not
problematical for me, but just the fact that it was mechanized in Coq.
Indeed, I agree with O'Connor's formalisation of the first incompleteness
theorem mechanized in Peter B. Andrews Q0, because, in principle, Coq could
be inconsistent and Q0 could be consistent at the same time. For me,
foundations of mathematics is not like a true religion, but something
like studies
in comparative religion.

My formation is mainly in pure mathematics (number theory), not in
foundations of mathematics. So, I'm rather curious of some results that
could be not interested at all for people with a solid formation in
foundations of mathematics: I'm just learning from the answers in FOM and
MetaMath groups and I'm understanding better the proof assistants from the
point of view of foundations of mathematics. I'm not claiming any
inconsistency in Coq, I'm just comparing this possibility with the
possibility of inconsistency of Q0. For me the inconsistency of Coq is a
rather theological claim.

Regards,
José M.



2018-08-06 10:27 GMT-04:00 Lawrence Paulson <lp15 at cam.ac.uk>:

> It's interesting to see a consistency claim stated in such an extreme
> form. Certainly these systems are designed with great care to be sound, and
> soundness bugs are taken very seriously. A couple of years ago, there was
> concern when it was discovered that a sufficiently devious Isabelle/HOL
> user could sneak in an elaborate form of circular definition, and from that
> prove 1=0. This is not my idea of a soundness bug (users should take
> responsibility for their definitions), but I agree that it deserved to be
> fixed. One has to be naïve to assume that no further bugs affecting
> soundness are present.
>
> Recently I have promoted the claim that formal proofs should be legible: a
> reader should be able to examine the proof document and assess the
> correctness of the progression of statements using their own intellect.
> This would complement the assurances we already get from the system
> architecture with its small deductive kernel, et cetera.
>
> It's interesting that you take O'Connor's formalisation of the first
> incompleteness theorem as problematical. What is the issue here?
>
> Larry
>
>
> > On 4 Aug 2018, at 23:59, José Manuel Rodriguez Caballero <
> josephcmac at gmail.com> wrote:
> >
> > 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180806/d3af3000/attachment-0001.html>