FOM: finite axiomatizability; categorical dis-foundations

[Colin McLarty]

Reply to simpson at math.psu.edu (Stephen G Simpson)
    
>    McLarty
>    wants to make something of the fact that the ZF includes an infinite
>    axiom scheme, replacement, but in my opinion the replacement scheme is
>    perfectly natural and doesn't seriously compromise understandability
>    or readability.


        I didn't make up the challenge, I only met it. Friedman "challenged"
me to axiomatize a topos suitable for classical analysis as simply as he did
ZF. You repeated it. When Awodey asked you what you meant by "simple" you
said in your post of Mon, 26 Jan 1998 12:15:34:

>If you insist on a precisely defined measure of simplicity, well, OK,
>as a first approximation let's take "number of bytes".  We can refine
>this later, but note that this crude measure is already interesting.
>If it turns out that the fully formal topos axioms have 50 times as
>many bytes as the fully formal set theory axioms, don't you think that
>would be interesting?

        Friedman's axioms, in fully formal statement, require infinitely
many bytes, and mine finitely many. If you no longer find this measure
interesting, I won't argue. What was the challenge about? 

    
>    The real question for proponents of "categorical foundations" is, what
>    do the topos axioms mean?  What picture do they refer to?  Is there an
>    underlying foundational conception?

        I entirely agree with this--only adding one letter. Where you have
"picture", I would have "pictures". It seems to me that our arguments have
all been aired. If you have further challenges I will consider them, though
I don't promise to shape all my work around your misgivings on categorical
foundations. 

Colin