[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Mon Aug 6 21:08:58 EDT 2018
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
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.
More information about the FOM