The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities

TL;DR

This paper analyzes the proof-theoretic complexity of advanced categorial grammar calculi, establishing cut elimination and undecidability results for systems with multiplicative, additive, and modal features.

Contribution

It provides the first proof of cut elimination and undecidability for Morrill's calculi with subexponential and bracket modalities.

Findings

Proved cut elimination for the systems.

Established algorithmic undecidability.

Showed these calculi can generate all recursively enumerable languages.

Abstract

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill's calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the ! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages.