Journal of Logic and Computation Advance Access originally published online on December 21, 2007
Journal of Logic and Computation 2008 18(4):589-600; doi:10.1093/logcom/exm084
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Lambek Calculus in Natural Deduction
Boeblingen, Germany
E-mail: ernstzimmermann{at}de.ibm.com
Received 21 June 2007.
| Abstract |
|---|
A formulation of Lambek calculus in natural deduction is given. New rules for Lambek's multiplicative, non-commutative conjunction are proposed, rules for Lambek's two implications are standard. Rules for Lambek's conjunction are variants of general elimination rules: a symmetric elimination rule and its specializations, left elimination rule and right elimination rule. Conversions hold for all these rules, but only the symmetric elimination rule is fully permutable. Due to a natural transformation for left and right elimination rules to the symmetric elimination rule with partial empty sequences of assumptions and vice versa, there hold two normalization theorems, one with a minimal set and one with a maximal set of permutations.
Keywords: Natural deduction; Lambek calculus