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

Re: Categorical Models of Linear (and other) logics



I've read with much interest the replies
to my question on the place of categorical
methods and models in logic.  The answers
(which ranged quite widely) certainly helped
me get the `feel' of current work.

There was an undercurrent in the replies
which was basic to the answers, but which
was never explicitly mentioned.  Yet I think
it's a crucial point which makes the entire
constructive/linear research programme distinct
from other approaches, and this is the focus
on proofs as first-rate objects in their own
right.  The whole "proofs as programs" 
paradigm requires a kind of modelling which
preserves information about proofs, and the
categorical perspective allows this --- in 
a way that other kinds of models (such as
algebras, like Heyting algebras, Dunn monoids, 
or frames, like Kripke structures or Routley-Meyer
models) don't.   

This is a *very* important difference between 
approaches.  For those of us who don't care 
about differences between proofs --- for 
whom logic is simply about what follows from 
what, and not how we *demonstrate*
what follows from what --- it is hard to see 
what the categorical approach adds to simple 
algebraic structures like Heyting algebras
and their substructural counterparts.  (If you
like you can see these as degenerate categories
in which there's only one arrow between a and b 
if there are any at all.)

I can see that the `proofs as important
objects' view is fine as far as the programming
approach goes.  But, what about other accounts
of logic?  Are there other paradigms of logical
investigation for which proofs are important 
objects?  

Sorry if this is all obvious for the rest of you,
for one coming from a different background (frames
and modal logics, and so on) this perspective 
takes some getting used to.

Thanks for any insight you might have,

Greg Restall

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Redemption rips through the surface | gar@arp.anu.edu.au  Automated Reasoning
of time in the cry of a tiny babe.  | Project, Australian National University
                 - Bruce Cockburn.  | Canberra, ACT 0200, Australia.
-=-=-=-=-=-=-=-=http://arp.anu.edu.au/arp/gar/gar.html-=-=-=-=-=-=-=-=-=-=-=-=