Some applications of categorial polymorphism

Martin Emms, The CIS Leopoldstr 139 8000 Munchen 40 Germany

July 21, 1993

The main concern of the paper is to introduce a certain categorial grammar system, namely Polymorphic Lambek Categorial Grammar (PLCG), to consider its application to quantification and coordination, and to compare this with other treatments of the same topics.^{1}

So to begin with, in section 1 I set out the basic aspects of quantification and coordination for which one needs an explanation. I then consider a series of possible accounts for these facts. The accounts considered are separated into two groups according to whether or not they are ‘type-driven’ . A type-driven account characterises words via some infinite, inductively defined notation (the ‘types’), and accords properties to expressions in a systematic way on the basis of the inductive structure of their ‘types’.

Section 2 considers the classical, non-type-driven accounts, and argues that they are not satisfactory. Within DYANA, a number of type-driven approaches have been and are being researched, and the approach to be argued for here, PLCG is one such. In the sections following section 2, these type-driven approaches are considered in turn. Section 3 concerns the Lambek calculus variety of categorial grammar, section 4 concerns the type-flexibility account stemming from [Partee, B. and Rooth, M., 1983], and developed considerably in [Herman Hendriks, 1990], section 5 concerns the polymorphic categorial account, and section 6 considers the ‘quantor types’ categorial proposal of Moortgat. My basic conclusions are that all the type-driven accounts are an improvement over the classical accounts, and that amongst these type-driven proposals, the polymorphic categorial account is the one which is unique in accounting for ambiguities by using no more than is required by syntax.

After this, in section 7 some possible further areas of coverage in PLCG are discussed. Finally there is an Appendix containing material on the following topics in the polymorphic system:

1. The definition of substitution

2. The official definition of the polymorphic calculus

3. The definition of the 2nd order Lambda calculus

4. String-semantics

5. Semantics for polymorphic types

6. Semantics of 2nd order Lambda calculus

7. The impossibility of ‘definitions by terms’ for the polymorphic logical constants

8. The general wide-scoping of a quantifier

9. The general wide-scoping of a junction

1Some technical rather than empirical aspects of the approach are addressed in [Emms, M. and Leiss, H., 1993], concerning Cut Elimination, and [Emms, M., 1993], concerning decidability. In 1994 a DYANA deliverable is projected addressing the question of the model theory for categorial polymorphism.

1 Empirical Aspects of Quantification and Coordination

1.1 Quantification

Quantifiers and proper names seem to be different kinds of expression. Proper names, such as Simon, Everton, are typically given to children shortly after they are born and are found on maps next to the representation of cities. Quantifiers do not do this. Also quantifiers are usually such that a native speaker can, by first attending to some empirical matters, decide whether a sentence featuring one is true (someone is absent, 3 orange tetrahedrons are absent, for example), and this holds even if the native speaker has perhaps never encountered before an utterance featuring the quantifier in question.^{2} Proper names lack this feature: a native speaker cannot judge the truth of a sentence featuring a proper name unless he has had some previous experience in which the name figured, and which served to identify the bearer of the name (someone said ‘That’s Simon’ or perhaps Simon wore a T-shirt with his name on). Sentences with proper names are thus context-sensitive in a way that sentences with quantifiers are not. There is the not unrelated graphological fact that proper names tend to be written as one word, and quantifiers as at least two, though this is not universal. Universal is the fact even when an argument can be mounted that a proper name has several parts, the decomposition is irrelevant to the reference of the name.

So on such grounds as these, one can say that there is a distinction to be made between proper names and quantifiers. However, in a sentence, a proper name can always be replaced with a quantifier, and vice versa. This interchangeability of proper names and quantifiers is the first fact that a linguistic proposal must get right.

This interchangeability might encourage one to give quantifiers and proper names the same category. However, everything else points to the fact that they should have different types, with proper names having type e and quantifiers having type ((e, t), t). By ‘everything else’, I mean plausible denotations can be assigned to sentences involving Simon and someone, on the basis of such typings. So, for example, considering sentences such as those in (1) below, the contribution of the verb and subject or verb and object to the overall sentence denotation can be expressed as in (2).

a. Simon came b. someone came c. John loved Simon d. John loved someone e. John gave Simon Mary f. John gave someone Mary g. John told Simon to go h. John told someone to go (1)

a. [[ came ]]([[ Simon ]])

b. [[someone]](x ↦ [[came]](x))

c. [[ loved ]]([[ Simon ]])

d. y ↦ [[someone]](x ↦ [[loved]](x)(y))

e. [[ gave ]]([[ Simon ]])

f. y, z ↦ [[someone]](x ↦ [[gave]](x)(y)(z))

g. [[ told ]]([[ Simon ]])

h. P, z ↦ [[someone]](x ↦ [[told]](x)(P)(z))

(2)

By the local scope properties of quantifiers, I will refer to the fact that the denotation of verb plus subject or object quantifier is essentially as in (2b,d,f,h). In other words, in general, there is a reading of a sentence containing a verb (or preposition) denoting P, and an adjacent quantifier, denoting G, such that their contrbution to the sentence denotation may be expressed as G_{Q}(G)(P), where G_{Q} can is defined recursively as:

2By ‘quantifier’ here I mean a combination of a determiner and a common noun, and common noun may be novel by being complex.

where a is any type and b is a conjoinable type^{3}, G_{Q}(G)(P^{(e,t)}) = G(P) G_{Q}(G)(P^{(e,a,b)})(x^{a}) = G_{Q}(G)(y^{e} ↦ P yx)

The second thing, then, that any linguistic proposal must do is that it must account for the local scope properties of quantifiers.

Finally there is the fact that sentences containing quantifiers tend to give rise to scope ambiguities. Here is an example:

(3) No-one could recall more than two-thirds of the speech

The subject wide-scope reading describes a situation in which each of a group of people has partial recollection of a speech, the missed part being perhaps different for each. For example, the members of the audience may have been distracted one at a time by filling in their names on a circulating form. The object wide-scope reading is one according to which there is a substantial chunk of the speech that no-one can recall. For example, this chunk, in constrast to a more vivid part, may have been just too confusing, or nondescript for anyone to remember afterwards.

The phenomenon of scope ambiguity is rather pervasive, and can be obtained with many different quantifiers. There are therefore three aspects of quantification that must be accounted for: interchangeability with proper names, the local scope properties, and finally scope ambiguity.

1.2 Coordination

Parallel to the problems posed by quantification are problems posed by coordination. The purely syntactic side of the problem is illustrated below. The first group of examples illustrate coordination in major, traditional categories of English, the second, coordination of strings that are not, uncontroversial, traditional consituents of English and German::

a. John [walks] and [talks] (VP case)

b. John [loves] and [hates] Mary (TV case) c. John [wants] and [needs] to go (VVP case) d. John [asked] and [persuaded] Mary to go (TVVP case) e. [Mark], [Jim] and [I] applied for the news-reader job (Proper name) f. [Every boy] and [every girl] solved a question in the exam (Quantifier) g. Every [man] and [woman] died (Common noun) h. Every [tall] and [handsome] man died (Adjective)

(4)

a. [I didn’t much like] and [Mary actually detested] the teacher

b. John gave [Mary a book] and [Suzanne a cake]

c. John told [Mary to go] and [Eric to stay]

d. He told [Jack to draw] and [Mary to paint] the castle

e. daß [Horst Rosa] und [Dieter Ingrid] gefällt f. daß [Horst groß] und [Dieter klein] ist g. ein Mann dem [der Daad 100 DM] und [der Universitat 1000 DM] geschenkt hat (5)

Accounting for these syntactic data, illustrating the extensive priveleges of junctions, is the first task of a linguistic proposal concerning coordination.

3The conjoinable types is the subset of the implicational types, tj→, containing t and such that if a is conjoinable, then so is (b→a)

Turning to semantics, consider the following mixture of consitituent and non-constituent coordination:

a. a man [came in] and [sat down]

b. [Jack played in] or [his brother commentated on] every Merseyside derby between 1971 and 1974. c. a [talented] and [hardworking] candidate applied for the job d. everyone seemed to be [lying on the floor] or [sitting on chairs] e. John wants to [go to the cinema] or [read a book at home] f. the manager expects [Cantona’s sudden running to stun] or [Gascoigne’s relentless passing to exhaust] the opposition defence (6)

They all have a reading, in fact the most preferred reading, in which the junction does not take widest scope. For example, in the reading of interest, the denotations of (15a,c) may expressed as having the following as arguments to other semantic functions:

a. x ↦ [[came in]](x) ∧ [[sat down]](x)

c. P ↦ x ↦ [[talented]](P)(x) ∧ [[hardworking]](P)(x)

(7)

This illustrates what I will refer to as the local scope properties of junctions. To express it more exactly, it seems we can say that in general, there is a reading of a sentence containing the coordination of two strings denoting P_{1} and P_{2} such that the contrbution to the sentence denotation may be expressed as G_{J}(C)(P_{1})(P_{2}), with G_{J} recursively defined as follows:

where P_{i} is of conjoinable type and C is ∧ or ∨:

G_{J}(C)(P_{1}^{t})(P_{2}^{t}) = C(P_{1})(P_{2}) G_{J}(C)(P_{1}^{a→b})(P_{2}^{a→b})(x^{a}) = G_{J}(C)(P_{1}x)(P_{2}x)

Accounting for the local scope properties of junctions is the second task that any account of coordination must achieve.

It is a fact, though, that the junction word and the associated coordinated strings, do not always contribute a component of denotation in the fashion of (7). These are cases where the junction takes wide scope. As the existence of wide-scope phenomena with junctions is not so widely agreed on for junction as it is for quantifiers, I will discuss a number of examples that underly the claim.

To begin with consider VP junctions, such as:

(8) a man came in and sat down

Undeniably, for this sentence, the reading with a man outscoping and is very much preferred. However, it seems to me that with a variation of lexical material, such a reading is possible. For example, on the subject of government responses to student demonstrations, one might say:

A brutal police baton charge disrupted considerably the 1963 Paris student demonstations and dispersed completely the 1990 Tianenmen Square demonstration.

(9)

There is a preference of a non-local scoping of the junction here. My intuitions are the same for the following sentence, said on the subject of Napoleonic successes throughout Europe:

That year, a French flag flew above a captured British fleet in Portugal, fluttered from the roof of the Austrian parliament building, and draped the gates to St. Petersburg.

(10)

Partee and Rooth consider every student failed or got a D, deciding that the junction cannot have non-local scope. Hendriks in [Herman Hendriks, 1990], however, proposed the lexical variant below, as said by a color-blind person watching a team leave the field:

(11) everyone is wearing a red shirt or is wearing a green shirt For the above he suggests, and I share the intuition, that or can have widest scope. So, in (9),

(10) and (11) we have examples in which a junction has scope over a scope-taking element which itself occurs outwith a VP coordination.

Below are some more examples intended to show the same thing with different kinds of coordination ^{4}

a. every man and woman died b. a man and woman were talking to themselves c. most Palestinians and Israelis want peace d. lots of Palestinians and Israelis want peace e. seventy percent of Britains and Americans want peace f. her debut and finale took place at Covent Garden g. she could remember her debut and finale  } CN

h. many German and French men died ADJ

i. every house in London and Paris has an escalating price NP

j. they want a maid or a butler (but I don’t know which)

k. the judge will say either that they are guilty or that they are not guilty S (12)

(12a–i) have natural readings in which and takes wide scope, as evidenced by the fact one can draw the ‘conjunction elimination’ inference from α [X_{1} and X_{2}] β to α X_{1} β. The relevant reading of (12j) has both a maid and a butler occurring de dicto. The reason for saying that or has wide-scope in (12k) is that on a narrow scope interpretation, the judge would be stating a tautology.

Therefore parallel to the quantifiers, there are three things to be explained by any linguistic proposal: the extensive priveleges of occurrence of junctions, the local scope facts, and the possibility of non-local scopes.

As will be seen below, it has proven difficult to find an account of quantification or coordination which covers the local scope properties, and which requires no further embellishment to account for scope ambiguity. In addition, it has proven difficult to deal with the relationship between proper names and quantifiers.

2 Accounts which are not type-driven

2.1 Quantification

The interchangeability of a proper name, such as Simon, and a quantifier, such as someone, points to the fact that they should have the same category, say c. However, as noted above Simon and someone have essentially different types. Within the Montagovian conception of the link between syntax and semantics, this a problem. One possible response is to depart a little from the strict Montagovian conception, so that having the same category as another expression need not imply having the same type. This is the move towards what has been called ‘flexible semantics’, and this will be discussed in section 4. Here I will discuss the possible ‘classical’ responses to the problem.

One kind of solution gives Simon and someone different categories (and types), and has them introduced into sentences by different rules and operations. Simon would combine with verbs simply by function application. Someone would, in each of the slots it might appear, combine by G_{Q}. The syntactic rules can be designed so that despite the difference of category, Simon and someone would still be interchangeable.

This logically possible proposal is seldom made, for perhaps the following two reasons. One is that many people adhere to a simplest syntax is best principle. Then, if a clearly simpler grammar would be obtained by puting the proper names and quantifiers into the same category, then that would be a better grammar. The second, is that many people adhere to a parametric variation principle, according to which the above grammar suggest similar grammars, and although these would not be not correct for English, they ought to be correct for some natural language. The problem then is that it would be easy to write a similar grammar which did not predict that proper names and quantifiers are always interchangeable. The same point might be made by simply saying that the grammar above would give no explanation of the fact that , or misses the generalisation that, proper names and quantifiers may be interchanged.

4Some of the (12) examples well known. (12a) occurs in Bergman, (12b) in [David Dowty, 1988], (12j) in [Partee, B. and Rooth, M., 1983]

Another kind of solution gives Simon and someone the same category and type, NP and ((e, t), t) respectively, and tries to resolve the apparent semantic problems. One way to do this would be to make both Simon and someone combine with verbs by the above mentioned G_{Q} operation, and to give the well known meaning postulate preventing proper names from being freely interpreted in the generalised quantifier type. This is the most popular response to the problem.^{5} I think there are objections to it, but they are rather subtle. One is a kind of parametric variation objection. The account subjects proper names to a meaning postulate, which leads one to speculate on the possibility of freely interpreted proper names, which under the typing would allow them to denote arbitary generalised quantifiers. Recall above I tried to characterise the proper names as in a certain way context sensitive. So freely interpreted proper names would correspond to expressions associated with a generalised quantifier in a context sensitive way. There do not seem to be such expressions.^{6} The other objection has to do with ‘sentence missing an NP’ analysis of extraction constructions. If NP were associated with the type e (which it is not on the proposal), then (men) who (like Marilyn Monroe) can be analysed as the intersection of two expressions with (e, t) denotations. However, with NP associated with type ((e, t), t), (men) who (like Marilyn Monroe) must be analysed as a combination of two expressions with types (e, t) and (((e, t), t), t). This can be done, but seems a puzzling complication.

So putting Simon and someone into different categories is not an ideal solution, and putting them both into the type ((e, t), t) is not either. These seem to be the only two classical ways to try to capture the basis semantic properties whilst at the same time accounting for the interchangeability of proper names and quantifiers, and neither is ideal. I will argue later that the type-driven approaches have something to offer in this area.

The third challenge posed by quantified sentences, as I mentioned above is that they exhibit scope ambiguity.

Before briefly discussing some the proposals that have been made to cover scope ambiguity, I want to consider a possible Gricean counter argument, by which scope ambiguity might be removed from the linguistic agenda. The view is sometimes expressed that scope ambiguities are somewhat artificial, existing in the mind of certain linguists but not really a significant part of actual language use. According to this view, in actual language use, we optimise our choice of words to the proposition we are trying to express, and no sentence can be the optimum form for two different propositions. For example, it is pointed out that the subject wide scope reading is the most likely for every man loves a woman, and that the object wide scope reading is more likely to be expressed by a stylistic variant, such as a passive sentence a woman is loved by every man, or a topicalisation, a woman, every man loves. This line of thought might then justify ‘univocal’ grammars, according to which sentences were not ambiguous. There are difficulties with this line of thought, however. One is that besides syntactic structure, lexical material has a substantial effect on reading preference, and by varying lexical material whilst keeping syntactic form constant, it is possible to switch preferences from subject wide scope to object wide scope. A second difficulty is that when sentences slightly more complicated than subject-verb-object are considered, there are examples where a single sentence seems to be the optimum form for expressing two different propositions. Consider the passage of a bill through the UK parliament. A univocal analysis of someone will try to amend every clause might be justified on the grounds that the object wide scope reading is better expressed by a topicalisation, every clause, someone will try to amend (passivisation does not seem here to offer a further possibility). But consider the possibilities if the proposition is embedded by a construction with takes an NP and infinitival VP as complements, such as cause:

5This or Montague’s PTQ variation of it, making verbs take quantifiers as arguments

6There are context-sensitive quantifiers, such as many men, but none that are simply associated with arbitrary quantifiers according to the context, in such a way that without knowledge of the context , there is no way to guage the truth of a sentence featuring the quantifier.

the possibility of killing the bill by delay caused someone to try to amend every clause

Here again the scopes of someone and every clause can be interchanged, but now there is no ready stylistic variant by which the reading with every clause outscoping someone might be better expressed: at least neither passivisation nor topicalisation are possibilities.

I think examples like this show that there is no justification for univocal grammars, and so scope ambiguity is a substantial problem on the linguistic agenda. There are three approaches to the problem that have existed in the literature for some time:

1. Montagues Quantifying-in approach, which is itself very closely related to the early transformational approach which went under the name of Quantifier Lowering.

2. Quantifier Storage, as put forward by Cooper, and extended by Keller.

3. Quantifier Raising, which is the latter day transformational approach. Very much the same idea surfaces in computational linguistics, dubbed as Quantifier Pulling by Hobbs and Schieber.

Quantifying-in. This is the hypthesis that there is an operation that takes Q and ‘… he_{i} … ’ to give ‘… Q … ’. The most common objection to this I will put in the following way: Montague’s account does not make ambiguity emergent from other aspects of the account. That is to say, there is a clear element of the account (the quantifying-in rule) that one could manipulate to affect only the coverage of scope-ambiguity, and leave syntactic coverage not altered at all. To say the same thing another way one could say that it is a modular account of ambiguity. A wellknown counter to this, is to point out that it is only approximately true that the quantifier rule could be dropped without loss of syntactic coverage - lost would also be coverage of sentences that contain pronouns and in which the pronouns are understood as linked to quantifiers. It remains unclear, however, how successful this counter is, because although certain aspects of anaphora are captured by the quantifying account, many are not: discourse anaphora, donkey sentences, E-type pronouns, Bach-Peters sentences.

The modularity or non-emergence of the Quantifying-in account of scope-ambiguity is, it seems to me, the favourite objection. It deserves some comment why modularity is an objection rather than simply an observation - why is modularity automatically bad ? The best evidence there is are the Rodman examples, linking extraction and scoping. In (13a), every room occur in a location such that is cannot be interpreted with widest scope, whilst in (13b) is illustrated that a relative clause cannot be formed by deleting an NP from this position.

a. Guinevere has a bone which is in every room b. every room which Guinevere has a bone which is in (13)

These sentences suggest that a theory should be not entirely modular in its account of ambiguity - alterations of the theory that affect its yield in terms of scope-ambiguities should have inevitable side effects in terms of extraction. I said above that a Quantifying-in account fares rather badly by this emergence criterion - one could drop the Quantifying-in operation and leave syntactic coverage unaffected. Into the balance, though, must go the fact there is one way to adjust a Quantifying-in account so that both scope ambiguity and syntactic coverage are affected. This was shown by Rodman. One assumes that relative clause are formed from sentences containing subscripted pronouns, with the sentence being scanned for a particular pronoun which is then deleted. Given just this, there is no reason to expect the above extraction and scoping correspondence. However, by adding to the relative clause formation rule the aspect that pronouns other than the deleted one are superscripted with ‘R’, and by assuming that quantifying-in and relative clause formation are alike ‘blind’ to these superscript pronouns, the extraction and scoping correspondence is predicted. However, the correspondence could be undone by making the superscript pronouns ‘visible’ to relative clause formation. So the linkage in this kind of account is rather weak. Also, it remains the case that the quantifying-in rule could be dropped wholesale without syntactic side-effects.

So much for modularity. There is also a parametric variation type objection to the Quantifying-in analysis: there is something implausible in the way that the quantifying-in operation is defined so as to ‘cover its tracks’. The quantifying-in account is more or less the transposition of the inductive definition of well formed formulae of First Order logic (FOL) into the grammar of English. However, in contrast with FOL, after two quantifiers have been combined with he_{1} loves he_{2}, the result looks just like the result of simply concatenating the quantifiers with the verb. One might expect that if not in English, then in some other language, the corresponding quantifying-in operation to leave some trace of its having been implicated in the analysis, and to thereby lead to the unique readability properties one has in FOL. Such cases have not been brought forward, so the quantifying-in account provides a parameter of variation that is never used.

Something like these objections seem to have been Cooper’s motivation in making the Quantifier storage proposal [Robin Cooper, 1983]. The proposal takes a step away from the strict Montagovian paradigm, and allows syntax to underdetermine the semantics. The combination of a quantifier with a verb is either given a meaning where the verb and quantifier are actually combined, or the expression is given a two dimensional meaning, with one part being the combination of a verb with some kind of variable meaning, and the other being a stored version of the quantifier. Expressions with such two dimensional meanings can have further derived meanings obtained by retrieving a quantifier from the store, where retrieval is not conditioned by any aspect of syntactic structure. The result is a grammar with no syntactically redundant parts, and nor does the grammar lead by any parametric variation argument to the expectation of FOL-like languages. Therefore the main objections to Quantifying-in do not apply.

However, given the decoupling of the syntax and the semantics, the modularity objection is not entirely avoided. Though there are no syntactic rules which could be dropped to lose only scope ambiguity and preserve syntactic coverage, there is certainly another simplification of the overall proposal that would have the same effect. The account associates a disjunction of semantic operations with certain syntactic rules, namely store or do not store. If the ‘store’ disjunct is dropped, with it goes all coverage of scope-ambiguity, whilst all other aspects of coverage are untouched.

There are also some empirical problems with the proposal in its most basic form, noted by Keller on examples such as

(14) every representative of a company died

a company is stored, every reprentative of x is stored, then once the sentence is complete, a company is taken from the store, followed by every representative of x. The result is an anomolous meaning, in which we might say that a company has acted as a vacuous quantifier, and the final result contains a free variable. To solve the problem, Keller introduced the idea of nested stores: a company is stored inside every representative of x, and the removal of quantifiers from storage is required to respect this hierarchical structure. Thus where Cooper obtains scope-ambiguity by letting the conventional heirarchical structure of sentences under-determine a certain intepretive process, Keller increases the dependency of this interpretive procedure on heirarchical structure.

Here one can make a parametic variation objection: one stops at a certain arbitrary point on a scale of dependency between the heirarchical structure and the interpretive procedure: one can imagine less dependency (Cooper’s original proposal) and more dependency. So long as one does not find these other points on the scale realised, then one can object that the overall logical design is not a natural one, providing parameters for variation that are never intended to be used.

Finally, I will describe the proposal of Quantifier Raising. One feature of the latter day transformational grammar architecture in which this proposal has its home is that there are Logical Form (LF) structures, which are derived from Surface Structures (SS). SS does the work of defining the well formed sentences. LF’s do not participate in that task, but are part of the mediation between form and meaning. There is single free-wheeling Move-α transformation, and a large number of well-formedness constraints filtering out many of the structures that Move-α generates. Instances of Move-α transformations might be called ‘Quantifier Raisings’, when the moved item is a quantifier, and the transformation is applied to an LF tree. Quantifier Raising (QR), then, is as an operation on trees, the inverse of Quantifier Lowering. In some ways, this switch from QL to QR, takes away the syntactic redundancy objection that is made to QL or quantifying-in: QR is not part at all of the inductive definition of the well formed sentences (SS), and so it can hardly be accused of being a redundant part. It does seem to me, though, that a form of parametric variation objection from earlier arises again here, concerning the lack of languages that express quantification in more or less exactly the same way as FOL. This is because the SS/LF division seems rather arbitary, and there is no logical obstacle to counting the trees output by the QR transformation as still parts of SS, leading to the expectation of FOL-like languages.

So the classical accounts of quantifier scope ambiguity, namely Quantifier Lowering, Storage and Raising, seem to suffer from either or both of the following drawbacks: they suggest the existence of FOL-like languages and they are modular in their treatment of ambiguity.

2.2 Coordination

Having discussed classical accounts of quantification I will turn now to coordination. Considering first the syntactic side of the problem, one can say that the constituent coordination cases in (4) could conceivably be dealt with by proposing simply enough separate phrase structure rules to generate each apparent kind of coordination. However, even ignoring the data in (5) there is a PV objection to this: to treat the data in this way would be to suggest that no less natural than English would be a language which positioned the conjuction word differently according to the categories being coordinated, exhibitting patterns like S and S, and VP VP, and NP NP and [Gazdar et al, 1985]. Then, of course, the more significant difficulty is that even with a large number of phrase-structure rules (based on traditional categories), the examples in (5) still cannot be dealt with, because the strings being coordinated do not fall into traditional categories.

The ‘classical+ approach to this syntactic difficulty to be considered here is that of ‘conjunction reduction+. Originated by Chomsky in 1957, it proposes (i) ‘deep’ structure sentential coordination and (ii) a conjunction reduction transformation to derive all the examples in (4) and (5). Though this covers the syntactic problems, there are semantic objections to the conjunction redunction analysis, which I describe below.

A line of objection that has been made in the past, but which I shall not use, is that a conjunction reduction analysis can give junctions too wide a scope – allowing a junction to have scope over some scope-taking element outwith the coordinated elements. For example, the conjunction reduction analysis will derive a man came in and sat down from a man came in and a man sat down, and therefore make it into a statement about potentially two different men ([Gazdar et al, 1985], [Partee, B. and Rooth, M., 1983], [Gamut, L.T.F., 1991]). However, if you accept that there are examples in which a junction should be interpreted with wide scope, as I argued above, then this cannot be an objection to conjunction reduction.

A slight variation on this line of objection though, does tell against conjunction reduction. Rather than objecting that it leads to readings with do not exist, one can object that it misses readings which obviously do exist. Recall the mixed collection of constituent and non-constituent coordination from (15).

a. a man [came in] and [sat down]

b. [Jack played in] or [his brother commentated on] every Merseyside derby between 1971 and 1974. c. a [talented] and [hardworking] candidate applied for the job d. everyone seemed to be [lying on the floor] or [sitting on chairs] e. John wants to [go to the cinema] or [read a book at home] f. the manager expects [Cantona’s sudden running to stun] or [Gascoigne’s relentless passing to exhaust] the opposition defence (15)

In all cases, the conjunction need not take the wide scope that the obvious conjunction reduction analysis would predict, so we have a prima facie argument that conjunction reduction (CR) is not the right way to derive examples of non-sentential junctions. However, as it stands, this is not a complete argument. We need to know that no non-obvious analysis involving CR will deliver the desired reading, and that can only be judged given the details of the grammar in which CR is embedded, and arguments for those other details. I mention below briefly some ways that the rest of the grammar can be adjusted to that in combination with CR, the readings missing for the sentences in (15 could be generated.

Considering (15a), a grammar allowing ‘quantifying-in’ could derive the sentence by inserting a man into he_{1} came in and sat down, which might in turn be obtained by CR from he_{1} came in and he_{1} sat down. Something similar could be applied to (15b). I would argue that this avenue to the missing reading is blocked by the objections to quantifying-in pointed out above.^{7}

To get the natural reading of (15c) seems to require one to view the combination of the determiner with the common noun as ‘surface’ only, deriving from a combination of a deteriminer with a ‘deep’ sentence, he_{1} is a talented and hard working candidate. Here even more obviously than in the quantifying-in case, the operation used by the grammar here is linguistically unrealistic. In other words, from a PV point of view we should expect more direct combinations of the determiner and the ‘deep’ sentence, to give quantifiers resembling a he is a talented and hardworking candidate.

To get the conjunction having local scope in (15d,e,f), it seems to be necessary to take a nonsuperficial view of the subcategorisation requirements of the main verbs involved. Superficially, the main verbs subcategorise for infinitival VP’s. At a semantically significant, non-superficial level, it has been argued, they subcategorise for sentences. In early TG, this took the form of ‘deep structure’ subcategorisation for a sentence, the subject of which underwent a ‘raising’ movement or a subject or object controlled ‘equi’ deletion. In latter day TG, this takes the form of surface subcategorisation for ‘sentences’, where these can contain phonologically null elements (15d,e), or be untensed (15f). So whether this avenue to the missing readings is available depends on the arguments for and against this non-superficial view of apparently VP embedding verbs. It would take us too far afield to consider very much of that debate here. I will just say that the case for the non-superficial view of VP-embedding verbs was made partly on the basis of their semantic properties, and Thomason was amongst the first to show how to reconcile their semantic properties with the superficial view of their grammar. Therefore, other things being equal, one should adopt this more superficial view.

Overall, the (15) examples show that CR, a transformational device, will only be semantically viable as the sole source on non-sentential junctions if there are a number of other transformational devices present in the grammar. In each case, objections can be raised to these other devices, and these therefore function indirectly as objections to CR.

Having considered the local scope properties of junctions, I will consider finally the non-local scope properties, as illustrated by the examples in (9), (10), (11) and (12). The apparent semantic properties of these sentences are what a CR analysis would lead one to expect, and so a possible explanation for them would be to assume the grammar to include CR. This seems to me to be a theoretical option despite above considerations. I just argued that CR is not adequate to do one of the tasks in an account of coordination, and that was allowing junctions to have local scope. This is no objection to the use of CR as a device to explain non-local scopes. However, if there must be a non-CR explanation of the local scope properties of junctions, then the addition to it of CR to explain the non-local scope properties will lead to an account that is modular or non-emergent in its explanation of ambiguity. One can say this because CR would be included solely as a device to account for ambiguity, being for syntactic purposes strictly redundant.

Looking at (12a-i), examples of coordination of noun-like items, it seems some of the work on non-Boolean conjunction gives a way to explain the apparent wide-scoped reading. For example, if the function of man and woman in (12a) was to introduce the set which is the union of men with women, the validity of the conjunction elimination inference would be explained. However, it is not clear that this non-intersective hypothesis concerning and, will explain the validity of conjunction elimination for (12c-i) . For (12b) we would have to assume something like that man and woman introduced the set of all possible couples. Then consider (12e): because one can take find a subgroup of the group supposedly introduced by Britains and Americans, which is seventy percent of the whole group, and which contains no Britains, the inference to seventy percent of Britains want peace should not be justified. The inference could perhaps be obtained with the assistance of a small push from pragmatics, relating to the relevance of all words in an utterance. For (12f,g), the non-intersective hypothesis needs to be combined with one about apparently distributive verbs combining with group subjects and objects, and to cover the adjective junction case (12h), the story needs at least to be elaborated further. Finally, (12i) seems to me to be a case where the non-intersective interpretation of and, together with a plausible distributivity supposition for in does not help at all in getting the desired result.

7It is interersting to note that making Quantifier Storage available instead of Quantifying-in will not in the same way make up the apparent reading deficit.

Conjunction reduction or the idea to use non-Boolean coordination, seem to exhaust the possible explanations of wide-scopes for junctions outside of the area of type-driven accounts.

To summarise what I think the forgoing disussion in this section and the previous section shows. The accounts which allowed for quantifier and junction scope ambiguity were in some way modular in their explanation of ambiguity. Also no satisfying way was seen to on the one hand to account for the interchangeability of quantifiers with proper names, and on the other hand, to account for their basic local scope properties. I will in what follows refer to this as the Simon/someone problem.

3 The Lambek Calculus

In this section I briefly describe a certain kind of categorial grammar, namely Lambek categorial grammar (LCG), and the successes and failures that is has in confronting the above problems It is as such the first of four sections considering particular type-driven approaches.

The consideration of quantification and coordination in LCG is of particular interest because it represents a kind of limit point for grammars making use of the two categorial connectives ‘/’ and ‘\’. It is also a proper subpart of Polymorphic Lambek categorial grammar, the system to be argued for in section 5, and many of the notions required here can be carried over. Also the argument for PLCG that I will make in section 5 is reinforced by acquaintance with the exact nature of the shortcomings of LCG.

The following is intended as a brief description of LCG. For more details see [Moortgat, 1988]. Categories are assumed to be built up from basic categories, using the binary categorial connectives ‘/’ and ‘\’. x/y categorises expression which that seek a y argument to the right, whilst y\x categorises those expression that seek a y argument to the left. The set of categories will be referred to as cat^{(/,\)}. ^{8} Then a set of ‘categorial rules’ involving these categories is defined, of the form:

x_{1}, … x_{n} ⇒ y (n ≥ 1), x_{i} and y being categories

A distinctive feature is that the set of rules is defined inductively. Using a term adopted from logic, sequent, in place of ‘categorial rule’, Lambek presented this inductive definition as a close variant of Gentzen’s sequent calculus for propositional logic. Lambek’s calculus, l^{(/,\)}, is given below:

(Ax)  x ⇒ x

(/L)  U, y, V ⇒ w T ⇒ x /L U, y/x, T, V ⇒ w  (\L)  T ⇒ x U, y, V ⇒ w\L U, T, x\y, V ⇒ w

(/R)  T, x ⇒ y /R T ⇒ y/x  (\R)  x, T ⇒ y \R T ⇒ x\y

8Lambek also considered a third connective, the ‘product’. I, in common with several authors, use the name Lambek calculus to refer to what is really the product-free calculus

Here U, T, V are sequences of categories (U,V possibly empty), w, x, y are categories. The fact that l^{(/,\)}derives r, I will notate as l^{(/,\)}|−r. With regard to the names of the rules, ‘L’ and ‘R’ stand for left and right. For example, (\L) (resp. (\R)), derives sequents with ‘\’ on the left (resp. on the right) of the sequent arrow, ‘ ⇒ ’. For certain purposes it is convenient to consider the addition of the ‘Cut’ rule

T ⇒ x U, x, V ⇒ wCut U, T, V ⇒ w

A natural space of possible interpretations for the language of categories, cat^{(/,\)}, is based on free algebras ⟨A, ·⟩, where · is a binary associative operation - the most natural example is choosing A to be be strings and · to be concatenation (note there is no unit element). The interpretation function, I, may assign to the basic categories any subset of A, and with respect to I, the denotation of a complex category is defined [[x/y]] = {a : ∀b ∈ [[y]], a·b ∈ [[x]]} (correspondingly for y\x. It has been shown [Buszkowski, 1982] that l^{(/,\)}|−x_{1}, …, x_{n} ⇒ y iff for all interpretations, [[x_{1}]]· . . . ·[[x_{n}]] ⊆ [[y]]. There is a sense, therefore, in which l^{(/,\)} represents a ceiling to the sequents one can help oneself to.

This Lambek style of grammar is associated also with a certain method for assigning meanings to strings. Meanings are assumed for basic expressions, with the correspondence between the categories and types: ν(np) = e, ν(s) = t, ν(x/y) = ν(y\x) = (ν(y), ν(x)).^{9} A proof, γ, of l^{(/,\)} can mapped into a semantic operation, G. So, if there is a proof, γ, of x_{1}, …, x_{n} ⇒ y, then a sequence of expressions with categories x_{1}, …, x_{n} and meanings m_{1}, …, m_{n}, has a possible meaning G(m_{1}, …, m_{n}). The operation, G, which goes with the proof, γ, is essentially defined by the Curry-Howard isomorphism [J-Y. Girard et al, 1989], but for practical purpose is defined using the term-associated calculus, l_{e}^{(/,\)}:

\begin{matrix}(Ax) & x : α ⇒ x : α \\ (/L) & U, y : α(β), V ⇒ w : ϵ T ⇒ x : β /L U, y/x : α, T, V ⇒ w : ϵ \\ (/R) & T, x : ζ ⇒ y : α /R T ⇒ y/x : λζα \end{matrix}

There are corresponding (\L) and (\R) rules. l_{e}^{(/,\)}derives sequents where in place of categories there are category:term pairs. The terms are drawn from the language of typed λ-calculus, which I shall refer to as L^{λ}. The types are essentially the language of implicational propositional logic, which I shall refer to as tj→. If we start with an l^{(/,\)} proof of r, add variables of the appropriate types to the antecedent categories of r, there is a unique way to add terms to the rest of the proof so as to get a proof of l_{e}^{(/,\)}. The term, α, associated with the succedent of r, represents the semantic operation. Here is an example of the calculation of such a term-asociated proof, where Φ_{1} and Φ_{2} are used as unknowns for terms :

np : x_{1} ⇒ np : Φ_{2} s : x_{2}(Φ_{2}) ⇒ s : Φ_{1}\L np : x_{1}, np\s : x_{2} ⇒ s : Φ_{1}  Φ_{2} = x_{1}, Φ_{1} = x_{2}(Φ_{2}), .˙ .Φ_{1} = x_{2}(x_{1})

Much more can be said concerning the Lambek calculus, and its metamathematical properties ([Buszkowski et al, 1988], [Benthem, 1991]). However, for my purposes in what follows, it will only be necessary to note the count-invariance property. Where x is basic, then the the x-count of y is 1 if y = x, is 0 if y is a basic category different to x, and is x-count(y_{1}) minus x-count(y_{2}), if y = y_{1}/y_{2} (corresondingly for y_{2}\y_{1}). For any l^{(/,\)}-derivable sequent the sum of the x counts of the antecedents equals that of the succedent [Benthem, 1986].

9This is the typing for the extensional version of the theory. There is a corresponding intensional version, but for expository purposes I am confining attention to the simpler extensional version. See the Appendix for some remarks concering the intensional version and the Curry-Howard isomorphism.

I will briefly illustrate the success cases for LCG in accounting for quantification and coordination. I will also note the cases that are not accounted for (see also [Emms, M., 1989], [Herman Hendriks, 1990]). For this, I will take as a point of departure the following Lambek Grammar:

A Lambek Grammar

1. The basis categories are {s, np, vpc, sc}

2. Lexical category assignment:

np  john, mary, he_{1}, he_{2}, …
s/(np\s), (s/np)\s every man, a woman, 2 policeman, …
np\s  walks
(np\s)/np  loves, is
((np\s)/np)/np  gives

(np\s)/sc  believes
sc/s  that
(np\s)/vpc  wants
((np\s)/vpc)/np told
vpc/(np\s)  to

3.1 Quantification

Evidently according to the above Lambek grammar sentences contain proper names can be generated and with appropriate denotations. The categorisations someone, which are simply certain categorial versions of the type ((e, t), t), allows the grammar to generate combinations of quantifiers with intransitive and transitive verbs, and furthermore with the appropriate semantic force. In other words in these cases the local scope properties of quantifiers are accounted for. The Simon/someone cases of combination with IV’s and TV’s will be accounted for via the derivability of the following sequents:

a. np, np\s ⇒ s

b. (np\s)/np, np ⇒ np\s c. s/(np\s), np\s ⇒ s d. (np\s)/np, (s/np)\s ⇒ np\s (16)

(16a,b,c) are obvious. The derivability of (16d) is shown below, as a term associated proof. One can see from the terms that the quantfier is combined with the verb in the desired way.

np:u_{1}, (np\s)/np:x, np:u_{2} ⇒ s:x(u_{2})(u_{1}) s:y(λu_{2}.x(u_{2})(u_{1})) ⇒ s:y(λu_{2}.x(u_{2})(u_{1})) /R np:u_{1}, (np\s)/np:x ⇒ s/np:λu_{2}.x(u_{2})(u_{1})  \L np:u_{1}, (np\s)/np:x, (s/np)\s:y ⇒ s:y(λu_{2}.x(u_{2})(u_{1}) \R (np\s)/np:x, (s/np)\s:y ⇒ np\s:λu_{1}.y(λu_{2}.x(u_{2})(u_{1})) (17)

However, the grammar does not allow quantifiers in all places that proper names are allowed. The following are not generated by the grammar.

John gave someone Mary (TTV case) John told someone to go (TVVP case)

(18)

The sentences in (18) are not recognised by the grammar. One can show this by giving a counter-model to the relevant sequents, where these are:

for some Q either s/(np\s) or (s/np)\s, np, ((np\s)/np)/np, Q, np ⇒ s (TTV case) np, ((np\s)/vpc)/np, Q, vpc/(np\s), np\s ⇒ s (TVVP case)

(19)

Proof that in l^{(/,\)} the TTV case is not derivable.

We give a countermodel to np, ((np\s)/np)/np, Q, np ⇒ s, for both of the values of Q.

We suppose:

[[np]] = \{□\}, [[ s ]] = \begin{cases}□ & ♡ & □ & □ \\ ◇ & ♡ & □ & □ \\ □ & ♡ & □ & ◇ \\ ◇♡□◇\} \end{cases}

It follows that,

[[np\s]] = \begin{cases}♡ & □ & □ \\ ♡□◇\} \end{cases} [[s/np]] = \begin{cases}□ & ♡ & □ \\ ◇♡□\} \end{cases} [[s/(np\s)]] = \{{□ \atop ◇\}},

[[(s/np)\s]] = \{{□ \atop ◇\}}

[[(np\s)/np]] = {♡□} [[((np\s)/np)/np]] = {♡}

Therefore whether Q = s/(np\s) or (s/np)\s, ◇ ∈ [[Q]], and so

there exists a,b,c,d (namely □, ♡, ◇, □) such that a ∈ [[np]], b ∈ [[((np\s)/np)/np]], c ∈ [[Q]], d ∈ [[np]], a · b · c · d ∉ [[s]].□

In contrast to IV and TV, TTV and TVVP have categorisations in which two arguments are sought in the same direction, something that is inevitable if the function has three arguments. The problem arises more acutely in Dutch , where the categorisation apt for a subordinate clause TV seeks two arguments in the same direction.

So, this Lambek grammar does not give a comprehensive solution to the interchangeability of Simon and someone. There are other potential categorisations that could be tried out. I will briefly mention two other obvious alternatives.

The most obvious alternative would be to give Simon and someone both the category np. I have already mentioned in the previous section some objections that can be made to a grammar which gives the same categorisation to proper names and quantifiers, and those objections would count here also. In the current case, there is another objection because the grammar would inherit Montague’s PTQ typing for verbs. I call this the ‘ptq verb objection’. In the extensional version of Montague’s typing, with ((e, t), t) in arguments, the typing predicts what I will call ptq verbs. A ptq verb, f, is such that the common noun man would occur transparently in x f a man, yet x f a man does not imply there is a man. From an empirical point of view there are no ptq verbs, yet in an extensional version of Montagues typing strategy, freely interpreted verbs would be predicted to be ptq verbs. A ‘verb + quantifier’ postulate can be formulated restricting the interpretation of verbs and to give them an apt behaviour. From the PV point of view, though, it would be strange that nothing behaves like a ptq verb. The objection is a little more involved in the intensional version of the typing, but I think still can be made. Freely interpreted verbs in the intensional typing have arguably the behaviour of intensional verbs. Other verbs are, in the PTQ proposal, subject to a meaning postulate which is in effect a composition of a natural extensionality postulate with the above mentioned verb + quantifier postulate. In this case no verbs are given the behaviour of ptq verbs, but again from a PV perspective their existence is still very much predicted: any verb which was subject simply to an extensionality postulate would be behave as a ptq verb. So, on these counts, I would argue that categorising proper names and quantifiers both as np to solve the Simon/someone problem is not a good strategy in a Lambek grammar. Moreover, though categorising Simon and someone as np makes them intechangeable, and covers the local scope properties of quantifiers, it does not lead to any solution to the other main problem, that of scope ambiguity (see above references).

The other obvious alternative categorisation leaves the quantifiers categorised as in the stated grammar, but changes the categories of expressions that combine with quantifiers, replacing the np’s that occur in argument position with quantifier categorisations. This also give Simon/someone interchange (because of the derivability of someone’s category from Simon’s), and will cover the local scope properties of quantifiers problem. The above ptq verb objection applies again, however. There are also syntactic objections, because expressions other than quantifiers may gain the quantifier categorisation. For example and Mary hates that man has the category (s/np)\s, which will lead to the following being predicted to be grammatical: Dave gave [and Mary hates that man] some money. Then finally, as above, the grammar does not generate all desired scope ambiguities (see above references).

In view of the fact that the Lambek grammar defined above cannot even recognise certain sentences containing quantifiers, it cannot be the case that the grammar gives a satisfactory account of quantifier scope ambiguity. However, for some of the quantifier-containing sentence that the grammar can recognise (though not all), it is also the case that the grammar can account for their ambiguity. It is of some interest to look at how much of the scope-ambiguity data the grammar does cover. One reason for this is that it illustrates generic advantages of a categorial grammar approach. The other reason is that one can see that there is a connection between the failure of the grammar to generate quantifiers in all allowed positions, and the failure to give all readings to generated sentences.

An exampe of a sentence which the grammar both generates and assigns all possible readings to is: every man loves a woman. The relevant sequent is s/(np\s), (np\s)/np, (s/np)\s ⇒ s. One of its possible proofs is:

s ⇒ s np, (np\s)/np, np ⇒ s s ⇒ s /R np, (np\s)/np ⇒ s/np  \L np, (np\s)/np, (s/np)\s ⇒ s\R (np\s)/np, (s/np)\s ⇒ np\s/L s/(np\s), (np\s)/np, (s/np)\s ⇒ s (20)

The associated term is x^{(et,t)}(λu_{2}^{e}[z^{(et,t)}(λu_{5}^{e}[y^{(eet)}u_{5}u_{2}])]), assuming x^{(et,t)}, y^{(eet)} and z^{(et,t)} are associated with the antecedents. This gives a subject-wide scope interpretation. Another possible proof is

s ⇒ s np, (np\s)/np, np ⇒ s s ⇒ s \R (np\s)/np, np ⇒ np\s/ L s/(np\s), (np\s)/np, np ⇒ s/ R s/(np\s), (np\s)/np ⇒ s/np  \L s/(np\s), (np\s)/np, (s/np)\s ⇒ s (21)

Here the associated term is z^{(et,t)}(λu_{2}.x^{(et,t)}(λu_{5}.y^{eet}u_{2}u_{5})), and we have an object wide scope interpretation.

Now in this case, the way the grammar accounts for ambiguity is very attractive. In short it is an emergent explanation. It is a syntactic explanation of ambiguity, and such explanation usually fall foul of the objection that the syntax incorporates certain elements simply in order to generate ambiguities. However, the Lambek grammar explanation of ambiguity, syntactic though it is, manages to avoid that objection: no part of the syntactic machinery is present exclusively to account for ambiguity. Instead ambiguity inevitably emerges from natural categorisations and the natural laws of category combination. To simplify the grammar in some way such as to generate no ambiguities it would be necessary to restrict the (Slash R) rule, and this could be expected to have syntactic consequences. In particular it would effect the classic Lambek categorial account of extraction, something which I will not go into here. This suggests strongly that perhaps an emergent account of scope-ambiguity is to be had with some system that has LCG as its core, and I will argue later that PLCG is the system that fulfils this expectation.

I will look at one more aspect of LCG’s ambiguity generation. The LCG grammar can recognise (22):

(22) John believes a man came in

However the grammar fails to allow the quantifier to have a de re interpretation. This shortcoming can be seen to be related to the failure of the grammar to give a full solution to the Simon/someone problem.

To begin with note came in has a derived categorisation np\((np\s)/s)\np\s, abbreviated as np\PV\np\s, by the following proof:

PV, np, np\s ⇒ np\s np, np\s ⇒ PV\(np\s) np\s ⇒ np\PV\(np\s) (23)

The associated term is λx^{e}λy^{(t,e,t)}[y(u_{1}^{(e,t)}(x))], assuming that u_{1}^{(e,t)} is the variable that is associated with the antecedent.

Now if the grammar provided a complete solution of the Simon/someone problem, and at least covered the local scope properties of quantifiers, we could expect that a quantifier would be combinable, in virtue of its categorisation, with an item of category np\PV\(np\s), to give an expression of category PV\(np\s), and that the associated semantic operation would be the earlier mentioned G_{Q}. Thus the meaning of the resulting combination would be:

= y^{(t,e,t)} ↦ z^{e} ↦ A(M)(x^{e} ↦ y(C(x))(z))

It is perhaps easy to see that if the grammar could assign this meaning to a man came in, it would be able to assign a de-re interpretation to a man is John believes a man came in. However, Lambek categorial grammar cannot do this, for notice that the derived categorisation of came in is an example of a category which seeks at least two arguments in the same direction. The PLCG account that will be given in section 5 is something which overcomes this ‘no two arguments in the same direction’ limitation of LCG with respect to the Simon/someone problem. Given the comments just made, it should perhaps prove unsurprising that this brings in its wake a solution to the problem of quantifier scope ambiguity.

3.2 Coordination

In the Lambek grammar given above, I mentioned no categorisation for coordination, and it can quickly be seen that no single categorisation of junctions will give coverage of all the desired cases. Just for example to cover S, IV and TV coordination, the junction will have to have impossible count properties. So, there is no pure LCG account of coordination.

However, coordination is certainly a phenomenon that people studying LCG have given their attention to, and what sometimes goes under the name of a ‘LCG account of coordination’ is obtained by combining LCG with some version of Gazdar’s account of cross-categorial coordination [Gazdar, G., 1980]. So for exampe on might suppose a generalised coordination operation, F_{C}, which would take three expressions, the first a junction, the second and third an expression of category x, and insert the junction between the second and third arguments, to give another expression of category x. Associated with this would be the semantic operation G_{C} defined earlier.

This combination of LCG with generalised coordination can deal with all the problems concerning coordination that were noted in the opening section (with the obvious proviso that the quantifiers be in Lambek recognisable positions).

To give a brief illustration, of this, first take one of the non-constituent coordination examples from earlier (many more examples are discussed in [David Dowty, 1988] and [Moortgat, 1988])

(24) dass [Horst Rosa] und [Dieter Ingrid] gefaellt I assume gefaellt is categorised as np\(np\s). Then the NP sequence, Horst Rosa has the derivable categorisation, s/(np\(np\s)), that is, ‘sentence missing verb’. The derived meaning is λf.f(r)(h). Correspondingly, Dieter Ingrid will have the derived meaning, λf.f(i)(d). Coordinating these two strings and combining with gefaellt gives:

G_{J}(∧)(λf.f(r)(h))(λf.f(i)(d))(g) = ∧(g(r)(h))(g(i)(d))

So (24) is recognised and assigned the correct meaning. Looking at the examples that I noted in section 1 under the heading ‘local scope’, one can check that indeed the junction is assigned local enough scope, and not forced to have widest scope, as the conjunction reduction analysis would entail.

Also the cases noted under the heading ‘non-local scope’, are accounted for. I will illustrate this on (12a), which is repeated below:

(25) every man and woman died

So assume every is here categorised as (s/(np\s))/cn, and let this be abbreviated as DET. man has the derived categorisation DET\(s/(np\s)), with the derived meaning λf.f(man′), which is equivalent to λfλg.f(man′)(g). Something corresponding goes for woman, and the sentence may be derived by coordination in the category DET\(s/(np\s)) followed by combination with every and died. The result is:

G_{J}(∧)(λfλg.f(man′)(g))(λfλg.f(woman′)(g))(every)(died) = ∧(every(man′)(died))(every(woman′)(died))

I have given a brief illustration of something that is established more thoroughly in [David Dowty, 1988] and [Moortgat, 1988]: that the coordination facts can be explained very easily by using the flexibility of categorisation that the Lambek calculus allows.

What we have seen overall concerning the Lambek calculus is as follows. First, that the Lambek grammar based on the most natural categorisations did not fully allow for the interchangeability of proper names and quantifiers. Second, in contrast with this rather poor outcome, the Lambek calculus also offered an attractive account of ambiguity for those cases that it covered - the ambiguity arose simply from the valid laws of category combination. Third, that although, there is no pure Lambek calculus account of coordination, a good account of all the coordination facts is obtained by combining a Lambek grammar with some variant of Gazdar+s cross-categorial coordination proposal. The simplicity of the explanation of the coordination facts seems to be a strong argument in favour of ensuring that any grammar has available the Lambek calculus based procedure for categorising strings to be coordinated.

In the following section I discuss Hendriks’ type flexibility proposal.

4 Hendriks’ type flexibility proposal

Hendriks, partly in response to the above noted shortcomings of the Lambek calculus with respect to quantification, has put forward a type-flexibility‘ account+. It and some of its drawbacks are the subject of this section.

What a flexible semantics envisages is that the usual condition on a standard Montagovian fragment that there be a function from categories to types should be relaxed to the requirement that there be a relation. Given the rule-to-rule architecture, this is likely to leave some syntactic analyses not properly interpreted, with a semantic operation invoked by the syntax but applied to objects for which it is not defined. What makes it possible to assume just a relation between categories and types, is that semantic type shifts are also assumed to be available, applicable to the arguments of a semantic operation, with the intention that these these shifts map the arguments of the operation to objects of the types for which the operation is defined.

Thus in a flexible semantics, a possible denotation of the syntactic object, F_{γ}(α, β), is G_{γ}(t_{i}(m_{1}), t_{j}(m_{2})), where t_{i} and t_{j} are type-shifts mapping m_{1} and m_{2} into types for which G_{γ} is defined. This is an example of a system that allows semantics to ‘non-deterministically’ exploit syntax, because the use of the syntactic operation, F_{γ} is compatible with a range of semantic operations, namely m_{1}, m_{2} ↦ G_{γ}(t_{i}(m_{1}), t_{j}(m_{2})).

The original motivation for a flexible semantics was that it allows the implication of semantic operations in the analysis of a sentence without the need for their reflection by possibly rather contrived syntactic operations [Benthem, 1986]. For example, consider the case of John does not snore. One could propose a unary syntactic operation mapping a sentence modifying version of not to the VP modifying version, associating with the syntactic operation the following ‘Geach’ operation:

m^{(a→b)} ↦ (w, g) ↦ x^{(c→a)} ↦ y^{(c→b)} ↦ z^{c} ↦ m(w, g)(x(z))(y(z))

However, one might complain that the syntactic operation was contrived. A flexible semantics whose set of type shifts included as t_{Geach} the above operation could explain the same facts without the contrived syntactic operation. A meaning of F_{<}(John, F_{>}(does, F_{>}(not,snore))) would be:

G_{<}([[John]], G_{>}([[does]], G_{>}(t_{Geach}([[not]]), [[snores]])))

One might hope to find a solution to at least part of the problem posed by quantification by making such a move to a flexible semantics. For quantifiers and proper names could have the same category, be introduced into sentences by the same rules, and yet have different types. According to whether a quantifier or proper name might be present, type-shifting would or would not be necessary preliminaries to the application of the semantic operation associated with the syntactic rule.

t_{Geach} might seem a promising type shift to do just this [Gamut, L.T.F., 1991]. A quantifier, of type ((e, t), t), has via t_{Geach}, also the type ((a, e, t), (a, t)), for any a. With a = e, this would allow combination with a TV, in its natural (e, e, t) type. However, this thematically misconstrues the TV QNP combination. In other cases of VP-negation, though, t_{Geach} gives just the right result.

Here it is that we come Hendriks’ account, which makes a particular proposal for the set of shifts, T, and in the context of a certain illustrative grammar. The set of type-shifts is given inductively, by way of a sequent calculus for the type-language tj→. This is the ‘Quantification calculus’, which we shall refer to as h→_{e}. Here is h→_{e}: The Quantification Calculus h→_{e}

AR (u⃗→a→v⃗→b) ⇒ (u⃗→((a→b)→b)→v⃗→b)
AL ((u⃗→(a→b)→b)→v⃗→c) ⇒ (u⃗→a→v⃗→c)
VR (u⃗→a) ⇒ (u⃗→((a→b)→b))
Cut  a ⇒ b b ⇒ c a ⇒ c

It should be noted that this is the calculus of [Herman Hendriks, 1987]. It is therefore extensional rather than intensional as is the calculus of [Herman Hendriks, 1990], and it places does not place the restrictions that the types b in AR, AL and VR be t. In exactly the same was as for l^{(/,\)}, a proof of a type-shift may be associated with a semantic operation and which operation that is is defined by means of a term-associated version of h→_{e}, which follows

Term associated h→_{e}

AR (u⃗→a→v⃗→b) : Φ ⇒ (u⃗→((a→b)→b)→v⃗→b) : λx⃗_{1}u⃗λT^{((a→b)→b)}λx⃗_{2}v⃗[T (λz^{a}[Φx⃗_{1}u⃗zx⃗_{2}v⃗])]
AL ((u⃗→(a→b)→b)→v⃗→c) : Φ ⇒ (u⃗→a→v⃗→c) : λx⃗_{1}u⃗λy^{a}λx⃗_{2}v⃗[Φ(x⃗_{1}u⃗)(λz^{(a→b)}[zy])(x⃗_{2}v⃗)]
VR (u⃗→a) : Φ ⇒ (u⃗→((a→b)→b)) : λx⃗_{1}u⃗λy^{(a→b)}[y(Φx⃗_{1}u⃗)]
Cut  _{a ⇒ b : Φ} _{b : Φ ⇒ c}_{a ⇒ c}

Flexible Montague Grammar, as defined in [Herman Hendriks, 1990], consists basically of the proposal to use the above defined set of type-shifts in combination with a simple grammar.

About this grammar we need only note the following. Proper names and quantifier are alike categorised as NP, but they are not lexically assigned the same type. Verbs combine with NP’s on the basis of the usual phrase-structure rules, with the semantic significance being always that the verb is applied to the NP. The NP argument places of verbs are type e, rather than of the quantifier type. Finally coordination is provided for in four cateogories S, V P, NP, T V, using the 2 rules schemes: for γ = AND, OR, ⟨F_{γ}, ⟨δ, δ⟩, δ⟩. The operation F_{AND} is such that F_{AND}(s_{1}, s_{2}) = s_{1} and s_{2}. Similarly for F_{OR}.

G_{AND}(m_{1}, m_{2}) = G_{J}(∧, m_{1}, m_{2}), and G_{OR}(m_{1}, m_{2}) = G_{J}(∨, m_{1}, m_{2}).

4.1 Quantification

FMG accounts for the problems posed by quantification. Obviously, the syntactic fact of the interchangeability of Simon and someone will be predicted.

The local scope properties of quantifiers are also captured, and how this is done is indicated in outline below (The notaton AR^{1} refers to the fact the AR type-shift is applied to the first argument place of a function, and a^{b} abbreviates ((a, b), b)):

Simon NP:e  died VP:(e, t)_{F_{<}} S:t  hit TV:(e, e, t)  Simon NP:e_{F_{>}} VP:(e, t)

somone NP:e^{t}  died VP:(e, t) AR^{1} VP:(e^{t}, t)_{F_{<}} S:t  hit TV:(e, e, t) someone NP:e^{t} AR^{1} TV:(e^{t}, e, t)_{F_{>}} VP:(e, t)

Besides the local scope properties of quantifiers, FMG also succeeds in covering quantifier scope ambigiuity, and two illustrtations of this are given below. The first case is the two way ambiguity of every man loves a woman

every man NP:e^{t}  loves TV:(e, e, t) a woman NP:e^{t} AR^{1} TV:(e^{t}, e, t) AR^{2} TV:(e^{t}, e^{t}, t)  _{F_{>}} VP:(e^{t}, t)_{F_{<}} VP:t  every man NP:e^{t}  loves TV:(e, e, t) a woman NP:e^{t} AR^{2} TV:(e, e^{t}, t) AR^{1} TV:(e^{t}, e^{t}, t)  _{F_{>}} VP:(e^{t}, t)_{F_{<}} VP:t

The second example is the de re/de dicto ambiguity of John believes a man came in:

John NP:e  believes PV:(t, e, t) a man NP:e^{t}  came in VP:(e, t) AR VP:(e^{t}, t)_{F_{<}} S:t_{F_{>}} VP:(e, t)_{F_{<}} S:t  John NP:e  believes PV:(t, e, t) a man NP:e^{t}  came in VP:(e, t) VR VP:(e, t^{t}) AR VP:(e^{t}, t^{t})_{F_{<}} S:t^{t} AR^{1} PV:(t^{t}, e, t)  _{F_{>}} VP:(e, t)_{F_{<}} S:t

Looking back to some of the accounts that were considered in section 2, one can wonder whether any of the objections raised against those apply to FMG. As a way to explain the interchangeability of Simon and someone, I considered the possibility of giving them the same category, and objected to the artificialy high type for proper names that this appeared to force. FMG explains the interchangeability of proper names and quantifiers exactly by giving them the same category, but under the assumptions of FMG, no artificially high type is forced on proper names, and so that objection no longer applies. Against Quantifier Lowering and Raising analyses of ambiguity, there was the objection that they gave reason to expect in natural language expressions of a kind that never do occur - expressions isomorphic to the well formed formulae of FOL. FMG is not subject to this objection either. I also mentioned Quantifier Storage, and problems for it which arose around sentences such as every representative of a company died. FMG, however, encounters no difficulties with these sentences. ^{10}

So it seems that FMG, on such counts as these, is an improvement over the accounts of scope ambiguity that I considered in section 2. FMG, however, does have some difficulties of its own. These will be looked at in section 4.3. Before that, though, I note the situation with respect to coordination.

4.2 Coordination

The FMG account is not a proposal that is intended to get cover some syntactic data that is generally found difficult to deal with in a generative grammar. It is primarily a strategy to avoid having to complicate a grammar in the face of semantic problems. So FMG does not itself have anything to say about the syntactic problem of non-constituent coordination. I will look in section 4.3 a moment at what happens when the type-flexibility idea is put into the setting of a grammatical proposal that can deal with non-standard constituent coordination.

However, restricting attention to coordination in major categories, it deserves to be noted that FMG does have the same coverage of the scope ambiguity phenomena, as had the ‘LCG account of coordination’. This is illustrated below.

An illustration is given below of how the two way ambiguity of every man and woman died is captured (q abbreviated (et, t) and d abbreviated (et, q)):

every DET:d  man CN:(et) and woman CN:(et) came in VP:(et) CONJ CN:(et)_{F_{>}} NP:q  AR^{1} VP:(qt)_{F_{<}} S:t

syntax.

10Quantifier Storage gets into the problem because it features binary semantic combinations (retrieval) whose use is completely separated from the syntax. Now, although in FMG, syntax and semantics are a little bit dislocated, the binary semantic operations are just the usual ones, and their use is strictly controlled by the

every DET:d  man CN:(et) and woman CN:(et) came in VP:(et) VR CN:(dq)  VR CN:(dq) VR DET:(dq, q)  CONJ CN:(dq)_{F_{>}} NP:q  AR^{1} VP:(qt)_{F_{<}} S:t

The way this coverage is achieved is obviously very similar to what happens in the LCG case, although it is not the case that we are simply considering notational variants here. In FMG there are the type-changes that go unaccompanied by category changes, with it being always the case in the end that it is the categories that dictate the semantic operations implicated in the derivation of a sentence. In the LCG case, one does not have this bipartite system. One might expect there to be differences in coverage between the two approaches arising from this, but in fact none such have ever been noted.

4.3 Objections to the Type Flexibility account

I mentioned that a problem for the Quantifying-in account was that it was not an emergent explanation, because the quantifying-in rule was syntactically redundant. I also argued that the Quantifier Storage account was not an emergent explanation - and this was even though no aspect of the syntax was strictly redundant. It seems to me that one can also argue that the flexibility account is not an emergent one, and again despite the fact that no aspect of the syntax is strictly redundant. In this case the non-emergence stems from the fact that one could get by with far fewer type-shifts. In fact if one had only argument raising of first arguments, then all sentences would receive an interpretation, but no sentence would receive two. In other words there is a simplification of the overall system that will lose it just the coverage of ambiguity.^{11}

Besides this, I think there are objections when the system is extended to one with larger syntactic coverage. There is a well known objection to the sufficiency of the type-shifts in a system covering reflexive pronouns, and I think a far more serious objection can be made to the overgeneration of the shifts in the context of a grammar covering non-constituent coordination. I will describe these objections in turn.

Reflexive pronouns do not occur in the FMG account. It has been observed before that if the account is extended to give some coverage of reflexive pronouns, then the resulting account semantically undergenerates. The idea is that a reflexive pronoun such as itself would be added to the grammar simply as a further member of the category NP. The type would be (eet, et), and the denotation would be the argument duplicator: f ↦ x ↦ fxx. A sentence such as the sun heats itself could then be derived, using the VR type shift to combine heats with itself. However, the sentence the sun heats itself and several small planets would receive no denotation. This is because the type-shifts do not allow a common type to be derived from the itself type, (eet, et) and the several small planets type, (et, t). Therefore, when the FMG account is altered to include reflexive pronouns, there is semantic undergeneration.

I mentioned above that the FMG account does not address the phenomenon of non-standard constituent coordination, and argued at the end of section 3 that any account of this should include a Lambek calculus based procedure for categorising strings to be coordinated. So what I will now consider is the combination of a Lambek grammar with the AR, VR and AL typeshifts, which I will call Flexible Lambek Grammar. Moortgat (1988, p238-243) also considers this account, as a natural way to obtain coverage of quantifier scope ambiguity. I will show that this semantically overgenerates.

Consider the following three instantiations of Harry believes α came in:

11Actually, in order to cover coordination of proper names with quantifiers, VR is required. So the cut-down set of shifts to consider is AR^{1} and VR applied just to e

Harry believes that \{ \begin{matrix}a man \\ John shouted and \\ John thinks that Mary \end{matrix} \} came in

Flexible Lambek Grammar is such as to suggest that the above sentences may by paraphrased as below:

\begin{matrix}(i)There is a man who \\ (ii)John shouted and is someone who \\ (iii)John thinks that Mary is someone who \end{matrix} \} Harry believes came in

Only in the case of α= a man, is this correct. The case where α = a man is given first below. It is simply a categorial transcription of the analysis given before covering the de re interpretation of a man.

John NP:e  believes (np\s)/s:(t, e, t) a man NP:e^{t}  came in np\s:(e, t) VR np\s:(e, t^{t}) AR np\s:(e^{t}, t^{t})_{F_{<}} S:t^{t} AR^{1} (np\s)/s:(t^{t}, e, t)  _{F_{>}} np\s:(e, t)_{F_{<}} S:t

For α = John shouted and or John thinks that Mary the readings (ii) and (iii) are generated by the following analysis:

Harry believes that s/s:(t, t)  α s/(np\s):(et, t)  came in np\s:(e, t) VR np\s:(e, (tt, t)) AR np\s:(((et, t), (tt, t))) VR s/(np\s):(((et, t), (tt, t)), (tt, t)) s:(tt, t) AR s/s:((tt, t), t)  s:t (26)

What is happening here is that in Flexible Lambek grammar, all that is required of an expression for it to engender ambiguity is that it have type (et, t). It is not so significant what its category is. every man engenders ambiguity whilst categorised np, and John believes that Mary engenders ambiguity whilst categorised s/(np\s). The problem with combining the type-flexibility proposal with LCG is that there will be many expressions of type (et, t), which are not quantifiers and do not cause ambiguity.

This seems to show that the type flexibility approach is not compatible with a grammar that includes a Lambek calculus based procedure for categorising strings, something which seemingly has to be there to account for non-standard constituent coordination. I take this to be the main objection against using the type-flexibility approach to give an account of quantification. A final remark on type-flexibility. One might wonder whether semantic overgeneration is a problem even when the type-flexibility is combined with a less powerful grammar than LCG. For again if there are expressions of type ((e, t), t), the flexibility approach is liable to see them as engendering ambiguity. For example, at a rudimentary level one might assign the type ((e, t), t) to an expression like is barbaric, used in sentences like to shout is barbaric, shouting is barbaric. If to shout and shouting had types (e, t), then the type-flexibility approach would allow one to interpret John thinks that to shout is barbaric as something like it is barbaric to be something that John thinks shouts.

As I mentioned at beginning of the section, the flexible semantics account was proposed in large part because it was seen that Lambek categorial grammar offered no account of quantification. In the next section, I describe the Polymorphic Categorial account, which is another response to the shortcomings of Lambek categorial grammar.

5 Polymorphic Lambek Calculus

The discussion of LCG revealed two things. First, some vary ordinary quantification structures are not generated. Second, that although LCG does not strictly contain an account of coordination, when LCG is combined with a basic mechanism for cross-categorial coordination, rather comprehensive coverage of the facts concerning coordination is obtained.

In this section a supersystem of LCG will be defined, something that I will call Polymorphic Lambek Categorial Grammar. The essential expansion is that the categorial vocabulary is extended to include category variables and their universal quantification.

The system allows an account of coordination to be directly formulated within it, in contrast to the hybrid status of the above discussed ‘LCG account of coordination. That is to say, the categorial system to be described places coordinate expressions on a par with other kinds of expressions, recognising them simply by categorial reduction rules on the basis of lexical categories, rather than recognising them by a combination of categorial reduction with some other mechanism. The system, in a sense, allows one to lexicalise the composition of G_{J} with the propositional connectives. Such a lexicalisation of coordination has been often been considered, and the system to be described gives just one particular format to the expression of this basic idea. I think the format is an attractive one, seen from the point of view of generalising architectural features of LCG - in particular the Curry-Howard isomorphism. However, more practical is the fact that one can formulate in the framework an account of quantification, an account solving the Simon/someone problem and covering quantifier scope ambiguities. This is because the system, in a sense, allows one to lexicalise the composition of G_{Q} with the generalised quantifiers.

The extended set of categories will be referred to as cat^{(/,\,∀)}. For the definition of cat^{(/,\,∀)}, a set of basic categories, bascat, must be assumed, and additionally a denumerably infinite set of category variables catvar, including, we will assume X and Y. I will use w, x, y as metavariables over cat^{(/,\,∀)} and X, Y, Z is a metavariables over catvar.

Definition 1 (The Polymorphic Categorial Language, cat^{(/,\,∀)})

(i) bascat ⊂ cat^{(/,\,∀)} (ii) if x and y are ∈ cat^{(/,\,∀)}, then x/y and x\y are ∈ cat^{(/,\,∀)}. (iii) catvar ⊂ cat^{(/,\,∀)} (iv) if Z ∈ catvar and x ∈ cat^{(/,\,∀)}, then ∀Z.x ∈ cat^{(/,\,∀)}.

Example categories of cat^{(/,\,∀)}are X, Y, X/Y, ∀X.X/Y. The intuitive idea is that an expression has a category ∀Z.x iff it has the category x[y/Z], for all y’s that may be substituted for Z.

The Polymorphic Lambek Calculus consists of the calculus l^{(/,\)} augmented by the following two rules^{12}

(∀L) \begin{matrix}U, x[y/Z], V ⇒ w \\ U, ∀Z.x, V ⇒ w \end{matrix}  (∀R) \begin{matrix}T ⇒ x \\ T ⇒ ∀Z.x \end{matrix}  [Z is not free ; in T]

In the case of LCG, expressions with categories in cat^{(/,\)} had semantic values whose types were essentially the language of implicational propositional logic, tj→. In the case of PLCG, expressions with categories in cat^{(/,\,∀)} shall have semantic values whose types are the language of quantified implicational logic, which I shall call tj^{(→,∀)}. Basically tj^{(→,∀)} allows for propositional variables and their universal quantification.

12I have given here a version of the (∀R) rule which is easier to read but slightly weaker than the ‘official’ version. See Appendix

To define tj^{(→,∀)}, a set of propositional variables, tvar, must be assumed. It will be assumed that in tvar are at least the two variables π, ω. θ is a metavariable over members of tvar. a and b serve as meta-variables over any type of tj^{(→,∀)}, the definition of which follows:

Definition 2 (tj^{(→,∀)}) a. e, t and s are ∈ tj^{(→,∀)} b. if θ ∈ tvar, then θ ∈ tj^{(→,∀)} c. if a and b are ∈ tj^{(→,∀)}then (a→b) is ∈ tj^{(→,∀)} d. if θ ∈ tvar and a is ∈ tj^{(→,∀)}, then ∀θ.a is ∈ tj^{(→,∀)}

Examples of types in tj^{(→,∀)} are (π→π), ∀π((e→π)→π) and ∀π(π→π). The intuitive idea is that a meaning of type ∀π.a is a function which takes a type b to a member of the type a[b/π].

The method for assigning meanings to strings in PLCG is akin to that in LCG. A proof, γ, of l^{(/,\,∀)} is mapped into a semantic operation, G. The operation, G, which goes with the proof, γ, is defined by the a term-associated calculus, H_{L∀}^{e}. Where the term-associated calculus for LCG featured terms of typed λ-calculus (which I will call L^{λ}), the term-associated calculus for LCG features terms of the language ‘2nd order Polymorphic λ-calculus’ (which I will call L^{(λ,Δ)}), credit for the invention of which is usually given to both Girard (1972) and Reynolds (1974).

Terms of L^{(λ,Δ)} carry their type as a superscript, and that type is drawn from tj^{(→,∀)}. One can have variables in these types (eg. λx^{π}.x^{π}), one can abstract over such variable types, deriving terms of quantified type (eg. Δπ.λx^{π}.x^{π}, of type ∀π(π→π)), and terms of quantified type can be applied to types (eg. Δπ.λx^{π}.x^{π}(t), of type (t→t)). A term (Δπ.Φ)(a) may reduce to Φ[a/π].

13

Here then is the term-associated calculus, H_{L∀}^{e}

(∀L) \begin{matrix}U, x[y/Z] : α(a), V ⇒ w : Φ \\ U, ∀Z.x : α, V ⇒ w : Φ \end{matrix}  (∀R) \begin{matrix}T ⇒ x : α \\ T ⇒ ∀Z.x : Δωα \end{matrix}  [Z is not free ; in T]

Note that in the (∀L) rule the type a is the type corresponding to the category y. By way of illustration of what has been introduced so far, (27) and (28) are examples of proofs constructed using the (∀R) and (∀L) rules respectively.

np:x^{e}, np\X:y^{(e,π)} ⇒ X:y(x) /R np:x^{e} ⇒ X/(np\X):λy^{(e,π)}.y(x) ∀R np:x^{e} ⇒ ∀X.X/(np\X):Δπ.λy^{(e,π)}.y(x) (27)

s:x^{∀π.((e,π),π)}(t)(y^{(e,t)}) ⇒ s:x^{∀π.((e,π),π)}(t)(y^{(e,t)}) np\s:y^{(e,t)} ⇒ np\s:y^{(e,t)}/L s/(np\s):x^{∀π.((e,π),π)}(t), np\s:y^{(e,t)} ⇒ s:x^{∀π.((e,π),π)}(t)(y^{(e,t)}) ∀L ∀X.X/(np\X):x^{∀π.((e,π),π)}, np\s:y^{(e,t)} ⇒ s:x^{∀π.((e,π),π)}(t)(y^{(e,t)}) (28)

(28) shows a way to derive an item of polymorphic category, ∀X.X/(np\X), from one of category np. (27) shows how to combine an item of polymorphic category, ∀X.X/(np\X), with an item of category np\s. The operation defined by (27) could be applied to an item which has a polymorphic category derivationally via (28). The result, using the above mentioned term reduction, should be:

(Δπ.λz^{(e,π)}.z(x^{e}))(t)(y^{(e,t)})

And by two steps of redunction, this is equivalent to:

▷ y^{(e,t)}(x^{e})

Actually, I am speaking a bit loosely here. Given a semantics for the terms,(27) shows a way to define a derived polymorphic meaning from any meaning, m^{e}, of type e. This meaning is not a notation, such as, Δπ.λz^{(e,π)}.z(x^{e}), and so strictly speaking, one cannot describe how this meaning combines with another using the vocabulary of term reduction. One must first show that there is a semantics for the terms involved such that the reductions preserve the denotations.

13For a formal definition of this language see the Appendix.

Doing this is not in fact completely straightforward. The problem can be seen if one looks a little more closely at what I said above was the intutive nature of an object of polymorphic type, ∀π.a: it was to be function which when applied to a type b, gave some member of a[b/π]. However, b could conceivably be ∀π.a, in which case a typical object, f, of type ∀π.a, has to be function which can apply to a set containing f. Functions, set-theoretically conceived, cannot do this.

There is a conservative and an ambitious response to this problem in defining the denotations of the terms. The conservative approach does not allow a function of quantified type to apply to a quantified type. This is the line that I have followed. The details are quite straightforward, and are given in the Appendix. The ambitious approach is exemplified by Girard, who has developed a category theoretic interpretation in which application is unrestricted. In accordance with this conservative position on the nature of functions of polymorphic type we will also observe a restriction on the use of the (∀L) rule: the category, x, chosen for the quantified variable must not itself contain quantified categories.

I will propose quantifiers to have meanings which are of type ∀π((e, π), π), and junctions which are of type ∀π(π, (π, π)). This means that they will be functions which apply to a type, a and return some object in a type depending on a. In the case of quantifiers the result will be in the type ((e, a), a), and in the case of junctions, the result will be in the type (a, (a, a)). As always, the notion of model will not allow the quantifiers and junctions to be freely interpreted in their types. Let Q_{P} be the polymorphic meaning of a certain quantifier, and let Q_{G} is to be the well-known generalised quantifier meaning, of type ((e, t), t). Correspondingly for J_{P} and J. As far as values at non-conjoinable types, Q_{P} and J_{P} are unrestricted. Within the conjoinable types they are defined recursively as follows:

Q_{P} (t) = Q_{G} Q(a→b)(P^{e→a→b})(x^{a}) = Q(b)(y^{e}→P yx)

J_{P} (t) = J_{G} J_{P} (a→b)(P_{1}^{a→b})(P_{2}^{a→b})(x^{a}) = J_{P} (b)(P_{1}x)(P_{2}x)

The above represents the ‘meaning postulate’ for quantifiers and junctions. One might wonder whether this postulate could be given by using the technique of ‘complex translations’. That is one might hope to specify the polymorphic version of a quantifier or junction by giving a term of L^{(λ,Δ)}, whose only free variable is a slot for the familiar meanings of the quantifiers or junctions. The impossibility of using this strategy in the present case is discussed in the Appendix.

I defined a Lambek grammar in section 3. I will discuss now a corresponding Polymorphic Lambek grammar. It is exactly the same as the earlier grammar except that (i) the categorisations of the quantifiers is different and (ii) the junctions appear amongst the lexical items. The quantifiers will have the categories ∀X.X/(np\X) and ∀X.(X/np)\X. The junctions will have the category ∀X.(X\X)/X. The category to type-correspondence is as before with the addition that ν(X) = π, ν(Y) = ω, ν(∀Z.x) = ∀ν(Z).ν(x).

The coverage of this polymorphic grammar will be described below. However, before proceeding to this empirical part, it may be proper to insert here some comments locating the current proposal in a wider historical and theoretical setting. I am discussing here a grammar which adds variables and their universal quantification to the basic categorial language. There have been proposals to add variables to a categorial grammar before [Zeevat et al, 1987], [Benthem, 1991], and indeed to give quantifiers and junctions categories involving variables just like those above, but with the omission of the universal quantifier. Such systems have in place of (∀L) and (∀R), a rule allowing a sequent with variables to be derived if a substitution instance of it can be derived. While there is a connection between l^{(/,\,∀)} and what might be called l^{(/,\)} plus substitution, the exact nature of this relation has yet to be clearly established. One might, for example, imagine that l^{(/,\)} plus substitution is effectively the restriction of l^{(/,\,∀)} to sequents whose quantifiers are outermost. However, the sequents s/X, np ⇒ s and np ⇒ s/(X\s) would be derivable in l^{(/,\)}plus substitution, but only in the first case does adding an outermost universal quantifier give a derivable sequent of l^{(/,\,∀)}. What seems clear is that for both systems there is a difficulty in constructing a decision procedure, because both calculi allowing for inference steps involving open-ended choice. Decidability for both is an open question. For a proof there is a decision procedure for l^{(/,\,∀)} as applied to a certain subclass of sequents see [Emms, M., 1993], building on work in [Moortgat, 1988], and [Benthem, 1991] on l^{(/,\)} plus substitution.

To return to now to empirical linguistic matters, I will describe now the coverage as regards quantificational phenomena. Coordination I will not say anything specifically about. This is because, as I mentioned at the outset, the PLCG account of coordination is the lexicalisation of the ‘LCG account of coordination’ - the hybrid of LCG with cross-categorial coordination. It should be clear that the PLCG account achieves at least the same coverage of the coordination data. In the Appendix there is an argument that a junction can be given arbitarily wide scope.

5.1 Quantification

As far as allowing for the interchange of proper names with quantifiers, in the case of LCG we could generate only the first two out of the following fours pairs of sentences. Under the present PLCG grammar all can be generated.

Simon someone } came

John loved {Simon someone

John gave \left\{{Simon \atop someone}\right\} Mary

John told {Simon someone to go

Then there is the question of the local scope properties of quantifiers, which is the question whether the sentences above are assigned appropriate meanings. This is the case. Here for example is the denotation of John gave someone Mary:

SOMEONE_{P} (eet)(gave)(m)(j) = SOMEONE_{P} (et)(y ↦ gave(y)(m))(j) = SOMEONE_{P} (t)(y ↦ gave(y)(m)(j)) = SOMEONE_{G}(y ↦ gave(y)(m)(j))

That this PLCG grammar will deal with interchangeability and the local scope properties of quantifiers is perhaps not surprising. Less obvious, is the fact scope ambiguity is also dealt with. I will now go through some examples of this.

First I will consider the two way ambiguity of a nun liked every boy. The subject wide scope reading is obtained on the basis of the following proof in l^{(/,\,∀)}, using the abbreviation x^{y∧} = y/(x\y), x^{∧y} = (y/x)\y):

s:AN(t)(P) ⇒ s:Φ  ⋮ TV:like, np^{∧(np\s)}:EB(et) ⇒ np\s:P ∀L TV:like, ∀Y.np^{∧Y}:EB ⇒ np\s:P /L np^{s∧}:AN(t), TV:like, ∀Y.np^{∧Y}:EB ⇒ s:Φ ∀L ∀X.np^{X∧}:AN, TV:like, ∀Y.np^{∧Y}:EB ⇒ s:Φ

I have left some of the semantic terms associated with succedent categories as unknowns in the above. On can quickly determine that P = EB(et)(like), and that so Φ = AN(t)(EB(et)(like)).

On this basis we have for a possible denotation of a nun liked every boy:

AN_{P} (t)(EB_{P} (et)(L)) = AN_{P} (t)(x ↦ EB_{P} (et)(L)(x)) = AN_{P} (t)(x ↦ EB_{P} (t)(y ↦ Lyx)) = AN_{P} (t)(x ↦ EB_{G}(y ↦ Lyx)) = AN_{G}(x ↦ EB_{G}(y ↦ Lyx))

The object wide scope reading is obtained on the basis of the following proof, using the abbreviation g = ((e, t), t):

⋮  ∀X.np^{X∧}:AN ⇒ np^{s∧}:AN(t) s:EB(gt)(P)(AN) ⇒ s:Φ TV:like ⇒ (NP^{s∧}\s)/np:P  \L ∀X.np^{X∧}:AN, np^{s∧}\s:EB(gt)(P) ⇒ s:Φ\L ∀X.np^{X∧}:AN, TV:like, np^{∧(np^{s∧}\s)}:EB(gt) ⇒ s:Φ∀L ∀X.np^{X∧}:AN, TV:like, ∀Y.np^{∧Y}:EB ⇒ s:Φ

The solution for P is λyλG.G(like(y)), so Φ = EB(gt)(λyλG.G(like(y)))(AN). On this basis we have as another possible denotation of a nun liked every boy

EB_{P} (gt)(y, G ↦ G(like(y)))(AN_{Q}(t)) = EB_{P} (t)(y ↦ AN_{G}(like(y))) = EB_{G}(y ↦ AN_{G}(x ↦ like(y)(x)))

There are several other possible derivations of these same two readings of the sentence. This was one which could have been handled with a Lambek grammar, as was pointed out earlier. The next example is the de re intepretation of an embedded quantifier, which could not be handled with a Lambek grammar. As will be seen, PLCG succeeds, where LCG fails because there is not the ‘no two arguments in the same direction’ restriction on categories that a quantifier may combine with. The de re reading is obtained on the basis of the following proof, using the abbreviation \overline{X} = ((np\s)/s)\(np\s):

⋮  ⋮ np:j, (np\s)/s:bel, \overline{X}:EM(tet, et)(P) ⇒ s:Φ np:x, np\s:walk ⇒ \overline{X}:λfλy[f(walk(x))(y)]\R np\s:walk ⇒ np\\overline{X}:P /L np:j, (np\s)/s:bel, \overline{X}/(np\\overline{X}):EM(tet, et), np\s:walk ⇒ s:Φ∀L np:j, (np\s)/s:bel, ∀X.X/(np\X):EM, np\s:walk ⇒ s:Φ

Here we have P = (λxλfλy[f(walk(x))(y)]), and so Φ = EM_{P} (tet, et)(λxλfλy[f(walk(x))(y)])(bel)(j)

So a possible denotation for John believes every man walks is:

EM_{P} (tet, et)(x, f, y ↦ f(walk(x))(y))(bel)(j) = EM_{P} (et)(x, y ↦ bel(walk(x))(y))(j) = EM_{P} (t)(x ↦ bel(walk(x))(j)) = EM_{G}(x ↦ bel(walk(x))(j))

The next case I want to look at is the reading of every man told a woman to go where a woman has wide scope. This was one of those sentences that was not even generated by the earlier Lambek grammar. First, let me review how the previous case was handled. Repeating the proof without the semantic terms we have: (using PV for (np\s)/s):

np,PV, PV\np\s) ⇒ s np, PV, np, np\s ⇒ s \R\R\R np\s ⇒ np\(PV\(np\s))/L np,PV, (PV\(np\s))/(np\(PV\(np\s))), np\s ⇒ s∀L np,PV,  ∀X.X/(np\X)  , np\s ⇒ s (29)

The proof may be seen as built up from a proof of np,PV, np, np\s ⇒ s. This sequent differs from the concluding sequent only by the presence of np instead of ∀X.X/(np\X).

Therefore we might get the desired reading of every man told a woman to go by starting from a proof of ∀X.X/(np\X), ((np\s)/vpc)/np, np, vpc ⇒ s, and building from it to a proof of ∀X.X/(np\X), ((np\s)/vpc)/np, ∀Y.(Y/np)\Y, vpc ⇒ s, on the model of (29). Here then is a proof of ∀X.X/(np\X), ((np\s)/vpc)/np, np, vpc ⇒ s:

s ⇒ s np\s ⇒ np\s vpc ⇒ vpc np ⇒ np /L s/(np\s), np\s ⇒ s  /L s/(np\s), (np\s)/vpc, vpc ⇒ s  /L s/(np\s), ((np\s)/vpc)/np, np, vpc ⇒ s (∀L) ∀X.X/(np\X), ((np\s)/vpc)/np, np, vpc ⇒ s (30)

Building on this in an analogous way to (29) would lead to the following (using T V V P for ((np\s)/np)/vpc):

s ⇒ s _{np\s ⇒ np\s} _{vpc ⇒ vpc} _{np ⇒ np}_{s/(np\s), np\s ⇒ s}_{s/(np\s), (np\s)/vpc, vpc ⇒ s}_{s/(np\s), ((np\s)/vpc)/np, np, vpc ⇒ s}_{(∀L)}_{∀X.np^{X∧}, ((np\s)/vpc)/np, np, vpc ⇒ s}  _{⋮}_{T V V P ⇒ ((∀X.np^{X∧}\s)/vpc)/np}  _{∀X.np^{X∧}, ((∀X.np^{X∧}\s)/vpc), vpc ⇒ s}_{(/L)}_{∀X.np^{X∧}, T V V P, (((∀X.np^{X∧}\s)/vpc)/np)\((∀X.np^{X∧}\s)/vpc), vpc ⇒ s}_{(∀L)}_{∀X.np^{X∧}, T V V P,  ∀Y.(Y/np)\Y  , vpc ⇒ s} (31)

However, this is not a possible proof, as in the last step, the (∀L) inference, as value for Y, the following is chosen, with abbreviations now done away with:

(((∀X.X/(np\X))\s)/vpc)/np

This is a category in which a polymorphic quantifier categorisation figures and is therefore not a possible instantiation if we are to abide by the restriction on variable instantiation that we have decided upon. All is not lost, however.

(31) is built upon (30). In (30) there is there is a (∀L) inference involving ∀X.X/(np\X), at which point X is instantiated to s. This is in fact the last step of (30). Dropping this last step from (30) we have a a proof of s/(np\s), T V V P, np, vpc ⇒ s. We will now build on this proof in somewhat the fashion that we built upon (30):

s ⇒ s _{np\s ⇒ np\s} _{vpc ⇒ vpc} _{np ⇒ np}_{s/(np\s), np\s ⇒ s}_{s/(np\s), (np\s)/vpc, vpc ⇒ s}_{s/(np\s), ((np\s)/vpc)/np, np, vpc ⇒ s}  _{⋮}_{np^{s∧}, ((np^{s∧}\s)/vpc), vpc ⇒ s}_{T V V P ⇒ ((np^{s∧}\s)/vpc)/np}  _{∀L}_{∀X np^{X∧}, ((np^{s∧}\s)/vpc), vpc ⇒ s}_{(/L)}_{∀X np^{X∧}, T V V P, (((np^{s∧}\s)/vpc)/np)\((np^{s∧}\s)/vpc), vpc ⇒ s}_{(∀L)}_{∀X np^{X∧}, T V V P,  ∀Y.(Y/np)\Y  , vpc ⇒ s} (32)

This proof will give the desired reading of every man told a woman to go. The term for the proof is

{AW ((et, e^{t}, t))(P)(go)(EM(t)) \atop where P = λy_{1}^{e}λy_{2}^{(et)}λy_{3}^{e^{t}}[y_{3}(told(y_{1})(y_{2}))]} ; (33)

AW_{P} (et, e^{t}, t)(d_{1}^{e}, d_{2}^{et}, d_{3}^{e^{t}} ↦ d_{3}(told(d_{1})(d_{2})))(go)(EM_{P} (t)) = AW_{P} (e^{t}, t)(d_{1}^{e}, d_{3}^{e^{t}} ↦ d_{3}(told(d_{1})(go)))(EM_{G}) = AW (t)(d_{1}^{e} ↦ EM_{G}(told)(d_{1})(go)) = AW_{G}(d_{1}^{e} ↦ EM_{G}(told)(d_{1})(go))

These three examples should give a fair idea of the approach to ambiguity that is made possible with this polymorphic grammar. I have given in the Appendix an argument that for all sentences containing a quantifier that are recognised by the grammar, the quantifier can be given arbitrarily wide scope.

If it is granted then that this polymorphic grammar is an empirically adequate explanation of the relevant facts concerning quantification, the question then arises of whether it is subject to any of the objections that were brought to bear on the non-type-driven accounts in section 2, and on the type-flexibility account in section 4.

First, we can observe that Simon and someone have different categories according to this PLCG account (these categories also are not equivalent: we have np ⇒ ∀X.X/(np\X), but not ∀X.X/(np\X) ⇒ np) I mentioned in section 2 that to give Simon and someone different categories is one strategy for responding to the fact that they have apparently different types. This, I said, would be subject to a PV objection, namely that it would become as easy to write a grammar in which Simon and someone can be interchanged, as one in which they are not. I would argue that this PLCG account is not subject to this PV objection. The difference is this. When the overall grammatical framework is PS-grammar, I can deduce nothing about the behaviour of proper names and quantifiers if I am simply told that in all languages the proper names have category PN and the quantifiers have category Q. I must wait to hear the PS rules. However, when the overall grammatical framework is PLCG-grammar, I can deduce something about the behaviour of proper names and quantifers if I am told their categories. This is the essential aspect of a type-driven approach. In particular, if I propose within the PLCG framework to categorise proper names as npand the quantifiers as ∀X.X/(np\X) and ∀X.(X/np)\X, this implies their interchangeability, as follows.

Suppose that U, np, V ⇒ w is derivable, for some U, V, one of which is non-empty (say V). It follows that U, ∀X.X/(np\X), V ⇒ w. See the left hand derivation below.^{14} On the other hand suppose that U, ∀X.X/(np\X), V ⇒ w is derivable. It follows that a Cut based derivation of U, np, V ⇒ w can be given, see the right hand derivation below. So by Cut Elimination, a Cut-free derivation (For the proof of Cut-elimination for l^{(/,\,∀)}, see [Emms, M. and Leiss, H., 1993]).

14Actually this needs to be qualified, for if U contains quantified categories, then the instantiation of the quantifier in will not be quantifier free. For a refined version of this interchangeability argument see the Appendix.

⋮  ⋮ U, np, V ⇒ w ⋮ V ⇒ np\(U\w) U, U\w ⇒ w  /L U, (U\w)/(np\U\w), V ⇒ w∀L U, ∀X.X/(np\X), V, ⇒ w  ⋮  ⋮ np ⇒ ∀X.X/(np\X) U, ∀X.X/(np\X), V ⇒ wCut U, np, V ⇒ w (34)

It was objected against Quantifier Lowering and Raising analyses of ambiguity, that because of their insertion and movement operations one should expect natural language that are isomorphic to the well formed formulae of FOL. The above PLCG accounts involves only concatenative operations, so this objection does not apply. Amongst the objections to Quantifier Storage, there were the problems centering around sentences such as every representative of a company died. PLCG also encounters no difficulties with these sentences. All of these positive points we were able to make concerning the flexible semantics proposal, FMG. I will now discuss those areas in which the PLCG account has some special advantage.

Against the FMG account of ambiguity, and indeed the others looked at in section 2, there was the objection that they are not emergent explanations of scope ambiguity. They all have some kind of ‘special purpose’ element for accounting for ambiguity, and allows that simplifications could be made which take away the ambiguity but leave intact syntactic facts.

The PLCG account of ambiguity, I would argue, is an emergent one. It is impossible to make simplifications that would take away the ambiguity but leave intact syntactic facts.

Two factors are crucial to PLCG’s ability to account for ambiguity. The first is the ability to raise the arity of functions by use of the (Slash R) inferences. The second is the polymorphism of the logical constants that leaves them able to combine with an adjacent item when that item has undergone arity raising. Neither of these seem to be special purpose mechanisms for ambiguity. Pushing the issue further, let us see whether anything other than ambiguity would be lost if one either made unavailable the (Slash R) inferences or lessened the extent of polymorphism.

John told (Mary to go) and (Jack to stay) is an example of non-constituent coordination. For PLCG to derive this sentence, the sequent np, vpc ⇒ x must be derivable in l^{(/,\)} for some x. Without using (Slash R) inferences, there are no such x. With the (Slash R) inference, a value for x could be ((VP/vpc)/np)\VP. Therefore making the (Slash R) inferences unavailable would lose the grammar not only the account of ambiguity but also the account of non-constituent coordination.

The PLCG account given above was one not covering extraction constructions. The standard categorial approach to extraction constructions would simply be to add relative pronouns to the lexicon, categorised as (cn\cn)/(np\s) and (cn\cn)/(s/np). However, as with non-constituent coordination, the success of this depends on having the (Slash R) inferences available. Therefore, once again, making the (Slash R) inferences unavailable would lose the grammar not only the account of ambiguity but also the account of extraction.^{15}

The second option for removing the explanation of ambiguity from the PLCG is to somehow lessen the extent of the polymorphism of the logical constants. The problem with this is not so much that this is a ‘simplification’ that has unwanted side-effects, but that it is not a simplification at all. For example one could leave the constants with their quantified categorisations but alter the (∀ L) rule to allow only particular instantiations of the categorisations. However, adding such side-conditions is seems a complication of the theory, not a simplification of it. Instead of changing anything on the categorisation side, one could revise the meaning postulates to subtract from the number of types at which the functions are significant. Again this is more of a complication than anything else, and to do it in such a way that just the account of ambiguity is lost is difficult. For example, in 1 to 5 below, the skeletal indications are given of a number of analyses possible in PLCG. 1 and 2 allow a wide-scope interpretation of a man in John believes that a man came in, whereas 3, 4 and 5 account for certain local scope properties. In order to subtract just ambiguity, 1 and 2 must be made semantically insignificant and yet 3,4, and 5 left significant. This requires making the determiner function not significant at the types for certain unary functions: D_{((t,t),t)}, and for certain binary functions: D_{((t,e,t),e,t)}, whilst leaving the determiner function significant at the types for other unary functions:D_{(e,t)} and other binary functions, D_{(e,e,t)} or D_{(et,e,t)}.

15Note, however, that the standard categorial account of extraction is not wholly persuasive, being limited to ‘peripheral’ extraction. In section 7 a possible PLCG solution to this problem is discussed.

1. [John believes that]_{s/s} [a man] [came in]_{np\((s/s)\s)}

2. [John]_{np} [believes that]_{(np\s)/s} [a man] [came in]_{np\(np\s/s)\np\s}

3. [John]_{np} [loves]_{(np\s)/np} [a man]

4. [John]_{np} [gave]_{((np\s)/np)/np} [a man] [Bill]_{np}

5. [dog]_{cn} [near]_{(cn\cn)/np} [a man]

To summarise the previous three paragraphs then, it appears that the PLCG account is emergent: the explanation of ambiguity emerges from features of the account whose purpose is to explain features of the language other than its ambiguity. This argument is reinforced if one considers the Rodman sentences, which were the primary source of evidence that ambiguity should be emergent.

Recall that Rodman observed that (35a) is an island-constraint violating extraction, and that (35b) is not interpretable as (35c):

a. (every room that Guinevere has a bone which is in)_{∀X.np^{X∧}} b. Guinevere has a bone which is in every room c. every room is such that Guinevere has a bone which is in it (35)

The PLCG grammar given here overgenerates in both of the above respects. However, interestingly any steps taken to modify the PLCG account so as to account for the fact that (35a) is underivable seem likely to also rule out (35c) as a reading of (35b). There follows an example of this. (35a) could not be derived if (36a) could not be, and this requires that the sequent (36b) be underivable:

a. (Guinevere has a bone which is in)_{(s/np)}

b. np, (np\s)/np, (∀Y.np^{∧Y})/cn, (cn\cn)/(np\s), (np\s)/np ⇒ s/np (36)

(36b) would be underivable if one had as a side condition to the (/R) inference that amongst the antecedents one could not have the relativiser categorisation, (cn\cn)/(np\s). (36b) is also a subgoal of the obvious way to derive reading (35c), so the side-condition to the (/R) inference would also rule out this route to the semantic overgeneration. There are several other routes to be considered, but all in fact are ruled out by the side-condition to the (/R) inference. Furthermore such a restriction to the (/R) need not be as ad hoc as it at first seems. One could argue that this island constraint phenomenon is a reflection of a locus of non-associativity in the language. Equivalent to the Lambek calculus would be a calculus whose antecedents were binary bracketted, but with structural rule available licensing arbitrary rebrackettings. This reflects the assumed associativity of the binary operation in the string-semantic models mentioned earlier. If we assumed, however, that the relativiser word is an exception to the associativity axiom, it would obviously be no longer appropriate to have an unrestricted rebracketting rule: it should not apply when the rebracketting would assume an associativity property that the relativiser does not have. Looking at (36b) again, in which ever way we assume the antecedent to be bracketted, it needs to be rebracketted if the sequent is to be derivable by an application of the (/R) rule, and hence we get the restriction on the application of (/R) when there is a relativiser amongst the antecedents.

Besides being an emergent account of ambiguity, this PLCG account does not suffer from the two other drawbacks facing the flexible semantics account which were pointed out in in section 4.3.

Thus there is not the strange obstacle to conjoining a quantified object NP and a reflexive. Neither are there the severe semantic overgeneration problems which were shown to afflict the combination of the Lambek calculus with the type-shifting machinery. In other words we do not have that Harry believes that John thinks that Mary came in can have the meaning John thinks that Mary is someone who Harry believes came in.

A final point of comparison that can be made is this. The PLCG grammar deals with coordination and quantification via the same expressive resources - variables and the universal quantification. Many people favour an approach to coordination that is essentially the same as that mentioned in the above PLCG grammar, and so make some use of the expressive resources of variables and their universal quantification. Because it is possible to account for quantification using the same resources, it would seem unmotivated to seek an account of quantification using other devices.

I will leave the discussion of PLCG for the moment, turning in the next section to one further instance of ‘type-driven’ account that has been proposed for quantification. I will return in section 7 and the Appendix to PLCG.

6 Moortgat’s Quantor Type proposal

PLCG consists of a certain kind of extension of the Lambek calculus. Moortgat has explored some other kinds of extension which might lead to an account of ambiguity. In [Moortgat, 1988] and [?], the possibility to use ‘extraction’, ↑, and ‘infixation’, ↓, connectives is discussed. x ↑ y would be the category of expressions having a slot into which if y expressions were inserted, x expressions would result. x ↓ y would be the category of expression such that when infixed into y expressions the result is an x expression. The reason why this bears on quantification, Moorgat argues, is that a quantifier might be categorised as s ↓ (s ↑ np) – they are infixed into expressions which themselves have a gap. Ignoring for the moment the difficulty that the sequent system is suited only to the expression the right rule for ↑ and the left rule for ↓, one can see on the basis of these rules, how an account of quantification could be obtained. These are the rules:

T_{1}, y : u, T_{2} ⇒ x : Φ ↑R T_{1}, T_{2} ⇒ x ↑ y : λu.Φ  U, x : α(β), V ⇒ w T_{1}, T_{2} ⇒ y : β ↓L U, T_{1}, x ↓ y : α, T_{2}, V ⇒ w

On this basis, (37a) would be a derivable rule:

a.  T_{1}, np : u, T_{2} ⇒ s : Φ T_{1}, s ↓ (s ↑ np) : α, T_{2} ⇒ s : α(λu.Φ) (37)  b.  T_{1}, T_{2}, np : u ⇒ s : Φ T_{1}, s ↓ (s ↑ np) : α, T_{2} ⇒ s : α(λu.Φ)

There is clearly a close correspondence between (37a) and Montague’s quantifying-in rule, so one can be sure to be able to reproduce typical Montagovian analyses of scope ambiguity. However, (37b) is also a derivable rule, and this will allow thematic roles to be misconstrued. This problem arises from the fact that with quantifiers in the category s ↓ (s ↑ np), they would be able to infix themselves anywere inside a string of category (s ↑ np), and not just at the location of the ‘gap’.

The response taken to this in [?] was to introduce a new binary category connective, the ‘quantor’, ˆ , and rules for it, with the idea that xˆ y behaved like that specialisation of y ↓ (y ↑ x) that quantifiers represent. The following rules were proposed (note that the left rule is more or less the above derived rule (37a).

7 FURTHER DISCUSSION OF POLYMORPHIC LAMBEK CATEGORIAL GRAMMAR35

U, x : u, V ⇒ y : Φ U′, y : α(λu.Φ), V′ ⇒ wˆ L U′, U, xˆ y : α, V, V′ ⇒ w  U ⇒ x : Φ  ˆ R U ⇒ xˆ y : λP.P (Φ)

Since then Moortgat [Moortgat, 1992] and a number of other authors, have argued for a move to calculi whose declarative unit is a pair consisting of a category and a string-description, so-called labelled deduction. This move aids the formulation of a complete set of rules for ↑ and ↓, but it remains the case that s ↓ (s ↑ np) is not an apt categorisation for quantifiers (see above reference p14). In a move parallel to the above mentioned ‘quantor’ type proposal, Moortgat argues for bringing in additional binding connectives within the labelled deductive framework, where instead of xˆ y there is three part q(x, y, z), where z is intended to reflect the fact that after the infixation of the quantifier in the ‘y missing x’ constituent, the result may be different to y. The left rule for this q connective is the obvious correspondent of (ˆ L) rule above, transposed into a labelled deductive framework. There follow some comments directed towards the ‘quantor type’ proposal concerning quantification. However, they carry over to the labelled deductive proposal.

My first observation is that although one categorisation for quantifiers will suffice for syntactic purposes, namely npˆ s, this will not suffice for semantic purposes. Consider the following:

a. every dog near a door died

b. I must see a doctor

c. Ich muß einen Arzt sehen

d. John seeks 30% of the shops on 2 streets (38)

If a door has the category npˆ s, then (38a) can be generated, but a door will be forced to have widest scope. If the grammar attempts to take seriously the difference between finite and nonfinite VP’s, then one might give see and must in (38b) the categories: vpnf/np and (s\np)/vpnf. Then, although (38b) can be generated using the category npˆ s for a doctor, the quantifier will be forced to have widest scope, and to be therefore interpreted de re. (38c) illustrates the zame thing for German. The semantic challenge posed by (38a-c) could be met if the quantifier had the additional categories npˆ cn, and npˆ vpnf. (38d) is intended to show the need for a further categorisation, npˆ (npˆ s), in order to handle a reading where 2 streets has wide scope with respect to 30%, but is de dicto nonetheless. Now all these cases can be captured by multiplying the category assignment, but if this move is made in response simply to semantic pressure, then the emergence objection looms large: a semantically adequate version of the proposal is open to simplifications that would lose the account only certain readings, and would leave syntactic coverage unaffected.

The second observation is simply a repeat of what I said at the end of the previous section. The addition of the connectives under discussion here says nothing per se about coordination, and the background assumption is that it will be dealt with by something which is essentially the same as the PLCG account of coordination. As demonstrated above, the mechanisms for coordination already suffice for quantification, and to that extent the further connectives aimed at quantification are unmotivated.

7 Further discussion of Polymorphic Lambek Categorial Grammar

In sections 2 through to 6 I have focussed on possible approaches to quantification and coordination, and given some reasons for preferring the PLCG account over a number of other accounts which are roughly equally able to cover the data in question. Leaving behind now this particular empirical issue, I would like to finish by looking first at a number of further areas of coverage that are under exploration within the polymorphic framework, and second some of the metamathematical questions arising.

EXTRACTION AND POLYMORPHISM Full coverage of extraction has been something that has proven impossible for LCG. Turning to extraction, PLCG offers the possibility of extending the coverage over that possible within LCG. LCG allows only for those cases where the ‘gap’ for the ‘extracted’ NP is in sentence initial or sentence final position. Thus (39a,b) can be captured in LCG but not (39c) (the brackets mark a ‘sentence but for missing NP’ string, and e marks where the missing NP should go):

a. the man who (e killed the dog) b. the dog which (the man killed e) c. the man who (John told e to kill the dog)

(39)

There is actually a way in PLCG to cover these cases of non-peripheral extraction like (39c). The relativiser is categorised as: ∀X.(cn\cn)/(X\s)/(X)/np). The above non-peripheral extraction would be captured by choosing as value for X (at a ∀L) inference), X = s/vpc. The meaning of the relativiser that is appropriate to this categorisation would be (under an extensional typing regime):

whatever type a, whatever P_{1}^{(e,a)}, whatever P_{2}^{(a,t)}, whatever P_{3}^{(e,t)}: [[who]](w, g)(D_{a})(P_{1})(P_{2})(P_{3}) = x^{e} ↦ (P_{2}(P_{1}x) ∧ (P_{3}x)

For a full coverage of extraction, one would also have to retain the usual categorial categorisations of the relativiser, (cn\cn)/(s/np) and (cn\cn)/(np\s). There are, by now, quite a large number of other categorial solutions to the problem of non-peripheral extraction. Above mentioned was ‘extraction connective’ proposal, stemming from [Moortgat, 1988]. There is also the ‘permutation modalities’ proposal stemming from in [Morrill et al, 1990]. A systematic comparison of these different approaches would take us too far afield in the present paper, but is obviously a priority in future work.

DYNAMICS AND POLYMORPHISM Briefly in the above, when describing Montague+s PTQ proposal, I mentioned the question of the coverage of anaphora, which is the other thing that the ‘Quantifying-in’ rule in PTQ does besides generating scope ambiguities. Now if ‘Quantifying-in+ were the only possible account of anaphora, one would have to suppose that on top of the PLCG account of ambiguity one also has the ‘Quantifying-in’ rule. Such a composite account would be very unattractive, because the ‘Quantifying-in’ rule would make the entire PLCG account of (quantifier-induced) ambiguity redundant. Therefore, advocating the PLCG approach to ambiguity seems to go hand in hand with advocating some account other than ‘Quantifying-in’ for pronoun binding phenomena. The natural candidate to fill this role is Groenendijk and Stokhof’s ‘dynamic-semantics’ account [G. Groenendijk and M. Stokhof, 1991]. This captures the semantic force of pronoun-containing sentences (and discourses) in an essentially different way to the PTQ account, and it is not the case that the account itself explains quantifier induced ambiguities. Combination of PLCG with the DMG account of pronoun binding would not therefore render the PLCG account of (quantifier-induced) ambiguity redundant. For illustration of the fact that a dynamic semantics account is very compatible with a PLCG account, an indication is given below of a ‘dynamicsemantics’ model.

A set of states, S is assumed, and the type ∗ ranges over them. The typical PTQ typings of expressions are roughly changed from (a, t) to (a, T), where T = ((∗, t), t). A possible model meets the following conditions:

Update: in D_{(∗,e)} are discourse markers, d_{n}, and whatever d_{i}, whatever state s, whatever x^{e}, there exists a unique state s′ such that d_{i}(s′) = x, and whatever j, j ≠ i, d_{j}(s) = d_{j}(s′).

This s′ will be notated as s_{x}^{d_{n}}

CN: there exists a d^{(s,e,t)}, call it man′, such that, [[man_{n}]](w)(s)(x^{e})(p^{∗t}) = 1 iff man′(w)(x) = 1 and p(s_{x}^{d_{n}}) = 1

VP: there exists a d^{(s,e,t)}, call it won′, such that,[[won]](w)(s)(x^{e})(p^{∗t}) = 1 iff won′(w)(x) = 1 and p(s) = 1 DET: [[a]](w)(s)(P^{(s,∗,e,T)})(Q^{(s,∗,e,T)})(p^{∗t}) = 1 iff there is an x^{e} such that P (w)(s)(x)(s′ ↦

Q(w)(s′)(x)(p)) = 1

PV: there exists a d^{(s,st,e,t)}, call it bel′, such that, [[believes]](w)(s)(Φ^{(s,∗,T)})(x^{e})(p^{∗t}) = 1 iff bel′(w)(w′ ↦ Φ(w′)(s)(p))(x) = 1 and p(s) = 1

PRO: [[he_{n}]](w)(s)(P^{(s,∗,e,T)})(p^{∗t}) = 1 iff P (w)(s)(d_{n}(s))(p) and p(s) = 1

Then instead of the generic, intensional function application operation of PTQ, one can assume that all steps of syntactic concatenation are associated with the operation G_{>_{i}}, defined:

G_{>_{i}}(m_{1}^{((s,∗,a),b)}, m_{2}^{a})(w, s) = m_{1}(w, s)((w′, s′) ↦ m_{2}(w′, s′))

In such a system it is possible for a man_{n} believes he_{n} won to receive its proper anaphoric interpretation, as follows (true is the characteristic function of S)

(i) [[a man_{n} believes he_{n} won]](w)(s)(true) = 1 ↔ there is an x^{e} such that (ii) [[mann]](w)(s)(x)(s′ ↦ [[believes he_{n} won]](w)(s′)(x)(true)) = 1 (ii) ↔ man′(w)(x) = 1 and (iii) [[believes he_{n} won]](w)(s_{x}^{d_{n}})(x)(true) = 1 (iii) ↔ [[believes]](w)(s_{x}^{d_{n}})(w′ ↦ s′ ↦ [[he_{n} won]](w)(s′))(x)(true) = 1 ↔ bel′(w)(w′ ↦ [[he_{n} won]](w)(s_{x}^{d_{n}})(true))(x) = 1 ↔ bel′(w)(w′ ↦ [[hen]](w′)(s_{x}^{d_{n}})(w′ ↦ s′ ↦ [[won]](w′)(s′))(true))(x) = 1 ↔ bel′(w)(w′ ↦ [[won]](w′)(s_{x}^{d_{n}})(d_{n}(s_{x}^{d_{n}}))(true))(x) = 1 ↔ bel′(w)(w′ ↦ won′(w′)(x))(x) = 1 Combining (i), (ii) and (iii): [[a man_{n} believes he_{n} won]](w)(s)(true) = 1 iff there is an x such that man′(w)(x) = 1 and bel′(w)(w′ ↦ won′(w)(x))

It is because of the uniformity of the semantic operation, that there is no obstacle to combining the essential ideas of DMG with LCG or PLCG - so long as the proof-to-operation map is changed in the appropriate way. The further details of such a combination of polymorphism with dynamics is another area for further research.

INTERROGATIVES AND POLYMORPHISM

There is some possibility of a PLCG treatment of interrogatives, the initial outlines of which are given below.

The starting point is the semantic analysis of interrogatives that has been proposed by Groenendijk and Stokhof [G. Groenendijk and M. Stokhof, 1991] (henceforth G+S 90). They have proposed an analysis of both embedded (40a) and unembedded (40b) interrogatives:

a. Mary knows who came in

b. who came in (40)

(40b) is interpreted ‘categorially’ (as they put it), as a one-place function, roughly the set of people that came in: [[(40b)]](w, g) = x^{e} ↦ [[came in]](w, g)(x)

With this semantic value for (40b), they can explain the question-answer relation between (40b) and an answer such as John. From the ‘categorial’ interpretation of a question, [[Q?]]_{C}, a ‘propositional’ interpretation, [[Q?]]_{P}, can be derived that is appropriate to embedded uses:

[[Q?]]_{P} (w, g)(w′) = 1 iff [[Q?]]_{C}(w′, g) = [[Q?]]_{C}(w, g)
[[(40a)]]_{P} (w, g) = [[know]](w, g)(p)([[Mary]](w, g)), where p(w′) = 1 iff
[[came in]](w′, g) = [[came in]](w, g)

(41)

Thus the ‘categorial’ interpretation is more basic, and it is proposed to be derived using the following syntactic and semantic mechanisms^{16}. The syntactic origin of an interrogative containing n WH-phrases is a sentence containing n pronouns. Akin to the ‘Quantifying-in’ rules, there are ‘WH-abstract’ rules that act iteratively upon this, inserting a WH-phrase for a particular pronoun. The associated semantic operation is the abstraction operation Thus the meaning of (40b), of type (e, t) is derived from a meaning of type t. If there were n WH-phrases, there would to begin with be a meaning of type t, then a meaning of type (e_{1}, t), and eventually a meaning of type (e_{n}, … (e_{1}, t) …).

16This is actually a simplified version that allows only who to be a WH-phrase. It also only concerns ‘in situ’ WH-phrases.

It is not obvious that to achieve this semantic coverage one needs to use such syntactic insertion operations and subscripted variables. An abstraction operation, does not really change a meaning of type a into a meaning of type (e, a), they really just rearrange a function of type a. To begin with one has an n-place function in the form of a meaning of type t, depending on assignments, and discriminating between assignments on the basic of some difference in the values assigned to a certain set of n variables. After the abstraction operations, one has the same n-place function in the form of a meaning of type (e_{n}, … (e_{1}, t) …), depending on assignments, but equating all assignments together. It seems one could arrive at the same end point in a different manner. To begin with one has an n-place function, and this is the meaning of the verb in the interrogative, of type (e_{1}, … (e_{n}, t) …). Combinations with WH-phrases could then take place, each accompanied by a step of argument permutation, from a meaning of type (e, a⃗, t) to a meaning of type (a⃗, e, t). The end result will be a form of the verb function that one began with, a form of type (e_{n}, … (e_{1}, t) …). This would use only concatenative syntactic operations and would give the same interpretations to who came in and who loves who as the G+S 90 proposal, and therefore suggest the possibility of a PLCG account, and such an account is outlined below.

For this, WH-phrases are given the same categorisation as quantifiers: ∀X.X/(np\X) and ∀X.(X/np)\X. Their meaning shall not quite be the argument permutation operation, mentioned above. We will arrange things so that if α is an expression of category x/np, and contains n WH-phrases, its semantic type will be (e, a⃗, b⃗, t), where ν(x) = (a⃗, t), and b⃗ is a sequence of types associated with the WH-phrases. Thus the argument sequence of the type is split into two parts, the first relating to yet to be encountered arguments, and the second relating to already encountered WH-phrases. On the permutation account described above, if α who were now built, the type of the result would be (a⃗, b⃗, e, t), with e becoming added on to the end of b⃗. What we shall actually suppose is that e is added on to the beginning of b⃗, so that the type of α who is (a⃗, e, b⃗, t). I work with this slight variation on the idea outlined above because it is easier then to give a recursive definition of the functions to be denoted by WH-phrases, which are:

[[who]](w, g)(D_{t})(d^{(e,c)}) = d [[who]](w, g)(D_{a,b})(d^{(e,a,c)}) = x^{a} ↦ [[who]](w, g)(D_{b})(y^{e} ↦ d(y)(x))

Example

W H(a_{1}, …, a_{n}, t)(d)^{(e,a_{1},...,a_{n},w^{},t)} =

x_{1}^{a_{1}} ↦ W H(a_{2}, …, a_{n}, t)(y^{e} ↦ dyx_{1})^{(e,a_{2},...,a_{n},w^{},t)} =

x_{1}^{a_{1}} ↦ x_{2}^{a_{2}} ↦ W H(a_{3}, …, a_{n}, t)(y^{e} ↦ dyx_{1}x_{2})^{(e,a_{3},...,a_{n},w^{},t)} =

⋮ =

x_{1}^{a_{1}} ↦ x_{2}^{a_{2}} ↦ … ↦ x_{n}^{a_{n}} ↦ W H(t)(y^{e} ↦ dyx_{1}x_{2} … x_{n})^{(e,w^{},t)} =

x_{1}^{a_{1}} ↦ x_{2} ↦ … ↦ x_{n}^{a_{n}} ↦ y^{e} ↦ dyx_{1}x_{2} … x_{n}

It has to be confessed that we have defined by recursion here a function which does not have a tj^{(→,∀)} type. Also the type of a consituent containing WH-phrases will not be the type corresponding to the category, though it will be a tj^{(→,∀)} type. There is a remnant of the category to type correspondence, however, in that each combination with the WH-phrase, lowers the ‘linguistic-arity’ of the function: there is one fewer argument place concerning which one can expect other expressions to contribute information.

Not all the argument places of a verb in a interrogative need be filled by WH phrases (though in English not just anything goes if the WH-phrase is ‘in situ’). One could have who told who to go. The categorial syntax will suggest that told who, of category (np\s)/vpc, and to go could be combined by function application and if this is done the right result would be obtained. One ignores here the mismatch of the type of told who, ((e, t), e, e, t) with what the category-to-type map suggests. It is possible to do this because the operations dictated by the syntax are still compatible with the types. The same goes for interrogatives that include quantifiers together with WH phrases, as in who gave who a Xmas card. In this fashion, the interpretations that G+S 90 suggest for unembedded interrogatives may be derived. For embedded interrogatives it is necessary to suppose that the conversion operation from the ‘categorial’ interpretation to the ‘propositional’ interpretation could be included in the meaning of the embedding verb. The polymorphism of the quantifiers and WH phrases would allow one then to account for some ambiguities possible with embedded interrogatives:

a. Bill knows who entered every shop

a1. (Bill knows)_{s/s} ((who entered)_{s/np} every shop)_{s}

a2. (Bill knows)_{s/s} ((who entered)_{((s/s)\s)/np} every shop)_{(s/s)\s} b. John knows who said who was there b1. John knows (who said)_{s/s} (who (was there)_{np\s})_{s} b2. John knows (who said)_{s/s} (who (was there)_{(np\(s/s)\s)})_{(s/s)\s} (42)

To distinguish the readings of (42a), suppose some people entered at least one shop, while others entered every shop. One reading has it that Bill knows who the latter group are, and a skeletal disambiguation corresponding to this reading is given in (42a1). Another reading has it that for every shop, Bill knows who the group of people are who entered that shop, and a skeletal disambiguation corresponding to this reading is given in (42a2).^{17} To distinguish the readings of (42b), suppose a crime was committed and a number of people were witnesses. Also two or three non-witnesses (they might be a doormen, or taxi-drivers) independently say who these witnesses are. Then one reading has it that John knows who these witness identifying people are, and (42b1) is the disambiguation for this reading. For the other reading, vary the situation to one in which each witness-identifier claims only to have seen one of the witnesses. This is shown in (42b2).

The above was an outline of a PLCG account of interrogatives, and the further details of this are a further area of research.

SOME METAMATHEMATICAL ISSUES

A first question arising is Cut Elimination for the polymorphic calculus. A proof of this has been worked out by myself and Hans Leiß[Emms, M. and Leiss, H., 1993].

As mentioned earlier, the question of the decidability of the calculus, remains unknown. However, it is shown in [Emms, M., 1993] that there is at least decidability on what one might call the ‘linguistically relevant’ sequents. To define these sequents, it is necessary to refer to the notion of polarity. The category polarity of an occurrence of x in y (pol(x, y)) is + if x = y, and pol(x, y/z) = pol(x, ∀Z.y) = pol(x, y) = opp(pol(x, z/y)). The sequent polarity of an occurrence of x in y is the category polarity if y is an antecedent, and is otherwise opposite. There is a decision procedure for l^{(/,\,∀)} sequents which may have any kind of negative occurrences of a polymorphic category but whose positively occurring polymorphic categories are drawn from the list:

∀X.X/(np\X), ∀X.(X/np)\X

∀ X.X/X

∀X.(cn\cn)/(X\s)/(X)/np)

∀ (X\X)/X (43)

The question of models for the polymorphic categorial language also arises. It was mentioned earlier that there is a natural semantics for cat^{(/,\)} based on a set of strings (not including the empty string) and assumed closed under concatenation. The natural generalisation of this would be interpret the quantified categories as intersections over all the particular values got by mapping the variables onto arbitrary sets of strings. However this has the consequence that (see Appendix):

17Groenendijk and Stokhof distinguish also a further reading which they call the ‘pair-list’ reading, similar to the second reading we have described, except that every shop makes a de-dicto contribution. How this may be accounted for is a question for further research.

for all interpretations,I, for all assignments g,

[[∀X.X/X]](g) = ∅, [[∀X.(X\X)/X]](g) = ∅, [[∀X.X/(np\X)]](g) = [[np]](g)

(44)

Intuitively the range of quantification is too wide. A possibility is to require the range of quantification to include just those sets which are the interpretations of closed categories. This is another area of ongoing research. Some examples have been constructed to show that such models exist, but there is no completeness result as yet.

8 Appendix

1. SUBSTITUTION

The categories of l^{(/,\,∀)} form a set of terms very like the terms of untyped λ-calculus: the slash connectives corresponding to the binary term forming operation of function application, and the prefixing of quantifier plus variable corresponding to the prefixing of a λ plus a variable. Accordingly, the definition of substitution, and lemmas concerning it are exactly as they are for untyped λ-calculus (see Hindley and Seldin Introduction to λ-calculus and combinators).

Definition 3 (Substitution)

1. X[a/X] = a

2. b[a/X] = b if b ∈ bascat

3. (b_{1}/b_{2})[a/X] = b_{1}[a/X]/b_{2}[a/X], correspondingly for ‘\’

4. (∀X.b)[a/X] = ∀X.b

5. (∀Y.b)[a/X] = ∀Y.b[a/X] if Y ∉ F V (a) or X ∉ F V (b)

6. (∀Y.b)[a/X] = ∀Z.b[Z/Y][a/X] if Y ∈ F V (a) and X ∈ F V (b), where Z is the ‘first’ variable not occurring free in b or a

Definition 4 (Equivalence under c.b.v., ∼) Let x contain an occurrence of ∀X.z. Where x′ is the replacement in x of ∀X.z by ∀Y.z[Y/X], Y ∉ F V (z), we shall say x ∼_{1} x′. Then x ∼ x′ if x′ comes from x by a finite, possible empty, series of ∼_{1} steps.

2. OFFICIAL DEFINTION OF THE CALCULUS

Definition 5 (The Polymorphic Lambek Calculus, l^{(/,\,∀)})

(Ax)  x ⇒ x

(/L)  U, y, V ⇒ w T ⇒ x /L U, y/x, T, V ⇒ w

(\L)  T ⇒ x U, y, V ⇒ w \L U, T, y\x, V ⇒ w

(/R)  T, x ⇒ y /R T ⇒ y/x  (\R)  x, T ⇒ y \R T ⇒ y\x

(∀L) U, x[y/Z], V ⇒ w ∀L U, ∀Z.x, V ⇒ w

(∀R)  T ⇒ x  ∀R T ⇒ ∀Z′.x[Z′/Z]  {[Z ∉ F V (T), \atop Z′ ∉ F V (∀Z.x)]}

Remark: The formulation of the (∀R) rule may seem a bit complicated, and one might wonder why one cannot make do with the simpler:

T ⇒ x ∀R T ⇒ ∀Z.x  [Z ∉ F V (T)]

In this respect consider the two sequents:

a. np/X, X/s ⇒ ∀X.X/(X\(np/s)) b. np/X, X/s ⇒ ∀Y.Y/(Y\(np/s))

(45)

(45a) and (45b) differ only by a c.b.v in the succedent, but under the simpler formulation of (∀R), while (45b) would have the proof below, (45a) would have no proof:

⋮  Y ⇒ Y np/X, X/s ⇒ np/s  \L np/X, X/s, Y\(np/s) ⇒ Y /R np/X, X/s ⇒ Y/(Y\(np/s)) ∀R np/X, X/s ⇒ ∀Y.Y/(Y\(np/s))

Under the actual formulation of (∀R), (45a) has the proof:

⋮  Y ⇒ Y np/X, X/s ⇒ np/s  \L np/X, X/s, Y\(np/s) ⇒ Y /R np/X, X/s ⇒ Y/(Y\(np/s)) ∀R np/X, X/s ⇒ ∀X.X/(X\(np/s))

3. 2ND ORDER POLYMORPHIC LAMBDA CALCULUS Unlike L^{λ}, L^{(λ,Δ)} has two distinct kinds of variable, tvar and var^{λ}. tvar has already been defined and is the set of type-variables of tj^{(→,∀)}. var^{λ} is once again a set of typed variables, this time having types drawn from tj^{(→,∀)}.

Definition 6 (Typed Terms of L^{(λ,Δ)}) a. if Φ^{a} ∈ var^{λ}, Φ^{a} ∈ L^{(λ,Δ)} b. if Φ^{a} ∈ var^{λ} and Ψ^{b} ∈ L^{(λ,Δ)} then (λΦ^{a}Ψ^{b})^{(a→b)} ∈ L^{(λ,Δ)} c. if Φ^{(a→b)} and Ψ^{a} are ∈ L^{(λ,Δ)}, then (Φ^{(a→b)}Ψ^{a})^{b} ∈ L^{(λ,Δ)} d. if θ ∈ tvar, then θ ∈ L^{(λ,Δ)} e. if θ ∈ tvar and Φ^{a} ∈ L^{(λ,Δ)} and θ is not free in the type part of any free variable of Φ^{a}, then (Δθ.Φ^{a})^{∀θ.a} ∈ L^{(λ,Δ)} f. if Φ^{∀θ.a} ∈ L^{(λ,Δ)} and b ∈ tj^{(→,∀)} and b does not contain quantifiers then (Φ^{∀θ.a}(b))^{a[b/θ]} ∈

L^{(λ,Δ)}

It should be noted that vitally θ, mentioned in clause e of the above as being abstracted over by Δ, is a variable of the language tj^{(→,∀)}, that is a member of tvar. θ does not refer to a member of var^{λ}. Or putting things another way, terms of L^{(λ,Δ)} feature occurences of types in other than superscript positions. The kinds of terms of L^{(λ,Δ)} that are governed by clauses e and f of the above are abstractions over types and applications to types. There is a restrictions on the formation of these terms. One can abstract a type-variable θ out of Φ^{a} only if θ is not free in the type part of any free variable of Φ^{a}. One can also consider a further restriction: that one can apply to a type b only if that type contains no quantifiers (this restriction is not incorporated in the definition of L^{(λ,Δ)} in Girard et al (1989)). Reasons for proposing these restrictions can be offered when the semantics of L^{(λ,Δ)} is considered.

Examples of typed term of L^{(λ,Δ)}:

{(Δπ(λx^{π}.x^{π})^{(π→π)})^{∀π(π→π)} \atop (46)}

Often the type parts will be surpressed so the term above might be given as:

{Δπ.λx^{π}.x^{π} \atop (47)}

(48a) is an example of a term that is excluded by the side-condition on type-abstraction terms, (48b) gives examples that would be excluded with the above mentioned restriction on type application:

{a. Δπ.x^{π}, x^{∀π.a}(∀π.a), Φ^{∀π.π→π}(∀π.π→π)(Φ^{∀π.π→π}) \atop (48)}

4. POLYMORPHIC STRING SEMANTICS

As described in section 3, natural models for the categorial language cat^{(/,\)}are based on free algebras ⟨A, ·⟩, where · is a binary associative operation. Considering models for cat^{(/,\,∀)}, it is natural to assume that interpretation will be relative to an assignment,and that for some subset, V RANGE, of 2^{A}, the clause for quantified categories will be, [[∀Z.x]](g) = {a : for all B ∈ V RANGE, a ∈ [[x]](g_{Z}^{B})}

If V RANGE is chosen to be equal to 2^{A}, then one has the consequences:

for all interpretations,I, for all assignments g,

[[∀X.X/X]](g) = ∅, [[∀X.(X\X)/X]](g) = ∅, [[∀X.X/(np\X)]](g) = [[np]](g)

(49)

That for all interpretations,I, for all assignments g,[[∀X.X/X]](g) = ∅

One can show the following supposition to be false: there is an I, there is a g, there is an a, such that a ∈ [[∀X.X/X]](g). We note the following entailments: a ∈ [[∀X.X/X]](g)

⇒ for all B, a ∈ [[X/X]](g_{X}^{B})

⇒ for all B, for all b ∈ [[X]](g_{X}^{B}), a·b ∈ [[X]](g_{X}^{B})

⇒ for all B, for all b ∈ B, a·b ∈ B

But this last condition is impossible. For example pick B to be {a}. Then a·a ∉ B. So the supposition is false. □

That for all interpretations, for all assignments g,[[∀X.(X\X)/X]](g) = ∅

One can show that the following supposition is false:

there is an I, there is a g, there is an a, such that a ∈ [[∀X.(X\X)/X]](g). The supposition entails: for all B, for all b ∈ B, for all c ∈ B, c·a·b ∈ B. This is impossible. For example pick B to be {a}. Then c·a·b ∉ B. Therefore the supposition is false. □

That for all interpretations,I, for all assignments g,[[∀X.X/(np\X)]](g) = [[np]](g)

First we show that [[np]](g) ⊂ [[∀X.X/(np\X)]](g), by supposing otherwise:

there is an n such that n ∈ [[np]](g) and n ∉ [[∀X.X/(np\X)]](g). Note n ∉ [[∀X.X/(np\X)]](g) ⇒ there is B and b such that

(i) b ∈ [[X\np]](g_{X}^{B}) and

(ii) n·b ∉ [[X]](g_{X}^{B})

Now consider the implications of n ∈ [[np]](g). n ∈ [[np]](g) ⇒ n ∈ [[np]](g_{X}^{B}). Therefore from (ii), (iii) b ∉ [[X\np]](g_{X}^{B}) (iii) contradicts (i). Therefore the supposition was false. Second we show that [[∀X.X/(np\X)]](g) ⊂ [[np]](g), by supposing otherwise: there is a q such that q ∈ [[∀X.X/(np\X)]](g) and q ∉ [[np]](g). Now q ∈ [[∀X.X/(np\X)]](g) ⇒ for all B, q·[[X\np]](g_{X}^{B}) ⊆ [[X]](g_{X}^{B}) ⇒

(i) for all B, q·[[X\np]](g_{X}^{B}) ⊆ B

Then consider the set B which is the product of [[np]](g) with some arbitrary b, that is let B be {n_{1}·b, n_{2}·b, …}, where n_{1}, n_{2} etc are the members of [[np]](g). For this B, [[X\np]](g_{X}^{B}) = {b}. Therefore, for this choice of B, (i) implies: {q·b} ⊆ {n_{1}·b, n_{2}·b, …} ⇒ q·b = n_{i}·b, for some n_{i} ∈ [[np]](g) ⇒ q = n_{i} for some n_{i} ∈ [[np]](g) ⇒ q ∈ [[np]](g) which contradicts part of the original supposition. □

Its clear that if the langauge cat^{(/,\,∀)} is interpreted as above, it will not reflect the uses to which we intend to put it. The second identity for example means that one could not assign and to the polymorphic categorisation ∀X.(X\X)/X. The third identity would mean that if every man is assigned the category, ∀X.X/(np\X), then it ought to have a disambiguation of category np, and on the assumption that np is assigned to e, this would mean that every man has a possible meaning of type e, which is bizarre. l^{(/,\,∀)} clearly is not complete with respect to the above semantics, and it is hard to see what sequent calculus rules would allow the derivation of the sequent ∀X.X/(np\X) ⇒ np.

So, we conclude that the choice that V RANGE = 2^{A} is not the correct one. The hypothesis currently under investigation is that a V RANGE should be allowed only if it represents the range of values that are run through by the closed categories.

5. POLYMORPHIC TYPE SEMANTICS

Montague, in Universal Grammar, identified a general notion of interpretation. The general notion of interpretation is of a triple, ⟨B, (G_{γ})_{γ∈Γ}, f⟩. At two levels of specialisation from this general notion we essentially find the space of semantic proposals involved in Lambek grammar, which I will call l^{(/,\)}-theories of reference. The first specialisation is to the case where the carrier set, B, of the algebra involved must be ∪(M_{a}), where the M_{a} are the meaning sets, indexed types in tj→, constructed relative to three sets, E, I and J. Such interpretations are referred to as fregean interpretations in UG. The second specialisation is that each G_{γ} is H_{L}^{δ}(P), where P is some l^{(/,\)} proof, and H_{L}^{δ} is a proof-to-operation map.

The interpretations that will be parts of the kind of model that will feature in a l^{(/,\,∀)}-theory of reference are also at two levels of specialisation from the general notion of interpretation, and these specialisations are parallel to but not the same as the specialisations that are invoked by a l^{(/,\)}-theory of reference.

Firstly the notion of interpretation is specialised to the case where the objects of the carrier set, B, are defined by meaning sets indexed by types from the set tj^{(→,∀)}. Such interpretations might be referred to as a polymorphic fregean interpretations. The second specialisation is that each G_{γ} is H_{L∀}^{δ}(P), where P is a proof of l^{(/,\,∀)} and H_{L∀}^{δ} is a new proofto-operation map. As with H_{L}^{δ}, the proof-to-operation map is essentially the Curry-Howard isomorphism, though now involving a dimension of that isomorphism that was discovered/created by Girard.

I gave the definition of tj^{(→,∀)} in the text. The types in tj→ were used to index a set of denotations. Something akin to this will hold also for the types in tj^{(→,∀)}. We will define, relative to the sets E and I, polymorphic denotation sets having index a, where a is a closed formula in tj^{(→,∀)}. These will be notated P D_{a}

All formulae of tj^{(→,∀)} will be given an assignment dependent interpretation. Those formulae, a, of tj^{(→,∀)} that are closed, will come to have the same interpretation no matter what assignment, and this assignment independent interpetation of a will be defined to be the polymorphic denotation set indexed by a. Those formulae of a that are open shall not index any polymorphic denotation set.

There will be a two-level approach to the interpretation of tj^{(→,∀)}. A denotation set, D_{a}, is defined relative to a choice of E and I. One can look at varying the choice of E and I as varying the choice of an interpretation function which operates on the atomic types of tj→. The usual denotation sets, D_{a}, can be seen as the extension of such an interpretation function to cover all of tj→. We will given the name ‘Level One interpretation’ to this alternative view of denotation sets, D_{a}, relative to E and I. For a given Level One interpretation of tj^{(→,∀)}, we will use D for the set comprising of all the interpretations of the members of tj→. That is:

D = {D_{a} : a ∈ tj→}

The Level One interpretation concerns only the tj→ part of tj^{(→,∀)}. The Level Two interpretation concerns all of tj^{(→,∀)}and gives assignment dependent interpretations. The range for these assignments will be the set of Level One interpretations, that is, D.

Definition 7 (Interpretation of tj^{(→,∀)}) Level One interpretation of tj^{(→,∀)} has:

(i) No assignments (ii) Interpretation function: I^{∗}(e) = E, I^{∗}(s) = I, I^{∗}(t) = {0, 1} (iii) [[]]^{∗}, the extension of I^{∗} to tj→: [[a]]^{∗} is the denotation set, D_{a}, relative to E, I.

Level Two interpretation of tj^{(→,∀)} has:

(i) Assignments: g ∈ Dtvar (ii) Interpretation function: I(e) = g ↦ I^{∗}(e), I(t) = g ↦ I^{∗}(t), I(s) = g ↦ I^{∗}(s) (iii) [[]], the extension of I to all of tj^{(→,∀)} as follows [[π]](g) = g(π) [[a→b]](g) = [[b]](g)^{[[a]](g)} [[∀π.a]](g) is {f : dom(f) = D, whatever τ ∈ D, f(τ) ∈ [[a]](g_{π}^{τ})}

An example of a member of [[∀π.(π→π)]](g), where g is arbitary, is the function f whose value at every τ ∈ D is the identity function on τ. We have to check whether f(τ) ∈ [[(π→π)]](g_{π}^{τ}):

f(τ) ∈ [[(π→π)]](g_{π}^{τ}) iff f(τ) ∈ [[π]](g_{π}^{τ})^{[[π]](g_{π}^{τ})} iff f(τ) ∈ τ^{τ}

Clearly if f(τ) is the identity function on τ, it meets this condition.

Definition 8 (Polymorphic Denotation set P D_{a}) Relative to E, I, for any closed formula, a, of tj^{(→,∀)}, P D_{a} = [[a]](g), where [[]] is the Level Two interpretation associated with E, I, and g is any g ∈ Dtvar

The notion of polymorphic meaning set, P M_{a}, is simply P D_{a}^{I×J}.

Definition 9 (Polymorphic Fregean Algebra) ⟨B, (G_{γ})_{γ∈Γ}⟩ is a Polymorphic Fregean Algebra iff for some E, I, B= ∪(PM_{a}), where the PM_{a} are the polymorphic meaning sets indexed by closed formulae of tj^{(→,∀)}, relative to E and I.

A polymorphic fregean interpretation is more or less the special case of a interpretation, where the algebra involved is a Polymorphic fregean algebras. Additionally, a polymorphic fregean interpretation must make reference to a mapping relating phraseset indices to closed formulae of tj^{(→,∀)}. Therefore a polymorphic fregean interpretation for a disambiguated language, L, is defined thus:

Definition 10 (polymorphic fregean interpretation of L, associated with E, I, J , ν)

Is a triple ⟨B, (G_{γ})_{γ∈Γ}, f⟩, where

(i) ⟨B, (G_{γ})_{γ∈Γ}, f⟩ is an interpretation, and ⟨B, (G_{γ})_{γ∈Γ}⟩ is a polymorphic fregean algebra (ii) whenever δ ∈ Δ and α ∈ X_{δ}, f(α) ∈ PM_{ν(δ)} (iii) whenever ⟨F_{γ}, ⟨δ_{η}⟩, ϵ⟩ ∈ S and m_{η} ∈ PM_{ν(δ_{η})} then G_{γ}(⟨m_{η}⟩) ∈ PM_{ν(δ)}

Having thus specialised of interpretations in respect of the nature of the carrier set, we must now specialise in respect of the nature of the operations. The specialisation is that the operations should be the image of a proof-to-operation map, H_{L∀}^{δ}.

I indicated in the text that this proof to operation map is defined via a term associated calculus. The essential element then in need of definition is the semantics of the terms.

6. SEMANTICS OF 2ND ORDER POLYMORPHIC LAMBDA CALCULUS

The semantic values of terms of L^{(λ,Δ)} will be functions whose first argument is an assignment, as was the case for terms of L^{λ}. However, the assignments will now concern both the typevariables, tvar, and the other variables, var^{λ}.

The range of assignments as far as members of tvar is concerned is D. The range of the assignments as far as members of var^{λ} is concerned is ∪(P D_{a})a is a closed formula of tj^{(→,∀)}. For those members of var^{λ}, x^{a}, where a is a closed formula of tj^{(→,∀)}, we require that g(x^{a}) ∈ P D_{a}. For those members of var^{λ}, x^{a}, where a is an open formula, there can be no such requirement since P D_{a} is not defined for open formulae. However, if g(x^{a}) ∉ [[a]](g), we shall call the assignment a pseudo-assignment. Pseudo-assignments are required only to ‘oil the wheels’ of the definition.

Definition 11 (Interpretation of Typed Terms of L^{(λ,Δ)}) Assignments:{g : g = g_{1} ∪ g_{2} g_{1} ∈ Dtvar, where a ∈ tj→ g_{2} ∈ (∪P D_{a})var^{λ}, where a ∈ tj^{(→,∀)} and is closed g_{2}(x^{a}) ∈ P D_{a}, if a is closed

Interpretation: I(e) = g ↦ E, I(t) = {0, 1}, I(s) = g ↦ I [[]], which extends I to all of L^{(λ,Δ)}: [[π]](g) = g(π) [[a→b]](g) = [[b]](g)^{[[a]](g)} [[∀π.a]](g) is {f : dom(f) = D, whatever τ ∈ D, f(τ) ∈ [[a]](g_{π}^{τ})} [[Φ^{a}]](g) = g(Φ^{a}), if Φ^{a} ∈ var^{λ} [[λΦ^{a}.Ψ^{b}]](g) is that function d_{1}^{(a,b)} such that for any member d_{2}^{a} of [[a]](g), d_{1}(d − 2) = [[Ψ^{b}]](g_{Φ^{a}}^{d_{2}}) [[Φ^{(a→b)}(Ψ^{b})]](g) = [[Φ^{a}]](g)([[Ψ^{b}]](g))

[[Δπ.Φ^{a}]](g) is that function d^{∀π.a} such that for any τ ∈ D, d(τ) = [[Φ^{a}]](g_{π}^{τ}). Note g_{π}^{τ} is probably a pseudo-assignment [[Φ^{∀π.a}(b)]](g) = [[Φ^{∀π.a}]](g)([[b]](g))

This semantics is intended to reflect the intuition that an object of type ∀π.a is a function from a type b to an object of type a[b/π]. As an illustration consider the interpretation of Δπλx^{π}.x^{π} (τ is a member of D):

[[Δπλx^{π}.x^{π}]](g) = τ ↦ [[λx^{π}.x^{π}]](g_{π}^{τ})

g_{π}^{τ} is probably a pseudo-assignment. Continuing with the interpretative procedure, however, we have (where d is a member of τ):

[[Δπλx^{π}.x^{π}]](g) = τ ↦ d ↦ [[x^{π}]](g_{π,x^{π}}^{τ,d}) = τ ↦ d ↦ g_{π,x^{π}}^{τ,d}(x^{π}) = τ ↦ d ↦ d.

So the interpretation of the non-basic expression Δπλx^{π}.x^{π} at an assignment depended on the interpretation of the non-basic λx^{π}.x^{π} at a number of pseudo-assignments. However, the interpretation of the non-basic expression λx^{π}.x^{π} at whatever pseudo-assignment was required, depended on the interpretation of the basic expression x^{π} at an assignment not a pseudoassignment. It will be the case that for all terms that do not violate the side-condition on type abstraction terms that the interpretation of an expression at an assignments will depend on the interpretations of its consituent basic-expression at assignments, not pseudo-assignments. On the other hand, a type-abstraction term which violates the above-mentioned restriction, such as Δπ.x^{π}, would have a denotation at an assignment that was determined by the denotations of its constituent basic expressions,(that is x^{π}) at pseudo-assignments:

[[Δπ.x^{π}]](g) = τ ↦ [[x^{π}]](g_{π}^{τ}) = τ ↦ g_{π}^{τ}(x^{π})

For all τ but one, g_{π}^{τ} is a pseudo-assignment. Notice also that [[Δπ.x^{π}]](g) is a constant function on types, and not a function from a type to an object in the type. Therefore the terms which violate the side condition on type-abstraction receive anomolous denotations.

There is also some explanation of the restriction on the formation of type application terms. An example of such a term is (Δπ.Φ^{a})(∀ω.b). Its interpretation would invoke assignments which do not exist:

[[(Δπ.Φ^{a})(∀ω.b)]](g) = [[Φ^{a}]](g′), where g′(π) = [[∀ω.b]](g)

The assignments were defined as taking type-variables to members of D, but g′(π) is not a member of D.

7. IMPOSSIBILTY OF TERM DEFINITIONS OF POLYMORPHIC CONSTANTS

The polymorphic junctions could be defined if there were some term, Φ_{JUNCT} of L^{(λ,Δ)}, of type (s, ∀π.((s, π), ((s, π), π))), having one free variable x^{(t,(t,t))} (I have switched here to the intensional version of the theory). Similarly the polymorphic determiners could be defined if there were some term Φ_{DET} of L^{(λ,Δ)}, of type ((s, et), ∀π.((s, se, π), π)), whose sole free variable was x^{((e→t)→((e→t)→t))}.

To search for the terms Φ_{JUNCT}^{(s,∀π.((s,π),((s,π),π)))} and Φ_{DET}^{(s,((s,et),∀π.((s,se,π),π)))}, one can exploit the Extended Curry-Howard isomorphism between proofs of the intuitionistic sequent calculus for tj^{(→,∀)}, and the terms of L^{(λ,Δ)}.

The term for the junction would exist if there was an lj^{(→,∀)}proof of (t, (t, t)) ⇒ (s, ∀π.((s, π), ((s, π), π))), with (t, (t, t)) not introduced into the antecedent by a Weakening inference. The only lj^{(→,∀)} proofs of (t, (t, t)) ⇒ (s, ∀π.((s, π), ((s, π), π))) that I can find, consist of a proof of ⇒ (s, ∀π.((s, π), ((s, π), π))) with an added step introducing (t, (t, t)) into the antecedent by a Weakening inference, such as:

8 APPENDIX 47

s→s π→π →L s, (s→π) ⇒ π Weak and Perm (s→π), (s→π), s ⇒ π →R and →R s ⇒ ((s→π)→((s→π)→π)) ∀R s ⇒ ∀π((s→π)→((s→π)→π)) →R ⇒ (s→∀π((s→π)→((s→π)→π)))  Weak (t→(t→t)) ⇒ (s→∀π((s→π)→((s→π)→π))) (50)

The term for the determiners would exist if there was an lj^{(→,∀)} proof of (et, et, t) ⇒ (s, (set), ∀π((s, se, π), π)). This can be refuted semantically, using the fact that lj^{(→,∀)}is sound on a classical semantics.

That (et, et, t) ⇒ (s, (set), ∀π((s, se, π), π)) is not valid

Suppose:

1. there is an interpretation I, an assignment g, and a p such that: p ∈ [[t]](g), p ∈ [[s]](g), p ∉ [[e]](g)

One can show that it follws from this supposition that p ∈ [[(et, et, t)]](g) and p ∉ [[(s, (set), ∀π((s, se, π), π))]](g), and therefore that (et, et, t) ⇒ (s, (set), ∀π((s, se, π), π)) is not valid.

First we find a sufficient condition for p ∈ [[(et, et, t)]](g): p ∈ [[(et, et, t)]](g) if p ∉ [[(et)]](g) or p ∈ [[(et, t)]](g) if p ∉ [[(et)]](g) or p ∈ [[t]](g) (discarding first disjunct) if p ∈ [[t]](g) (discarding first disjunct)

By assumption 1, the above is true, therefore p ∈ [[(et, et, t)]](g)

Second we find a sufficient condition for p ∉ [[(s, (set), ∀π((s, se, π), π))]](g): p ∉ [[(s, (set), ∀π((s, se, π), π))]](g) if p ∈ [[s]](g) and p ∈ [[(set)]](g) and p ∉ [[∀π((s, se, π), π)]](g) if p ∈ [[s]](g) and (p ∉ [[s]](g) or p ∈ [[(et)]](g)) and p ∉ [[∀π((s, se, π), π)]](g) if p ∈ [[s]](g) and (p ∈ [[(et)]](g)) and p ∉ [[∀π((s, se, π), π)]](g) if p ∈ [[s]](g) and (p ∉ [[e]](g) or p ∈ [[t]](g)) and p ∉ [[∀π((s, se, π), π)]](g) if p ∈ [[s]](g) and (p ∈ [[t]](g)) and p ∉ [[∀π((s, se, π), π)]](g) if p ∈ [[s]](g) and (p ∈ [[t]](g)) and there is a B such that p ∉ [[((s, se, π), π)]](g_{π}^{B}) if p ∈ [[s]](g) and (p ∈ [[t]](g)) and there is a B such that (p ∈ [[(s, se, π)]](g_{π}^{B}) and p ∉ [[π]](g_{π}^{B})) if p ∈ [[s]](g) and (p ∈ [[t]](g)) and there is a B such that ((p ∉ [[s]](g_{π}^{B}) or p ∈ [[(se, π)]](g_{π}^{B})) and p ∉ B) if p ∈ [[s]](g) and (p ∈ [[t]](g)) and there is a B such that ((p ∉ [[(se)]](g_{π}^{B}) or p ∈ [[π]](g_{π}^{B})) and p ∉ B) if p ∈ [[s]](g) and (p ∈ [[t]](g)) and there is a B such that ((p ∈ [[s]](g_{π}^{B}) and p ∉ [[e]](g_{π}^{B})) and p ∉ B)

By taking B to be [[e]](g) one can see that supposition 1 entails that the above condition is true and therefore entails that p ∉ [[(s, (set), ∀π((s, se, π), π))]](g) □

8. GENERAL WIDE-SCOPING OF A QUANTIFIER

In the text, I gave a quick argument that PLCG generally predicts the interchange of proper names and quantifiers. Here a version of that argument is given, this time taking account of complications that arise if it is elected to work with the restricted form of the (∀L) rule. l^{(/,\,∀)} refers to the unrestricted version of the calculus. l^{(/,\,\overline{∀})} refers to the version of the calculus with the restricted (∀L) rule. ∀^{+}(x) refers to the number of positively occuring quantifiers in x. What can be shown concerning interchange is the following:

Lemma 1 (Interchange) l^{(/,\,∀)}|− U, np, T_{1}, V ⇒ w iff l^{(/,\,∀)}|− U, ∀X np^{X∧}, T_{1}, V ⇒ w l^{(/,\,∀)}|− U, T_{2}, np, V ⇒ w iff l^{(/,\,∀)}|− U, T_{2} ∀X np^{∧X}, V ⇒ w

For l^{(/,\,\overline{∀})} there is the condition: ∀^{−}(U, T_{i}, V) = ∀^{+}(w) = 0. For both l^{(/,\,∀)} and l^{(/,\,\overline{∀})}, the right-to-left implications can be strengthened to allow T_{1} (or T_{2}) to be empty.

The proof of the interchange lemma for l^{(/,\,\overline{∀})} uses the following Instantiation lemma (where l^{(/,\,\overline{∀})}⊢^{n} r refers to the derivability of r by a proof with n or less nodes.

Lemma 2 (Instantiation) l^{(/,\,\overline{∀})}⊢^{n} U, x, V ⇒ w and ∀^{−}(U, x, V) = ∀^{+}(w) = 0 implies:

(a) for some \overline{x}, ∀^{+}(\overline{x}) = ∀^{−}(\overline{x}) = 0, l^{(/,\,\overline{∀})}⊢^{n} U, \overline{x}, V ⇒ w and l^{(/,\,\overline{∀})}|− x ⇒ \overline{x}

(b) for some \underline{w}, ∀^{+}(\underline{w}) = ∀^{−}(\underline{w}) = 0, l^{(/,\,\overline{∀})}⊢^{n} U, x, V ⇒ \underline{w} and l^{(/,\,\overline{∀})} ⊢^{n} \underline{w} ⇒ w

Proof of Instantiation

Without loss of generality, we can restrict attention to proofs with zero-complexity axioms. The proof is then by induction on the sizes of such proofs. For size 1 proofs there is nothing to show. So suppose the lemma (parts a) and b)) for all proofs (ending in zero-complexity axioms) of size less than n, and consider an arbitrary size m proof of U, x, V ⇒ w.

a) First consider the case where x is not the active category, then U, x, V ⇒ w, is concluded by some rule R, from some r_{1}, containing x, and possibly one further sequent, r_{2}. See proof (i) below:

i ⋮1 ⋮2 r_{1}[x] r_{2} R U, x, V ⇒ w  b  ⋮1′  ⋮2 r_{1}[\overline{x}/x] r_{2}R r[\overline{x}/x] (51)

Whichever rule R is, it can be confirmed that ∀^{−}(r_{1}[x]) = 0, and so the inductive hypothesis applies, giving for some ∀-free \overline{x} such that l^{(/,\,\overline{∀})}⊢^{m−1} ⇒ x ⇒ \overline{x}, l^{(/,\,\overline{∀})}⊢^{m−1} r_{1}[\overline{x}/x]. Thus proof (ii) above establishes the claim.

Suppose now that x is the active category. We consider the possibilities for the final step in the proof of U, x, V ⇒ w.

x = a/b. We have, where m_{1} + m_{2} + 1 = n, the proof (i) below:

i  ⋮m_{1}  ⋮m_{2} U, a, V ⇒ w T ⇒ b/L U, a/b, T, V ⇒ w  ii  ⋮m_{1}  ⋮m_{2} U, \overline{a}, V ⇒ w T ⇒ \overline{b}/L U, \overline{a}/\underline{b}, T, V ⇒ w

The inductive hypothesis applies to the subproofs, so for some quantifier-free \overline{x} and \underline{b}, such that l^{(/,\,\overline{∀})}|− x ⇒ \overline{x}, and l^{(/,\,\overline{∀})}|−\underline{b} ⇒ b, we have the upper sequents of (ii). (ii) establishes the claim because l^{(/,\,\overline{∀})}|− a/b ⇒ \overline{a}/\underline{b}

x = ∀Y.z. We have the proof (i) below

i  ⋮n − 1 U, z[y/Y], V ⇒ w∀L U, ∀Y.z, V ⇒ w  ii  ⋮n − 1 U, z′, V ⇒ w

Because y must be quantifier free, the inductive hypothesis applies to the subproof, so for some quantifier-free z′, such that l^{(/,\,\overline{∀})}|− z[y/Y] ⇒ z′, we have the proof (ii) above. (ii) establishes the claim because we have l^{(/,\,\overline{∀})}|−∀Y.z ⇒ z[y/Y], and l^{(/,\,\overline{∀})}|−z[y/Y] ⇒ z′, and therefore l^{(/,\,\overline{∀})}|−∀Y.z ⇒ z′.

b) First consider the case where w is not the active category, then U, x, V ⇒ w, is concluded by some rule R, from some T ⇒ w, and possibly one further sequent, r_{2}. See (i) below:

i ⋮1 ⋮2 T ⇒ w r_{2} R U, x, V ⇒ w  ii  ⋮1′  ⋮2 T ⇒ \underline{w} r_{2} R U, x, V ⇒ \underline{w} (52)

Whichever rule R is, it can be confirmed that ∀^{−}(T ⇒ w) = 0, and so the inductive hypothesis applies, giving for some ∀-free \underline{w} such that l^{(/,\,\overline{∀})}|− \underline{w} ⇒ w, l^{(/,\,\overline{∀})}⊢^{m−1} T ⇒ \underline{w}. Thus proof (ii) above establishes the claim.

Now consider the case that w is the active category. There is only the possibility that that last step is (/R), (∀R) being ruled out by the supposition that ∀^{−}(w) = 0. We have the proof (i) below:

i  ⋮n − 1 U, x, V, b ⇒ a /R U, x, V ⇒ a/b  ii  ⋮n − 1 U, x, V, \overline{b} ⇒ \underline{a} /R U, x, V ⇒ \underline{a}/\overline{b}

By applying the inductive hypothesis twice in succession to the subproof of (i) we conclude that for some quantifier-free \underline{a} and \overline{b} such that l^{(/,\,\overline{∀})}|− \underline{a} ⇒ a, and l^{(/,\,\overline{∀})}|−b ⇒ \overline{a}, we have l^{(/,\,\overline{∀})}⊢^{m−1} U, x, V, \overline{b} ⇒ \underline{a}. Hence we have the following proof (ii), and this establishes the claim because l^{(/,\,\overline{∀})}|− \underline{a}/\overline{b} ⇒ a/b

End of proof

Proof of Interchange

Right-to-left. For both l^{(/,\,∀)} and l^{(/,\,\overline{∀})}, use Cut to replace np in the antecedents with ∀X np^{X∧} or ∀X np^{∧X}, which are both derivable from np.

Left-to-right

l^{(/,\,∀)}: Given the supposition that l^{(/,\,∀)}|− U, np, T_{2}, V ⇒ w, the following derivation establishes that l^{(/,\,∀)}|− U, ∀X np^{X∧}, T_{2}, V ⇒ w:

⋮  ⋮ U, np, T_{2}, V ⇒ w U, U\(w/V), V ⇒ w  Slash R T_{2} ⇒ np\(U\(w/V))(/L) U, (U\(w/V))/(np\(U\(w/V))), T_{2}, V ⇒ w(∀L) U,  ∀X.X/(np\X)  , T_{2}, V ⇒ w

l^{(/,\,\overline{∀})}: We suppose that l^{(/,\,\overline{∀})}|− U, np, T_{2}, V ⇒ w, and that ∀^{−}(U, T_{2}, V) = ∀^{+}(w) = 0. By successively applying the Instantiation lemma we infer the existence of quantifier-free \overline{U}, \overline{V}, and \underline{w}, such that l^{(/,\,\overline{∀})}|− U ⇒ \overline{U}, l^{(/,\,\overline{∀})}|− V ⇒ \overline{V}, l^{(/,\,\overline{∀})}|− \underline{w} ⇒ w, and l^{(/,\,\overline{∀})}|− U, np, T_{2}, V ⇒ w. Hence the following derivation establishes that l^{(/,\,\overline{∀})}|− U, ∀X np^{X∧}, T_{2}, V ⇒ w:

\underline{w} ⇒ w U ⇒ \overline{U} V ⇒ \overline{V}  ⋮ \overline{U}, np, T_{2}, \overline{V} ⇒ \underline{w} U, \overline{U}\(\underline{w}/\overline{V}), V ⇒ w  Slash R T_{2} ⇒ np\(\overline{U}\(\underline{w}/\overline{V}))(/L) U, (\overline{U}\(\underline{w}/\overline{V}))/(np\(\overline{U}\(\underline{w}/\overline{V}))), T_{2}, V ⇒ w(∀L) U  ∀X.X/(np\X)  , T_{2}, V ⇒ w

End of Proof The Left-to-Right part of the proof of interchange above, essentially also proves that a quantifier can be given arbitrarily wide-scope. It is simply necessary to check out the term-associated versions of the proof establishing the claim to see that the term associated with the quantifier has widest scope. For the polymorphic grammar given in the text, the preconditions of the interchange lemma for l^{(/,\,\overline{∀})} are met.

9. GENERAL WIDE SCOPING OF A JUNCTION

We would like that, where ∀^{−}(U, T_{1}, V) = ∀^{−}(U, T_{2}, V) = ∀^{+}(w) = 0, if l^{(/,\,\overline{∀})}⊢ U,T1, V ⇒ w and l^{(/,\,\overline{∀})}⊢ U,T2,V ⇒ w, then l^{(/,\,\overline{∀})}⊢ U, T 1, ∀X.(X\X)/X, T 2, V ⇒ w, and with the term associated with the junction taking widest scope.

By the Instantiation lemma, we infer the existence of quantifier-free \overline{U}, \overline{V}, and \underline{w} such that l^{(/,\,\overline{∀})}|− U ⇒ \overline{U}, l^{(/,\,\overline{∀})}|− V ⇒ \overline{V}, l^{(/,\,\overline{∀})}|− \underline{w} ⇒ w, l^{(/,\,\overline{∀})}|− \overline{U},T1, \overline{V} ⇒ \underline{w} and l^{(/,\,∀)}|− \overline{U},T2,\overline{V} ⇒ \underline{w}

The required proof ⊢ U, T 1, ∀X.(X\X)/X, T 2, V ⇒ w is:

⋮  ⋮  ⋮ \overline{U}, T 1, \overline{V} ⇒ \underline{w} Slash R T 1 ⇒ \overline{U}\(\underline{w}/\overline{V})  U, \overline{U}\(\underline{w}/\overline{V}), V ⇒ w  \overline{U}, T 2, \overline{V} ⇒ \underline{w} (\L) U, T 1, (\overline{U}\(\underline{w}/\overline{V}))\(\overline{U}\(\underline{w}/\overline{V})), V ⇒ w  Slash R T 2 ⇒ \overline{U}\(\underline{w}/\overline{V})/L U, T 1, ((\overline{U}\(\underline{w}/\overline{V}))\(\overline{U}\(\underline{w}/\overline{V})))/(\overline{U}\(\underline{w}/\overline{V})), T 2, V ⇒ w∀L U, T 1, ∀X.(X\X)/X, T 2, V ⇒ w

References

[Benthem, 1986] J. van Benthem. Essays in Logical Semantics. Reidel, Dordrecht.

[Benthem, 1991] J. van Benthem. Language in Action. Studies in Logic, North-Holland, Amsterdam.

[Buszkowski, 1982] W. Buszkowski Compatibility of a Categorial Grammar with an Associated Category System. Zeitschrift fur Math. Logik, 28.

[Buszkowski et al, 1988] W. Buszkowski, W. Marciszewski, J. van Benthem. Categorial Grammar. Benjamins, Amsterdam.

[Robin Cooper, 1983] Robin Cooper. Quantification and Syntactic Theory Dordrecht, Reidel.

[David Dowty, 1988] David Dowty. Type Raising, Functional Composition, and Non-constituent Conjunction. In Categorial Grammars and Natural Language Structures, Oehrle, R., Bach, E. and Wheeler, D. (eds.). Dordrecht.

[Emms, M., 1989] Martin Emms. Polymorphic Quantifiers. In Torenvliet, M.S.L. (ed.) Seventh Amsterdam Colloquium, pp 139–163.

[Emms, M., 1993] Martin Emms. Parsing with Polymorphism. In proceedings of Sixth Annual Conference of the European Association for Computational Linguistics, 1993

[Emms, M. and Leiss, H., 1993] Martin Emms and Hans Leiss. Cut Elimination in the Second Order Lambek Calculus.

[Gamut, L.T.F., 1991] L.T.F. Gamut. Logic, Language and Meaning, Volume 2: Intensional Logic and Logical Grammar. Chicago Press, Chicago.

[Gazdar, G., 1980] G.Gazdar. A Cross-Categorial Semantics for Coordination. Linguistics and Philosophy, 3, pp. 407–409.

[Gazdar et al, 1985] G. Gazdar, E. Klein, G. Pullum, I. Sag. Generalised Phrase Structure Grammar. Harvard University Press, Cambridge, Massachusetts.

[J-Y. Girard et al, 1989] J-Y. Girard, P. Taylor and Y. Lafont. Proofs and Types Cambridge University Press, Cambridge.

[G. Groenendijk and M. Stokhof, 1991] G. Groenendijk and M. Stokhof. Dynamic Montague Grammar. In ‘Quantification and Anaphora I+, DYANA Deliverable R2.2.A.

[G. Groenendijk and M. Stokhof, 1991] G. Groenendijk and M. Stokhof. Partitioning Logical Space. Annotated handout for the Second European Summerschool on Logic, Language and Information, Leuven.

[Herman Hendriks, 1987] Herman Hendriks. Type Change in Semantics: the Scope of Quantification and Coordination In E. Klein and J. van Benthem (eds.) Categorial Grammar: its Current State. University of Amsterdam: Institute for Language, Logic and Information.

[Herman Hendriks, 1990] Herman Hendriks. Flexible Montague Grammar. In DYANA Deliverable R1.2.A. University of Amsterdam: Institute for Language, Logic and Information.

[Moortgat, 1988] Michael Moortgat. Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus. Dordrecht: Foris Publications.

[Moortgat, 1990] Michael Moortgat. The Quantification Calculus: Questions of Axiomatisation. In DYANA Deliverable R1.2.A. University of Amsterdam: Institute for Language, Logic and Information.

[Moortgat, 1992] Michael Moortgat. Generalised quantifiers and discontinuous type constructors. to appear in Discontinuous Constituency, W.Sijtsma and A. van Horck (eds.) Mouton de Gruyter, Berlin.

[Morrill et al, 1990] G. Morrill, N. Leslie, M. Hepple, G. Barry. Categorial Deductions and Structural Operations. In G. Barry and G. Morrill (eds.) Studies in Categorial Grammar, Edinburgh Working Papers in Cognitive Science.

[Partee, B. and Rooth, M., 1983] Barbara Partee and Mats Rooth. Generalized conjunction and type ambiguity. In Meaning, Use, and Interpretation of Language, Volume 6, pp53-95, Bauerle, R., Schwarze, C. and Stechow, A. (eds.) . Berlin Linguistic Analysis: de Gruyter.

[Reynolds, 1974] J.C Reynolds. Towards a theory of type structure. In Colloquium sur la programmation, 1974, pages 408–423.

[Stockwell et al, 1973] R. Stockwell, P. Schachter, B. Partee. The Major Syntactic Structures of English. Holt, Rinehart and Winston, New York.

[Zeevat et al, 1987] H. Zeevat, E. Klein, J. Calder. Unification Categorial Grammar. in N. Haddock, E.Klein and G.Morrill (eds.) Categoiral Grammar, Unification Grammar, and Parsing. Edinburgh Working Papers in Cognitive Science, Volume 1.