FOM: categorical pseudofoundations

[Harvey Friedman]

This is a response to McLarty, 11:27AM 2/2/98. Before I respond, let me
correct a confusing typo in my 3:01PM 1/31/98. I wrote

Nobody calls graph theory foundations of computer science,
yet it is the language in which almost (local) foundations of computer
science is cast - e.g., for circuits, networks, etcetera.

I meant to write

Nobody calls graph theory foundations of computer science,
yet it is the language in which almost all (local) foundations of computer
science is cast - e.g., for circuits, networks, etcetera.
*********************************

Also, I want to get into a detailed comparison with McLarty's
axiomatization. But before I do this, I would like a single clean correct
statement of his axiomatization, which includes his corrections to errors
in response to Tennant and Riis.
***********************************

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. This
is analogous to the universal instantiation rule which allows one to
substitute any (appropriate) term for a universal quantifier. These is
simply an application of first order classical predicate calculus with
equality, which is the accepted vehicle for presentation of exact thought
(although obviously in any presentation of exact thought additional issues
always appear that are particular to the subject at hand). 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 one reason - not the only
reason - that it remains so comparatively complicated and ad hoc looking as
f.o.m. But this in no way diminshes the usefulness of Cartesian closed
categories and topoi and the like for presentation of some important core
mathematics.

Of course, one can make the totally unnatural requirement that one use
predicate calculus without this rule of substitution, and force the axioms
of set theory into such a mold. One would still have a much simpler system.
But I don't know how to do this so that it meets the very high standards
that the systems with this rule of substitution meets. Therefore I chose
not to lower the standards for this purpose.

There is yet another reason why it is virtually compulsory to use this rule
of substitution for genuine f.o.m. Mathematicians freely use the separation
principle without hesitation, using any well defined mathematical property.
They don't stop to analyze the exact structure, and show how to derive that
instance of separation by means of any series of steps. I.e., they don't
stop and dissect it into projections and products and coproducts and
compositions, etcetera. It's just one step. In contrast, categorical
psudofoundations seems to want to make a big deal of how this can be
dissected into stages. This is very unnatural for f.o.m., but may well be
useful for other purposes.

By the way, there are important distinctions, from the point of view of
genuine f.o.m., to be made with regard to the formulas used in separation,
and these can be made clear to mathematicians, who can appreciate their
significance. I.e., whether the formula is arithmetical, or whether it has
quantification over uncountable domains, etcetera. Such distinctions and
their significance appear most naturally in set theoretic foundations.