Non-associative, Non-commutative Multi-modal Linear Logic
Eben Blaisdell, Max Kanovich, Stepan Lvovich Kuznetsov, Elaine Gouvêa Pimentel, Andre Scedrov · Lecture notes in computer science · 2022
Abstract Adding multi-modalities (calledsubexponentials) to linear logic enhances its power as a logical framework, which has been extensively used in the specification ofe.g.proof systems, programming languages and bigraphs. Initially, subexponentials allowed for classical, linear, affine or relevant behaviors. Recently, this framework was enhanced so to allow for commutativity as well. In this work, we close the cycle by considering associativity. We show that the resulting system ( $$\mathsf {acLL}_\varSigma $$ acLLΣ ) admits the (multi)cut rule, and we prove two undecidability results for fragments/variations of $$\mathsf {acLL}_\varSigma $$ acLLΣ .