Displacement logic for anaphora

•Logical grammar account of anaphora and binding principles.•Both syntactic (limited contraction) and lexical (displacement logic) duplication.•Combining additives, S4 modality, limited contraction and displacement logic.•Proposal of negation as failure in categorial grammar.•Proof-theoretical study including Cut-elimination and Curry–Howard labelling.

The displacement calculus of Morrill, Valentín and Fadda (2011) [25] aspires to replace the calculus of Lambek (1958) [13] as the foundation of categorial grammar by accommodating intercalation as well as concatenation while remaining free of structural rules and enjoying Cut-elimination and its good corollaries. Jäger (2005) [11] proposes a type logical treatment of anaphora with syntactic duplication using limited contraction. Morrill and Valentín (2010) [24] apply (modal) displacement calculus to anaphora with lexical duplication and propose extension with a negation as failure in conjunction with additives to capture binding conditions. In this paper we present an account of anaphora developing characteristics and employing machinery from both of these proposals.