Re: sketch theory

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

Dear John,

Barr & Wells "Toposes, Triples and Theories", Section 4.4, give some
examples of LE-sketches (= finite limit sketches) that includes sketches
for the theories of finite limit categories and of elementary toposes.
They don't include CCCs, but you should at least get the idea. The basic
trick (corresponding to the logical one of Freyd's "essentially
algebraic" theories) is to think of these theories as being given
algebraically with some of the operators (e.g. composition, pairing)
being partial and with domain of definition described by equations. You
then introduce those domains of definitions as nodes in the sketch, with
arrows, diagrams and cones constraining them to be finite limits in a
way that corresponds to the equations.

Incidentally, Palmgren and I recently came up with a new logical
characterization of finite limit theories, using a logic of partial
terms. It leads to a neat proof of the initial model theorem. However, I
also believe there is a specific but non-obvious advantage of sketches
over logical syntax in that sketches do not rely on having canonical
finite limits. Suppose a sketch has two distinct nodes a and b, and
manages to constrain them both to be finite limits of the same diagram.
In a model, a and b can be interpreted as different objects (though, of
course, they have to be isomorphic).

Regards,

Steve Vickers.

John Baez wrote:
> Dear Categorists -
>
> Andrei Rodin pointed out this paper by Charles Wells:
>
> http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
>
> I took a look.  In section 4.1 it mentions that people have given a finite
> limits sketch for cartesian closed categories.  I'm curious about how this
> works,  Unfortunately the list of references given here is quite long.  Can
> anyone help me find a reference on a sketch for CCC's?
>
> Best,
> jb
>
>