[FOM] proof assistants and foundations of mathematics

[Lawrence Paulson]

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