FOM: Alternatives to ZFC in actual use

[Harvey Friedman]

McLarty 1:47PMs 4/2/99 writes:

>Joe Shipman wrote:
>
>>Here is my question: was any statement of ordinary mathematics (that is,
>>a statement about sets of rank less than omega+omega) ever proved from
>>Grothendieck Universes, in which the Universe assumption was really
>>used?
>
>        Short answer: yes, the Weil conjectures, Faltings's work (including
>the proof of the Bieberbach conjecture), Wiles's theorem--pretty much
>anything that uses derived functor cohomologies.

I was interested in this issue some time ago and asked around. I was given
to undertand that the use of Grothendieck Universes is mere convenience,
and it is well known to experts how to completely avoid this.

In short, my impression has been that the Universes are not really used.
It's just convenient hot air.

Incidentally, the Bierbach conjecture was first proved by Debranges
(speeling may be incorrect) by classical methods, where no issue of
Universes appears. Are you talking about another proof by Faltings?

>        Longer answer: proofs like these are not given from the ground up.
>For example Deligne published his proof of the last Weil conjecture in a 34
>page article (in 1973) which relies heavily on Grothendieck's Seminaire de
>Geometrie Algebrique du Bois Marie--where Grothendieck used his universes.
>Obviously all the steps can be filled in without universes, just as Harvey's
>recent combinatoric theorems can be proved without using subtle cardinals
>(only assuming their consistency with ZFC).

This is the most eggregiously misleading statement I have seen made on the
FOM! When I prove these combinatorial theorems using the consistency of
large cardinals, this is regarded as a necessary use of large cardinals
that cannot be removed. When Grothendieck universes are - from what I
gather - routinely removed, they are completely removed.

Your statement indicates to me that you may not have the slightest idea of
what I am up to.

>Three years later Deligne
>published a book showing how to actually circumvent toposes in his proof,
>and thus avoid SOME appeals to Grothendieck universes. That is Deligne's SGA
>4 1/2 (Springer Lecture Notes in Math no.569) and its bibliography gives
>references to everything I've mentioned. Has anyone checked how the whole
>proof would look in ZFC without universes? I doubt it.

There is a big difference between just using topoi and using universes. But
of course, even just using full topoi is already very strong - like type
theory. However, again I have been told that the use of toposes in these
things is very weak - only part of toposes are used. Presumably the
fragments of topoi that were ever used were very very weak.

>        The more common way to avoid Grothendieck universes in this part of
>number theory is to forget rigor. See for example _Introduction to Etale
>cohomology_, Gunter Tamme (Springer-Verlag, c1994). A very nice book on its
>subject but unconcerned with FOM. It simply ignores the difference between
>sets and proper classes and assures the reader (quite correctly in practice)
>that this will not lead to any trouble.

>From what you write, I cannot tell what system this approach is formalizable in.

I am going to try to get an expert in this area to coment for the FOM.