Relational semantics for a fragment of linear logic (Q2874885)

Linear logic (LL) was introduced by \textit{J.-Y. Girard} [Theor. Comput. Sci. 50, 1--102 (1987; Zbl 0625.03037)]. In LL, formulas represent \textit{resources}. Thus, the rules contraction and weakening are not generally admissible in LL, since resources \textit{may be} used exactly once. They are, however, admissible when applied to resources marked with certain modalities. LL has found many applications in computer science. Since Girard [loc. cit.], \textit{phase semantics} has traditionally been used as a semantics for LL, although Kripke-style semantics (cf., e.g., [\textit{G. Allwein} and \textit{J. M. Dunn}, J. Symb. Log. 58, No. 2, 514--545 (1993; Zbl 0795.03013)]) and other type of semantics (cf., e.g., [\textit{R. Di Cosmo} and \textit{D. Miller}, ``Linear logic'', in: Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. (2015), \url{http://plato.stanford.edu/archives/spr2015/entries/logic-linear}]) are available.NEWLINENEWLINEThe aim of the present paper is to provide a relational semantics for MALL, the multiplicative additive fragment of LL. MALL results from LL when dropping the two dual modalities referred to above. The author leans on the ``canonical extensions method'' and proceeds as follows. Taking the non-associative Lambek calculus (NLC) as the basic substructural logic, using canonical extensions, it is shown how to obtain a relational semantics for extensions of NLC. Then, the same strategy is followed in order to provide a relational semantics for MALL in Section 4, while in Section 5 it is discussed how the phase semantics and the relational semantics for MALL just defined are related to each other. It is argued that the main advantage of the latter over previous relational semantics (such as that provided in [Allwein and Dunn, loc. cit.]) and over phase semantics is that it allows a modular and uniform treatment of additional axioms and operations.NEWLINENEWLINEFor the entire collection see [Zbl 1280.03005].