The Coq mailing list

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

Dear William,

  For me it is ok to finish the discussion, because I confirmed my initial worries about the paper/PhD Thesis "Essential Incompleteness of Arithmetic Verified by Coq”. I quote the author (from this mailing list):

• "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”

Indeed, my prediction yesterday was, I quote myself: “My modest conclusion is that Russell O’Connor formally mimicked the Gödel-Rosser argument in Coq, but he did not consider the rôle of Coq in the foundation of mathematics as a whole”. So, I think that I understood the paper. 

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