Subexponentials in non-commutative linear logic

TL;DR

This paper explores the proof theory of non-commutative linear logic with subexponentials, focusing on cut-elimination conditions and decidability results, extending the understanding of logical systems where formulae are organized as lists rather than sets.

Contribution

It introduces conditions for cut-elimination in non-commutative linear logic with subexponentials and provides new decidability and undecidability results for these systems.

Findings

Conditions for cut-elimination in non-commutative subexponential systems

New decidability results for non-commutative linear logic

Undecidability results under certain configurations

Abstract

Linear logical frameworks with subexponentials have been used for the specification of among other systems, proof systems, concurrent programming languages and linear authorization logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organized as sets and multisets of formulae not being possible to organize formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut-elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.