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.
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
References
- Gentzen G. Untersuchungen ueber das logische Schliessen. Mathematische Zeitschrift (1934/1935) 39:176–210. 405–431.[CrossRef]
- Lambek J. The mathematics of sentence structure. The American Mathematical Monthly (1958) 65:154–170.[CrossRef]
- Prawitz D. Natural Deduction (1965) Stockholm: Almqvist and Wiksell.
- Schroeder-Heister P. A natural extension of natural deduction. JSL (1984) 49:1284–1300.[CrossRef]
- Troelstra A. Natural deduction for intuitionistic linear logic. Annals of Pure and Applied Logic (1995) 73:79–108.[CrossRef][ISI]
| ||||||||||||||||||||||||||||||||||||||||||||||