A MODAL VIEW OF LINEAR LOGIC

We present a sequent calculus for the modal logic S4, and building on some relevant features of this system (the absence of contraction rule s and the confinement of weakenings into axioms and modal rules) we sh ow how S4 can easily be translated into full propositional linear logi c, extending the Grishin-Ono translation of classical logic into linea r logic. The translation introduces linear modalities (exponentials) o nly in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.