FOM: Friedman on schemes and anonymous critics

[Colin McLarty]

Harvey Friedman  Sun, 15 Mar 1998 wrote:

        About my posted first order axioms for categorical set theory:

>In fact, the axioms you wrote down are not only very clumsy in comparison
>to standard axioms for set theory, they also are unusable as formal f.o.m.
>For example, as I have said on the fom, I do not believe that one can
>actually conveniently formalize mathematics in any formal system without
>schemes. This is because mathematicians routinely use mere expressibility
>(by wffs) as a sufficient criterion for object formation (i.e., forms of
>comprehension), and do not carefully break up the relevant wffs into their
>componenents and successively build up terms or introduce symbols by
>definition for the components. This feature of the formalization of
>mathematics is well known to people who actually do formalization of
>mathematics - e.g., the Mizar people.

        This is interesting to me, and I don't know much about it. Randall
Holmes also wrote in to agree on the need for schemes. Is convenience of
application an aspect of simplicity of axioms?   
 


        Among the open problems I gave in categorical foundations was one
involving current problems in (co-)homology theories.

>Appears not to be a problem in global f.o.m., but a much more specialized
>matter. I'll look into this, starting with writing to my colleagues here to
>see what they have to say. By the way, your remarks a long time ago on the
>fom about justifying categorical foundations via Wiles' proof of FLT was
>received by several people here as bullship. The impression was that you
>piggyback on some fashionable avenues in core mathematics where categorical
>foundations is a minor side issue.

        I wonder what you said about me to these people, and more exactly
how they responsed. Could we even know who they are?

        Neither I nor the search engine on the FOM archives recall me using
Wiles's proof to justify categorical foundations. On 11 Nov 1997 I said
Wiles's proof is more popular today than fom. On 25 Nov 1997 I said one
long-term project in categorical fom is to see how far we can simplify
Grothendieck's work and other that grew from it (which would certainly
include the Langland's program, and so Wiles's proof). And on 22 Jan 1998 I
mentioned that category *theory* is indispensible to all those proofs. The
context was specifically practice and not fom. 

Colin