Counting the Number of Proofs in the Commutative Lambek Calculus

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageAmerican English
Title of host publicationJFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday
StatePublished - 1999


  • Applied Mathematics
  • Mathematics

Cite this