## Hans-Joerg Tiede

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

### 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 --> 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.

Dvi-file

PS-File

PDF-File

Bibtex Entry