Grishin ([10]) proposed enriching the Lambek calculus with multiplicative disjunction (par) and coresiduals. Applications to linguistics were discussed by Moortgat ([15]), who spoke of the Lambek-Grishin calculus (LG). In this paper, we adapt Girard’s polarity-sensitive double negation embedding for classical logic ([8]) to extract a compositional Montagovian semantics from a display calculus for focused proof search ([1]) in LG. We seize the opportunity to illustrate our approach alongside an analysis of extraction, providing linguistic motivation for linear distributivity of tensor over par ([3]), thus answering a question of [11]. We conclude by comparing our proposal to that of [2], where alternative semantic interpretations of LG are considered on the basis of call-byname and call-by-value evaluation strategies. Inspired by Lambek’s syntactic calculus, Categorial type logics ([14]) aim at a proof-theoretic explanation of natural language syntax: syntactic categories and gramma...