The use of exponentials in linear logic greatly enhances its expressive power. In this paper we focus on nonassociative noncommutative multiplicative linear logic, and systematically explore modal axioms K, T, and 4 as well as the structural rules of contraction and weakening. We give sequent systems for each subset of these axioms; these enjoy cut elimination and have analogues in more structural logics. We then appeal to work of Bulinska extending work of Buszkowski to show that several of these logics are PTIME decidable and generate context free languages as categorial grammars. This contrasts associative systems where similar logics are known to generate all recursively enumerable languages, and are thus in particular undecidable.
翻译:指数在线性逻辑中的使用极大地增强了其表达能力。本文聚焦于非结合非交换乘法线性逻辑,系统探讨了模态公理K、T和4以及收缩与弱化结构规则。我们针对这些公理的每个子集给出了相继式系统;这些系统拥有切割消去性质,并在更具结构性的逻辑中存在对应类比。随后,我们借鉴Bulinska扩展Buszkowski工作的成果,证明其中若干逻辑在PTIME内可判定,并能作为范畴语法生成上下文无关语言。这与那些已知可生成所有递归可枚举语言(因而特别不可判定)的结合性系统形成了鲜明对比。