FOM: Kreisel on categories

[Vaughan R. Pratt]

>From: Torkel Franzen <torkel at sm.luth.se>
>
>It's probably not the passage you have in mind, but there is a comment
>in a similar spirit in "Proof theory: a personal report":
>
>        For example, some mathematicians espouse category theory
>        as a new, purely mathematical foundational scheme. But what
>        has been done is to take relatively sophisticated
>        structural notions (category, functor) defined (informally)
>        in terms of ordinary unstructured mathematical notions
>        (class, function) and attempt to kick away the traces -
>        'explaining' the latter in terms of the former. Whatever
>        the organizational power of category theory in different
>        parts of mathematics, this attempt at foundations is an
>        exercise in self-deception.

It would be interesting to have the reaction of category theorists to
this passage.  (I'm not a category theorist myself, though I've been
including increasingly hefty doses of Lawvere theories, n-categories,
monads, and categorical logic in my algebraic logic course within the
past ten years.)

I have a couple of problems with the above reasoning, the greater of
which can be illustrated with the following story.

The star ship Enterprise encounters an alien ship and befriends its
crew.  As often happens with such encounters the aliens speak good
English, but Data discovers that he cannot discuss mathematics with his
counterpart Rydzkyl.  The two go at it for ages.  The first to get the
hang of the other's mathematics happens to be Rydzkyl, who now finds
that he can explain his mathematics to Data by translating it into
Data's terms.  Data sighs with relief, then says "Rydzkyl, the only
reason your mathematics seems so complicated is that at bottom it is
based on the same foundations I use, but you won't admit it!"

The lesser problem has to do with whether the sequence
category-functor-natural transformation is "relatively sophisticated"
compared with class and function.  While this is true when starting
from sets, geometric foundations reverse the order of sophistication.
Categories, functors, and natural transformations are the fundamental
entities of geometric foundations, being its vertices, edges, and faces
respectively.  "Set" and "function" are relatively sophisticated
notions.

Regrettably I can't point to any generally accepted 2-categorical
axiomatization of category theory, although geometry and category
theory do feed into each other very strongly.  But the very simple
geometry of n-cells would provide an ideal geometric foundation that
should be just as convincing to category theorists as the discreteness
of sets is as a foundation for set theorists.  Category theorists
simply do not think like set theorists (which makes conversations with
them about set theory baffling and frustration).

The underlying reason for the wide gap between set theorists and
category theorists is that the two subjects are essentially opposites.
Set theory is based on the principle of separation, category theory is
based on the principle of connection.

Connection and separation are independent entities.  Characterizing
connection as absence of separation does not define connection, it is
merely a way of understanding the connection concept in separation
terms, and likewise for the other direction.

This is very clear when you look inside a computer, which contains two
entirely distinct forms of logic, the logic of bits as separation
(maintain the distinction between 0 and 1), and the logic of wiring
topology as connection.  Bits are not all the absence of wire, indeed
wire carries bits, and by the same token wire is not the absence of
bits.

Boolean logic is the logic of separation, linear logic is the logic of
connection.  This is why linear logic makes perfect sense to category
theorists and relatively little sense to set theorists.

Brouwer attempted to develop the connective or continuum aspect of
geometry at a time when mathematics was in the process of embracing the
set concept as more fundamental than geometry.  Tertium non datur
expresses discreteness of sets, whereas the continuum to Brouwer was
connected and could not be cut so cleanly.  (This is reflected in the
standard topology on the reals, which cannot be cut symmetrically, one
side must be open and the other closed.)  From this perspective it is
hard to imagine Brouwer accepting Heyting algebras as a formalization
of the connectedness of the continuum.  Intuitionistic logic only
rejects the absence of the tertium, it does not assert its existence.
The continuum is the tertium.

I'd love to see Colin McLarty's paper "Axiomatizing a Category of
Categories" (JSL 56:4 1243-1260) reworked with geometry as the basis.

Vaughan