FOM: categorical pseudofoundations

[Harvey Friedman]

reply to McLary, 3:29PM 2/2/98.   I wrote:

>>The axiomatization I gave using axiom schemes uses only very few axioms -
>>not infinitely many. This is because an axiom scheme is a *single axiom* in
>>the appropriate form of predicate calculus which uses the obvious rule of
>>substitution. I.e., you replace a schematic letter with any formula.

You replied:
>
>        That's a nice idea. Certainly it is not standard.

Thanks for the praise. And thank you for sending your book to me.

People are fully aware of the difference between finitely many axiom
schemes and infinitely many axioms, even if they are r.e. Finitely many
axiom schemes mean finitely many ideas. The only reason I emphasized the
rule of substitution is that you suggested that it is relevant to the
comparison between the two axiomatizations.

>When people say
>(as Simpson did in his post of 11:01:31 today) that Peano arithmetic and
>Zermelo set theory are not finitely axiomatizable, they are assuming no use
>of these schematic letters.

I think they just meant this in the obvious technical sense, but knew full
well that it is not relevant to the present comparison.

>        Nor did you use schematic letters in your posted version of the
>axioms (in Fri, 23 Jan 1998 00:54:20). You gave a syntactic description of
>the formulas to be used: "Here phi(x) is any formula in the language in
>which y is not free."

I thought the matter was completely understood and recognized. I have known
of this way of looking at it - through substitution - for some time, since
this way of looking at it had some uses in other contexts.

>        To me, this use of schematic letters is quite nice, and makes your
>axioms more elegant than I had realized. It also shows that finding the
>"appropriate form of predicate calculus" (as you say above) is part of
>finding the axioms--and so, specifying that form of predicate calculus will
>have to be part of giving the axioms. By not specifying it, you led both me
>and Simpson to misunderstand your axioms.

Let's ask Steve if he misunderstood my axioms.

>It illustrates what Saunders Mac
>Lane has said: "Putting down axioms in a formal language is another way of
>making a mistake, not a way of avoiding mistakes".

I don't fully understand this quote. Please explain.

>        I suspect that my axioms, as posted, are briefer than yours would be
>along with a description of the logic. Certainly there will be no orders of
>magnitude difference either way.

I don't agree with this. You need the same underlying logic, although you
can get away without schematic letters. In any case, this underlying logic
counts for zero complexity. And you haven't addressed my point that you
can't do any ultimate foundation without schemes/schematic letters. I.e.,
in an appropriate sense, a finitely axiomatized version of VBC or ZC with
bounded separation isn't adequate since it doesn't reflect the way that
mathematicians use and think of separation, and this difference can be
expected to be crippling in sufficiently complicated uses of separation.

I was going to go into more detail with the comparison after you give us a
clean version in which you correct for Tennant and Riis, and cerify for us
that all of the bugs have been removed. In my opinion, there is an order of
magnitude difference on several different counts.