[Prev][Next][Index][Thread]
a paper on *-autonomous categories and linear logic
Dear colleagues,
The following short paper
Coherence of the Double Involution on *-Autonomous Categories
by J.R.B. Cockett, M. Hasegawa and R.A.G. Seely
available from the authors' pages
http://www.kurims.kyoto-u.ac.jp/~hassei/papers/#STAR
http://www.math.mcgill.ca/rags/
might be of some interest for those woking on proof theory/type theory
and semantics of Linear Logic. It addresses the following "coherence"
question.
Many formulations of proof nets and sequent calculi for Classical
Linear Logic (CLL) take it for granted that a type A is "identical" to
its double negation A^{\bot\bot}. On the other hand, it has been
assumed that *-autonomous categories are the appropriate semantic
models of (the multiplicative fragment of) CLL. However, in general,
in a *-autonomous category an object A is only "canonically
isomorphic" to its double involution A^{**}. This raises the questions
whether *-autonomous categories do not, after all, provide an accurate
semantic model for these proof nets and whether there could be
semantically non-identical proofs (or morphisms), which must be
identified in any system which assumes a type is identical to its
double negation.
Fortunately, there is no such semantic gap: in this paper we provide a
"coherence theorem" for the double involution on *-autonomous
categories, which tells us that there is no difference between the
up-to-identity approach and the up-to-isomorphism approach, as far as
this double-negation problem is concerned. This remains true under the
presence of exponentials and/or additives. Our proof is fairly short
and simple, and we suspect that this is folklore among specialists,
though we are not aware of an explicit treatment of this issue in the
literature.
Best,
Robin Cockett
Masahito Hasegawa
Robert Seely