Modalities in linear logic weaker than the exponential “of course”: Algebraic and relational semantics

Abstract

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator □ on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential “of course” of linear logic. We define an algebraic semantics by interpreting the modality □ as a unary operationμ on an IL-algebra. Then we introduce a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of □ is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras.