Categorial Grammar and Discourse

Figure 1: Proof for ‘a man adores a woman’

3 From Lambek Proofs to Semantical Recipes

Proof theory teaches us that there is a close correspondence between proofs
and lambda terms. The lambda term which corresponds to a given proof can
be obtained with the help of the so-called Curry-Howard correspondence. Van
Benthem [1986] observed that the lambda term that we get in this way also
gives us a correspondence between Lambek proofs on the one hand and the
intended meanings of the resulting expressions on the other. In the present
exposition of the Curry-Howard-Van Benthem correspondence I shall follow
the set-up and also the notational conventions of Hendriks [1993]. For more
explanation, the reader is referred to this work, to Van Benthem [1986, 1988,
1991] and to Moortgat [1988].

The idea behind the correspondence is that we match each rule in the
Lambek calculus with a corresponding semantic rule and that, for each proof,
we build an isomorphic tree of semantic sequents, which we define as expres-
sions T⁰ ` γ, where T⁰ is a sequence of variables and γ is a lambda term with
exactly the variables in T⁰ free. The semantic rules that are to match the
rules of the Lambek calculus above are as follows. (The term γ[u := w (β)]
is meant to denote the result of substituting w(β) for u in γ.)

<<   <   1   2   3   4   5   6   7   >   >>