FOM: Grothendieck universes

[Stephen G Simpson]

Colin McLarty 16 Apr 1999 13:56:35 writes:
 > I said Grothendieck believes cohomology in number theory can have
 > no genuine mathematical meaning without universes (specifically,
 > without derived functor cohomology)
 > 
 > Steve Simpson replied:

That's not exactly what I replied to.  What I replied to was your
statement in 16 Apr 1999 11:44:32 that ``Grothendieck regards those
proofs as essential uses of universes since the proofs which eliminate
universes have no genuine mathematical meaning.''  To me the key here
is the word ``essential''.  

But anyway, please do look up and tell us exactly what Grothendieck
said along these lines.  I want to know Grothendieck's context for the
phrases ``essential use of universes'' and ``genuine mathematical
meaning'', or reasonable facsimiles of these phrases, or as close as
you can come to reasonable facsimiles.  Since you say that the
relevant writings of Grothendieck are unpublished, it's particularly
important to get extended verbatim quotes.

By the way, in everything you have posted about alleged essential uses
of Grothendieck universes, you seem to be implicitly assuming that all
existing discussions of derived functor cohomology in the literature
rely on Grothendieck universes.  Is this really the case?  Has nobody
ever proposed a way of doing derived functor cohomology without
Grothendieck universes?  I seem to remember derived functor cohomology
occurring in some course that I took as a graduate student (probably
from Quillen), but I'm also fairly sure that Grothendieck universes
were not in that course or its prerequisite courses.

Another issue: In your interpretation of Grothendieck's alleged claims
about alleged essential uses of Grothendieck universes, what is the
sense of your phrase ``genuine mathematical meaning''?  Would you care
to make it a little clearer?

Regarding Friedman's work on the incompleteness phenomenon, you claim
to understand and appreciate the familiar and valid f.o.m. point that
ConZFC lacks ``genuine mathematical meaning''.  However, are you using
this phrase in the same sense in both the Friedman and Grothendieck
contexts?  I wonder.  It seems to me that ConZFC is ``mathematically
meaningless'' in a relevant sense which does not apply at all to
elimination of Grothendieck universes.  On the one hand, ConZFC
directly involves logical and metamathematical concepts -- formulas,
rules of inference, the axioms of ZFC, etc.  On the other hand, the
methods for eliminating Grothendieck universes are of a standard
mathematical nature, well known to number theorists.

If I'm right about this, then it seems to me there is nothing left of
your Friedman/Grothendieck comparison of 16 Apr 1999 11:44:32.

Even if we focus solely on the Grothendieck context, your statements
appear incoherent.  You say

 > Grothendieck (and even I) knows the methods are *quite* meaningful
 > mathematically. They have real, practical importance, since they
 > are also the methods for calculating specific cohomology groups in
 > particular cases.  He uses them.

but this seems to flatly contradict what you said before.  First you
said ``the proofs which eliminate universes have no genuine
mathematical meaning''.  Now you say ``the methods are *quite*
meaningful mathematically'', have practical importance for
calculation, etc.  Which is it?

Perhaps you are playing on some extremely subtle distinction between
``the proofs'' and ``the methods''?  If so, what is the distinction?

This kind of clarification is important, *if* you want people to know
what you are talking about.  Do you?

-- Steve

PS (for Martin Davis).

It's a dirty job, but somebody has to do it.