The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

I think this conversation is very interesting for us (especially since
many students read this mailing-list) ,
 may be is not so much about coq but about what it means to "prove" something.

Indeed many have the misleading idea that proving something is
equivalent to being "certain" of its truth.
This in turn comes from a common linguistic misunderstanding that
"truth" is a single concept. It is not!

Every discipline has a different idea for it:
Historic Fact(/truth), Legal truth, Physics/A valid model, math, (may
be logic is still different)
and if we include also some "woo" we have religious truth, and
critical truth (art, I think....)
(I apologise for errors or imprecision in the former sentence, I'm not
a researcher in most of the mentioned areas..)


A proof only hold over a certain set of  axioms. Those compose the
MODEL you are in.
Some models are Coherent, some other are not (and true=false there)
It is *possible* that our reality is re-presentable by an (arbitrary
complicated) model, but we can not really know. It is also not very
well defined what that would actually mean.
If that is the case, it is also *possible* that such model is not
coherent. I actually like to think this is the case :-)

With my limited knowledge of the topic, inspired by this conversation,
I would dare to ask a question to this list:
-is there any proof in any (not proved incoherent yet) system showing that
"it must exist a coherent systems complex enough to support Godel theorem"?
sometimes I wonder if they are just going to be bound to be
incoherent, and the proof "true=false" is often just so gigantic that
escape human comprehension.




On 3 May 2018 at 16:27,  
<Rajeev.Gore AT anu.edu.au>
 wrote:
>
> Hi William,
>
> I beg to differ. I know some logic and proof theory but I am learning
> Coq, so I am very interested in this discussion. Please continue :)
>
> Of course, if multiple people agree with William then he has a point.
>
> raj
>
> 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.''
>
> --
> Rajeev Gore'
> Professor, Logic and Computation Group,
> Research School of Computer Science
> ANU College of Engineering and Computer Science
> The Australian National University
> Canberra ACT 2601
> Tel:   +61-2-61 25 86 03
> Fax:   +61-2-61 25 86 51
> Email: 
> Rajeev.Gore AT anu.edu.au
> Web:   http://arp.anu.edu.au/~rpg
> ANU CRICOS Provider Number - 00120C
>