FOM: Categorical "foundations"?

[Vaughan Pratt]

From: Harvey Friedman <friedman at math.ohio-state.edu>

>Let us say that we instead start with the continuum as Pratt suggests.
>Where do I go from here in a philosophically careful way? Don't get me
>wrong. I think this may be fruitful, but I don't see topoi in it.

Just to remind people, I said that the geometric interpretation
of category starts from its underlying graph as the expression of
connectedness (what computer scientists are referring to when they talk
of the "topology of a network") and adds subdivisibility of edges in
terms of composition.  (You can look at it synthetically if you prefer,
using composition to build bigger edges from smaller deterministically;
the advantage I see of the analytic view is that it starts from a
single morphism and carves it up nondeterministically, i.e. cutting it
at various places, a familiar intuition.)

As Colin has said, one can go in various directions starting from the
unadorned notion of category.  My favorite direction is closed categories
in general.  I am not particularly fond of toposes because most of what
I want to do that would require a topos setting is better founded on sets.

In this viewpoint the dual of anything is nearby, whence complete atomic
Boolean algebras as dual to sets are also better treated in set theory
(with general Boolean algebras however it is not so clearcut).  Abelian
groups on the other hand, especially topological ones, are better handled
in a category-theoretic setting, otherwise you miss out on the most
important parts of the Abelian group picture.  This is where category
theory was born; toposes evolved only out of the reluctance of Bill
Lawvere and others to switch from composition-based to membership-based
foundations when working with sets, on the ground that categories provide
the best foundation bar none.

This is not to deny the usefulness of toposes in some situations.  A very
nice example is Mike Barr's topos-theoretic treatment of fuzzy logic.
A central problem for fuzzy logic is that fuzziness itself seems not to be
a fuzzy notion: the value of membership in a real set is a precisely given
real.  Mike fixes this by making predicates on membership values equally
fuzzy, accomplished by taking \Omega to be the unit real interval [0,1].
Because a topos is closed, this means that all predicates, both basic
and higher order, are referred to \Omega making them all equally fuzzy.

As a counterchallenge to Harvey I would ask him whether there exists
a comparably slick way in ZFC of making all predicates at all types
equally fuzzy for any a priori given degree of fuzziness.  (There is
nothing particularly magic about the continuum [0,1]; three degrees of
fuzzy membership, {0,1,2}, would do just as well for this purpose.)

The point here is that although some problems in logic are better treated
with sets, others especially those involving higher order nonclassical
logic seem to go more smoothly with categories.  (Note that I said logic
here; I don't think there is any disagreement that some other topics
such as homology definitely go better with categories.)

As a point of calibration let me describe how far it is from categories
to toposes.  First one requires cartesian closedness, namely that there
is a specified final object 1 and specified binary product operation
(functor) meeting certain coherence criteria, and that the binary
operation has a right adjoint (constructive Galois connection) in each
argument, providing exponentiation (or implication) X^Y.  What this
means is that the maps from XxY to Z are in a specified bijection with
those from X to Z^Y (and hence with those from Y to Z^X by the symmetry
(commutativity) of XxY).  It is at this stage that each object acquires
the ability to test equality of its elements (maps from 1).

Second one requires a subobject classifier \Omega having a distinguished
element (map from 1) called *true*.  \Omega is the intuitionistic
counterpart of 2 in the common notation 2^X for the power set of X.
This is where the notion of characteristic function of a subset of X
appears, namely as any morphism from X to \Omega.

In any cartesian closed category with such a subobject classifier,
every characteristic function automatically determines a subobject of X
(an isomorphism class of monics to X, a notion that is prior to that of
cartesian closedness), but the converse need not hold.  The defining
characteristic of a topos is the axiom that for any object X its
subobjects and its characteristic functions are in bijection.

For example in the category Set of sets (which emerges as structure on
the ZF universe the instant you have defined composition of functions,
long before anyone has even mentioned the notion of category), a subobject
of a set X is the equivalence class of all functions to X whose image is
a given subset X' of X, while the characteristic function of X' is the
evident function from X to {0,1}.  It is obvious from this description
that in Set, subobjects and characteristic functions are in bijection.

Once you have arrived in topos land and corrected for the toposy-turvy
view of everything, whatever else you feel like adding to better
approximate ZFC is relatively easily understood since by this stage
the the situation when viewed in the appropriate mirror is now fairly
set like.

One might suppose that after all this work to transport category
theorists to the land of set theory, one might be in a very remote and
special corner of the categorical universe, far from one's place of birth,
abelian categories, the foundation today for the application of categories
in homological algebra etc.  The remarkable fact however, observed only
months ago by Peter Freyd after a few days of reflection on a question I
posed to the category mailing list about the possibility of such a fact,
is that the defining structure of toposes and that of abelian categories
are identical up to the question of the relationship between 0 and 1
(initial and final object, false and true if you like).

Call models of this common theory AT (abelian-topos) categories.  In an
AT category, false implies true, i.e. there is a (necessarily unique)
arrow from 0 to 1.  Freyd shows that every AT category is the product of
an abelian category and a topos.  An AT category is an abelian category
when its topos component is degenerate (the singleton category), and
a topos when its abelian component is degenerate.  A quick test for
each is to look at 0: if Ax0 ~ 0 (0 is an annihilator with respect to
product) then it is a topos, while if there exists a map from 1 to 0
(also necessarily unique, and necessarily making 0 and 1 isomorphic)
then it is an abelian category.

This may help explain why category theorists find themselves so at home
with toposes: they haven't really been transported to a remote hostile
land, they have merely given up their previously cherished zero object
(simultaneously initial and final) that pervades homology, group theory,
etc. in favor of 0 as an annihilating initial object and 1 as a final
object (which if 0 would make everything collapse since Ax1 ~ A whence
A ~ 0 for all A).

For me, insights of this sort qualify as foundational.

Vaughan Pratt