FOM: Wiener's theorem; Grothendieck universes

[Martin Davis]

At 07:02 PM 4/20/99 -0400, simpson at math.psu.edu 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
explicit.



                           Martin Davis
                   Visiting Scholar UC Berkeley
                     Professor Emeritus, NYU
                         martin at eipye.com
                         (Add 1 and get 0)
                       http://www.eipye.com