FOM: categorical dys-foundations

[Stephen G Simpson]

Responding to Harvey's observation that a comprehensive "categorical
foundations" doesn't exist, Vaughan Pratt writes:
 > This claim, frequently made on FOM, reflects not so much on the coherence
 > of categorical foundations as on the technical narrowness of those making
 > the claim.

Vaughan, I'm surprised at you.  The FOM list is no place for
insubstantial attacks based on "technical narrowness" or other alleged
educational deficiencies.  Perhaps you think that Harvey and I are
overlooking some relevant facts.  If that's what you think, please ask
someone to call the relevant facts to our attention and to explain
coherently why they are relevant.

Concerning the issue of "technical narrowness", Harvey has actually
published some important papers on closely related topics such as
realizability and intuitionistic set theory.  I haven't published
anything on these topics, but I've slogged my way through a fair
amount of categorical literature, including several of the topos books
that you mentioned.  I appreciate these books, but my considered
opinion is that they fall far short of being f.o.m.  I'm sorry that
this bothers you, but there it is.

Here on the FOM list, Harvey and I have repeatedly challenged the
advocates of "categorical foundations" to explain themselves.  The
challenge has not been met.  The attempts to meet it have dissolved
into incoherence.  McLarty's wild claims about real analysis and topos
theory have been examined rather thoroughly and found wanting.  You
yourself have attempted to explain "categorical foundations" in terms
of a picture of morphisms as directed line segments or something like
that, but even your category-theoretic colleagues don't seem to have a
clue as to what you are talking about or how your picture might
contribute to f.o.m.

 > What is your criterion for "comprehensive"? 

I'm not prepared right now to draw up a list of criteria for a
comprehensive f.o.m.  However, one necessary condition would certainly
be a demonstrated ability to coherently explain real analysis and
other core mathematics in terms of underlying foundational concepts.
Since category theory doesn't do this, it can't be called f.o.m.
Moreover, categories are always defined in terms of sets, so sets are
more fundamental.

 > If a comprehensive bibliography whose books tell essentially the
 > same story doesn't meet it

Any good library contains long lists of books on many topics,
e.g. algebraic K-theory, or perhaps the sex life of butterflies.  This
doesn't mean that any of these topics constitute f.o.m.

 > then I would suggest that either your criterion is set unreasonably
 > high

The standards of what constitutes genuine f.o.m. are indeed very high.
But they are not unreasonably high.  High standards are necessary, in
order to protect genuine f.o.m. against envious attackers, such as the
"list 2" crowd.  In the present state of knowledge, category theory
qua f.o.m. just doesn't cut it.  I'm not saying that category theory
could never cut it, but right now it has a very long way to go and it
may never get there.

 > or you are grossly underestimating the coherence, technical depth,
 > and overall mathematical quality of the picture jointly painted by
 > this literature.

I'm not underestimating it.  Many mathematicians denigrate category
theory as "general nonsense".  I don't agree with that opinion.  I
think that category theory has its uses in specialized branches of
mathematics such as algebraic topology and algebraic geometry.  On the
other hand, I'm not an expert in algebraic topology and algebraic
geometry, so I leave it to those experts to judge.

 > This is serious work, which you do a serious injustice in
 > dismissing so casually.

I'm not dismissing it, casually or otherwise.  I'm sure that the books
you mentioned are all very serious and well-meaning.  I view them as
expounding some interesting technical relationships between certain
aspects of category theory and certain aspects of mathematical logic.
The only point about category theory that I have tried to make here on
the FOM list is that topos theory isn't f.o.m.

-- Steve