The Coq mailing list

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

Because there are some persons interested in this debate about foundations of mathematics in Coq, I will add some points.

To say that the consistency of Peano arithmetic was verified using Coq is misleading. This sentence promotes the idea that the consistency of arithmetic was verified, in metamathematical way, using the software Coq as a tool (this is how mathematicians outside the Coq community may think about it). A better way to express it could be: the consistency of Coq is stronger than the consistency of Peano arithmetic. Nevertheless, this specification is only needed for theorems related to Foundations of Mathematics and Model Theory. For example, it is fine to say that the infinitude of prime numbers was verified in Coq, because this theorem does not belong to the foundations of mathematics (it is elementary number theory).

There is a claim of proof of existence of God in Coq : https://github.com/FormalTheology/GoedelGod   

But the programmers of this proof were careful enough to ask to themselves the following questions: 

** Is the "god" of ontological proofs the same "god" of common religions? **

** Isn't it impossible to prove god's existence by pure reason? **

** How is this useful? **

In the same way, we could ask us the questions (I added my personal subjetive answers):

** Is the type nat of Coq the set of natural numbers ? ** (no, it is just its standard model)

** Isn't it impossible to prove consistency of Peano arithmetic by pure reason? ** (it is impossible to prove the consistency of arithmetic following Hilbert's standards)

** How is this useful? ** (to be critical of the validity of foundational theorems in Coq is useful, because it opens the door to new formal systems to do Foundations of Mathematics and Model Theory in a more natural way)

   

2018-05-03 8:47 GMT+02:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

José said:

  After this experience, I take less seriously when someone claims to have verified a theorem in Coq, because “isn't about logic; it is about proving stuff in Coq”.  

Well José this is true about any proof made by any mathematician in the world. They do proofs in a logical system (most often set theory) of which consistency can only be believed to be true. Let me quote (and translate very approximately) bourbaki’s introduction:

“To sum up we believe that mathematics will survive and that it will not fall appart from a contradiction suddenly discovered. But we do not pretend this belief comes from anything else than experience. This is not much but it has been since 25 centuries that math learned, and did not fall, from its errors. It is enough to consider the future with serenity.”

For French speaking:

“En résumé, nous croyons que la mathématique est destinée à survivre, et qu'on ne verra jamais les parties essentielles de ce majestueux édifice s'écrouler du fait d'une contradiction soudain manifestée; mais nous ne prétendons pas que cette opinion repose sur autre chose que l'expérience. C'est peu diront certains. Mais voilà vingt-cinq siècles que les mathématiques ont l'habitude de corriger leurs erreurs et d'en voir leur science enrichie, non appauvrie; cela leur donne le droit d'envisager l'avenir avec sérénité.”

Of course, if other members of the mailing list want to continue the discussion proposing new ideas, it will be a pleasure to read them.

Sincerely Yours,

José M.

On May 3, 2018, at 4:07 AM, Harrison, William L. <harrisonwl AT missouri.edu> wrote:

I hate to be “that guy”, but...

Hasn’t this discussion already wandered far away from the subject of this mailing list (i.e., Coq)?

Sent from my iPhone

On May 2, 2018, at 7:58 PM, "roconnor AT theorem.ca" <roconnor AT theorem.ca> wrote:

On Thu, 3 May 2018, Jose Manuel Rodriguez Caballero wrote:

Russell said:
"I also want to point out that proving that PA is consistent doesn't by itself mean that there isn't a proof that PA is inconsistent”
Ok, we are not talking the same language. In my world: PA is consistent means that there isn't a proof that PA is inconsistent (a proof that 1=0 formalized inside PA). I’m following
Hilbert’s metamathematical standards: https://plato.stanford.edu/entries/hilbert-program/

"In my world: PA is consistent means that there isn't a proof that PA is inconsistent"

Firstly, your statement is incomplete.  There isn't a proof according to what system?  Please, if you are going to dive into logic like this, don't use the term "proof" unaddorned like this.  Mathematical statements are not provable in any absolute sense.  Mathematical statements are only provable or not within some deduction system.  Coq can prove something, or ZFC can prove something or PA can prove something, and these different systems form completely different classes of statements of what they can or cannot prove.

Secondly, your definition is wrong.  "PA is consistent" either means "it is not the case that PA is inconsistent" or it means "there exists some statement S such that PA doesn't prove S", or it means that "PA doesn't prove the statement '1=0' ".  These three definitions are generally considered equivalent, but they are all distinct from your definition.

The statment "it is not the case that PA is inconsistent" is entirely distinct from "there isn't a proof that PA is inconsisent (in some system)".  For any given statment, "S is not true" and "T doesn't prove S" are entirely distinct in general.

Thirdly, the definition of "X is consistent" under discussion is formally defined right here @ https://github.com/coq-contribs/goedel/blob/a232fade79805c9339aaa4ec2c641723095e2c4e/folProof.v#L109 If you don't like that definition, that's fine.  But that statement is what is being proved by Coq in this development.

Let me reiterate again that "Essential Incompleteness of Arithmetic Verified by Coq" is only claiming that "PA is consistent" is provable in Coq (and this is just a side remark within that paper).  This is a claim that you can directly verify yourself by downloading the development and checking it in Coq and seeing for yourself that Coq indeed considers the deduction valid.  The paper does not directly claim that "PA is consistent" is true; that would only follow if you assume that Coq is sound, and the paper doesn't discuss the soundness of Coq.

Proving the Essential Incomplentess of PA in Coq is like proving the Feit-Thompson theorem in Coq, only much simpler.  It is an exercise that is meant to teach/learn how to create proofs of things in Coq in practice. The paper isn't about logic; it is about proving stuff in Coq.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''