In this paper, we explore the Lambek-Grishin calculus LG: a symmetric version of categorial grammar based on the generalizations of Lambek calculus studied in Grishin [1]. The vocabulary of LG complements the Lambek product and its left and right residuals with a dual family of type-forming operations: coproduct, left and right difference. The two families interact by means of structure-preserving distributivity principles. We present an axiomatization of LG in the style of Curry’s combinatory logic and establish its decidability. We discuss Kripke models and Curry-Howard interpretation for LG and characterize its notion of type similarity in comparison with the other categorial systems. From the linguistic point of view, we show that LG naturally accommodates non-local semantic construal and displacement — phenomena that are problematic for the original Lambek calculi. 1 Background The basic Lambek calculus [2] is a logic without any structural rules: grammatical material cannot ...