The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Andrej said

Proofs done in Coq follow a standard of rigor which is an order of
magnitude above the standard of peer reviewed mathematics journals.
People who produce mechanised proofs in general have a much, much
better understanding of logic and foundations than most mathematicians
who publish papers. Your comments are out of place and couched in
ignorance.

I agree my comments are couched in ignorance, I'm just a Master student. I began to learn type theory, Coq, model theory and category theory in January 2018 (all together). All my publications are above number theory and my theorems can be easily mechanized in Coq without foundation issues. I was enthusiastic of Coq because I though that it could help to avoid arguments by authority in mathematics, but I was wrong and you help me to recognize my mistake. Thank you.

 

2018-05-03 14:44 GMT+02:00 Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>:

To clarify this discussion, perhaps we should be distinguishing two
concepts which seem to be mixed in the discussion:

1/ that of *foundations*

2/ and that of *logical rigor*.

*Foundations* is the quest for a coherent framework (or language)
to develop mathematics and reasoning, within strict rules to avoid
paradoxes (contradictions). About a century ago, there was even
some hope that such a system could prove every possible theorem ...
including its own coherence.

Some of the greatest mathematicians/logicians devoted a great
deal of efforts to get one, without success. Then Gödel came and
everything changed: he showed than as soon as your foundational
system F is powerful enough to express PA, then F "cannot prove
the consistency of (the internal copy of) itself" unless F is
inconsistent. For many, this landmark result put an end to the
quest of foundations.

But not for everyone though: it is significant that precisely
R. O'Connor's implementation of Gödel's result in Coq is discussed
the way it is now on Coq-Club ...

*Rigor* is about choosing a system of rules, accepting it as primitive,
and formalize as much as possible within that system. Rigor is not
concerned with the consistency of this primitive system but it is
very concerned with the systematic encoding of every proof within
its strict rules. With the advances of computer science and computer
assisted proofs, what is considered as rigorous has been changed
significantly: the primitive system should be designed in a way
such that checking whether some proof sketch respects the allowed
rules is a *decidable problem* (or even more, a tractable problem).
The natural language is not accepted as rigorous any more. Computers
(I mean, the program that runs the proof/type-checking algorithm)
cannot be corrupted to "believe" in an argument ... or even avoid
checking sub-case 22 because it is symmetric to case 21.

One of the great advantages of the automated formal proof-systems is
the stability of proofs. Imagine that some day a contradiction is
discovered in Coq (or in Coq + some extension, as what happened in
2013/14), then Coq will hopefully be modified to avoid the
contradiction (like when naive set theory was replaced with ZF
for instance) in a way to keep as much of the existing system as
possible so that proof-scripts that make no use (of the features
that allowed) the contradiction will still be accepted as correct
proofs in the modified Coq. And such a check could be done mostly
automatically now.

Personally, I am not interested in the quest for foundations any
more because I believe it is a hopeless quest. To justify the
consistency of a system, you always need to use a "stronger"
system of which the consistency is even more questionable ...

But I am very interested in logical rigor. And frankly, it is order
of magnitudes more common to encounter lack of rigor than logical
paradoxes.

Best regards,

Dominique