—ач T≥'α[/r] T'β U'u∙V,'γ [/l]
x ' x T0 ' λv.α U0,w,T0,V0 ' Y[u := w(β)]
V,T'L [\r] t0' β u-u-v0'γ [\l]
T0 ' λv.α U0,T0,w,V0 ' γ[u := w(β)]
Note that axioms and the rules [/L] and [\L] introduce new free variables.
With respect to these some conditions hold. The first of these is that only
variables that do not already occur elsewhere in the tree may be introduced.
To state the second condition, we assume that some fixed function type
from categories to semantic types is given, such that type(a / b) = type(b
\ a) = (type(b), type(a)). The condition requires that the variable x in
an axiom x ' x must be of type(c) if x ' x corresponds to c ' c in the
Lambek proof. Also, the variable w that is introduced in [/L] ([\L]) must
be of (type(b), type(a)), where a / b (b \ a) is the active category in the
corresponding sequent.
With the help of these rules we can now build a tree of semantic sequents
that is isomorphic to the Lambek proof in Fig. 1; it is shown in Fig. 2.
The semantic sequent at the root of this tree gives us a recipe to compute
the meaning of ‘a man adores a woman’ once we are given the meanings
of its constituting words. Let us suppose momentarily that the translation
of the determiner ‘a’ is given as the term λP0λP∃x (P0(x) ∧ P(x)) of type
(et)((et)t) and that the remaining words are translated as the terms man,
adores and woman of types et, e(et) and et respectively, then substituting
λP0λP∃x (P0(x) ∧ P (x)) for D and for D0 in the succedent and substituting
man, adores and woman for P, R and P0 gives us a lambda term that readily
reduces to the sentence ∃x (man(x) ∧ ∃y (woman (y) ∧ adores (y)(x))).
The same recipe will assign a meaning to any sentence that consists of a
determiner followed by a noun, a transitive verb, a determiner and a noun (in
that order), provided that meanings for these words are given. For example,
if we translate the word ‘no’ as λP0λP-∃x(P0(x) ∧ P(x)) and ‘every’ as
λP0λP∀x (P0(x) → P(x)), substitute the first term for D, the second for
D0, and man, adores and woman for P, R and P0 as before, we get a term
that is equivalent to -∃x(man(x) ∧ ∀y(woman(y) → adores(y)(x))), the
translation of ‘no man adores every woman’.