Completeness Results for Polymorphic Lambek Calculus

Martin Emms

Abstract

We study an extension of the Lambek calculus which allows the universal and existential quantification of category variables, which we call the polymorphic Lambek calculus. In particular we consider several notions of model for the quantifier-free calculus and how they may be extended to the calculus with quantifiers. We consider first the string-semantic models and show that if quantifiers are interpreted as ranging over arbitrary sets of strings, the polymorphic calculus is incomplete. Taking this a failing of the semantics and not the calculus, we refine the semantics so that quantifiers range over sets of strings that are the interpretation of categories. We show completeness for the /, \, ∀ fragment. We then consider the residuated semi-group models, and interpreting the quantifiers by g.l.b’s and l.u.b.’s we show completeness for the /, \, •, ∀, ∃ fragment. We finally consider the ternary frame semantics.

Contents

1 The Polymorphic Lambek Calculus 76

2 String-Semantics 78

2.1 Background: Quantifier-free, product-free calculi . . . . . . . . . . . . . . . . . . 78 2.1.1 String-semantic models of l^{(/,\)} . . . . . . . . . . . . . . . . . . . . . . . . 78 2.1.2 S^{inf} -soundness of l^{(/,\)} . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 2.1.3 S^{inf} -completeness of l^{(/,\)} . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 2.1.4 Variations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80

2.2 Quantified, product-free calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 2.2.1 Choices for the range of quantification . . . . . . . . . . . . . . . . . . . . 82 2.2.2 P S_{1}^{inf} -incompleteness of l^{(/,\,∀,∃)} . . . . . . . . . . . . . . . . . . . . . . . 84 2.2.3 P S_{2}^{inf} -soundness of l^{(/,\,∀,∃)} . . . . . . . . . . . . . . . . . . . . . . . . . . 85 2.2.4 P S_{2}^{inf} -completeness of l^{(/,\,∀)} . . . . . . . . . . . . . . . . . . . . . . . . . 86 2.2.5 Open question: P S_{2}^{inf} -completeness of l^{(/,\,∀,∃)} . . . . . . . . . . . . . . . 88 2.2.6 Open question: P S_{2}-completeness . . . . . . . . . . . . . . . . . . . . . . 88 2.2.7 The P S_{2,3}^{inf} class . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 3 Residuated Semi Group models 92

3.1 Background: quantifier-free calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 92 3.1.1 Residuated Semi Group models for l^{(/,\)}, l^{(/,\,•)} . . . . . . . . . . . . . . 92 3.1.2 RES-completeness of l^{(/,\,•)} . . . . . . . . . . . . . . . . . . . . . . . . . 92

3.2 Quantified Calculi with product . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 3.2.1 Residuated Semi Group models for Quantified Calculi . . . . . . . . . . . 93 3.2.2 P RES-completeness for l^{(/,\,•,∀,∃)} . . . . . . . . . . . . . . . . . . . . . . 94 3.2.3 Open question: P RES-completeness for l^{(/,\,∀,∃)} . . . . . . . . . . . . . . 95

4 Ternary Frame Semantics 96 4.1 Background: quantifier-free calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 96 4.2 Quantified Calculi with product . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

4.2.1 Restrictions on accessibility which give incompleteness . . . . . . . . . . . 98

5 Concluding Remarks 99

1 The Polymorphic Lambek Calculus

Categorial grammar is familiar to most people as the study of the logical properties of categories built up from a set of basic categories, by the categorial connectives, ‘/’, ‘\’ and ‘•’. In recent years, however, proposals have been made to extend this classical categorial language and we will be concerned here with a certain extension allowing for quantification over category variables. In short, we have, in addition to basic categories, also category variables, and where x is a category, then we have also ∀X.x and ∃X.x. With respect to a number of possible semantics, we will investigate the soundness and completeness of various calculi with these quantifiers ^{1}, where the calculi will have the single axiom scheme x ⇒ x, and then a selection from the following rules:

1For other aspects of these calculi see [Emms, 1992], [Emms, 1993b], [Emms, 1993c] (linguistic applications), [Emms, 1993a] (parsing), [Emms and Leiß, 1993] (Cut-elimination), [Emms, 1993d] (recognising power)

U, y, V ⇒ w T ⇒ x/L U, y/x, T, V ⇒ w  T, x ⇒ y/R T ⇒ y/x

T ⇒ x U, y, V ⇒ w\L U, T, x\y, V ⇒ w  x, T ⇒ y\R T ⇒ x\y

U, x, y, V ⇒ w•L U, x•y, V ⇒ w  T_{1} ⇒ x T_{2} ⇒ y•R T_{1}, T_{2} ⇒ x•y

U, x[y/Z], V ⇒ w∀L U, ∀Z.x, V ⇒ w  T ⇒ x  ∀R, Z! T ⇒ ∀X.x[X/Z]

U, x, V ⇒ w  ∃L, Z! U, ∃X.x[X/Z], V ⇒ w  T ⇒ x[y/X]∃R T ⇒ ∃X.x

U, x, V ⇒ w T ⇒ xCut U, T, V ⇒ w

The rules derive sequents from sequents where a sequent is an antecedent sequence of categories followed by ‘ ⇒ ’ and then a single category. w, x, y (resp. U, V, T) range over categories (resp. sequences of categories, U and V possibly empty). For the most part we will be concerned with calculi in which T may not be empty. The rules are labelled with L and R according to whether they concern the presence of a connective to the left- or the righthand side of the sequent arrow. The rules (∀R) and (∃L) are subject to the side condition that Z is not free below the line, and X is not free in QZ.x, this latter part allowing QX.x[X/Z] to be an alphabetic variant of QZ.x (we notate alphabetic variance as ∼). As a guide to intuitions, a sequent containing a free variable, ought to be read as making a universal statement, which would hold true under all possible values of the variable (and not as an existential statement, holding true for some possible value of the variable).

In general we will use l superscripted with a series of connectives to stand for the calculus obtained by taking the left and right rules for the connectives in the series. Thus l^{(/,\,•,∀,∃)} stands for calculus with all the above rules. l^{(/,\,•)} is the calculus original proposed in [Lambek, 1958], but we in common with several authors will refer to l^{(/,\)} as the Lambek calculus. When we allow that T may be empty, and thereby allow sequents to be derived with an empty antecedent, we will subscript the name of the calculus with ϵ. See [Lambek, 1958] and [Emms and Leiß, 1993] for proofs that derivability is preserved under substitution throughout for a free variable, under change of a bound variable, and under elimination of the Cut rule.

We will consider soundness and completeness of the calculi with quantifiers with respect to several notions of possible semantics. In the model constructions, the value of a category, x, will often be taken to be the set of sequences which derive it, which we will notate as A[x], spoken as the ‘antecedents of x’. This presupposes the following lemma:

Lemma 1 (A[x] is compositional) If A[x] = A[x′], then A[x/y] = A[x′/y], A[y/x] = A[y/x′], A[x•y] = A[x′•y], A[y•x] = A[y•x′], A[QX.x] = A[QX.x′].

Proof

If A[x] = A[x′], then x ⇒ x′ and vice-versa. Using these one can show x/y ⇒ x′/y, y/x ⇒ y/x′, x•y ⇒ x′•y, y•x ⇒ y•x′, QX.x ⇒ QX.x′, and vice-versa. From these, the desired identities of antecedents follow. □

2 String-Semantics

The so-called ‘string-semantics’ for the basic categorial language is a semantics that stays very close to the linguistic motivations for the language. Categories are interpreted as sets of strings, and a category x/y is interpreted as exactly those strings which if combined with a y string would give an x string. In section 2.1 below, we recap the basics for quantifier-free calculi, before considering the quantified case in section 2.2.

2.1 Background: Quantifier-free, product-free calculi

2.1.1 String-semantic models of l^{(/,\)}

We begin by considering l^{(/,\)} and the so-called string-semantic completeness of l^{(/,\)}[Buszkowski, 1982].

Def: String-Semantic model

⟨S, •, [[]]⟩ is a string-semantic model if

• S = closure under binary, associative • of some denumerable set V of atomic strings

• ⟨S, •⟩ is free apart from associative identities

• [[]] maps categories to subsets of S 1. [[x/y]] = {a ∈ S : ∀b ∈ [[y]], a•b ∈ [[x]]}

2. [[y\x]] = {a ∈ S : ∀b ∈ [[y]], b•a ∈ [[x]]}

One can easily show that any such model is uniquely determined by the values of the basic categories, so that one can alternatively define the models by an interpretation for the basic categories, to be extended according to the above two conditions. We have made one departure from [Buszkowski, 1982] in the above definition, and this is that we have omitted a requirement that V be finite. The class of all string-semantic models we will refer to as S^{inf}. The corresponding class requiring V to be finite, we will refer to as S ^{2}.

Besides the l^{(/,\)} derivable sequents, [Buszkowski, 1982] considers the sequents obtained when the calculus is extended with additional axioms. There are two situations in which this might arise. In the first one wants to relate a number of particular categories to one another, for example making ‘vp[sing]’ and ‘vp[pl]’ subcategories of ‘vp’, via the axioms vp[sing] ⇒ vp and vp[pl] ⇒ vp. In the second situation one wants to alter the interpretation of the connectives in some general way, requiring for example that x ⇒ y/(y/x), be satisfied for all x and y. The difference between the two situations then is whether one wants to add particular sequents as axioms, or to add sequent schemata. [Buszkowski, 1982] treats the first case, that is the addition of a set R of axiom sequents. We will consider the further generalisation of this is to the addition of a set, R of axiom schemata. For any quantifier free calculus, L, we define the satisfaction relation, ⊧, to hold between a model and a sequent, x_{1}, …, x_{n} ⇒ y, when [[x_{1}]]• … •[[x_{n}]] ⊆ [[y]]. We shall say that a model satisfies a set R of schemata when it satisfies all instances of the schemata.

2Thus S denotes the same class of models as it does in [Buszkowski, 1982].

Following [Buszkowski, 1986], where K stands for either S^{inf} or S, we will say that a sequent is a K-consequence of a set of axiom schemata R if in all K models satisfying R, the sequent is also satisfied. By K-soundness and completeness of L for consequence we refer to the property^{3}:

for any sequent, T ⇒ y

T ⇒ y is a K consequence of R iff L + R + Cut |−T ⇒ y.

In the case that R is empty, we speak of the soundness and completeness of l^{(/,\)}+ Cut for validity. In view of Cut elimination, this is a property of l^{(/,\)}.

2.1.2 S^{inf}-soundness of l^{(/,\)}

For every possible set of axiom schemata, R, one easily shows S^{inf} soundness of l^{(/,\)} for consequence. This clearly entails S-soundness.

Proof

Suppose M is an S^{inf} model satisfying R and consider a derivable sequent T ⇒ x, and its proof. We must show that M satisfies T ⇒ x. The leaves of the proof are either instances of the R schemata, or of the l^{(/,\)} axiom scheme, x ⇒ x. In the first case, by supposition M satisfies these leaves. In the second case, every model satisfies any instance of x ⇒ x. So the leaves of the proof are satisfied in M. Hence it will suffice to show that the rules of the calculus preserve satisfaction. In the following we suppose the premises of a rule are satisfied and not the conclusion.

• Cut. We obtain the sequent U, T, V ⇒ w, from U, x, V ⇒ w and T ⇒ x. There are u⃗ ∈ [[U]], t⃗ ∈ [[T]] and v⃗ ∈ [[V]] such that u⃗t⃗v⃗ ∉ [[w]] ^{4}. Because t⃗ ∈ [[T]], we have t⃗ ∈ [[x]], and therefore u⃗t⃗v⃗ ∈ [[w]], which is a contradiction.

• /L. We obtain the sequent is U, x/y, T, V ⇒ w from U, x, V ⇒ w and T ⇒ y. For some u⃗ ∈ [[U]], a ∈ [[x/y]], b⃗ ∈ [[T]], v⃗ ∈ V, we have u⃗ab⃗v⃗ ∉ [[w]]. We have b⃗ ∈ [[y]], and therefore ab⃗ ∈ [[x]]. Therefore we have u⃗ab⃗v⃗ ∈ [[w]], which is a contradiction.

• /R. We obtain the sequent T ⇒ x/y from T, y ⇒ x. For some t⃗ ∈ [[T]], some b ∈ [[y]], t⃗b ∉ [[x]]. But t⃗b ∈ [[x]], which is a contradiction.

• \L, or \R: as for the /L and /R cases.

3Note the presence of the Cut rule here: in the absence of additional axioms, Cut may not be eliminated.

4By u⃗ ∈ [[U]] we refer to the concatenation of a sequence of objects belonging to the individual categories making up U. When U is empty, u⃗ does not refer to anything. In our arguments we will not consider such possibilities as a separate case, but instead continue to write u⃗, on the understanding that au⃗ and u⃗a refer to the same thing as a.

End of Proof

2.1.3 S^{inf}-completeness of l^{(/,\)}

In [Buszkowski, 1982] it is shown that for every set of additional axiom sequents, R, l^{(/,\)} is S-complete for consequence. This entails the corresponding property with respect to S^{inf}. However, the proof does not generalise to the case of the addition of a set of axiom schemata, R. By a slight variant of the proof for S, in fact a simplification, one can show S^{inf} -completeness for consequence, under the addition of a set, R, of schemata. We give this proof below. Besides giving a completeness result for entailment from axiom schemata, we give the proof below because it will serve later on as a part of the proof of a corresponding result for the calculi with quantifiers. Buszkowski’s proof of S-completeness is given in section 2.1.4.

Let L be l^{(/,\)}+ Cut + R, for some set of axiom schemata R. We construct a canonical model, M, ⟨S, •, [[]]⟩:

S = the set of all sequences of categories

• = sequence concatenation

[[x]] = A[x]

M is a model

• Case: x/y. We need to show {T ∈ S : ∀T_{1} ∈ S(if L |−T_{1} ⇒ y, then L |−T, T_{1} ⇒ x)} = {T ∈ S : L |−T ⇒ x/y} Left to Right. Note, L |−y ⇒ y, hence L |−T, y ⇒ x, hence L |−T ⇒ x/y (by /R) Right to Left. Let T_{1} be arbitrarily chosen such that L |−T_{1} ⇒ y. Hence L |−x/y, T_{1} ⇒ x (by /L), hence L |−T, T_{1} ⇒ x (by Cut, assuming L |−T ⇒ x/y)

• Case: y\x. Similar to x/y □

M satisfies R

Suppose x_{1}, …, x_{n} ⇒ y is an instance of a schema in R. For each x_{i} choose an arbitrary T_{i} ∈ [[x_{i}]]. Thus L |−T_{i} ⇒ x_{i}. We obtain therefore L |−T_{1} … T_{n} ⇒ y, and therefore, T_{1} … T_{n} ∈ [[y]]. Thus we have [[x_{1}]]• … •[[x_{n}]] ⊆ [[y]]. □

M is a countermodel to underivable sequents

Suppose L |− / x_{1}, …, x_{n} ⇒ y. .˙ . x_{1}, …, x_{n} ∉ [[y]]. Note L |−x_{i} ⇒ x_{i}, .˙ . x_{i} ∈ [[x_{i}]]. .˙ . [[x_{1}]]• … •[[x_{n}]] ⊈ [[y]] □

2.1.4 Variations

Finite set of Atomic Strings

When the set of atomic strings must be finite, as it must be in a S model, then the above construction is not a possible model. [Buszkowski, 1982] gives a proof of S-completeness for consequence, under the addition of a set of axioms R. For every particular sequent which cannot be derived from R, a particular model, M, is constructed satisfying R and not satisfying the sequent. Suppose we have l^{(/,\)}+ R + Cut |− / x_{1}, … x_{n} ⇒ y. Let C be the set of subcategories of R and the x_{1}, …, x_{n} and y. We will use the notation A ↓_{C} [x] to refer to the set of sequences over C which derive x. The model ⟨S, •, [[]]⟩ is:

S is all sequences of categories over C

• is sequence concatenation For x ∈ C, [[x]] = A ↓_{C} [x]

M is a model

First the model above specifies the values of only those categories in C. Concerning the categories outside C, it is clearly possible to choose the interpretation for these categories so that the conditions concerning the connectives are met. For the members of C, the reasoning here is as it was in the case of S^{inf}, but with attention paid to the restricted pool from which the antecedents are drawn, for example:

• Case: x/y. We need to show {T ∈ C^{+} : ∀T_{1} ∈ C^{+}(if L |−y, then L |−T, T_{1} ⇒ x} = {T ∈ C^{+} : L |−T ⇒ x/y}. Left to Right. Because L |−y ⇒ y, and y ∈ C, we have L |−T, y ⇒ x. Hence L |−T ⇒ x/y (by /R) Right to Left. Let T_{1} ∈ C^{+} be arbitrarily chosen such that L |−T_{1} ⇒ y. Hence L |− x/y, T_{1} ⇒ x (by /L), hence L |− T, T_{1} ⇒ x (by Cut, assuming L |−T ⇒ x/y) □

M satisfies the axioms in R

Suppose a_{1}, …, a_{n} ⇒ b is an axiom in R. For each a_{i} choose an arbitrary T_{i} ∈ [[a_{i}]], i.e. such that T_{i} ∈ C^{+} and L |−T_{i} ⇒ a_{i}. We obtain therefore L |−T_{1} … T_{n} ⇒ b, and because T_{1} … T_{n} ∈ C^{+}, therefore, T_{1} … T_{n} ∈ [[b]]. Hence [[a_{1}]]• … •[[a_{n}]] ⊆ [[b]], and the axiom is satisfied in M. □

M is a countermodel to x_{1}, …, x_{n} ⇒ y

We have supposed the L |− / x_{1}, …, x_{n} ⇒ y, and therefore x_{1}, … x_{n} ∉ [[y]]. Since L |−x_{i} ⇒ x_{i} and x_{i} ∈ C^{+}, we have x_{i} ∈ [[x_{i}]], so M does not satisfy x_{1}, …, x_{n} ⇒ y. □

We note that the proof will not work for the case of derivation from additional axiom schemata, R. The counter-example for an underivable sequent has to satisfy R, and to guarantee this we need to include in the set of atomic strings all of the subcategories of every instance of a schema in R, resulting in an infinite set of atomic strings.

Empty Antecedents

The string-semantics for l_{ϵ}^{(/,\)} is also considered in [Buszkowski, 1986]. It will have relevance later on to the discussion of quantified calculi, and so the basic details are mentioned here. Note that l_{ϵ}^{(/,\)}|−x/x, and therefore l_{ϵ}^{(/,\)}|−y/(x/x) ⇒ y. This second sequent is not satisfied in all string semantic models, and therefore l_{ϵ}^{(/,\)} is not sound with respect to these models. The natural extension to obtain soundness is to assume that the underlying algebra ⟨S, •⟩, contains an element, ϵ which is a right and left identity for the • operation. Clearly we will have ϵ ∈ [[x/x]], and because each member a of [[y/(x/x)]] is equal to a•ϵ, we will have that each a is in [[y]]. S_{ϵ}^{inf} and S_{ϵ} are defined in the same way as S^{inf} and S with the addition that underlying algebras contain the required identity element, ϵ. We define satisfaction as before with one addition to take care of sequents with an empty antecedent, ⇒ x. In this case we will say the sequent is satisfied if ϵ ∈ [[x]]. With very small modifications the earlier proof of l^{(/,\)} soundness can be adapted to be a proof of l_{ϵ}^{(/,\)} soundness. The completeness proofs can also easily be adapted, with the empty sequence serving in the canonical model as the ϵ item.

String semantic completeness of l^{(/,\,•)}

One can try to extend the above proofs to the calculus with product. The natural clause governing interpretation for the product is:

[[x•y]] = {a ∈ S : ∃b_{1} ∈ [[x]], ∃b_{2} ∈ [[y]], a = b_{1}•b_{2}}

Soundness of l^{(/,\,•)} may easily be proved. However, as [Buszkowski, 1986] points out, completeness for consequence fails. If we choose R to be p ⇒ p•p, then p ⇒ p/p is a K consequence where K is S^{inf} or S^{5}. However p ⇒ p/p cannot be derived under the assumption of p ⇒ p•p as an axiom.

There remains the question of the completeness of l^{(/,\,•)} for validity, that is under the assumption of no additional axioms. The straightforward extension of the proofs for S^{inf} and S completeness will fail. Consider S^{inf}. The canonical interpretation, [[x]] = A[x], does not meet the condition required by the product. We note that (x•y)/z, z ∈ A[x•y]. For simplicity assume x, y and z are basic and all different. To conform to the condition for the product we then require (x•y)/z ∈ [[x]], and z ∈ [[y]], which is to say l^{(/,\,•)}|−(x•y)/z ⇒ x, and l^{(/,\,•)}|−z ⇒ y neither of which is true. The same example will be a problem for the proof of S-completeness, by assuming that (x•y)/z is a subcategory of the supposed underivable sequent.

A somewhat involved proof of l^{(/,\,•)} completeness has been given in [Pentus, 1993]. At the time of writing the author is not in a position to judge the impact this proof might have, in particular on the later sections of the paper when quantifiers are also considered.

2.2 Quantified, product-free calculi

2.2.1 Choices for the range of quantification

When we turn to quantified calculi, a first question to be considered is whether we should have basic categories, as well as variables. This is because variables which do not become bound in the course of a proof could be replaced by basic categories, and vice versa. Nonetheless, despite the possibility that the theory could be developed on the basis of a constant-free calculus, we will choose to have a fixed denumerably infinite set of variables, and a varying denumerable set of basic categories.

What we will call polymorphic string-semantic interpretations are based on the above discussed string semantic interpretation, as follows.

Def: Polymorphic string-semantic model

⟨S, •, V, [[]]⟩ is a polymorphic string-semantic interpretation if

• S is the closure, under •, of some denumerable V

• ⟨S, •⟩ is free apart from associative identities

• V ⊆ P(S), V non-empty • [[ ]] maps categories and assignments into P(S)

5If a model satisfies p ⇒ p•p, then [[p]] = ∅.

1. [[x/y]]^{g} = {a ∈ S : ∀b ∈ [[y]]^{g}, a•b ∈ [[x]]^{g}}

2. [[y\x]]^{g} = {a ∈ S : ∀b ∈ [[y]]^{g}, b•a ∈ [[x]]^{g}}

3. for basic x, [[x]]^{g} is independent of g

4. for variables X, [[X]]^{g} = g(X).

5. [[∀X.y]]^{g} = ∩{[[y]]^{g_{X}^{A}} : A ∈ V}

6. [[∃X.y]]^{g} = ∪{[[y]]^{g_{X}^{A}} : A ∈ V}

Categories are interpreted now with respect to assignments, where the assignments maps variables to sets in V, which will be refered to as the range of quantification. A question with which we will be concerned is which subsets of S are available to serve as the value of a variable. The simplest, but as it turns out, incorrect answer to this is that all subsets of S should be available. For this reason the range of quantification is given as an explicit parameter in the definition of the model ^{6}. It is an easy exercise to show that a model is uniquely determined by the values of the basic categories and the range of quantification, so that one can alternatively define models by a range of quantification and interpretation for the basic categories to be extended according to the above conditions on the connectives.

Def: Satisfaction

M, g ⊧ x_{1}, …, x_{n} ⇒ y iff [[x_{1}]]• … •[[x_{n}]]^{g} ⊆ [[y]]^{g}.

Where K is a class of possible polymorphic string-semantic models, we say

Def: Consequence

T ⇒ x is a K-consequence of a set of axiom schemata R if for all models, M, when M, g ⊧ R for all assignments g, then M, h ⊧ T ⇒ x for all assignments h

We will restrict schemata to not include free variables, so that we allow x/y, y ⇒ x as a schema, but not x/Y, Y ⇒ x. This is one way (amongst others) to prevent axioms from making statements about particular variables^{7}. We noted earlier that for the quantified calculi we had preservation of derivability under substitutions for free variables, and changes of bound variable. This extends to the case where we have additional axiom schemata.

Various conditions that one might impose on V that we will consider are:

Choices for the range of quantification

1. V = P(S)

2. V covers the categories:

{[[x]]^{g} : x a category, g an assignment} ⊆ V.

3. V is covered by the closed categories: V ⊆ {[[x]]^{g} : x is a closed category, g is an assignment}

The class of polymorphic models allowing for the set of atomic strings to be infinite we will refer to as P S^{inf}, and adding subscripts 1,2 or 3 will indicate restriction to models in which V meets the corresponding conditions. We will consider the P S_{1}^{inf}, P S_{2}^{inf} and P S_{2,3}^{inf} classes of models. Note that P S_{1}^{inf} ⊆ P S_{2}^{inf}.

6Thus our models are very akin to the so-called general models of 2nd Order logic, introduced by [Henkin, 1950].

7For example, the only models which would make the axiom X ⇒ Y true for all assignments, have V as a singleton, and this makes for example Y ⇒ X true for all assignments, despite the fact that it is not derivable from X ⇒ Y.

As in the previous section, when we omit the superscript ‘inf’ this indicates the restriction to models based on a finite set of atomic strings.

2.2.2 P S_{1}^{inf}-incompleteness of l^{(/,\,∀,∃)}

The P S_{1}^{inf} class chooses the quantifier range to be simply the power set of the underlying set of strings. This condition embodies the most obvious candidate for the semantics of the quantified calculi. One might call this unrestricted quantification, because in all models, all sets of strings are available as possible values for a variable. Nonetheless P S_{1}^{inf} is a restriction of the class P S^{inf} because only models are allowed which make all sets of strings available.

We will show that a calculus including the quantifier rules will be incomplete w.r.t. P S_{1}^{inf}. Not all instances of the schemata below are derivable (if for example x and y are assumed to be atomic then one can easily see that all attempts at a proof will fail). However, all instances of these schemata are satisfied in all P S_{1}^{inf} models.

• ∀X.X/X ⇒ y

• ∀X.X\X/X ⇒ y

• ∀X.(X/y)\X ⇒ y

• x ⇒ ∃X.y/(X/X)

• x ⇒ ∃X.y/(X\X/X)

The fact that these schemata are always satisfied depends on: (any model, any g)

1. [[∀X.X/X]]^{g} = ∅

2. [[∀X.X\X/X]]^{g} = ∅

3. [[∀X.(X/y)\X]]^{g} ⊆ [[y]]^{g}

4. [[∃X.y/(X/X)]]^{g} = S

5. [[∃X.y/(X\X/X)]]^{g} = S

Proof of 1, 4

We use / and \ here not only as categorial connectives, but as operations on sets of strings. We note that {b}/{b} = ∅. For suppose a ∈ {b}/{b}. Then a•b ∈ {b}, which implies a•b = b, and this contradicts our assumption that the algebras are free.^{8} Therefore, when B = {b}, [[X/X]]^{g_{X}^{B}} = ∅, and therefore [[∀X.X/X]]^{g} = ∅. Also because A/∅ = S, we have [[y/(X/X)]]^{g_{X}^{B}} = S, and therefore [[∃X.y/(X/X)]]^{g} = S. □

Proof of 2, 5

We note that {b}\{b}/{b} = ∅. For suppose a ∈ [[X\X/X]]^{g_{X}^{B}}. Then b•a•b = b, which again contradicts the assumption that the algebras are free. Therefore [[X\X/X]]^{g_{X}^{B}} = ∅, where B = {b}, and therefore [[∀X.X\X/X]]^{g} = ∅. We also have [[y/(X\X/X))]]^{g_{X}^{B}} = S, and therefore [[∃X.y/(X\X/X)]]^{g} = S. □

8More generally when there is a longest string in B, B/B = ∅

Proof of 3

First suppose [[y]]^{g} is empty. For all B we require [[∀X.((X/y)\X)]]^{g} ⊆ [[(X/y)\X]]^{g_{X}^{B}}, but when B = ∅, the right-hand side is S\∅, which is empty. Hence [[∀X.((X/y)\X)]]^{g} is empty. Now assume [[y]]^{g} is non-empty, and suppose q ∈ [[∀X.(X/y)\X]]^{g}, and q ∉ [[y]]^{g}. For all B ⊆ S, we have q ∈ [[(X/y)\X]]^{g_{X}^{B}}. Choose B = b•[[y]], for some b. Then b ∈ [[X/y]]^{g_{X}^{B}}, and so we require b•q ∈ b•[[y]]^{g}, which implies that q ∈ [[y]]^{g}. □

It deserves mention that some of the above counterexamples would not apply to the versions of the calculi that allow empty antecedents, and correspondingly have an identity element in every model. ∀X.((X\X)/X) ⇒ y, and x ⇒ ∃X.y/(X\X/X) remain underivable and semantically valid, thereby refuting completeness. However, [[X/X]]^{g}, is no longer the empty set for every g, containing in every model the identity element, and thus ∀X.X/X ⇒ y and x ⇒ ∃X.y/(X/X) are no longer semantically valid. They remain underivable. The case of ∀X.(X/y)\X ⇒ y changes in the opposite respect, remaining semantically valid, but with the allowance of empty antecedents, becoming derivable.

What do these considerations show ? For completeness we must revise either the calculus or the semantics. We will revise the semantics. This is because on the above semantics we will not obtain a calculus which serves some of the grammatical purposes of polymorphism. For example, one would like to assign and the category ∀X.(X\X)/X. Any complete calculus based on the above semantics must allow any y to be derived from this category, giving and the unexpected property that it can satisfy the subcategorisation requirements of any word.

We will not alter the calculus, and instead allow for the possibility that the range of quantification is less than P(S). This is also linguistically natural. Think again of assigning the category ∀X.(X\X)/X to the word and. When V is identified with P(S), then this categorisation forces every set of strings to be closed under the operation of inserting and between members of that set. However, and does not have this property. What we can say is that for any category, if strings to either side of and have that category, then the combination has that category. Thus we seem to require that any set of strings which is the value of a category is closed under the operation of inserting and between members. In other words one would like the range of quantification to be the values of categories. In this way one comes to Conditions 2 and 3 above. According to Condition 2, V need not contain every set of strings, but must at least contain the values of all categories. Because every set in V is the value of some category under some assignment (namely a variable), Condition 2 gives one sense in which the range of quantification coincides with the values of categories. Condition 3 in tandem with Condition 2 demands somewhat more, namely that the range of quantification coincides with the values of closed categories.

In the succeeding sections will look at soundness and completeness with respect to P S_{2}^{inf} and P S_{2,3}^{inf}.

2.2.3 P S_{2}^{inf}-soundness of l^{(/,\,∀,∃)}

For any L which includes either or both of the quantifier rules, plus Cut and a set of axiom schemata R, we show P S_{2}^{inf} -soundness for consequence. Note that this entails P S_{2}-soundness.

Proof Assume L |−T ⇒ x, and that for M ∈ P S_{2}^{inf}, we have that for every g, (M, g) satisfies R, and for some g′, (M, g′) does not satisfy T ⇒ x.

Consider the proof of T ⇒ x. The leaves are either instances of R schemata, and are therefore satisfied for every g, or are instances of x ⇒ x, and are therefore satisfied for every g. Hence it will suffice to show that the rules of the calculus preserve the property of being satisfied in every g. In the following we assume the premises of a rule are satisfied for every g, but not the conclusion. The cases for Cut, /L,/R,\L,\R are minor alterations of the corresponding cases in the proof of l^{(/,\)}-soundness, and so we give just the quantifier cases. Note that the argument for ∀L and ∃R makes use of the fact that models meet Condition 2, namely that V covers the categories.

• ∀L. We obtain the sequent U, ∀X.x, V ⇒ w from U, x[y/X], V ⇒ w. There is an assignment g, there are u⃗ ∈ [[U]]^{g}, a ∈ [[∀X.x]]^{g}, v⃗ ∈ [[V]]^{g} such that u⃗av⃗ ∉ [[w]]^{g}. Since a ∈ [[∀X.x]]^{g}, then for any B ∈ V, a ∈ [[x]]^{g_{B}^{X}}. Because V covers the categories, V contains [[y]]^{g}, and choosing B to be [[y]]^{g}, [[x]]^{g_{B}^{X}} = [[x[y/X]]]^{g}. Therefore a ∈ [[x[y/X]]]^{g}, and therefore U, x[y/X], V ⇒ w is not satisfied in the assignment g, which is a contradiction.

• ∃R (similar to ∀L). We obtain the sequent T ⇒ ∃X.x from T ⇒ x[y/X]. There is an assignment g, and there are t⃗ ∈ [[T]]^{g}, such that t⃗ ∉ [[∃X.x]]^{g}. So for no B ∈ V, t⃗ ∈ [[x]]^{g_{B}^{X}}. Because V covers the categories, V contains [[y]]^{g}, and choosing B to be [[y]]^{g}, [[x]]^{g_{B}^{X}} = [[x[y/X]]]^{g}. Therefore t⃗ ∉ [[x[y/X]]]^{g}. Therefore T ⇒ x[y/X] is not satisfied in the assignment g, which is a contradiction.

• ∀R. We obtain the sequent T ⇒ ∀X.x[X/Z], where Z ∉ F V (T), and X ∉ F V (∀Z.x), from T ⇒ x. There is an assignment g and some t⃗ ∈ [[T]]^{g}, t⃗ ∉ [[∀X.x[X/Z]]]^{g}. Therefore for some B ∈ V, t⃗ ∉ [[x[X/Z]]]^{g_{B}^{X}}. By the choice of X, [[x[X/Z]]]^{g_{B}^{X}} = [[x]]^{g_{B}^{Z}}. Also since Z ∉ F V (T), [[T]]^{g} = [[T]]^{g_{B}^{Z}}. Therefore we have t⃗ ∈ [[T]]^{g_{B}^{Z}}, and t⃗ ∉ [[x]]^{g_{B}^{Z}}. So we have that T ⇒ x is not a satisfied in the assignment g_{B}^{Z}, which is a contradiction.

• ∃L (similar to ∀R). We obtain the sequent U, ∃X.x[X/Z], V ⇒ w, where Z ∉ F V (U, V, w), and X ∉ F V (∃Z.x), from U, x, V ⇒ w. There is an assignment g, and some u⃗ ∈ [[U]]^{g}, v⃗ ∈ [[V]]^{g}, a ∈ [[∃X.x[X/Z]]]^{g}, such that u⃗av⃗ ∉ [[w]]^{g}. For some B ∈ V, a ∈ [[x[X/Z]]]^{g_{B}^{X}}. By the choice of X, [[x[X/Z]]]^{g_{B}^{X}} = [[x]]^{g_{B}^{Z}}. Also since Z ∉ F V (U, V, w), [[U]]^{g} = [[U]]^{g_{B}^{Z}}, [[V]]^{g} = [[V]]^{g_{B}^{Z}}, [[w]]^{g} = [[w]]^{g_{B}^{Z}} . Therefore we have u⃗ ∈ [[U]]^{g_{B}^{Z}}, a ∈ [[x[y/X]]]^{g_{B}^{Z}}, v⃗ ∈ [[V]]^{g_{B}^{Z}}, and u⃗av⃗ ∉ [[w]]^{g_{B}^{Z}}, so U, x, V ⇒ w is not satisfied in g_{B}^{Z}, which is a contradiction.

End of Proof

2.2.4 P S_{2}^{inf}-completeness of l^{(/,\,∀)}

Where L is l^{(/,\,∀)}, together with a set of R axiom schemata and Cut, we give now a proof of P S_{2}^{inf} -completeness of L. The discussion in section 2.1.4 should make it clear why we are considering product-free calculi. We are also considering calculi without ∃. We will consider later what problems arise in extending the proof to one for calculi with ∃. We will also consider the question of whether P S_{2} completeness may be proved.

For each set of axiom schemata, R we construct a canonical model, M = ⟨S, •, V, [[]]⟩ thus:

Canonical Model S = all sequences of categories

• = sequence concatenation V = {A[x] : x is a category} [[x]]^{g} = A[sub(x)], where sub is any substitution allowed by g

In the last clause, sub refers to an infinite simultaneous substitution, mapping each variable to some category. Such a sub is extended in the obvious way to a function applying to every category^{9}. We say a substitution sub ‘is allowed by g’ if for each variable, X, g(X) = A[sub(X)]. Note more than one substitution may be allowed by g.

Recall that the completeness proof for l^{(/,\)} used [[x]] = A[x]. We are using here a somewhat corresponding idea. We cannot use exactly the same idea, namely, [[x]]^{g} = A[x], because the left-hand side depends on g, whereas the right-hand side does not. Note also that not every set of sequences of categories appears in the range of quantification, V: where a and b are distinct basic categories, {a, b} ∉ V. Thus the canonical model is not in P S_{1}^{inf}.

[[]] is well defined

We must verify that [[]] is well defined because more than one substitution may be allowed by one assignment. We must show that for all substitutions, f_{1}, f_{2}, for all categories x, if for all variables, A[f_{1}(X_{i})] = A[f_{2}(X_{i})], then A[f_{1}(x)] = A[f_{2}(x)]. The substitutions f_{1} and f_{2} may precipitate changes of bound variable in x, but because the antecedents of categories which differ from each other only by a change of bound variable are identical, we can assume that f_{1} and f_{2} are such as to cause no change of bound variable. Then we use Lemma 1 for each of the free-variables of x, and for each of its occurrences, in order to infer that A[f_{1}(x)] = A[f_{2}(x)].

M is a model

By the definition of V and the interpretation, we have that V covers the categories. It remains to check that [[]] conforms to the conditions on syntactic structure.

• Case: variable, X. We must show [[X]]^{g} = g(X):

T ∈ [[X]]^{g}

iff for any sub allowed by g, T ⇒ sub(X) iff for any x such that g(X) = A[x], T ⇒ x iff T ∈ g(X)

• Case: basic category, x. Consider two distinct assignments, g_{1}, g_{2}. We must show [[x]]^{g_{1}} = [[x]]^{g_{2}}. Because x contains no free variables, whatever substitutions, f_{1} and f_{2} are allowed by these assignments, f_{1}(x) = f_{2}(x), hence [[x]]^{g_{1}} = [[x]]^{g_{2}}.

• Case: [[x/y]]^{g}. Let sub be an arbitrary substitution allowed by g, and write x̃ for sub(x), and ỹ for sub(y). We need to show that {T ∈ S : ∀T_{1} ∈ S(if L |−T_{1} ⇒ ỹ, then L |−T, T_{1} ⇒ x̃)} = {T ∈ S : L |−T ⇒ x̃/ỹ}. See corresponding case in proof of S^{inf} completeness for l^{(/,\)}.

• Case [[∀X.x]]^{g}. Let f be an arbitrary substitution allowed by g. Because A[z] = A[z′], when z ∼ z′, we can assume that ∀X.x is such that the substitution f causes no changes of bound variable. Let f_{X}^{z} be the substitution differing from f only by assigning z to X. We need: ∩{A[f_{X}^{y}(x)] : A[y] ∈ V} = A[f(∀X.x)].

9In application to a quantified term, ∀Y.y, such that Y occurs free in sub(X_{i}) for one of X_{i} ∈ F V (∀Y.y), there is a change of bound variable to the first variable not in F V (∀Y.y) nor sub(X_{i}) for any X_{i} ∈ F V (∀Y.y).

Left to Right. Suppose for all A[y] ∈ V, T ∈ A[f_{X}^{y}(x)]

Pick Z ∉ F V (T, f(Y)), where Y ∈ F V (∀X.x). We have L |− T ⇒ f_{X}^{Z}(x)

.˙ .L |−T ⇒ ∀Z.f_{X}^{Z}(x)

By the choice of Z, ∀Z.f_{X}^{Z}(x) ∼ f(∀X.x) .˙ .L |−T ⇒ f(∀X.x). Right to Left. Suppose T ∈ A[f(∀X.x], i.e. L |−T ⇒ ∀X.f_{X}^{X}(x) .˙ .for all y, L |− T ⇒ (f_{X}^{X}(x))[y/X] (By Cut, and ∀L) suppose T ∉ ∩{A[f_{X}^{y}(x)] : A[y] ∈ V} .˙ .for some A[y] ∈ V, T ∉ A[f_{X}^{y}(x)]. But f_{X}^{y}(x) ∼ (f_{X}^{X}(x))[y/X], therefore L |− /T ⇒ (f_{X}^{X}(x))[y/X] which is a contradiction. □

M satisfies the axiom schemata R

Let x_{1}, …, x_{n} ⇒ y be an instance of an axiom schema. Let g be an arbitrary assignment and let sub be allowed by g. For each x_{i} choose an arbitrary T_{i} ∈ [[x_{i}]]^{g}, i.e. such that L |−T_{i} ⇒ sub(x_{i}). By preservation of derivability under substitution, we have L |−sub(x_{1}), …, sub(x_{n}) ⇒ sub(y). We obtain therefore L |−T_{1} … T_{n} ⇒ sub(y), i.e. T_{1} … T_{n} ∈ [[y]]^{g}. Hence we have shown [[x_{1}]]^{g}• … •[[x_{n}]]^{g} ⊆ [[y]]^{g}.

M is a countermodel to underivable sequents

Suppose for all g, [[x_{1}]]^{g}• … •[[x_{n}]]^{g} ⊆ [[y]]^{g}. Let sub be a null substitution. By the definition of V we can choose a g^{∗} such that sub is allowed by g^{∗}. We have L |−sub(x_{i}) ⇒ sub(x_{i}), hence sub(x_{i}) ∈ [[x_{i}]]^{g^{∗}}. Therefore under the supposition, we have sub(x_{1}), …, sub(x_{n}) ∈ [[y]]^{g^{∗}}, and therefore L |−sub(x_{1}), …, sub(x_{n}) ⇒ sub(y). Since sub is null we conclude L |−x_{1}, …, x_{n} ⇒ y.

2.2.5 Open question: P S_{2}^{inf}-completeness of l^{(/,\,∀,∃)}

We cannot extend the above proof to the case of calculi with existential quantifiers. As with the product, we have the problem that the canonical interpretation does not conform to the condition imposed by the connective. Consider ∃X.a/(X/X), and assume that it contains no free variables. To simplify, we will consider the case of the canonical model when there are no additional axioms. In the canonical model, in all assignments, then we would have [[∃X.a/(X/X)]]^{g} = A[∃X.a/(X/X)]. Clearly ∃X.a/(X/X) ∈ A[∃X.a/(X/X)], so we require that for some A ∈ V, ∃X.a/(X/X) ∈ [[a/(X/X)]]^{g_{X}^{A}}, and therefore for some y, ∃X.a/(X/X) ⇒ a/(y/y). However, there is no such y. For supposing there was such a y, then consideration of possible proofs gives that for some variable Z not occurring in y, we have L |−Z ⇒ y and L |−y ⇒ Z. By the soundness of L, then these two sequents by satisfied in every model and assignment, and this could only be the case if every model had a singleton range of quantification. In section 2.2.7 examples are given of models in the P S_{2,3}^{inf} class, which are ipso facto members of the P S_{2}^{inf} class, and these have non-singleton ranges of quantification.

P S_{2}^{inf} -completeness of l^{(/,\,∀,∃)} is therefore an open question.

2.2.6 Open question: P S_{2}-completeness

As in the case of l^{(/,\)}, the above construction is not possible when the set of atomic strings is required to be finite.

We might try to repeat the technique used for l^{(/,\)}. There the addition of a set of axioms rather than schemata was considered, and the atomic strings were taken to be the the subcategories of an underivable sequent together with the subcategories of the additional axioms, calling this set C. We then specified the interpretation as far as it concerned the members of C, arguing that it was clearly possible to extend this interpretation for categories outside of C in a way conforming to the conditions on interpretations.

In the quantified case it is not possible to isolate in this way the interpretation of the members of C from that of categories outside C. The canonical interpretation for quantified categories in C depends on all members of V, which itself must contain the interpretation of all categories, whether in C or not.

In order to guarantee that V contains the value of every category, perhaps the most natural assumption to make is that V is {A ↓_{C} [x] : x is some category}, and the same canonical interpretation as before is used. A problem arises in showing that this obeys the conditions on connectives. Choosing y outside C, it is possible that A ↓_{C} [sub(y)] is empty. If the canonical interpretation is to obey the conditions on connectives, we then require [[ sub(x/y) ]] to contain every sequence over C. However it will not be the case that every sequence derives sub(x/y).

P S_{2} completeness is therefore an open question.

2.2.7 The P S_{2,3}^{inf} class

Condition 2 is that V should contain all category values. Condition 3 is that V should contain only the values of closed categories. The two conditions together give that V should consist of exactly the values of closed categories. This combined condition is no recipe for constructing models as it makes V and the values of closed categories mutually dependent. There is clearly a question as to whether any such models exist. Our main aim in this section is to show the existence of polymorphic models meeting these two conditions.

Example One:

S is any set of strings closed under concatenation.

V= {S}

The interpretation is such that for basic categories, [[x]]^{g} = S.

For Condition 2, we simply check that V is closed under /,\, and ∩ and ∪. Because V contains only one set, Condition 2 entails Condition 3.

Example Two:

S is any set of strings closed under concatenation.

V = {S, ∅}.

The interpretation is such that for basic categories [[x]]^{g} ∈ V.

We note [[∃X.X]]^{g} = S ∪ ∅ = S, and that [[∀X.X]]^{g} = S ∩ ∅ = ∅. Thus V meets Condition 3. For Condition 2, we check that V is closed under /,\, and pairwise ∩, and ∪. This gives that unions and intersections over arbitrary subsets of V are contained in V.

Example Three:

S: {α, β}^{+}

V= {{αβ}, {α}, {β}, ∅, S}

We assume that for some basic category, s, [[s]]^{g} = {αβ}, for some basic category, np, [[np]]^{g} = {α}, and that all basic categories have a value identical to one of these.

For Condition 3 we note that V= {[[s]]^{g}, [[np]]^{g}, [[np\s]]^{g}, [[np/np]]^{g}, [[s/(np/np)]]^{g}}.

In showing Condition 2, we have to argue otherwise than in the previous examples because we do not have that the union over an arbitrary subset of V is in V. However, we require only the containment in V of unions (and intersections) over those subsets that represents the spectrum of values through which some category might range as the interpretation of some variable is varied. Define a spectrum of x, relative to an assignment g and a variable X as {[[x]]^{g_{A}^{X}} : A ∈ V}. Condition 2 may be reformulated as the requirement that all spectra are subsets of V, and this we will show, considering only categories with no vacuous quantification (vacuous quantifiers can be discarded without changing the denotation). The property is entailed by:

all spectra sp_{1}, sp_{2} of x are in (i) P(V) and (ii) if x is complex then for all B_{1}, B_{2} ∈ {{α}, {β}, {αβ}}, B_{1} ∈ sp_{1}, B_{2} ∈ sp_{2} implies B_{1} = B_{2}.

Proof

We show this by induction on the complexity of a category x. Consider variables and basic categories. Clearly the spectra of these are subsets of V, and so we have (i). Because x is not complex, (ii) is trivially true. Now for induction assume we have the property for all categories of complexity less than n and consider a category, x of complexity n.

• x = y/z. We first note the behaviours of / and \ on V:

\begin{matrix}/, \ & \{αβ\} & \{α\} & \{β\} & ∅ & S \\ \{αβ\} & ∅, ∅ & ∅, ∅ & \{α\}, ∅ & S, ∅ & ∅, S \\ \{α\} & ∅, \{β\} & ∅, ∅ & ∅, ∅ & S, ∅ & ∅, S \\ \{β\} & ∅, ∅ & ∅, ∅ & ∅, ∅ & S, ∅ & ∅, S \\ ∅ & ∅, S & ∅, S & ∅, S & S, S & ∅, S \\ S & S, ∅ & S, ∅ & S, ∅ & S, ∅ & S, S \end{matrix}

Let sp(x/y), sp(x) and sp(y) be spectra with respect to some g, some variable, X. By induction sp(x), sp(y) ⊆ V. Therefore, for any A ∈ V, [[y]]^{g_{X}^{A}}, [[z]]^{g_{X}^{A}} ∈ V, and by inspection we have that [[y/z]]^{g_{X}^{A}} ∈ V. Therefore sp(x/y) ⊆ V, i.e. (i). By inspection we see also that it is only possible for [[y/z]]^{g} to be in {{α}, {β}, {αβ}}, if in fact [[y/z]]^{g} = {α}. Hence we have (ii).

• x = z\y. There is a similar argument for this case.

• x = ∃X.y. Let sp be a spectrum of ∃X.y, for some assignment g and variable Z. Consider [[∃X.y]]^{g_{Z}^{A}}, for some A ∈ V. This is ∪sp_{A}, where sp_{A} is the spectrum of y for g_{Z}^{A} and the variable X. By induction, sp_{A} ⊆ V. When y is not complex, then sp_{A} is either a singleton subset of V or V itself, and so ∪sp_{A} ∈ V. When y is complex, then by induction we have that sp_{A} contains at most one member of {{α}, {β}, {αβ}}. This gives that ∪sp_{A} ∈ V. Therefore sp ⊆ V, i.e. (i). We must now show (ii) because ∃X.y is complex. First note that if y is not complex, y = X, and the unique spectrum of ∃X.y is {S}, and so (ii) is trivially satisfied. So suppose y is complex and suppose B_{1}, B_{2} ∈ {{α}, {β}, {αβ}}, such that B_{1} ∈ sp_{1}(∃X.y) and B_{2} ∈ sp_{2}(∃X.y) and suppose that B_{1} ≠ B_{2}. This implies spectra sp′_{1} and sp′_{2} of y and B′_{1}, B′_{2} ∈ {{α}, {β}, {αβ}}, such that B′_{1} ≠ B′_{2}, which contradicts our inductive assumption.

• x = ∀X.y. There is a similar argument for this case.

End of Proof We have now shown the P S_{2,3}^{inf} class is not empty. We now sketch a completeness proof for l^{(/,\,∀)}- the existential quantifiers are omitted because of the difficulties that were noted in the previous section.

Where for P S_{2}^{inf} completeness, we took the range of quantification in the canonical model to be the antecedents of any category, the natural move here is to set V to be the antecedents of any closed category:

Canonical Model

S = all sequences of categories

• = sequence concatenation

V = {A[x] : x is a closed category}

[[x]]^{g} = A[sub(x)], where sub is any substitution allowed by g

At two points of the proof for P S_{2}^{inf} we made use of the fact that V contains A[X], for any variable. We no longer have this, and to carry out the corresponding steps in the proof for P S_{2,3}^{inf}, we need the following as yet unproven lemmas

if L |−T ⇒ sub(x) for all sub taking variables to closed categories, then L |−T ⇒ sub′(x), where sub′ is any substitution.

if L |− / T ⇒ x then for some sub taking variables to closed categories: L |− / sub(T) ⇒ sub(x)

Clearly the model meets Condition 3. The model also meets Condition 2, because when x is open, [[x]]^{g} = A[sub(x)], for any substitution allowed by g. By the definition of V, sub(x) is closed and so A[sub(x)] ∈ V. It remains to check that the interpretation obeys the conditions on the connectives and that the model is counterexample to an underivable sequent.

We encounter a problem in showing that the canonical interpretation of universally quantified categories meets the required conditions. Consider [[∀X.x]]^{g}. Let f be an arbitrary substitution allowed by g. We need: ∩{A[f_{X}^{y}(x)] : A[y] ∈ V} = A[f(∀X.x)]. Previously we argued the left to right direction choosing for y a Z ∉ F V (T, f(Y)), where Y ∈ F V (∀X.x). This choice is not available in the current setting. At this point then we need the first of the above mentioned lemmas, taking us from the supposition that L |−T ⇒ sub(x) for all sub taking variables to closed categories, to the supposition that L |−T ⇒ sub′(x), where sub′ is any substitution.

In the proof for P S_{2}^{inf}, our argument that the model was a counterexample to any underivable sequent relied on the fact it was possible to choose an assignment, g_{∗} such that one allowed substitution is the null substitution: one assigns each variable the antecedents of that variable. Then to find a counterexample to an underivable T ⇒ y, for each x_{i} ∈ T, we chose x_{i} as a member of [[x_{i}]]^{g_{∗}}. We cannot argue in this way, because there is no longer a guarantee that an assignment exists, with respect to which one allowed substitution is null. Here we need to use the second of the above mentioned properties, namely that if L |− / T ⇒ x then for some sub taking variables to closed categories: L |− / sub(T) ⇒ sub(x). To find a counterexample to T ⇒ x, we then take the assignment such that g(X) = A[sub(X)], for each variable. For each x_{i} ∈ T, we have sub(x_{i}) ∈ [[x_{i}]]^{g}. On the other hand, we have sub(x_{1}), …, sub(x_{n}) ∉ [[y]]^{g}

3 Residuated Semi Group models

The ‘string semantics’ of the previous section was very concrete, and constructed the value of a category as a set of strings. There has also been investigation in the categorial grammar literature of a somewhat more abstract semantics which simply assumes the existence of objects which may serve as the values of categories. These are the residuated semi-group models. We begin by giving the relevant background for the quantifier-free calculi. We then consider how this notion of model should be extended to give a semantics also to the quantified calculi.

3.1 Background: quantifier-free calculi

3.1.1 Residuated Semi Group models for l^{(/,\)}, l^{(/,\,•)}

Def: Residuated Semigroup

⟨M, •, /, \⟩ is a residuated semi group if

• M is closed under •, /, \

• the operation • is associative

• M partially ordered

• the operations relate to the ordering in the following way

a ≤ c/b iff a•b ≤ c iff b ≤ c\a

Following [Buszkowski, 1986], we will refer to the class of all residuated semi-groups as RES. Where C varies over connectives, and C over the corresponding operation, we define a RESinterpretation as follows:

\underline{Def: RES model} ⟨M, •, /, \, [[]]⟩ is a RES-model if:

• ⟨M, •, /, \⟩ ∈ RES

• Condition on [[]], where C is ‘/’,‘\’,‘•’

[[C(x, y)]] = C([[x]], [[y]]).

As ever, it would be equivalent to define interpretation to concern just the atomic categories, to be extended in accordance with the above conditions. Satisfaction, ⊧, is defined:

Def: satisfaction

⟨R, [[]]⟩ ⊧ x_{1}, …, x_{n} ⇒ y iff [[x_{1}]]• … •[[x_{n}]] ≤ [[y]]

By an easy induction, using the inequalities required for a RES model, one show that the rules of l^{(/,\)} and l^{(/,\,•)} are satisfaction preserving, and thus that they are sound for consequence.

3.1.2 RES-completeness of l^{(/,\,•)}

One can quickly define from a S^{inf} model, a RES model, and one satisfying the same sequents. Thus completeness of l^{(/,\,•)} with respect to the S^{inf} class would entail completeness with respect to the RES class. However, as noted earlier, there are difficulties in giving a stringsemantic completeness proof for l^{(/,\,•)}, and for this reason an independent RES completeness proof is given. In [Buszkowski, 1986] it is shown that l^{(/,\,•)} is RES-complete for consequence under the addition of any set R of axioms. As a preliminary we outline of a slight variant of Buszkowski’s proof of RES-completeness.

Assume a particular set R of axiom schemata, and let L be l^{(/,\,•)}+ R + Cut. The canonical model is:

Canonical Model

M = {A[x] : x is a category}
where C = /,\,•, C(A[x], A[y]) = A[C(x, y)]
A[x] ≤ A[y] iff L |−x ⇒ y.
[[x]] = A[x]

That the operations of the canonical model are well defined follows from Lemma 1. That the ordering is well defined is also quickly shown. We must check that • is associative, that the defined ordering is a partial order, and that that the required inequalities hold. All of this is straightforward, and we give just one example for the inequalities:

A[x] ≤ A[z]/A[y]
iff A[x] ≤ A[z/y]
iff x ⇒ z/y
iff x•y ⇒ z
iff A[x•y] ≤ A[z]
iff A[x]•A[y] ≤ A[z]

Thus we have a residuated semi-group. From the definition of the operations, it is immediate that the model meets the conditions concerning the connectives, so that we have a RES-model. One easily shows that all instances of the axiom schemata R are satisfied and that no underivable sequent is.

Product Free Version

One might ask about the corresponding completeness of l^{(/,\)}. There is no corresponding version of the above proof if we do not have the product in the syntax: the product in the syntax was used to define the product operation of the residuated semigroup. However, we can show RES-completeness of l^{(/,\)}in two ways. One is to take the S^{inf} models of l^{(/,\)} and regard them as RES-models. Another route to RES completeness is via the observation that l^{(/,\,•)} is a conservative extension of l^{(/,\)}. Thus an underivable sequent, T ⇒ x, of l^{(/,\)} is also an underivable sequent of l^{(/,\,•)}. The version of the completeness theorem for l^{(/,\,•)} that assumes no additional axioms, then gives that there is a countermodel to T ⇒ x. Thus we have that l^{(/,\)} is complete for validity (i.e. in the absence of Cut and additional axioms).

3.2 Quantified Calculi with product

3.2.1 Residuated Semi Group models for Quantified Calculi

For the quantified calculi we assign a value to a category relative to an assignment as usual, and interpret universal and existential quantifiers via greatest lower and least upper bounds.

\underline{Def: P RES model} ⟨M, •, /, \, [[]]⟩ is a RES-model if:

• ⟨M, •, /, \⟩ ∈ RES

• Condition on [[]], where C is ‘/’,‘\’,‘•’ [[C(x, y)]]^{g} = C([[x]]^{g}, [[y]]^{g}). [[x]]^{g} = g(x), if x is variable [[x]]^{g_{1}} = [[x]]^{g_{2}}, if x is basic [[∀X.x]]^{g} = g.l.b ({[[x]]^{g_{X}^{A}} : A ∈ M}) [[∃X.x]]^{g} = l.u.b ({[[x]]^{g_{X}^{A}} : A ∈ M})

Here we have not included the range of quantification as a separate parameter: the range of quantification is identified with the carrier of the residuated semi-group. This is because, unlike in the string-semantic case, no incompleteness arises from this insistence on the maximum range of quantification.

We will show P RES-completeness for consequence of l^{(/,\,•,∀,∃)}.

3.2.2 P RES-completeness for l^{(/,\,•,∀,∃)}

Let L be L + Cut + R for some set of axiom schemata R. The canonical model M is defined thus:

Canonical Model

M = {A[x] : x is a category} where C = /,\,•, C(A[x], A[y]) = A[C(x, y)] A[x] ≤ A[y] iff x ⇒ y. [[x]]^{g} = A[sub(x)], for any substitution sub allowed by g

M is a model

This mainly as before. We have now additional work to show that the proposed interpretation conforms to the conditions on the connectives:

• x is basic: the interpretation is clearly independent of assignment.

• x is a variable, X. Suppose g(X) = A[y]. [[X]]^{g} = A[sub(X)] = A[y]

• Where C is a binary connective [[C(x, y)]]^{g}. Let sub be allowed by g. We require [[C(x, y)]]^{g} = C([[x]]^{g}, [[y]]^{g}). C([[x]]^{g}, [[y]]^{g}) = C(A[sub(x)], A[sub(y)]) = A[C(sub(x), sub(y))] = A[sub(C(x, y))].

• [[∀X.x]]^{g}. We require that A[sub(∀X.x)] is the g.l.b. of {A[sub_{X}^{y}(x)] : A[y] ∈ M}. A[sub(∀X.x)] is a l.b.: we require that for any y, A[sub(∀X.x)] ≤ A[sub_{X}^{y}(x)], i.e L |−sub(∀X.x) ⇒ sub_{X}^{y}(x). We can assume without loss of generality that sub precipitates no changes of bound variables in ∀X.x, i.e. sub(∀X.x) = ∀X.sub_{X}^{X}(x). Therefore by a (∀L) inference, L |−sub(∀X.x) ⇒ sub_{X}^{y}(x). A[sub(∀X.x)] is a g.l.b.: Let A[z] be a l.b. of {A[sub_{X}^{y}(x)] : A[y] ∈ M}. That is suppose for any y, L |−z ⇒ sub_{X}^{y}(x) If Z is some variable not free in x, nor sub(Y), where Y ∈ F V (x), then sub(∀X.x) ∼ ∀Z.sub_{Z}^{Z}(x[Z/X]) ∼ ∀Z.sub_{X}^{Z}(x). Let Z be also not free in z. We have L |−z ⇒ sub_{X}^{Z}(x), and by the choice of Z, we have L |−z ⇒ ∀Z.sub_{X}^{Z}(x). Therefore L |−z ⇒ sub(∀X.x), and sub(∀X.x) is the g.l.b.

• [[∃X.x]]^{g}. We require that A[sub(∃X.x)] is the l.u.b. of {A[sub_{X}^{y}(x)] : A[y] ∈ M}. A[sub(∃X.x)] is a u.b.: we require that for any y, A[sub_{X}^{y}(x)] ≤ A[sub(∃X.x)], i.e L |−sub_{X}^{y}(x) ⇒ sub(∃X.x). Without loss of generality we can assume that sub(∃X.x) = ∃X.sub_{X}^{X}(x). Therefore by a (∃ R) inference, L |−sub_{X}^{y}(x) ⇒ sub(∃X.x). A[sub(∃X.x)] is a l.u.b.: Let A[z] be a u.b. of {A[sub_{X}^{y}(x)] : A[y] ∈ M}. That is suppose for any y, sub_{X}^{y}(x) ⇒ z If Z is some variable not free in x, nor sub(Y), where Y ∈ F V (x), then sub(∃X.x) ∼ ∃Z.sub_{Z}^{Z}(x[Z/X]) ∼ ∃Z.sub_{X}^{Z}(x). Let Z be also not free in z. We have that L |−sub_{X}^{Z}(x) ⇒ z, and by the choice of Z, we have L |−∃Z.sub_{X}^{Z}(x) ⇒ z. Therefore L |−sub(∃X.x) ⇒ z, and sub(∃X.x) is the l.u.b.

As in earlier proofs, it is easy to show that all axioms are satisfied in all assignments, and that for any underivable sequent there is an assignment that leaves it unsatisfied: the assignment allows a null substitution.

3.2.3 Open question: P RES-completeness for l^{(/,\,∀,∃)}

We consider now quantified, product-free calculi. As with the product-free, quantifier-free calculus, there are two ways to approach this.

On the first, we might try to regard the string-semantic models as P RES-models. We gave a completeness proof for l^{(/,\,∀)} with respect to the class of P S_{2}^{inf} models, that is those models in which the range of quantification may be fail to contain some sets of strings but must contain the value of every category. We cannot, however, always regard the range of quantification of a P S_{2}^{inf} model as the carrier of a RES model: the range of quantification is not necessarily closed under the (string-semantic versions of the) /,\ and • operations.

On the second approach, we check whether l^{(/,\,•,∀,∃)} is a conservative extension of l^{(/,\,∀,∃)}, because then completeness for l^{(/,\,•,∀,∃)} will entail completeness for l^{(/,\,∀,∃)}. However, l^{(/,\,•,∀,∃)} is not a conservative extension of l^{(/,\,∀,∃)}, as we now show.

Proof

The following product free sequent is derivable in l^{(/,\,•,∀,∃)}, but not l^{(/,\,∀,∃)}(where a, b and c are atomic and distinct):

a/d/c, ∀X.X/(X\b)/X, c, d, d\c\b ⇒ a

We first argue that the sequent will only have a proof if we can find an \overline{X} that make the leaves of the following proof derivable:

a/d/c, \overline{X} ⇒ a \overline{X}, d\c\b ⇒ b c, d ⇒ \overline{X} \R d\c\b ⇒ \overline{X}\b  /L/L a/d/c, \overline{X}/(\overline{X}/b)/\overline{X}, c, d, d\c\b ⇒ a ∀L a/d/c, ∀X.X/(X/b)/X, c, d, d\c\b ⇒ a

One can quite quickly eliminate other possible proofs shapes by applying the following observations about proofs. 1) Let the spine of a product free category be recursively defined spine(x/y) = ⟨/, spine(x)⟩, spine(y\x) = ⟨\, spine(x)⟩, spine(∀X.x) = ⟨∀, spine(x)⟩, with spine(x) = ⟨⟩ otherwise. One can easily show that when a series, ζ, of inferences belonging to { Slash L, Slash R, ∀L, ∀R }, separates a pair of inference steps # and $ belonging to { Slash L, ∀L }, associated with two consecutive connectives on the spine of a category, then there is an alternative proof, ordering ζ before # and $, and with # and $ consecutive. 2) Slash (and ∀) Right inferences can be ordered before all others without loss of generality. 3) Quantifier-free sequents must satisfy count-invariance [van Benthem, 1986].

The derivability of the sequent thus reduces to the problem of finding an \overline{X} making the following derivable:

1. a/d/c, \overline{X} ⇒ a
2. \overline{X}, d\c\b ⇒ b
3. c, d ⇒ \overline{X}

Clearly, in the case of l^{(/,\,•,∀)}, c•d is such a value for \overline{X}. We will show that there is no product-free value.

First \overline{X} clearly cannot be atomic. If the principal connective of \overline{X} is a slash, then to solve 1, this must be ‘\’, whilst to solve 2, this must be ‘/’. This leaves just the possibility that \overline{X} is quantified. Suppose \overline{X} is Q_{1}Y_{1} … Q_{n}Y_{n}.y, n ≥ 1. We can assume that the quantifiers are not vacuous: dropping a vacuous quantifier will give another solution for \overline{X}. In the case that n = 1, the candidate solution is either ∀Y_{1}.Y_{1} or ∃Y_{1}.Y_{1}, and the first is not a solution for 3, whilst the second is not a solution for 1 or 2. If n > 1, then y must have a slash as principal connective, either left or right. Also the proofs of 1 and 2 must end with a succession of n (QL) inferences, transforming Q_{1}Y_{1} … Q_{n}Y_{n}.y to y_{1} in the proof of 1, and to y_{2} in the proof of 2. The two proofs will therefore contain the premises:

1′: a/d/c, y_{1} ⇒ a
2′: y_{2}, d\c\b ⇒ b

y_{1} must have a principal left slash, and y_{2} a principal right slash, but both y_{1} and y_{2} will have the same principal slash as y. Hence there is no quantified solution for \overline{X}. □

4 Ternary Frame Semantics

In moving from the string semantics to the residuated semi-groups we made one kind of abstraction, abandoning the idea that the value of a category should be a set of linguistic items. The ternary frame semantics represents another direction of abstraction, in which categories are still interpreted as sets of linguistic items, but the interrelation of these items is abstractly defined by a 3-place ‘accessibility’ relation. Below we recap the basics of this for quantifier-free calculi, before then considering the quantifiers.

4.1 Background: quantifier-free calculi

Def: Associative Ternary Frame

⟨W, R⟩ is an associate ternary frame if • W is a non-empty set

• R a ternary relation on W

• ∀x, y, z, u ∈ W (∃s(Rxys ∧ Rszu) iff ∃t(Rxtu ∧ Ryzt))

Def: Associative Ternary Frame Interpretation

⟨W, R, [[]]⟩ is an associative ternary frame interpretation if

• ⟨W, R⟩ is an associative ternary frame

• [[]] assigns the categories subsets of W, subject to: [[a•b]] = {x : ∃y, z(Ryzx ∧ y ∈ [[a]] ∧ z ∈ [[b]])} [[a\b]] = {x : ∀y, z(Ryxz ∧ y ∈ [[a]] ⟶ z ∈ [[b]])} [[b/a]] = {x : ∀y, z(Rxyz ∧ y ∈ [[a]] ⟶ z ∈ [[b]])}

Def: satisfaction

⟨W, R, [[]]⟩ ⊧ x_{1}, …, x_{n} ⇒ y iff [[x_{1}• … •x_{n}]] ⊆ [[y]].

Concerning l^{(/,\,•)} it is known [Dosen, 1990]:

l^{(/,\,•)} |−a ⇒ b iff every interpretation relative to every associative ternary frame satisfies a ⇒ b

The worlds of the canonical model are categories, and the accessibility relation, R is R(x, y, z) iff l^{(/,\,•)} |−z ⇒ x•y.

4.2 Quantified Calculi with product

In the same way that the string-semantic models were extend to give a semantics to calculi with quantifiers, one can revise the above to give interpretation relative to an assignment

Def: Quantified Associative Ternary Frame Interpretation

⟨W, R, V, [[]]⟩ is quantified associative ternary frame interpretation if

• previous conditions

• V ⊆ P(W)

• further conditions on [[]] [[x]]^{g} = g(x) of x is a variable [[x]]^{g} = [[x]]^{h} if x is basic [[∀X.x]]^{g} = ∩{[[x]]^{g_{X}^{A}} : A ∈ V} [[∃X.x]]^{g} = ∪{[[x]]^{g_{X}^{A}} : A ∈ V}

As in the case of the string-semantics, one may wish to consider restrictions on V such as: 1. V= P(W), 2. V covers the categories, 3. V is covered by the closed categories. The soundness of the quantified calculi with respect to this notion possible model under the imposition of Condition 2 is easily shown. Clearly also we may view a string semantic model as a ternary frame model, taking the strings as the worlds and the accessibility relationship as R(a, b, a•b). Thus the earlier completeness for l^{(/,\,∀)} with respect to P S_{2}^{inf} entails completeness for l^{(/,\,∀)} with respect to ternary frames in which V covers the categories.

4.2.1 Restrictions on accessibility which give incompleteness

For the string-semantic models we showed by means of particular examples that completeness did not hold under the restriction that V was in all cases the power set of the underlying algebra. Naturally, if we restrict the ternary frame-models to those which are effectively a representation of a string-semantic model, then the examples will function as they did before.

We will show now that there is more than one way to restrict the accessibility relation, Rxyz, making it approximate more or less closely the process of constructing z by concatenating x with y, and thereby make the previous counterexamples to completeness again effective. Consider the following constraints:

atom ∃z∀x∀y¬(Rxyz)

destinations ∀x∀y∃zR(xyz)

decompose if Rxyz and Rxy′z then y = y′

We will show that imposing atom and destinations will force [[∀X.X/X]]^{g} = ∅, and not force [[∀X.(X/np)\X]]^{g} ⊆ [[np]]^{g}, whilst destinations with decompose will force [[∀X.(X/np)\X]]^{g} ⊆ [[np]]^{g}, and not force [[∀X.X/X]]^{g} = ∅. Thus the two ways restrict the accessibility relation both give incompleteness, and this incompleteness shows itself in different counterexamples in each case.

Proof

Consider models with an accessibility relation constrained by atom and destinations. Consider a ∈ [[∀X.X/X]]^{g}. Thus for any B ⊆ W, a ∈ [[X/X]]^{g_{X}^{B}}. By the atom condition, there is some some b such that ∀x∀y¬(Rxyb). So choosing B = {b}, we have ∀z(Rabz ⟶ ¬(Rabz)). This could only be true for ¬∃z(Rabz), which contradicts destinations. Therefore [[∀X.X/X]]^{g} is empty.

Now consider a ternary frame with W = {q, n}, R = {xyn : x, y ∈ W }. This is associative, satisfies atom and destinations, and does not satisfy decompose. We will suppose that [[np]]^{g} = {n}, and show that [[∀X.X/(np\X)]]^{g} = {q, n}. Thus in this interpretation, [[∀X.(X/np)\X]]^{g} ⊈ [[np]]^{g}. For any A ⊆ W, x ∈ [[X/(np\X)]]^{g_{X}^{A}} iff ∀y∀z(y ∈ [[np\X]]^{g_{X}^{A}} , Rxyz ⟶ z ∈ [[X]]^{g_{X}^{A}}) iff ∀y(y ∈ [[np\X]]^{g_{X}^{A}} ⟶ n ∈ A) Therefore x ∈ [[X/(np\X)]]^{g_{X}^{A}} for all x. For if n ∈ A, the succedent is true, and if n ∉ A, then the antecedent is false.

Consider now models with an accessibility relation constrained by destinations, decompose. Suppose q ∈ [[∀X.((X/np)\X)]]^{g}, and q ∉ [[np]]^{g}. Thus for any B ⊆ W, q ∈ [[((X/np)\X)]]^{g_{X}^{B}}. For some b, put B = {z : ∃n ∈ [[np]]^{g}, Rbnz}. Then b ∈ [[X/np]]^{g_{X}^{B}} iff for all n ∈ [[np]]^{g}, for all z such that Rbnz, there is n′ ∈ [[np]]^{g} such that Rbn′z. Thus b ∈ [[X/np]]^{g_{X}^{B}}. Since q ∈ [[((X/np)\X)]]^{g_{X}^{B}}, then for all z such that Rbqz, there exists n ∈ [[np]]^{g} such that Rbnz. By destinations, there is some z such that Rbqz, so for some n ∈ [[np]]^{g}, Rbnz. Because we have Rbqz and Rbnz, we have by decompose, q = n, and thus q ∈ [[np]]^{g}.

Now consider the ternary frame with W = {a, b}, R = {xyy : x, y ∈ W }). This is associative, does not satisfy atom, and satisfies destinations and decompose. We show that [[∀X.X/X]]^{g} ≠ ∅. For any A ⊆ W, x ∈ [[X/X]]^{g_{A}^{X}} iff ∀y∀z(y ∈ A, Rxyz ⟶ z ∈ A) iff ∀y, (y ∈ A, Rxyy ⟶ y ∈ A)

Therefore, for each A ⊆ W, [[X/X]]^{g_{A}^{X}} = W, and therefore [[∀X.X/X]]^{g} = W.

End of Proof

5 Concluding Remarks

The main aim of this paper has been to take the so-called string-semantic tradition of quantifierfree Lambek calculus and to see how it may be extended to the calculus with quantifiers. We saw seen that the quantifiers cannot be interpreted as simply ranging over arbitary sets of strings: the calculus will in this case will be incomplete. We then sought to formalise the idea that the quantifiers should range over those sets of strings that are the value of a category. We considered classes of models which allow the range of quantification to be less than every possible set of strings, and concerning which we could specify two further conditions. The first was that the range of quantification must cover the categories, meaning that it must contain as a subset the values of all categories. Since all members of the range of quantification are the value of some category, this condition formalises one sense in which the range of quantification should coincide with values of categories. We showed completeness of the /,\,∀ calculus with respect to this notion. The second condition was that every set in the range of quantification should be the value of some closed category. The conditions together formalise the idea that the range of quantification should coincide with the values of the closed categories. We showed the existence of models meeting the conditions, and conjectured completeness, indicating two as yet outstanding lemmas which would suffice for completeness.

Having considered string-semantics, we considered briefly also two further semantic traditions in the categorial grammar literature. The valuations into a residuated semi-group were taken to be apt for the quantified calculi if the values were particular g.l.b’s and l.u.b’s. With respect to this notion of model we showed completeness of the /,\,•,∀,∃ calculus. As a side observation, we noted that the quantified calculus with product is not a conservative extension of the quantified calculus without product. For this reason completeness for the product-free quantified calculus remains an open question. We finally considered the ternary-frame semantics. Because the polymorphic string semantic interpretations are a special case of a polymorphic ternary frame interpretation, the completeness results for the polymorphic string semantic interpretations carry over. We then reconsidered the counterexamples to completeness that arose in the stringsemantics when quantifiers were allowed to range over arbitrary sets of strings. We found that with different ways of restricting the accessibility relationship in order to approximate the relationship between two strings and their concatenation, different ones of the previous counterexamples reemerge as counterexamples.

Concerning the polymorphic string semantics a number of questions remain unanswered. Besides those mentioned in the text, a question awaiting further research is how constrained we are in choosing the range of quantification. In particular, with the interpretation of the basic categories as fixed elements of the range of quantification, is there more than one range of quantification possible ? If there is more than one, what is the pattern amongst the possibilities ?

References

[Buszkowski, 1982] Wojczech Buszkowski. Compatibility of A Categorial Grammar with an associated Category System. In Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28, 1982

[Buszkowski, 1986] Wojczech Buszkowski. Completeness results for Lambek Syntactic Calculus. In Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 32, pp 13–28, 1986

[Dosen, 1990] Kosta Dosen. A Brief Survey of Frames for the Lambek Calculus Bericht 5-90, Zentrum Philosophie und Wissenschaftstheorie, Universität Konstanz.

[Emms, 1989] Martin Emms. Polymorphic Quantifiers. In Torenvliet, M.S.L. (eds) Seventh Amsterdam Colloquium Proceedings, pp139–163

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

[Emms, 1993b] Martin Emms. Some Applications of Categorial Polymorphism. In dyana Deliverable R1.3.A, 1993

[Emms, 1993c] Martin Emms. Movement in Labelled and Polymorphic Calculi. Proceedings Rome Workshop

[Emms, 1993d] Martin Emms. Extraction Covering Extensions of the Lambek Calculus are not Context Free. In Dekker, P. and Stokhof, M. (eds) Ninth Amsterdam Colloquium Proceedings, p268–286

[Emms, 1992] Martin Emms. Logical Ambiguity. PhD Thesis, Centre of Cognitive Science, Edinburgh.

[Emms and Leiß, 1993] Martin Emms and Hans Leiß. Cut Elimination in the Second Order Lambek Calculus. In dyana Deliverable R1.1.A, 1993

[Henkin, 1950] L. A. Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15, 81–91, 1950.

[Lambek, 1958] Joachim Lambek. The mathematics of sentence structure. American Mathematical Monthly, 65:154–170, 1958.

[Pentus, 1993] Mati Pentus. Lambek Grammars is L-complete. preprint, Dept of Mathematical Logic, Moscow University, 1993

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