Philippe de Groote: Proof-theoretic Aspects of the Lambek-Grishin Calculus

We compare the Lambek-Grishin Calculus as defined by Moortgat (LG) with the non-associative classical Lambek calculus introduced by de Groote and Lamarche (CNL). We provide a translation of LG into CNL, which allows CNL to be seen as a non-conservative extension of LG. We then introduce a bimodal version of CNL that we call 2-CNL. This allows us to define a faithful translation of LG into 2-CNL. Finally, we show how to accommodate Grishin's interaction principles by using an appropriate notion of polarity. From this, we derive a new one-sided sequent calculus for LG.