The Coq mailing list

[Cody Roux <cody.roux AT inria.fr>]

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