Categorical Models of Linear (and other) logics
I've read with interest the discussion of categorical models
of linear logics. I've wrapped my brain around the recent
results, and I've enjoyed it immensely. I do have a question
about categorical models, however, and I think that this
list is as good a place as any to have them answered.
My question is this.
* What are categorical models of logics good for?
Possible answers are as follows.
1. They help us understand our term assignment systems for
2. They help us prove results about our logics, as we can
use category theory.
3. We can show that our favourite logic corresponds to some
already-found structure in category theory, and hence, our
logic gets brownie-points for being `natural.'
4. The category (or class of categories) we are interested in
is the *intended model* for our logic. That is, we are using
our logic to model some phenomenon, which we have already
presented categorically. As we have shown that this category
(or class of categories) is a model of our logic, we thereby
show that our logic models nicely the phenomenon of interest.
Are any of these answers correct? If so, which of them?
Or are they missing the point? Are categorical models interesting
for some other reason?
I'd be very interested if there are any results like those
foreshadowed in answer `4' actually appear in the literature on
linear logic. The most I can find is answers in the ballpark
of 1, 2 and maybe 3.
Replies can be sent to the list, or to me. Either is fine.
Thanks a bundle,
Redemption rips through the surface | firstname.lastname@example.org Automated Reasoning
of time in the cry of a tiny babe. | Project, Australian National University
- Bruce Cockburn. | Canberra, ACT 0200, Australia.