This paper addresses some of the issues involved in categorical models of intuitionistic linear logic. In particular, one of the contributions of the paper is the result that the notion of model given in earlier papers (Benton, Bierman, de Paiva, Hyland) is equivalent to having a symmetric monoidal adjunction between a SMCC and a CCC. Thus, assuming one believes that logical operations should behave well with respect to contexts, our notion of model is just what one obtains by assuming that there is a way to embed ordinary IL into ILL. In other words, we have a semantic reconstruction of the ! operation.
The paper is available via the WWW .
Abstract: Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (`of course') modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad.
This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.