Counting the Number of Proofs in the Commutative Lambek Calculus

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 \vdash \alpha has, it suffices to enumerate all the \Delta \vdash \beta which are “minimal”, such that \Gamma \vdash \alpha is a substitution instance of \Delta \vdash \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.