[FOM] proof assistants and foundations of mathematics

[Arnon Avron]

Maybe I am wrong, but I think that what worries  Jose
about Coq is the *mathematical* reliability, and even the consistency,
of the very complicated mathematical typed sytem on which Coq
itself is based.  Someone who has doubts about *that* will not fully trust 
proofs in Coq even if he takes it for granted that its
type system  was implemented correctly, and no cosmic rays were affecting 
its behavior either.

Arnon Avron


On Mon, Aug 06, 2018 at 09:08:58PM -0400, Timothy Y. Chow wrote:
> Jose Manuel Rodriguez Caballero 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".
> 
> The usual concern about a proof assistant is that it is *correctly*
> implemented, as opposed to "consistent"; the adjective "consistent"
> is usually applied to systems of axioms, rather than the proof
> assistant.
> 
> The distinction is especially important in the case of Coq, which
> you seem to be particularly worried about, since Coq is flexible
> enough to handle a variety of sets of axioms.
> 
> 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).
> 
> Regarding #1, determining the consistency of a set of axioms in the
> abstract is not really the job of the developers of a proof
> assistant. The proof assistant is just supposed to be able to track
> the step-by-step correctness of a proof.  If there is an unknown
> inconsistency in, say, ZFC, then that is hardly something you can
> blame a proof assistant for---nor does it really matter, since a
> proof assistant is just supposed to check that an alleged theorem
> really follows from ZFC, and it can accomplish this just fine
> whether or not ZFC is consistent.
> 
> Regarding #2, as Larry Paulson said, the proof assistant communities
> are generally very cognizant of the concern, and don't claim 100%
> perfection. If you have a specific concern (as opposed to some
> general, vague skepti/racism), then they are usually interested in
> hearing it.  However, I think it is true that if you have general
> doubts about the correctness of a particular proof assistant, and
> you cannot articulate precisely what's bothering you, then there's
> only so much someone can do to increase your confidence in its
> correctness.  They can only point you to some other proof assistant,
> or invite you to write your own.  This is probably what you sensed
> as a "goodbye."  As you've phrased it, it sounds unfriendly, but
> beyond forcing the community to say "Nothing is perfect" (which they
> will be happy to say if you ask them politely), I don't know what
> more you can expect.  If one wants to accomplish something, it does
> no good to sit idle, paralyzed by doubt.
> 
> I also don't think that results such as Goedel's theorem are any
> different from any other branch of mathematics as far as proof
> assistants are concerned.  I can't make sense of your doubts about
> whether proof assistants can be used for the foundations of
> mathematics, and I wonder if those doubts are based on some
> misunderstanding about what proof assistants, or the foundations of
> mathematics, are intended to achieve.
> 
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom