FOM: set/cat "foundations"

[Vaughan Pratt]

From: Till Mossakowski 1:53PM 2/26/98.
>Perhaps a problem of categorical foundations is that the meta-theory
>of first-order logic is naive set theory. For categorical foundations,
>one might need a more category-based formalism, like sketches
>(but sketches themselves are definitely too weak). Hopefully, such a
>formalism would make Lawvere's axioms more concise.

From: Harvey Friedman Thu, 26 Feb 1998 16:09:44 +0100
>You may well be putting your finger on an important aspect of what is
>missing, and what needs to be done to make categorical foundations a
>reality. I should add that I don't fully understand exactly what you are
>saying here. What is a sketch?

A sketch is the categorical counterpart of a first-order theory.
It specifies the language of the theory in terms of limits and colimits
of diagrams.  The language of (finitary) quantifier-free logic is
representable entirely with finite product (FP) sketches, i.e. no colimits
and only discrete limits.  FL sketches allow all limits, e.g. pullbacks
which come in handy if you want to axiomatize composition of morphisms
as a total operation (not possible with ordinary first order logic or
FP sketches).

Colimits extend the expressive power of sketches in much the same way
that least-fixpoint operators extend the expressive power of first order
logic (made precise by a very nice theorem of Adamek and Rosicky), but
completely dually to limits.  (Fixpoint operators are not obviously dual
to anything in first order logic.)

The machinery of sketches is either appealingly economical and elegant
or repulsively complex and daunting depending on whether you look at it
from the perspective of category theory or set theory.

As a formalism for categorical foundations sketches have the same
weakness as Colin's axiomatization of categories: they are based
on ordinary categories, with no 2-cells.  (Again let me stress the
importance of 2-categories, i.e. not just line segments but surface
patches, for foundations.)  On the one hand I'm sure this is not an
intrinsic limitation of sketches, on the other I don't know what's been
done along those lines to date.  Higher-dimensional sketches are surely
well worth pursuing.

Vaughan Pratt