FOM: the attack on Cat

[Steve Awodey]

Dear fom readers:

Recently a few people have indicated that they are growing tired of the
category theory debate; and I'm sure that many others are, as am I.  So I'd
like to call general attention to the fact that I and the other category
theorists posting to this list are not involved in an even-handed  Set vs.
Cat debate over which system provides the "best" or "correct" foundations -
along the lines of the old "three-schools of foundations" debate.
        Rather, I think I can speak for the other "Cat" participants, that
we are responding to what seems a rather ill-willed, public attack on our
discipline by a few people with very little knowledge of it and very strong
opinions.  For the most part, our goal has been to defend the field by
attempting to explain the methods and motivation of category and topos
theory - and certainly not to obscure the issues or to challenge the
utility or significance of any other methods, or anyone's research.  The
"other side", by contrast, appears bent on discrediting the legitimate use
of category theory in foundations - for what reasons I cannot begin to
image.
        I consider a public attack of this kind both unprofessional and
unscholarly.  I hope those who tire of the debate will appreciate that I
(and the other young logicians posting on the "Cat" side) can hardly afford
not to defend the field against what appears to be simply irresponsible
slander.

Steve Awodey
Philosophy
CMU

P.s.: In response to Steve Simpson's most recent posting:

>
>Date: Sat, 31 Jan 1998 16:04:27 -0500 (EST)
>From: Stephen G Simpson <simpson at math.psu.edu>
>Subject: FOM: IHOL vs topos; Boolean algebra vs Boolean ring; topos challenges
>
...
>
>What does "isomorphism" have to do with it?  Is Awodey now saying that
>IHOL is "isomorphic" to topos theory (in some unspecified sense)?
>

The precise sense was specified by Butz in the posting of 29 Jan 1998
15:09:36, to which I referred.  The details, as Butz mentioned, are easily
accessible in the book by Lambek & Scott, and elsewhere - a good deal of
logic-related topos research in the '70s was along these lines.
        Here's a brief explanation: Avoiding technicalities that play no
role here, the relevant notion may be described as "isomorphism up to
isomorphism".  The standard, category theoretic notion is equivalence of
categories.  In the example under discussion here, it means that if you
start with a theory  T  in IHOL and take the topos  E(T)  it generates,
then take the theory  T(E(T))  associated to that topos, the result will be
"the same" theory as  T , _up_to_ the kind of syntactical
intertranslatabilty which obtains between the theories of boolean algebras
and boolean rings.  (I would regard this as a syntactic isomorphism.)  The
composite operation E(T(-)) has an analogous property.
        The point is that it's not just a matter of having some
translations going each way, as Simpson thought, but that these are
mutually inverse in this "up to isomorphism" sense.  This is the basis of
the claim -  made not only by me, but by a chorus of topos theorists on
this list (and plenty of publicly available research) - that topos theory
is "equivalent" to IHOL, in a strong and rigorous sense of "equivalent"
that is not worth quibbling over.
        It's also not worth quibbling over what exactly is meant by IHOL -
this can be found in the references already cited, and there's nothing
sneaky going on.  It's a perfectly standard notion of intuitionistic,
higher-order logic.
        Such remarks as:

>Awodey is relying on Carsten Butz's posting of 29 Jan 1998 15:09:36,
>in which Butz partially explained the nature of some alleged
>translations between IHOL and topos.  Note however that Butz and
>Awodey haven't explained exactly what they mean by IHOL.  I expect
>that, if pressed, they would define IHOL in a way that would be in
>some sense equivalent to topos.

are simply outragious.

Motivation:

As for the question of motivation, I for one am happy to invoke the
inference that Simpson recently "suggested":  If X is equivalent Y, and X
is well-motivated fom, then so is Y.  Here using the notion of
"equivalence" that was just considered.  By "well-motivated fom" I don't
mean that it's the only possible fom, but only that it doesn't warrant the
kind of attack that's been launched against topos theory here.
        However, we need not rely on this inference via"equivalence" to
show that topos theory has logical motivations of just this sort - for
Lawvere's early papers on the subject (including the pretopos
"hyperdoctrine" ones) show that part of the motivation for the orginal
definition of an "elementay topos" was this very IHOL logical
interpretation of the axioms.  So the equivalence between topos theory and
IHOL is really a result of Lawvere's skill at axiomatics, and not a mere
accidental connection, as it were.  This in response to the outragiously
irresponsible remark:

>Similarly, topos theory was invented by algebraists for their own
>purposes.  One of the purposes was to subsume set theory under
>category theory, via a slavish translation.  The translation
>accomplishes nothing, except to enable algebraists to talk about
>"categorical foundations", while obliterating the f.o.m. motivation
>that underlies set theory.

...

>
>I'm glad that McLarty (30 Jan 1998 12:46:45) has answered the first of
>my three topos challenges (24 Jan 1998 20:16:05), by posting a fully
>formal definition of topos.  It's 1868 bytes long and uses 13
>primitives, compared to 299 bytes and three primitives for finite set
>theory.  I'm pleasantly surprised!  Another comparison: 2437 bytes and
>13 primitives for topos with extra axioms, versus 646 bytes and one
>primitive for ZFC.  Does Awodey want to discuss other measures of
>simplicity?
>

        I remind you that my main question was "What is such a comparison
supposed to demonstrate?".   Moreover, I've already mentioned one measure
of simplicty that I consider significant, and under which the topos axioms
are notably simpler than those for ZFC.  Another measure - less significant
to my mind - is simple cardinality.