Journal of Logic and Computation Advance Access published online on December 21, 2007
Journal of Logic and Computation, doi:10.1093/logcom/exm084
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original papers |
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