Abstract

Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose $$\text {NL}_\lambda $$, which is NL supplemented with a single structural inference rule (“abstraction”). Abstraction closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of the abstraction inference, there has been some doubt that $$\text {NL}_\lambda $$ should count at a legitimate substructural logic. This paper argues that $$\text {NL}_\lambda $$ is perfectly well-behaved. In particular, it enjoys cut elimination and an interpolation result. In addition, perhaps surprisingly, it is decidable. Finally, I prove that it is sound and complete with respect to the usual class of relational frames.