Complexity of Nonassociative Lambek Calculus with classical logic

TL;DR

This paper investigates the computational complexity of combining classical logic with Nonassociative Lambek Calculus, showing that the resulting logic remains decidable in exponential time despite added classical connectives.

Contribution

It proves that merging classical logic with NL (BFNL) preserves decidability, specifically in exponential time, expanding understanding of nonassociative logical systems.

Findings

NL without classical connectives is polynomial-time decidable.

Adding classical connectives makes the consequence relation undecidable.

Distributive classical connectives retain exponential-time decidability.

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.