Explorations in Subexponential Non-associative Non-commutative Linear Logic

TL;DR

This paper explores an extended non-associative, non-commutative linear logic system with multimodalities, demonstrating a classical analogue and embedding of the intuitionistic calculus, advancing understanding of structural rule applications.

Contribution

It introduces a classical multi-succedent analogue of a non-associative, non-commutative logic system with multimodalities, and shows faithful embedding of the intuitionistic calculus.

Findings

Classical analogue of the intuitionistic system is constructed.

Faithful embedding of a large fragment of the intuitionistic calculus.

Extension of the logic system with multimodalities and structural rule licensing.

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, exhibiting a classical one-sided multi-succedent classical analogue of our intuitionistic system, following the exponential-free calculi of Buszkowski, and de Groote, Lamarche. A large fragment of the intuitionistic calculus is shown to embed faithfully into the classical fragment.