FOM: Grothendieck universes

[Stephen G Simpson]

Colin McLarty 16 Apr 1999 11:44:32 writes:

 > Grothendieck and his heirs have theorems of number theory formally
 > provable in ZFC. Grothendieck regards those proofs as essential
 > uses of universes since the proofs which eliminate universes have
 > no genuine mathematical meaning.

Did Grothendieck really say things like this?  If he did, it's
interesting from at least a sociological point of view.  Could you
please provide some quotes or page references where Grothendieck says
this kind of thing?  If there are no quotes from Grothendieck, some
quotes from his prominent heirs will do.

But in addition to the sociological issue, there is also the
scientific question of whether the pronouncements of ``Grothendieck
and his heirs'' (as interpreted by you) are correct.

Do you agree with ``Grothendieck and his heirs'' that the proofs in
question are essential uses of Grothendieck universes?  Do you agree
with ``Grothendieck and his heirs'' that the well known methods of
eliminating Grothendieck universes from these proofs are
mathematically meaningless?

-- Steve