The Hidden Structural Rules of the Discontinuous Lambek Calculus

TL;DR

This paper explores the structural properties of the discontinuous Lambek calculus, showing its equivalence to a multimodal calculus and demonstrating how certain structural rules are absorbed within its hypersequent calculus.

Contribution

It establishes an equivalence between the hypersequent calculus of the discontinuous Lambek calculus and an omega-sorted multimodal calculus, revealing structural rule absorption.

Findings

hD is equivalent to mD via a faithful embedding

hD absorbs the structural rules of mD

The calculus maintains no structural rules explicitly

Abstract

The sequent calculus sL for the Lambek calculus L (lambek 58) has no structural rules. Interestingly, sL is equivalent to a multimodal calculus mL, which consists of the nonassociative Lambek calculus with the structural rule of associativity. This paper proves that the sequent calculus or hypersequent calculus hD of the discontinuous Lambek calculus (Morrill and Valent\'in), which like sL has no structural rules, is also equivalent to an omega-sorted multimodal calculus mD. More concretely, we present a faithful embedding translation between mD and hD in such a way that it can be said that hD absorbs the structural rules of mD.