Subject: categories: correction

From: Paul Taylor <[email-masked]>
Date: Sun, 15 Feb 1998 18:05:35 GMT

> My motication (in 1987 this was)
This should have been 1984 (and motivation).

I'd also like to add:

I had some difficulty in getting my ideas about stable coequalisers
across (partly, of course, my fault, because I didn't get the rigt
answer, involving stable transitive closures, until 1993).  People
said, "while programs can't possibly be described by finitary first
order theories, because the theory of the natural numbers is an
example".

I knew that, and it wasn't what I meant.  This illustrates a subtlely
in first order categorical logic: that the relevant structure consists
of *less* than all finite (limits and) stable disjoint colimits. The
categorical structure corresponding to first order logic is a (Heyting)
pretopos, which need not have coequalisers of arbitrary parallel pairs.
For example, the category of compact Hausdorff spaces is a pretopos but
does not have all stable coequalisers. (I have a feeling I haven't
got this quite right, and Peter Freyd is going to jump on me. I shouldn't
be so foolish as to answer mathematical questions on the modem from home!)

More recently, Jiri Rosicky and Peter Johnstone have considered the
question of what theories can be expressed with finite sketches.
As Peter Freyd showed in 1972, this includes the natural numbers.
My results and those of Jiri and Peter are more complicated forms of
Peter Freyd's original observation.

Finally, since my more recent work on categorical recursion, I no
longer think that a coequaliser diagram is the best way of presenting
a WHILE program categorically (though the diagram I would use now
expresses the same logical content).

Paul