The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Consistency of Coq in as much as it is rigorously proved at all depends as 
far as I understand on the consistency of much more than Peano arithmetic - 
basically it is equivalent to the consistency of a fairly strong version of 
ZF set theory with universes.

Vladimir.


On Sep 27, 2011, at 11:50 AM, 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