FOM: Alternatives to ZFC in actual use

[Colin McLarty]

Harvey Friedman wrote, on the use of Grothendieck universes in number theory:
 
>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.

        It is well known even to me how to avoid it. That is why I wrote:

>>Obviously all the steps can be filled in without universes, 

but I got in trouble for continuing: 

>>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.

        The combinatorial theorems are formally derivable in (ZFC plus the
consistency assertion). But you claim the consistency assertion is
unmotivated and unmathematical unless it is derived from existence of the
cardinals.

        Similarly Grothendieck knew that formal proofs were available
without using universes. But those formal proofs seemed to him unmotivated,
vast seas of technicality, lacking the clear mathematical motivation of his
method--and indeed those proofs were found precisely by eliminating the
universes from Grothendieck's methods. 

> When Grothendieck universes are - from what I
>gather - routinely removed, they are completely removed.

        This is a real difference. On the level of bare, formal provability,
your combinatorial theorems require the consistency assumption in addition
to ZFC. The Weil conjectures, for example, do not require consistency of
Grothendieck universes. The similarity is: just as you feel the consistency
assumptions only make sense when you derive them from existence of the
cardinals; so Grothendieck feels individual calculations of cohomology only
make sense in the general context of derived functor cohomology. 

Harvey wrote:

>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 strength depends on which toposes you mean, and what you mean by
"using". Quantifying over Grothendieck toposes is effectively the same thing
as using universes. You can use one or another Grothendieck topos,
quantifying over its objects just as you quantify over sets, without
committing yourself to any universe sized set.

        Grothendieck toposes are very much stronger than is needed--like
transfinite type theory with a type for each ordinal number. One goal of
elementary topos theory is to weaken this and still get the unified proofs
Grothendieck sought.

I wrote:

>>        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.

and Harvey replied:

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

        My phrase "forget rigor" should tip you off that this approach is
not formalizable. Ditto when I say it is "unconcerned with FOM". It simply
ignores real foundational problems. It is commonly used and it "works" for
the "working number theorist". But we should not confuse it with FOM.

Harvey wrote:

>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?

        Yes, I meant Mordell when I said Bieberbach.