FOM: Thinking and faking with universes

[Harvey Friedman]

Reply to McLarty 5:34PM 4/9/99 and 12:32AM 4/12/99. The disappointing thing
about McLarty's postings is that he has been asked to explain what the
point is of considering, say, maps from gigantic objects into the small
(relatively) concrete objects that people are really interested in. His
responses contain virtually no substantial mathematical information - just
a huge pile of names and references to books (and some papers)!

The idea of the FOM is to provide substantial productive interchange among
a wide range of scholars interested in f.o.m. Surely McLarty can do more
than this. Surely this matter can be clarified without resorting to
technical jargon, in a way that is totally accessible to people on FOM.

McLarty 5:34PM 4/9/99 writes:

>        Historical nuance: universes were a clear and present issue to
>Grothendieck, Deligne as they first created the cohomology of schemes, and
>they thought about large structures as part of their serious number theory.
>You can see this in the SGAs.

What does "issue" mean? Are you trying to suggest that these two people
thought they needed large structures as part of their serious number
theory, or just that they liked the extra generality in Lemmas?

>        Practical nuance: even today number theorists who understand the
>proofs do also think, for convenience, about large structures such as the
>category of Abelian sheaves on a given scheme--only they do not think hard
>about it. It is quite routine and they know they could avoid it even as a
>routine. They teach the large structures to students as you can see in
>MODULAR FORMS AND FERMAT'S LAST THEOREM or any introduction to etale
>cohomology--or in Johan de Jong's course on etale cohomology two years ago
>at Harvard.

My expert does not think about large structures when thinking about Wiles'
proof of FLT. I talked to a second expert. Here is a what he said on this
point:

FRIEDMAN:

>2. But when you think about the actual number theory proofs such as Wiles,
>you don't think in terms of such gigantic objects. You think about finite
>objects or at most countable objects. Maybe sometimes real numbers enter.

SECOND EXPERT:

Yes.

McLarty writes:

>        Certainly the very small structures are "where the action is" in the
>number theoretic proofs.

The issue is: what is then the nature of the "uses" of universes - since
they are not "where the action is"?

>        I say Friedman's analogy [with using vast set theory to introduce
>algebraic numbers] fails in the historical and practical senses. Algebraic
>numbers were not discovered using Friedman's parody. No one today would
>refer to Friedman's parody in a proof in algebraic number theory, nor teach
>it to students.

Why not see "Since every field has an algebraic closure...", or "take the
algebraic closure of..."? Why doesn't that appear and why not teach it? In
Lang's Algebra textbook, "every field has an algebraic closure" is proved
on page 273 using the maximal ideal principle. This proof is riddled with
set theory. It isn't until page 390 that the case of real closed fields is
discussed, where the algebraic closure construction requires no significant
set theory. In fact, Lang's book is a good example of a lot of points I am
making. Almost all of the topics are proved in quite high generality, and
need substantial amounts of set theory - at least the proofs that are
formalized. But we know that when one gets serious about relatively
concrete mathematics, the set theory is superfluous in this area of
mathematics. In fact, there is almost nothing in this book that is concrete
at all! But the nonconreteness is only there because this material can
smoothly and naturally be presented in such great generality - not because
this generality is useful at all in any concrete situation!!

>I am precisely NOT ascribing Friedman's kind of foundational significance to
>them. I have said all along that they are formally dispensible. I am saying
>there is also a historical, practical aspect to foundations: What ideas did
>people need in order to create this theory?--though perhaps they can be
>eliminated in hindsight. And what ideas do people need to work with a
>theory?--though perhaps they can be eliminated in principle.

I question the word "need." Don't you think that the Lang's Algebra
situation is entirely indicative of the real situation? If not, explain why
not. After all, the Lang's Algebra situation is something that a reasonable
number of people on the FOM can relate to.

McLarty writes 12:32AM 4/12/99:

>	This post replies to some taunts from Friedman, and
>to his surprising suspicion that sheaf theory per se is a
>kind of fluff invented so mathematicians can talk about bigger
>sets than they need to.

I didn't say that's why sheaf theory was invented, or even why universes
were invented. They seem to be "a kind of fluff" - but I never expressed
that opinion about the reasons they were invented.

I should point out that McLarty in an earlier posting writes as follows:

>	I suspect there are no essential uses of the axiom
>of replacement in the general results of the Grothendieck
>school (as in Elements de Geometrie Algebrique, and the Seminaire
>de Geometrie Algebrique de Bois Marie) nor in the applications
>of cohomology in number theory (such as our icons Deligne,
>Faltings, and Wiles).

Friedman wrote:

>>First of all note that Mathias' expert - see Mathias, 6:24AM 4/9/99 -
>>agrees with me and my expert on the essential points, characterizes a
>>number of McLarty's wilder statements "over the top."
>
>	Both experts agree with me that universes do in fact
>appear in the proofs where I said they do. That seems to me the
>essential point.
>
>	Shipman started the thread by asking whether
>Grothendieck universes had even been used to prove a theorem of
>ordinary mathematics. I said they had, if you take published
>proofs at face value, but the uses were well known to be
>eliminable in principle. The experts both agree that is true.
>
>	Unfortunately Mathias's note to his expert says we are
>arguing about whether or not universes are essentially involved
>in the proofs. I have said from the start that they are not
>essential. Mathias's interpretation makes my statements "wild"
>indeed--and clearly wrong.

The reason your statements may be viewed as "over the top" is that you are
probably giving people a misleading impression as to the nature of the use
of universes in number theory. The question is, perhaps, the level of
superfluosness.

>	The uses are "fake" in the sense that they invoke
>stronger set theoretic axioms than the ultimate result needs.
>They are "real" in the sense that they actually occur in the
>published record.

What is misleading is to characterize them as "uses." I think that people
on the FOM deserve a clearer analysis of the nature of these "uses." I am
proposing that Lang's Algebra book be a guide to the discussion that can be
readily related to by many on the FOM.

Here is one of perhaps hundreds of places in Lang where an ambiguous use of
"use" occurs that is relevant to this discussion:
On page 310, we see this:

**********
"We shall prove that the complex numbers are algebraically closed." [the
fundamental theorem of algebra.] THIS WILL ILLUSTRATE ALMOST ALL THE
THEOREMS WE HAVE PROVED PREVIOUSLY. (capitals are mine).
...
...
Since R has characteristic 0, every finite extension is separable."
**********

The material earlier about separable field extensions and the like, and
also Galois theory, which is used heavily in this proof, are all presented
in very great generality, involving substantial uses of set theory.

QUESTIONS: Is Lang ****USING**** substantial set theory to prove this
theorem? Are the uses of universes McLarty quotes any different in
character?

>	Obviously, since we all agree the uses are eliminable
>in principle, they are not a foundational issue in Friedman's
>sense. That is fine with me.

What is unclear is whether the "uses" of universes are of a character that
they raise foundational issues at all - and what kind of foundational
issues? Certainly there is the important foundational issue of the
legitimacy of proofs using universes - in certain senses of "using". And
also, just legitimacy of universes themselves.

I then ask McLarty to tell us why and how large objects were ever injected
into the picture when one is seeking information about small objects -
i.e., what is gained by this injection. He then provides numerous
references, but NO INFORMATION. Can McLarty tell us something about this in
clear, understandable terms, on the FOM - in the simplest case? Avoid
jargon, or at least define the necessary jargon.