The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.