Summary
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
negri@helsinki.fi
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