The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.org>]

I agree with Cody. Inconsistent Peano arithmetic would be a much much bigger 
thing than Coq being inconsistent.

I think I was told that De Bruijn jokingly liked to say that proving the 
inconsistence of PA was a "interesting but
tricky PhD subject".

Note also that if you have a proof of inconsistence of PA, you should easily 
translate it into a Coq paradox, since
Coq is an extension of PA.

I personally doubt that such a paradox exists in PA, and even more than we 
will see one in our lifetime. But there
certainly is some thrill in hearing about this.

Best,

Benjamin



Le 28 sept. 2011 à 11:31, Cody Roux a écrit :

> 
> 
> ----- Mail original -----
>> De: "Vincent Siles" 
>>Â <vincent.siles AT ens-lyon.org>
>> À: "Coq-Club Club" 
>>Â <coq-club AT inria.fr>
>> Envoyé: Mardi 27 Septembre 2011 17:50:13
>> Objet: [Coq-Club] a question about CIC/Coq consistency
>> Hi everyone,
>> I just bumped into this [1] and since I don't know much about CIC
>> consistency proofs,
>> I was wondering if it relied on peano consistency or not ?
>> 
>> 
>> Cheers,
>> Vincent
>> 
>> [1] http://www.cs.nyu.edu/pipermail/fom/2011-September/015816.html
> 
> The alleged proof of inconsistency takes place in a system so weak 
> (Robinson arithmetic) that every formal (and informal) proof ever made in 
> any system would have been carried out in an inconsistent one. So either 
> you should be much more worried than you are, or much less worried :)
> 
> Here is a fun discussion at the n-category cafe:
> http://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html
> 
> All the best,
> 
> Cody