Decidable Exponentials in Nonassociative Noncommutative Linear Logic

TL;DR

This paper investigates the decidability of exponentials in nonassociative noncommutative linear logic, showing that certain modal and structural rule combinations lead to PTIME decidable systems with context-free language generation.

Contribution

It systematically explores modal axioms and structural rules in nonassociative noncommutative linear logic, establishing decidability results and language generation capabilities.

Findings

Several logics are PTIME decidable.

Generated languages are context-free.

Contrasts with associative systems that generate all recursively enumerable languages.

Abstract

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.