Tableaux for the Lambek-Grishin calculus

TL;DR

This paper develops a labeled modal tableau system for the Lambek-Grishin calculus, a symmetric extension of categorial grammar, and demonstrates its linguistic applicability by proving that LG-based grammars are context-free.

Contribution

It introduces a tableau proof system for LG and proves that LG grammars are context-free, enhancing the proof-theoretic understanding of this logical framework.

Findings

Developed a labeled modal tableau calculus for LG.

Proved LG grammars generate context-free languages.

Complemented previous work on LG's expressive power.

Abstract

Categorial type logics, pioneered by Lambek, seek a proof-theoretic understanding of natural language syntax by identifying categories with formulas and derivations with proofs. We typically observe an intuitionistic bias: a structural configuration of hypotheses (a constituent) derives a single conclusion (the category assigned to it). Acting upon suggestions of Grishin to dualize the logical vocabulary, Moortgat proposed the Lambek-Grishin calculus (LG) with the aim of restoring symmetry between hypotheses and conclusions. We develop a theory of labeled modal tableaux for LG, inspired by the interpretation of its connectives as binary modal operators in the relational semantics of Kurtonina and Moortgat. As a linguistic application of our method, we show that grammars based on LG are context-free through use of an interpolation lemma. This result complements that of Melissen, who proved that LG augmented by mixed associativity and -commutativity was exceeds LTAG in expressive power.