The Coq mailing list

[roconnor AT theorem.ca]

In my development of Goedel's incompleteness theorem I also prove the 
consistency of Peano Arithmetic.  Thus if Peano Arithmetic were 
inconsistent then Coq would be inconsistent.

On Tue, 27 Sep 2011, Vincent Siles wrote:

> 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

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