FOM: proof theory and foundations

[Stephen G Simpson]

Colin McLarty writes:

 > Category theory uses proof theoretic considerations, for weak
 > fragments of first order logic (what we call "low in the
 > heirarchy") for various mathematical purposes. And a lot of us find
 > it interesting for foundations that so much of category theory
 > lives that low ....

This reminds me of a loose end left over from the earlier discussion
of category theory.  In advocating so-called "categorical foundations"
(i.e. topos theory plus sufficiently many additonal axioms to imitate
set-theoretic foundations), McLarty and Awodey had claimed as one of
its virtues etc. the fact that there is an elegant or convenient set
of axioms that are "essentially algebraic", i.e. equational with
partial functions.  Yet, as Friedman pointed out in 15 Mar 1998
06:41:02, the axioms given by McLarty here on the FOM list are not of
this form, in fact far from it.  So, in order to rationally evaluate
the claims of "categorical foundations", we need to see these
"essentially algebraic" axioms.  I know that Awodey and McLarty have
referenced a long paper by Freyd, but it would be valuable to see
these axioms spelled out from scratch in a relatively small space,
here on the FOM list.  I seem to recall that McLarty said he might
eventually get around to doing this.

I don't know whether this has anything to do with what McLarty is now
calling "low in the hierarchy".

-- Steve