Explorations in Subexponential non-associative non-commutative Linear Logic (extended version)

TL;DR

This paper explores an extended non-associative, non-commutative linear logic system with subexponentials, analyzing its classical version and embedding properties, building on prior exponential-free calculi and modal extensions.

Contribution

It introduces a classical multi-succedent version of the logic, demonstrating faithful embedding of the intuitionistic calculus into the classical fragment.

Findings

Classical multi-succedent calculus successfully embedded the intuitionistic version.

The system extends previous exponential-free calculi with multimodalities.

The logic supports local structural rule application via subexponentials.

Abstract

In a previous work we introduced a non-associative non-commutative logic extended by multimodalities, called subexponentials, licensing local application of structural rules. Here, we further explore this system, considering a classical one-sided multi-succedent classical version of the system, following the exponential-free calculi of Buszkowski's and de Groote and Lamarche's works, where the intuitionistic calculus is shown to embed faithfully into the classical fragment.