The Coq mailing list

[roconnor AT theorem.ca]

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