FOM: Using Universes? The expert speaks again

[Harvey Friedman]

>    Reply to McLarty 4:50Pm 4/8/99:

I spoke to my expert in detail again. Here is what I have to report:

1. This statement of McLarty is true:

>    	They [Universes] are not formally indispensible to the number
>theoretic results. That has long been clear to mathematicians
>and I said it in my first post on this thread. They are in fact
>present in virtually all cohomological number theory today
>including at least one key reference in Wiles's proof of the
>semi-stable Taniyama-Shimura.

2. This statement of Friedman is true:

>>*The use of universes in FLT - or any serious number theory - has never,
>>even remotely, been any kind of issue. Nobody who understands such proofs
>>does anything but think about very small structures from the start till the
>>end. The number theorists are perfectly well aware of this. And they didn't
>>have to do any work to eliminate large structures.*

The only hedge I detected is this: if one wants to think about large
structures then one can easily do so. But all of the action is in small
structures. Which brings me to the next point:

3. This analogy of Friedman is perfectly appropriate - surely with regard
to Mordell's conjecture and FLT. And also probably for the other icons such
as Weil conjectures:

>>##Suppose I prove some facts about the complex algebraic numbers. I may
>>well quote that they are the unique algebraic closure of the field of
>>rational numbers. I may well provide a reference to Lang's Algebra, where
>>it is proved that every field has a unique algebraic closure. Now in full
>>generality, this uses some serious set theory. Not only the axiom of
>>choice, but also in the form of Zorn's Lemma - with its implicit
>>comprehension - and also even power set and replacement if done too
>>slickly! Aha!! I am "using" serious abstract set theory - essentially all
>>of Zermelo set theory. Bullshit!##

4. According to the expert, the real reason that the obvious eliminability
of Universes is not frequently pointed out in the literature is just that
it is so obvious. But the expert says that if there was ever a problem,
then a lot of attention would then be paid to it! Also, some of the people
LIKE them.

Again, I think that the analogy with algebraic closure is appropriate. A
lot of people LIKE the idea that any field whatsoever has a unique
algebraic closure. People like this even if the only application they make
of it in their own work is the algebraic closure of finite fields and the
rational numbers. Thus they can either choose to "apply"

every field has a unique algebraic closure

or they can choose to "apply" any of the following:

every finite field has a unique algebraic closure
the field of rationals has a unique algebraic closure
every countable field has a unique algebraic closure.

or, if they want,

the field of reals has a unique algebraic closure.

Now this last statement can be viewed as an application of "every field has
a unique algebraic closure"! And that uses a lot of set theory. But there
is the well known proof that the field of complex numbers is the unique
algebraic closure of the field of real numbers. This does not use such set
theory.

When discussing "real uses," one must at least be sensitive to this simple
kind of distinction of "apply."

The expert does not think that these "applications" of Universes are more
serious than this.

5. The expert confirmed that there would be great interest in removing
Universes if there was ever a problem in doing so.

Also the expert confirmed that there will be great interest in finding
genuine uses of Universes in the integers. That this would be a real
foundational event - not like the nonevent of the present obviously
removable uses of Universes.
*****

>       	So you believe that Grothendieck is not a serious number
>theorist, nor is Deligne. They won Fields Medals, sure, but that is
>just politics.

That conclusion does not logically follow from anything that I have said.

>    	That is bare ignorance. Check it with your expert. Please.

I did. I guess my expert is the one that is ignorant?
>
>       	I consider John Tate and Barry Mazur serious number
>theorists. Do you? Now look at their articles in MODULAR FORMS AND
>FERMAT'S LAST THEOREM--entirely aimed at explaining the FLT proof.
>Large structures come up much less often here than in some other
>parts of Mazur's work but they still come up.

So obviously eliminable that it presumably wasn't worth mentioning the
eliminability.

Finite combinatorists normally say things like "we work in the category of
finite partial orderings." Are they using class theory? The most literal
interpretation of this is that they are forming the proper class of partial
orderings whose domain is a finite set. Maybe this uses universes! (I know
that you are not that crazy).

>       	The category of commutative Hopf algebras over a ring is no
>small structure, just to take one example from Tate's article. A
>single Hopf algebra can have arbitrarily large cardinality.

The category of groups, rings, or fields is no small structure, just to
take one example from lots of articles. A single group, ring, or field can
have arbitrarily large cardinality. So what?

>This
>brings us to the real point: Wiles's proof may formally need only
>some very small Hopf algebras. But quite serious number theorists,
>who understand the proof, find it simpler to work from general
>theorems on the large structure.

Just like many people might find it easier to work from "every field has an
algebraic closure" before getting serious about analyzing the finite or
countable fields and their algebraic closures that are actually relevant to
the mathematics.

You are simply trying to ascribe foundational significance where there is
none.

>       	The Grothendieck duality theorem for a finite field K, deals
>with universe-sized categories and functors based on K.

The expert says: if you want to, or insist. But only controllable
categories and functors play any role.

>The proof
>that Wiles cites, by Altman and Kleiman, is taken with acknowledgment
>from Grothendieck's SGA and it uses universe-sized sets. You could
>avoid them but Altman and Kleiman use them. If these sets exist, so
>do Grothendieck universes.

They probably really LIKE them. That doesn't mean that they have a USE for
them in serious number theory.
>
>       	If you think of Wiles as a serious number theorist,
>take his word for the importance of the theorem: In the introduction
>to his paper he says the "turning point in the whole proof came
>in spring 1991" when he saw he could use Grothendieck duality
>theory (page 451).

Same as above.

>	Grothendieck universes were a step in first creating the
>cohomology of schemes, especially to prove the Weil conjectures.
>They succeeded. No simpler rigorous treatment is yet known,
>though there is a familiar vastly more complicated treatment that
>avoids using universes.

The expert disagrees. He/she says that elimination of Universes is
**routine** for such things as Weil conjectures, and not "vastly more
complicated, intellectually."
>
>	Universe-sized sets are routinely used, without comment,
>in the literature including introductions to etale cohomology--
>and even the standard graduate introduction to algebraic geometry
>and number theory, Hartshorne ALGEBRAIC GEOMETRY (Springer 1977).
>They occur in essentially every application of derived functor
>cohomology. You may regard this as ignoring rigor, or as implicit
>use of universes.

Just as very substantial set theoretic methods are used in standard
graduate introductions to algebra - e.g., in fields have unique algebraic
closures.
*****

I repeat: the really interesting foundational matter is finding genuine
unremovability of Universes in the integers. In fact, there is presently no
genuine unremovability of Universes for any statement about sets of limited
rank! This is because, e.g., regularity properties about projective sets of
real numbers either can be proved in ZFC or require large cardinals far
beyond Universes.