Proof nets for grammatical logic

A "proof net" is a kind of compressed proof that was developed for linear logic in the late 1980s. They have been studied a great deal ever since for a number of reasons, one of which is that linear logic is a close relative of the Lambek logics that are useful in linguistic syntax under the modern-day rubric of type-logical grammar. A good source to learn about type-logical grammar and linguistics is my now passé 2004 book (not in most libraries but available cheaply as an ebook, though try to ignore Ch. 6), but also Glyn Morrill's 1994 book (not available cheaply but found in many libraries). For learning about linear logic, type-logical grammar, and proof nets all under one roof, the one and only source is Richard Moot's PhD dissertation, a real tour-de-force. My own dissertation (which grew up into the book) is quite embarrassing compared to this masterpiece, which is still available here.

I'm currently working on a survey paper about proof nets and other proof "compressions." I've actually been working on this paper for about ten years, but I really feel I might finish it soon. The purpose is to highlight the subject for the broader logic community, and to focus primarily on how the proof compressions become more and more geometrical as the logic gets stricter control over the arrangement of formulae. For classical propositional logic, the most compressed proof object is a "matrix" of atoms derived from the formula tree. The condition ensuring provability of the formula is basically set-theoretical, there is not much geometry to it. For linear logic, one keeps track of multisets of formulae (counting occurrences), and so the proof net provability condition is more graph-theoretical. For the associative Lambek logic we no longer have commutativity of the formulae, and the corresponding proof net condition comes to involve "planarity" of the graph. This is fundamentally a geometric condition that can be expressed using topology. The most restricted logic of all is the nonassociative Lambek system, and extending the proof nets to this case has to involve more specific topological conditions which I am still working out for my paper.

All of this seems important to me because if linguistic grammar is to be modeled type-logically, the "proofs" of sentences should be able to be carried out in a highly compressed fashion if the system is to have cognitive relevance. Generally, the brain's innate computational abilities seem to invoke highly efficient methods that are implemented in the neural "analog computer." But that leads me to a discussion of analog computation in the brain, which should be left to another post.