• Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic , Mathematical Structures in Computer Science, vol. 5, pp. 41-68, Cambridge University Press, 1995.

    Sara Negri

    It is well known that Intuitionistic Logic can be faithfully embedded into (Intuitionistic) Linear Logic. For the embedding, or translation, different solutions have been proposed (cf. Girard (1987), Troelstra (1992), Danos et al. (1993)). The purpose of this paper is to study the embedding from a semantical viewpoint, by investigating into the relationship between various models for Intuitionistic Logic and for Intuitionistic Linear Logic. We will follow this pattern: given a structure which is a model for Intuitionistic Linear Logic we explain how to reconstruct inside it a structure which is a model for Intuitionistic Logic. In the first section this procedure is worked out for the algebraic semantics of quantales with modality (cf. Rosenthal (1990), Troelstra (1992), Yetter (1990)). Here it is proved in detail that every quantale with modality gives rise to a frame included in it; furthermore the isomorphism between the complete lattice of modalities on a quantale and the complete lattice of subframes of a quantale is established. Finally, the largest subframe included in a quantale is described. By a result due to G. Sambin, frames and quantales are representable by means of formal topologies and pretopologies respectively (cf. Battilotti and Sambin (199?)). In the appendix, by an extension of these representation theorems to quantales with modality, we show that any quantale with modality is isomorphic to the class of saturated subsets of a suitable pretopology endowed with an operator, already introduced in Sambin (1989), and called {\it stable interior operator}. As an application, we show, given a formal pretopology with a stable interior operator representing a quantale, how to obtain a formal topology representing the subframe determined by the modality. All these semantical considerations lead to consider, in the second section, ``natural'' requirements on translations from Intuitionistic Logic into Intuitionistic Linear Logic. More explicitly, we define a faithful translation corresponding to the insertion of a subframe into its matching quantale with modality, and such that translated formulas are equivalent to their exclamation. Furthermore we define a faithful translation which is also a translation of schemes, that is which commutes with substitution. In the final section we deal with categorical semantics, extensively studied in Linear Logic literature (cf. Barr (1991), Mart\'\i\/-Oliet and Meseguer (1991), de Paiva (1989), Seely(1989), etc.). We study sufficient (and in a way necessary) conditions so that the co-Kleisli construction, applied to a category which is a model for Linear Logic, gives rise to a categorical model for Intuitionistic Logic. In particular, we propose an answer to a question, raised in Seely (1989), concerning the existence of coproducts in the co-Kleisli category. Finally, we show that the algebraic construction developed in the first part is just a particular case of this categorical one, namely its reduction to partial orders.

    Back to Sara's homepage.

    Last modified April 24, 1997