structures (boxes) are first order definable relations. They can thus be ex-
pressed within first order logic and within the first order part of ordinary
type logic (i.e. the logic that was described in Church [1940], Gallin [1975]
and Andrews [1986]). This allows us to treat noun phrases as expressions
of a single type (a generalized kind of generalized quantifiers) and to have a
simple rule for coordination in arbitrary categories (see Muskens [forthcom-
ing] for a discussion of the latter). In this paper we build on the result and
show how the system can also be attached to Lambek Categorial Grammar.
The rest of the paper consists of five main sections. The first takes us from
English to Lambek proofs and the second takes us from Lambek proofs to
semantical recipes. After the third section has described how we can emulate
boxes in type logic, the fourth will take us from semantical recipes to boxes
and the fifth from boxes to truth conditions.
2 From English to Lambek Proofs
I shall assume familiarity with Lambek’s calculus and rehearse only its most
elementary features. Starting with a set of basic categories, which for the
purposes of this paper will be {txt, s, n, cn} (for texts, sentences, names and
common nouns), we define a category to be either a basic category or anything
of one of the forms a / b or b \ a, where a and b are categories. A sequent
is an expression T ` c, where T is a non-empty finite sequence of categories
(the antecedent) and c (the succedent) is a category. A sequent is provable if
it can be proved with the help of the following Gentzen rules.
T, b ` a
T ' a/b
[/R]
b, T ` a
T ' b\a
[\R]
T ` b U,a,V ` c
--------—-----[/L]
U, a/b, T, V ` c
T ` b U,a,V ` c
--------—-----[\L]
U, T, b\a, V ` c
An example of a proof in this calculus is given in Fig. 1, where it is shown
that (s/(n\s))/cn, cn, (n\s)/n, ((s/n)\s)/cn, cn ` s is a provable sequent. If
the categories in the antecedent of this sequent are assigned to the words ‘a’,
‘man’, ‘adores’, ‘a’ and ‘woman’ respectively, we can interpret the derivability
of the given sequent as saying that these words, in this order, belong to the
category s.