Formal properties of NLλ
Chris A. Barker, Chung-chieh Shan · 2014
Abstract Chapter 17 explores the formal properties of NL‐lambda. This is done indirectly, by first studying NL‐CL, a type‐logical grammar with standard structural postulates. We prove that NL‐CL is sound and complete with respect to the usual class of relational models. We then prove that NL‐CL is conservative over NL (the non‐associative Lambek grammar). That is, a sequent in NL is a theorem in NL iff it is a theorem of NL‐CL. We then prove that NL‐CL is equivalent to a restricted version of NL‐lambda. We prove cut elimination for NL‐lambda. This clears the way for showing that NL‐lambda is decidable. In addition, we extend NL‐lambda to a still‐decidable version that handles syntactic displacement (which was handled in Part I by postulating silent expressions called gaps). We briefly mention a variant of NL‐CL that corresponds to unrestricted NL‐lambda.