FOM: Re: wrap on universes

[Colin McLarty]

reply to Friedman Fri, 16 Apr 1999 18:11:43

This also addresses Martin Davis's post.

Friedman:
>As far as the statement about Grothendieck: in my second "grand conjecture"
>I conjectured that these "uses" of universes are fake in the sense that
>they can be eliminated by restriction. Now elimination by restriction is
>going to result in perfectly mathematically meaningful assertions. For
>instance, eliminating
>
>every field has an algebraic closure
>
>in favor of
>
>every countable field has a countable algebraic closure
>
>is perfectly mathematically meaningful in any normal sense of the word.

        I hve already shown how to avoid "universes" of inaccessible rank.
You can formalize the Grothendieck style proofs quite directly using a
"universe" V(w+w). This still leaves you infinitely higher in rank than is
formally required for, say, Wiles's theorem. 

        The way practitioners eliminate universes, in principle, in favor of
very small data is not by restriction. Rather you replace all mention of
instances by referring directly to the data that make them up.

        It is as if an algebraic number theorist were to eliminate

every field has an algebraic closure

by avoiding mention of fields or any sets of rationals, and using a
metatheorem instead:

Let a0...an be any n+1 rational numbers, then the following is provable
        "there is a rational y such that (an.y^n)+.....+a0 = 0"

        This is also routinely possible. But if you tried to actually
rewrite Hecke ALGEBRAIC NUMBERS this way, you would either just copy the
usual treatment while insisting it is all "metatheorems", or else you would
make it humanly incomprehensible.