FOM: Wiener's theorem; Grothendieck universes

Martin Davis martin at
Tue Apr 20 19:49:46 EDT 1999

At 07:02 PM 4/20/99 -0400, simpson at wrote:
> My impression is that the technology for
>eliminating Grothendieck universes is routine, simply a matter of
>cutting things down to size at appropriate places.  McLarty has
>exaggerated the difficulty of this.  There is no remotely similar
>routine procedure that will take you from Gelfand's soft proof to
>Wiener's original hard proof.  (However, the Shoenfield absoluteness
>theorem can be used to eliminate the use of AC from Gelfand's proof.)
No. But I believe there is a similar procedure that would directly (without
invoking Shoenfield) cut Gelfand's proof down by replacing the general
theorems using AC (ideal can be extended to maximal ideal & Hahn-Banach) by
the particular cases actually used, where (I conjecture) it can all be made

                           Martin Davis
                   Visiting Scholar UC Berkeley
                     Professor Emeritus, NYU
                         martin at
                         (Add 1 and get 0)

More information about the FOM mailing list