First-order linear logic and categorial grammars

First-order linear logic is the extension of multiplicative linear logic with first-order quantifiers. From the logical point of view, the logic has a simple graphical proof theory in the form of proof nets. I will show that the Lambek calculus and several of its extensions are natural fragments of first-order linear logic.

I argue that first-order linear logic should be seen as a sort of "machine language" underlying these different formalisms. This view provides a useful way to compare the different formalisms and allows us to show that although they start from different logical primitives, upon translation into first-order linear logic many of these treatments turn out to produce equivalent formulas in first-order linear logic.