We wish to announce the following paper made available for ftp on our
WWW site.
Theory and Applications of Categories, Vol. 3, 1997, No. 5, pp. 85-131
Proof theory for full intuitionistic linear logic,
bilinear logic, and mix categories
by
J.R.B. Cockett and R.A.G. Seely
ABSTRACT
This note applies techniques we have developed to study coherence in
monoidal categories with two tensors, corresponding to the tensor-par
fragment of linear logic, to several new situations, including Hyland and
de Paiva's Full Intuitionistic Linear Logic (FILL), and Lambek's Bilinear
Logic (BILL). Note that the latter is a noncommutative logic; we also
consider the noncommutative version of FILL. The essential difference
between FILL and BILL lies in requiring that a certain tensorial strength
be an isomorphism. In any FILL category, it is possible to isolate a full
subcategory of objects (the ``nucleus'') for which this transformation is
an isomorphism. In addition, we define and study the appropriate
categorical structure underlying the MIX rule. For all these structures,
we do not restrict consideration to the ``pure'' logic as we allow
non-logical axioms. We define the appropriate notion of proof nets for
these logics, and use them to describe coherence results for the
corresponding categorical structures.
Theory and Applications of Categories, Vol. 3, 1997, No. 5, 85-131
http://www.tac.mta.ca/tac/
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1997/n5/n5.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1997/n5/n5.ps
We would draw your attention to the following "highlights":
- we develop proof nets for FILL (as well as bilinear logic - but this
latter is shown equivalent to the system of non-commutative *-autonomous
categories we studied in an earlier paper
[BCST],
so that is not new).
- our proof nets seem very like the "naive" sequent calculus that
Schellinx has shown does not admit cut elimination; we analyze the
apparent "paradox" in claiming a normalization result for this system of
proof nets, and relate our work to previous work of Hyland and dePaiva.
- we show several equivalent formulations of bilinear logic =
non-commutative *-autonomous categories. One interesting one is that
if one requires of a FILL category that a natural transformation
equivalent to the tensorial strength given by the weak distributivity is
isomorphic, then you get the full bilinear logic.
- we introduce a generalisation of the notion of "nuclear map" suitable
for weakly distributive categories, and show the nucleus of a FILL
category is *-autonomous.
- we give a rigorous definition of what it means for a category to
satisfy the MIX rule (previous attempts dealt only with the existence of
the required maps, and not the necessary coherence also needed), and
prove a coherence theorem for this doctrine.
- these last two points are linked by the observation that a weakly
distributive category satisfies MIX iff its nucleus does. As a
consequence we note that "cartesian" weakly distributive categories
(where the tensor is cartesian product) must satisfy MIX.
The paper is available by ftp as a
PS
file or as a
DVI
file
as well as on Robert Seely's
WWW home page
and the TAC home page.
For assistance with ftp, please contact rags@math.mcgill.ca.
Robin Cockett
Robert Seely