[Prev][Next][Index][Thread]

Re: Categorical Models of Linear (and other) logics


>>>>> "Greg" == Greg Restall <Greg.Restall@cisr.anu.edu.au> writes:

    Greg> * What are categorical models of logics good for?

    Greg> Possible answers are as follows.

    Greg> 1. They help us understand our term assignment systems for
    Greg> these logics.

    Greg> 2. They help us prove results about our logics, as we can
    Greg> use category theory.

    Greg> 3. We can show that our favourite logic corresponds to some
    Greg> already-found structure in category theory, and hence, our
    Greg> logic gets brownie-points for being `natural.'

    Greg> 4. The category (or class of categories) we are interested
    Greg> in is the *intended model* for our logic.  That is, we are
    Greg> using our logic to model some phenomenon, which we have
    Greg> already presented categorically.  As we have shown that this
    Greg> category (or class of categories) is a model of our logic,
    Greg> we thereby show that our logic models nicely the phenomenon
    Greg> of interest.

    Greg> Are any of these answers correct?  If so, which of them?  Or
    Greg> are they missing the point?  Are categorical models
    Greg> interesting for some other reason?

Coming from type theory I'd maybe emphasize things differently. I
think categorical models can help you very much when you present a
logic and when you are considering extensions. Category theory gives
you a very concise language to talk about features of a logic in
particular when you want to consider the structure of proof objects
(i.e. it is the natural language for abstract proof theory).

Sometimes this conciseness can be essential to find a proof (this
relates to point 2). A nice example in my area is Hofmann's and
Streicher's proof for the non-provability of the uniqueness of
identity proofs in Martin-L"of's type theory. The question is very
elementary: Can we construct a proof object in intensional type theory
with an equality type (and Martin L"of's standard elimination constant
eq-peel) which proves that any two proofs of an equality are
themselves equal. When one first looks at this problem it seems that
the solution should be trivial but then one seems to be running
against a wall. Naturally, in this situation one starts to try to
prove the converse, i.e. one is looking for a model which refutes
uniqueness. Alas, all the standard models have this property (we can
even show this formally if we define standard model in a certain
way). So the problem we were faced with was to construct a
non-standard model with a certain property. The solution is very easy
to express in categorical terms: the category of groupoids
(i.e. categories where every morphims is an iso) gives rise to the
model we are looking for. Intuitively the idea is clear, we replace
sets by groupoids and equality by isomorphism. Now, since isos are not
necessarily unique we can show that this construction can be used to
refute the uniqueness property. Here a categorical model is the
natural way to express the solution to a problem which can be stated
w.o. any reference to categories.

-- 
Thorsten Altenkirch	(alti@cs.chalmers.se)
Computer Science, Chalmers University of Technology, Sweden
DISCLAIMER: All opinions expressed here are my own.
WWW URL: http://www.cs.chalmers.se/~alti