The Coq mailing list

[Недзельский Михаил <MichaelNedzelsky AT yandex.ru>]

Vladimir Voevodsky пишет:
> A question: where is a mistake in the following reasoning?  
>
>
> 1. assume that "classical Peano arithmetics is inconsistent" i.e. there is a 
> finite sequence of deductions in the corresponding  theory which constitutes a proof of 
> False (=not True),
>
> 2. using double negation trick this sequence can be translated into a 
> sequence of deductions in a strongly normalizing intuitionistic  type system 
> with inductive N and inductive empty type which will create an inhabitant of 
> (not not not True),
>
> 3. inhabitance of (not not not True) is equivalent to the inhabitance of the 
> empty type,
>
> 4. strong normalization implies that the empty type is not inhabited. 
>
> Therefore, "classical Peano arithmetics" is consistent. 
>
> ???
>
> Vladimir.
>
>
>   

It seems that in order to formalize given reasoning you need a formal 
system with strength >= strength of PA (especially step 4).  If PA is 
inconsistent, then this formal system is also inconsistent, so both "PA 
is consistent" and "PA is inconsistent" will be theorems in this formal 
system.

Michael Nedzelsky