A note on undecidability of propositional non-associative linear logics

TL;DR

This paper introduces a new non-associative, non-commutative propositional linear logic and proves that it, along with its classical variants, is undecidable, highlighting fundamental limits of these logical systems.

Contribution

It defines NACILL, a novel non-associative, non-commutative propositional linear logic, and establishes its undecidability along with classical variants.

Findings

NACILL is undecidable.

Extensions with exchange and contraction are undecidable.

Classical involutive and cyclic variants are also undecidable.

Abstract

We introduce a non-associative and non-commutative version of propositional intuitionistic linear logic, called propositional non-associative non-commutative intuitionistic linear logic (NACILL for short). We prove that NACILL and any of its extensions by the rules of exchange and/or contraction are undecidable. Furthermore, we introduce two types of classical versions of NACILL, i.e., an involutive version of NACILL and a cyclic and involutive version of NACILL. We show that both of these logics are also undecidable.