The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I am not sure I understand. If PA is inconsistent then I can prove  
"not True" in it. Using the "double negation trick" (see Godel's "On  
intuitionistic arithmetic and number theory" and intro to it by  
Troelstra in Godel's "Collected Works", v1, 1986) I can, presumably,  
translate  this proof into a construction of a proof term for "not not  
not True" and, therefore, for "not True" and for "False".

As far as I understand, there is a claim that "constructive type  
systems" can be proved in an elementary way (syntactically) to be  
consistent. Then this would constitute an "elementary" proof of  
consistency of PA which is, presumably, impossible.

So my question is which of these arguments is incorrect?

Vladimir.



On Dec 29, 2009, at 10:34 AM, Stefan Monnier wrote:

> > 1. assume that "classical Peano arithmetics is inconsistent"
> [...]
> > Therefore, "classical Peano arithmetics" is consistent.
> > ???
>
> So you basically have a function of a type of the form "¬A → A"  
> for some
> particular A.  Note that this is only problematic if you can prove  
> ¬A,
> since otherwise you can never call that function anyway.
>
>
>       Stefan