Lambek calculus in natural deduction
A formulation of Lambek calculus in natural deduction is given. New rules for Lambeks multiplicative, non-commutative conjunction are proposed, rules for Lambeks two implications are standard. Rules for Lambeks 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.
lambek calculus natural deduction