The Coq mailing list

[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.''