Abstract

We present a complete pretopology semantics for a system of Intuitionistic Linear Logic where the storage operator is split into a contraction and a weakening component and then recovered again from them. The semantics for weakening and contraction has been explored by Bart Jacobs [13] in a categorical setting. However, a completeness theorem is not given in [13] and the approach taken there does not accommodate the case of non-commutative linear logic. Besides, we think it useful to have an intuitive, Kripke-type semantics for the bimodal system. Extensions of the exponential-free linear logic with modalities weaker than Girard's operater '!' have been recently considered by Anna Bucalo [3]. The canonical model construction of [3] is based on and extends the standard phase-space semantics for linear and substructural logics . The subtle point from our standpoint, however, is in recovering the linear logic storage operator from weaker modalities. It did not seem possible to modify the approach of [22, 21, 3] to account for the interaction needed between the contraction and weakening modalities, if one wants to recover the linear logic storage operator. We propose a new solution here using the space of all, rather than only the Dedekind-MacNeille closed ideals