NL_λ as the Logic of Scope and Movement

Lambek elegantly characterized part of natural language. As is well-known, his sub-structural 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 NL_λ, 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 NL_λ should count at a legitimate substruc-tural logic. This paper argues that NL_λ 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.