Departments of Linguistics, Cognitive Science and Computer Science
Lindley Hall
Indiana University
Bloomington
IN, 47405, USA
htiede@cs.indiana.edu
http://www.cs.indiana.edu/~htiede
This paper is concerned with the study of the number of proofs of a sequent in the commutative Lambek calculus. We show that in order to count how many different proofs in beta/eta-normal form a given sequent Gamma --> alpha has, it suffices to enumerate all the Delta --> beta which are ``minimal'', such that Gamma --> alpha is a substitution instance of Delta --> beta. As a corollary we obtain van Benthem's finiteness theorem for the Lambek calculus, which states that every sequent has finitely many different normal form proofs in the Lambek calculus.