A Scope-Taking System with Dependent Types and Continuations

Different scope-taking mechanisms have been proposed for capturing quantifier scope alternation, including covert operations of quantifier movement, type-changing rules, storage devices. In this paper we propose a new scope-taking system with dependent types and continuations. The key elements of our formal framework are: (i) richly typed system; (ii) contexts for determining the relative scoping of quantifiers; (iii) recursive procedure by which the interpretation is computed and the dependently typed context is built along the surface structure tree. The main advantage of our proposal is that it does not overgenerate—it produces all and only the attested readings for the defined fragment. The core idea behind the proposal is that certain lexical elements are responsible for inverting scope: relational nouns and locative prepositions. This allows us to provide a principled solution to the question of why certain constructions missing such elements block inverse scope.