Complexity of Nonassociative Lambek Calculus with classical logic
Paweł Płaczek
TL;DR
The paper tackles the complexity of the nonassociative Lambek Calculus extended with classical connectives by proving that BFNL’s finitary consequence relation is decidable in exponential time. It develops a sequent calculus with nonassociative contexts, and a semantic apparatus based on partial residuated Boolean algebras and residuated frames to bridge syntax and algebra. A key contribution is an explicit EXPTIME upper bound derived from embedding partial algebras into total residuated structures and analyzing prime filters, frames, and complex algebras. The results clarify the landscape around BFNL (and related logics) by establishing upper bounds and discussing lower bounds for both constant-free and constant-inclusive variants, with implications for distributive and Boolean/non-Boolean extensions of NL.
Abstract
The Nonassociative Lambek Calculus (NL) represents a logic devoid of the structural rules of exchange, weakening, and contraction, and it does not presume the associativity of its connectives. Its finitary consequence relation is decidable in polynomial time. However, the addition of classical connectives conjunction and disjunction (FNL) makes the consequence relation undecidable. Interestingly, if these connectives are distributive, the consequence relation is decidable in exponential time. This paper provides the proof that we can merge classical logic and NL (i.e. BFNL), and still the consequence relation is decidable in exponential time.