Undecidability of the Lambek calculus with subexponential and bracket modalities

TL;DR

This paper proves that the derivability problem in an extended Lambek calculus with subexponential and bracket modalities is undecidable, highlighting limits of computational tractability in advanced linguistic formalisms.

Contribution

It establishes the undecidability of the Lambek calculus with exponential and bracket modalities, and analyzes the complexity of its restricted fragments.

Findings

Undecidability of the calculus with these modalities.

Restricted fragments are in NP complexity class.

Insights into the computational limits of linguistic formalisms.

Abstract

The Lambek calculus is a well-known logical formalism for modelling natural language syntax. The original calculus covered a substantial number of intricate natural language phenomena, but only those restricted to the context-free setting. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways. In particular, Morrill and Valentin (2015) introduce an extension with so-called exponential and bracket modalities. Their extension is based on a non-standard contraction rule for the exponential that interacts with the bracket structure in an intricate way. The standard contraction rule is not admissible in this calculus. In this paper we prove undecidability of the derivability problem in their calculus. We also investigate restricted decidable fragments considered by Morrill and Valentin and we show that these fragments belong to the NP class.