FOM: categorical pseudofoundations: Friedman and Kanovei

[Colin McLarty]

reply to Friedman Mon, 2 Feb 1998 12:53:30

>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.

        That's a nice idea. Certainly it is not standard. 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.

        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."

        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. 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 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. 
 
>Set theoretic
>foundations and categorical pseudofoundations both use classical first
>order predicate calculus with equality as the underlying system; set
>theoretic foundations makes more powerful use of it, in a way that
>categorical pseudofoundations does not.

        This is well put, and the main thing I have gotten from this debate
is a better sense of why you value this so highly. It remains that I do not
find this use of predicate calculus the sine qua non of f.o.m. 



I will also reply to kanovei Mon, 2 Feb 98, but this is the last time I will
post a trivial proof in categorical set theory for someone who knows nothing
about the subject:

>Can someone present a consistent proof, 
>from the McLarty axioms 1 - 15, of the following theorem: 

>there is a real function which equals 0 on Q and 1 on R - Q 

Here is the proof: 

Q and R-Q are complementary subsets of R (this is the definition of R-Q). So
you can define a function f on R by defining it separately on R and R - Q
(this is the definition of "complementary"). So define f as have the
constant value 0 on Q and 1 on R - Q.