Abstract
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 language | American English |
|---|---|
| Title of host publication | JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday |
| State | Published - 1999 |
Disciplines
- Applied Mathematics
- Mathematics