[FOM] "Salvaging" Voevodsky's talk
Roger Bishop Jones
rbj at rbjones.com
Mon Jun 6 15:42:53 EDT 2011
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!
More information about the FOM