[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

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 
skepticism), 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