The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Dear José,

thank you for explaining that you are a Master's student, and not just
a random internet crank and/or a troll, which I assumed you to be. I
apologize for that.

There is no argument by authority here. We keep telling you that you
are bringing up things that are very well known and that people
already understand. You keep dismissing what you are being told and
you are pushing your own agenda. From my perspective it looks like you
do not *want* to understand, a typical sign of an internet crank. But
as a Master student you have many things to learn, in which case the
better thing is to point you at places where you can learn them.

For example, a useful one might be Randy Pollack's "How to believe a
Machine-Checked Proof?"
(http://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf) There you will see
what the real issue are when it comes to understanding mechanized
proofs. They do not revolve around the things you are bringing up,
because the issues you are bringing up are very general and they apply
to every formal system and all meta-reasoning. Your points can be
translated almost word-for-word when we replace CiC with ZFC.

One last time: CiC is a formal system. In this system it is possible
to produce a proof that PA is consistent, and Russell O'Connor has
done so. These observations are not possible to attack, unless you
actually deny the existence of the Coq files on GitHub. You could also
try to find a mistake in the definition of "PA is inconsistent" in
those files, but I very much doubt you can succeed, as a number of
people looked at it.

The rest is the *interpretation* of what it means that these files
exist. Such a discussion may be of interest to some people on the
list, but it must necessarily have an educational character, as there
can be nothing new in it. The same discussion has been replayed many
times with respect to other formal systems. All the remarks you made
were either the same as old stuff people said many decades ago, or
were just mistakes. Some were also impolite because you said things
like "Russell O'Connor did not prove in Coq that PA is consistent",
were told this was not the case, and then you kept saying it. Please
do not confuse your own interpretation of what Russell did (such as it
is) with what he actually did (he explain this very clearly). I also
respectfully ask you to listen to other people's arguments. Several
people had the patience to explain to you (I did not, unfortunately)
the difference between "truth" and "provability", that "provable" must
always refer to a formal system, that you were not careful enough in
your wording, etc. I think they tried to help.

With kind regards,

Andrej






On Thu, May 3, 2018 at 3:05 PM, José Manuel Rodriguez Caballero
<josephcmac AT gmail.com>
 wrote:
> 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
>>
>>
>>
>