Categorial Symmetry

This thesis constitutes an exploration into categorial type logics, attempting the reduction of natural language grammar to proof theory. Originating in Lambek's proposal for a syntactic calculus, the field has since grown to accommodate various competing extensions. For while the suitability of Lambek's work as a logic of strings has remained unchallenged, the question as to how its expressivity is to be improved upon in accordance with the empirical facts, in light of its suspected (and later confirmed) context-freeness, has generated considerable less consensus. By far the most of the resulting proposals, however, share a striking asymmetry that traces back to Lambek. Roughly, derivability is considered a relation between a possible multitude of hypotheses (the categories assigned to the individual words) and a unique conclusion (the category of the phrase made up from the hypotheses). The possibility of dispensing with the asymmetric treatment of the concepts of hypothesis and conclusion that permeates categorial type logics was first put forward by Grishin. While meant as an exercise in abstract algebra, his proposals have recently been investigated for their linguistic applications by Moortgat and associates, culminating in their definition of the Lambek-Grishin calculus. Crucially, expressivity is gained through the very act of treating hypotheses and conclusions on par, lending empirical support to the recovery of symmetry. In this dissertation, we provide a thorough linguistic and proof-theoretic investigation into the Lambek-Grishin calculus, many whose formal properties have yet to be established due to its relative youth.