A propositions-as-types approach to the generalized crossover effect

Abstract

It has recently been suggested that the crossover effect, standardly understood as a constraint on anaphoric dependencies between quantifiers and pronouns, extends to presupposition projection. Although this observation calls for a unified account of how presupposition can interact with quantifier scope and anaphora, existing theories fail to provide one. We address this challenge by adopting Dependent Type Semantics, a type-theoretical framework that represents propositions as types. In this approach, the interactions among quantifier scope, anaphora, and presupposition are analyzed through a process called type checking, based on which the generalized version of the crossover effect can be uniformly derived.