Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)


Chronological Thread 
  • From: <Rajeev.Gore AT anu.edu.au>
  • To: <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
  • Date: Thu, 3 May 2018 14:27:30 +1000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Rajeev.Gore AT anu.edu.au; spf=Pass smtp.mailfrom=Rajeev.Gore AT anu.edu.au; spf=None smtp.helo=postmaster AT mail2-drop-p3.anu.edu.au
  • Ironport-phdr: 9a23:1fOvcxVMNA9ju7ddj1XdKSs93CTV8LGtZVwlr6E/grcLSJyIuqrYbBeEt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YlsN+g6FVrhyhqRJh3oDbYo+VOv1kfqPcZt4aWXNBU9xNWyFbHo+xbY0CBPcBM+ZCqIn9okMDoByiCwa2BuPg1CFHhmHs0aM71OQhCx/J0Rc6ENIIrXTYtsv6O7oPUeyv1qbI0CzOYvVL0jnz74jIdwouofCKXb9oa8XRz1QvGxnbgVqNtIzpJSma1vkVv2iU7upgSeKvi3M8pA1rvjevwcIshpHTho8U0FzL6T92zJ4uJd2kUkF7Z9CkEJxKty6HLYd5XN4tQ3xutS0nybMGoYa2cDUExZg73RLSa/2Kf5KJ7x/sTuqcLzN1iGp4dL+/mxq+61asxvHyW8WuzlpGszRJnsPNu3wQ0RHY99KJReFn/ki73DaCzwDT5f9AIUAzjafbLoQuwr80lpYNqEjMAzX2mELujKOPbkUp9PKk5P7hYrX7vJOTKZJ7ihzkPqs0h8yzGeU4Mg4QUGiH4emwybPu8VHjTLhKj/A6iKjUvZ/AKckVoqO1GwpV3Zwi6xa7ATemytMYnXwfIVxZYh2HjZbmNE/QIPziDPm/hE6snylwyv/cOL3hH4/BIWben7f8Z7py8VNcxBIpzd9D/5JUFq0BIPXrV0Dts9zYFwY1PBCww+b6E9pwzZgeWGKKAq+BKqzeq16I5uQ1I+mNfoAZojj9K+J2r8Lp2CsynkZYdq2017MWbmq5F7JoORPKW3f0hsY9FjJehAM8QeH0znKFSzN7bnCvGa8w+3cyFdT1I53EQ9X5urWD0SqlWLJRfG1uA1aRV3rkasONRqFfO2qpPsZ9n2lcBvCaQIg72ET27V6o+/9cNuPRvxYgm9fm3dlx6ffUkEhopzVyEoKQ33zLRnwmxzpUFQ9z57h2pAlG8nnGybJx2qYKHNpOof5FT0EzKMyElrEoO5XJQgvEO+yxZhOmT9GhW29jS9swx4VLb1x6A5C61VbK2TfsDrMI0bWWVsQ5


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




Archive powered by MHonArc 2.6.18.

Top of Page