The logic of Quantifier Raising

Displaced scope is a hallmark of natural language, and Quantifier Raising (QR) has long been the standard tool for analyzing scope. Yet despite the foundational importance of QR to theoretical linguistics, as far as I know, there has never been a study of its formal properties. For instance, consider the decidability problem: given an initial syntactic structure, is there an algorithm that will determine whether a semantically coherent QR derivation exists? If at least one such derivation exists, is the number of semantically different analyses always finite? How do we know when we have found them all? Do the answers to these questions depend on imposing scope islands or other constraints on QR, such as forbidding vacuous movement, re-raising, remnant raising, raising of names, repeated type lifting, and so on? I settle these issues by defining QRT (Quantifier Raising with Types), a substructural logic that is a faithful model of QR in the following respect: every semantically coherent QR derivation corresponds to a semantically equivalent proof in QRT, and vice-versa. Since QRT is decidable and has the finite readings property, it follows that a broad class of theories that rely on QR also have these properties, without needing to place any formal constraints on QR. I go on to study the special relationship between type lifting and QR, drawing an analogy with eta reduction in the lambda calculus. Allowing unrestricted type lifting does not compromise decidability. In addition, it turns out that QR with type lifting validates the core type shifting principles of Flexible Montague Grammar, a paradigm example of an in-situ type-shifting approach to scope taking. This suggests that QR is compatible with a local, directly compositional view of scope taking. These results put Quantifier Raising on a reassuringly firm formal footing. EARLY ACCESS