The Coq mailing list

["Harrison, William L." <harrisonwl AT missouri.edu>]

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