[with Francesco Paoli] “The Geometry of Non-Distributive Logics”, Journal of Symbolic Logic 70:4 (2005) 1108–1126.
In this paper, we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness. We show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic, and we indicate how proofs in this system may be labelled with terms exhibiting a kind of Curry-Howard isomorphism. This natural deduction system is inspired both by Shoesmith and Smiley’s multiple conclusion systems for classical logic and Girard’s proofnets for linear logic.
This paper is joint work with Francesco Paoli.
Comments
Very nice paper, Greg.
As usual, I find myself wondering about distributive lattices, since distributivity is so natural from the logical and semantic points of view but rather awkward from the proof theoretic one. It would seem that to do this kind of trick for DLL as opposed to LL you would need to allow multiple somethings - multiple input and output points, sets of formulae labelling nodes or something. I should remember Shoesmith and Smiley here, as I was around when they were writing their book, but I don’t offhand.
Posted by: John Slaney at June 14, 2004 08:19 PM
Thanks! The positive words mean a lot.
The next paper in the grand plan covers distributive lattice logic, and it’s nice that you can do it with the same rules for links (with the addition of explicit weakening links too, if you like). The difference is in the global structural properties, which have the effect that proofs can have multiple premises and multiple conclusions. Here’s an example proof of distribution. Note that it uses different notation. The nodes are labelled with rules and the arcs are labelled with formulas (but the notations are intertranslatable).
The difference between this stuff and S&S is in the tratment of structural rules and the proofnet inspired global structural properties (the switching stuff, etc). But the parallels become clearer in the general setting.
Posted by: Greg Restall at June 14, 2004 09:01 PM
Have you seen Cockett and Seely’s paper about this logic, which they call finite sum-product logic? You may be particularly interested in their Appendix B, which gives a geometric normal form for proof terms in the unit-free case.
Seperately, it seems odd to talk about proof nets for the additives without even mentioning the brilliant work of Hughes and van Glabbeek, which (at last!) gives a decent and well-behaved proof net theory for MALL.
(I tried to include links above, but this system seems to strip out HTML when I preview a comment. The URLs are:
http://www.tac.mta.ca/tac/volumes/8/n5/8-05abs.html
http://boole.stanford.edu/~dominic/papers/mallnets.html)
Posted by: Robin at September 1, 2004 06:40 PM
Yes, our bibliography needs filling out. I saw these papers myself only after we drafted this one, and sent it off to the journal. We’ll update it when we get our referee feedback. Thanks for the pointers! If anyone thinks we should refer to other things, please let us know.
Posted by: Greg Restall at September 8, 2004 04:37 PM
Very nice paper, Greg.
As usual, I find myself wondering about distributive lattices, since distributivity is so natural from the logical and semantic points of view but rather awkward from the proof theoretic one. It would seem that to do this kind of trick for DLL as opposed to LL you would need to allow multiple somethings - multiple input and output points, sets of formulae labelling nodes or something. I should remember Shoesmith and Smiley here, as I was around when they were writing their book, but I don’t offhand.
Posted by: John Slaney at June 14, 2004 08:19 PM