Lambek Calculus with Banged Atoms for Parasitic Gaps

Lambek Calculus is a non-commutative substructural logic for formalising linguistic constructions. However, its domain of applicability is limited to constructions with local dependencies. We propose here a simple extension that allows us to formalise a range of relativised constructions with long distance dependencies, notably medial extractions and the challenging case of parasitic gaps. In proof theoretic terms, our logic combines commutative and non-commutative behaviour, as well as linear and non-linear resource management. This is achieved with a single restricted modality. But unlike other extensions of Lambek Calculus with modalities, our logic remains decidable, and the complexity of proof search (i.e., sentence parsing) is the same as for the basic Lambek calculus. Furthermore, we provide not only a sequent calculus, and a cut elimination theorem, but also proof nets.