[FOM] proof assistants and foundations of mathematics

[Mario Carneiro]

On Sat, Aug 11, 2018 at 12:18 AM José Manuel Rodriguez Caballero <
josephcmac at gmail.com> wrote:

> There are some people doing foundations of mathematics in Coq (I will no
> mention names) and it would be a shame if their work will be dismissed in
> the future because of some problem with the foundations of mathematics. In
> my case, I have not personal interests in this question, because my own
> mathematical results (published in Journal of Number Theory) are rather
> classical and they can be formalized in any practical proof assistant.
>

This is an interesting position. If I read it correctly it is
anti-formalization, in the sense that it is better to have a mathematical
result not formalized at all, so that it remains foundationally ambiguous
(with the presumption that it can fit in a relatively weak logic), rather
than to have it formalized in a proof assistant with an unnecessarily
strong logic.

Of course this goes against the intuition that a theorem that has been
formalized in *any* proof assistant is more likely to be correct than one
that has not. But this is not really a comparison on equal footing since
this position is concerned with "human error" in the verification that a
statement is in fact provable from a formal system, while you are more
concerned with the possibility that the proof is valid but the underlying
logic is not consistent. (I think you said that you are not seriously
concerned with a failure of consistency, but I don't know how else to make
sense of your differential trust of Q0 over CIC.) Indeed, "it would be a
shame if their work will be dismissed in the future because of some problem
with the foundations of mathematics" sounds like a worry that CIC is
inconsistent.

I would argue that having a theorem formalized in Coq (or similar) puts you
in a much better situation to understand exactly what assumptions are
needed in a theorem, since you can analyze the proof as given for use of
axioms. It is fully possible within these systems to avoid the use of this
or that axiom, and the computer can also check that you have done so. So in
that sense Coq will verify more than just the bare statement "theorem X is
provable in CIC", it can also use other systems in place of CIC even if
this is the main logic for the system. Proving things in this way may
require additional effort from the formalizer, but the point is that if you
have some theorem X you believe to be provable in Q0, and this proof is
formalized in Coq it provides a much higher degree of confidence in the
statement "theorem X is derivable in Q0" than an informal proof (making no
direct reference to Q0 or CIC) would. More specifically the additional work
needed to check Q0 derivability given the formal proof in Coq is smaller
than checking Q0 derivability given an informal text.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180811/5d119324/attachment-0001.html>