Multi-modalities and non-commutativity/associativity in functorial linear logic: a case study
Carlos Olarte, Elaine Pimentel
TL;DR
This work proposes a modular framework that unifies modal and substructural logics by labeling LL exponentials with indices from a pre-ordered set $I$, yielding $!^{i}$ as a flexible family whose behavior can vary in classicality and in associativity/commutativity. It formalizes a non-commutative, non-associative linear logic $\mathsf{acLL}_\Sigma$ with a subexponential signature $\Sigma=(I,\preccurlyeq,f)$, where contexts are ordered lists and rules act deeply, governed by structural flags in $f$. To express and reason about multi-modal LL, the paper develops linear nested sequents (LNS) with end-active variants, decomposing promotion into local steps via nesting operators in associative and non-associative settings. The associative case uses $\mathsf{LNS}_{\mathsf{LL}}$ with local promotion rules and a functorial signature to model modal axiom sets, while the non-associative case introduces a skeleton-based approach that preserves tree structure. Overall, the work advances a modular, scalable framework for substructural modal logics with flexible exponentials, with the aim of extending LL’s applicability to complex systems and enriching the computational interpretation of subexponentials in non-standard contexts.
Abstract
Similar to modal connectives, the exponential ! in intuitionistic linear logic (ILL) is not canonical, in the sense that if $i\not= j$ then $!^i F\not\equiv !^j F$. Intuitively, this means that we can mark the exponential with labels taken from a set I organized in a pre-order $\preceq$, obtaining (possibly infinitely-many) exponentials ($!^i$ for $i\in I$). There are, however, two main differences between multi-modalities in normal modal logics and subexponentials in linear logic. i. substructural behaviour. Subexponentials carry the possibility of having different structural behaviors; ii. nature of modalities. Normal modal logics start from the weakest version, assuming only axiom K, then extensions are considered, by adding other axioms. Exponentials in linear logic "take for granted" the behaviors expressed by axioms T and 4. Regarding (i), originally subexponentials could assume only weakening and contraction axioms, but later non-commutative/non-associative systems allowing commutative/ associative subexponentials were presented. Concerning (ii), Guerrini et al unified the modal and LL approaches, with the exponentials assuming only the linear version of K, with the possibility of adding modal extensions to it. This discussion was brought to multi-modal case, where subexponentials consider not only the structural axioms for contraction and weakening, but also the subexponential version of axioms {K,4,D,T}. In this work, we intend to join these two studies. This means that $!^{i}$ can behave classically or not, model associative and commutative systems or not, but also with exponential behaviors different from those in LL. Hence, by assigning different modal axioms one obtains, in a modular way, a class of different substructural modal logics.