[FOM] "Salvaging" Voevodsky's talk

[Roger Bishop Jones]

On Monday 06 Jun 2011 09:52, Panu Raatikainen wrote:
> Martin-Löf's intuitionistic theory of types may be
> formulated without a universe, ML_0, or with one
> universe, ML_1.

We may also note that Voevodsky makes use of universes, even 
to the extent of using a patch to COQ which delivers some 
kind of "universe polymorphism" at the expense of making the 
system formally inconsistent!

So on multiple grounds it is evident that Voevodsky uses a 
system in which the consistency of PA is provable!

Roger Jones