Extraction in the Lambek-Grishin Calculus

We propose an analysis of extraction in the Lambek-Grishin calculus (LG): a categorial type logic featuring subtractions A circle divide B and B (sic) A, with proof-theoretic behavior dual to that of the usual implications A/B,B\A. Our analysis rests on three pillars: Moortgat's discontinuous type constructors ([6]); their decomposition in LG as proposed by Bernardi and Moortgat ([1]); and the polarity-sensitive double negation translations of [3] and [5], inspiring the Montagovian semantics of our analysis. Characteristic of the latter is the use of logical constants for existential quantification and identity to identify the extracted argument With its associated gap.