[FOM] "Salvaging" Voevodsky's talk

[Panu Raatikainen]

Martin-Löf's intuitionistic theory of types may be formulated without  
a universe, ML_0, or with one universe, ML_1.

ML_0 is equiconsistent with PA, but ML_1 can prove the consistency of PA.

(see e.g. Beeson's 1985 book)


Best, Panu



"Panu Raatikainen" <panu.raatikainen at helsinki.fi>:

> If I am not totally confused, there are versions of constructive  
> type theory which prove the consistency of PA (right?).
> I wonder what Voevodsky would say about that?
>
> Best, Panu
>
>
> On Sat, Jun 04, 2011 at 06:51:22PM -0400, Timothy Y. Chow wrote:
>
>> The last part of his lecture argues that constructive type theory is a
>> better approach to foundations than traditional approaches are, because it
>> is more robust to possible contradictions.
>
>
> -- 
> Panu Raatikainen
>
> Ph.D., University Lecturer
> Docent in Theoretical Philosophy
>
> Theoretical Philosophy
> Department of Philosophy, History, Culture and Art Studies
> P.O. Box 24  (Unioninkatu 38 A)
> FIN-00014 University of Helsinki
> Finland
>
> E-mail: panu.raatikainen at helsinki.fi
>
> http://www.mv.helsinki.fi/home/praatika/
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>



-- 
Panu Raatikainen

Ph.D., University Lecturer
Docent in Theoretical Philosophy

Theoretical Philosophy
Department of Philosophy, History, Culture and Art Studies
P.O. Box 24  (Unioninkatu 38 A)
FIN-00014 University of Helsinki
Finland

E-mail: panu.raatikainen at helsinki.fi

http://www.mv.helsinki.fi/home/praatika/