An Undecidability Result for Polymorphic Lambek Calculus

Martin Emms, Centrum für Informations- und Sprachverarbeitung, Universität München, Wagmüllerstr. 23, München 80538

                          emms@cis.uni-muenchen.de

1 Introduction

A precursor to linear logic was introduced in [Lambek, 1958], who proposed a single conclusion sequent calculus which lacked the structural rules of Contraction, Weakening and Permutation. Three connectives are treated, two directed implications / (right to left),\ (left to right), and a product, which can be identified with linear logic’s multiplicative conjunction. This calculus was introduced as a means for reasoning about sequences of linguistic objects, a domain in which the customary structural rules are clearly not generally valid. On grounds of linguistic expressivity, there are motivations for considering the calculus which results from the addition of second order quantifiers – the Polymorphic Lambek Calculus (PLC). For example, where [Pentus, 1992] shows that grammars based on the Lambek calculus can recognise exactly the context-free languages, [Emms, 1993c] shows that grammars based on PLC can recognise a strictly larger class of languages. By now a certain amount is known about PLC. Besides the above mentioned recognising power result, there is in [Emms, 1993b], [Emms, 1994a] discussion of several kinds of linguistic applications, in [Emms and Leiß, 1993] a Cut elimination result, in [Emms, 1994b] several completeness results, and in [Emms, 1993a] a decidability result for a subset of all possible sequents. An open question, however, has been decidability in the general case. We will show below that PLC can embed the extension of PLC with the structural rules of Permutation, Contraction and Weakening, and thereby obtain a proof of the undecidability of PLC. We will also show that the connectives (/,\,∀) suffice to express a variety of other connectives, amongst which are the product, •, the existential quantifier, and the multiplicative unit, 1.

2 Preliminaries

Assume a denumerably infinite set of variables. We specify various propositional languages by L, followed by a series of connectives drawn from the set {1, 0, ⊤, /, \, •, ∀, ∃}. The calculi of concern will be defined with reference to Figures 1 and 2. Following the linear logic tradition according to the role of the context, the connectives 1, /, \, and • are described as multiplicative, whilst 0 and ⊤ are referred to as additive. The rules derive sequents from sequents, where a sequent is an antecedent sequence of formulae, followed by ‘ ⇒ ’, and then a single formula. w, x, y range over formulae, U, V, T range over sequences of formulae. x[y/Z] stands for the substitution of y for Z in x, defined to include a change of bound variable to avoid accidental capture. 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 will use l superscripted with a sequence of connectives ⟨c_{i}⟩_{1≤i≤n} to stand for the calculus obtained by taking the identity axiom scheme, together with the rules associated with each of the

x ⇒ x

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, V ⇒ w 1 L U, 1, V ⇒ w  ⇒ 1

U, 0, V ⇒ w

T ⇒ ⊤

Figure 1: Identity axiom, and rules for /,\,•,∀,∃,1,0, ⊤

T_{1}, T_{2} ⇒ w Weak T_{1}, x, T_{2} ⇒ w  T_{1},x, x, T_{2} ⇒ wContr T_{1}, x, T_{2} ⇒ w  π(T) ⇒ wPerm T ⇒ w

Figure 2: Structural Rules connectives c_{i}, with in the case of ∀L and ∃R, the formula y substituted for the bound variable being drawn from the appropriate language: L(⟨c_{i}⟩_{1≤i≤n}). A parameter that may be varied is whether sequents with an empty antecedent sequence are admitted. When this is the case we subscript the name of the calculus with ϵ (clearly the axiom scheme ⇒ 1 is omitted when there is no ϵ subscript). The calculi including the second-order quantifiers we will refer to as polymorphic. In this notational scheme, l^{/,\,•} is the calculus proposed in [Lambek, 1958]. For any of the calculi that may be defined in this way, the derivability of the following Cut rule can be shown (by an inductive argument on the sizes of the premise proofs of a Cut^{1})

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

Let LJ2 be l_{ϵ}^{1,/,•,∀} + W eak + Contr + P erm. This is a formulation of 2nd order intuitionistic propositional logic. It is also the case that the Cut rule is derivable in LJ2, as is shown in [Tait, 1966] (using a semantic argument). The undecidability of LJ2, which will be used below, is shown in [Löb, 1976],[Gabbay, 1981].

It is clear that l_{ϵ}^{1,/,•,∀} + P erm can be seen as a notational variant of second-order intuitionistic multiplicative linear logic, referred to as IMLL2 in [Lincoln et al, 1995].

A simple property of any of the l^{/,\,...} or l_{e}^{/,\,...} calculi is^{2}:

Lemma 1 (Unknown Elimination) where l is one of the l^{/,\,...} or l_{e}^{/,\,...} calculi then

there is an \overline{X} with F V (\overline{X}) ⊆ F V (U, V, w) such that l |−U, \overline{X}, V ⇒ w l |−T_{1} ⇒ \overline{X} ⋮ l |−T_{n} ⇒ \overline{X}\} iff \{l |−U, T_{1}, V ⇒ w ; ⋮ ; l |−U, T_{n}, V ⇒ w

Proof: for one direction use Cut and Cut Elimination, for other choose \overline{X} = U\w/V (shorthand for u_{n}\ … u_{1}\w/v_{n}/ … /v_{1}) When we use this to infer the derivability of two premises U, \overline{X}, V ⇒ w and T ⇒ \overline{X} from U, T, V ⇒ w we write:

\overbrace{U, \overline{X}, V ⇒ w T ⇒ \overline{X}}^{U, T, V ⇒ w}

3 Polymorphic Reconstruction of Structural Rules

It is well known that the absence of structural rules can be compensated for by adding new axiom schemes and Cut. Example where l is l^{1,/,•,\,...} or l_{ϵ}^{1,/,•,\,...},

1Lambek’s proof of Cut elimination for l^{/,•,\} by induction on the complexity of the Cut formula, does not work for the polymorphic calculi. The absence of the contraction rule, however, allows a similarly simple proof to be given by induction on proof size. See [Emms and Leiß, 1993].

2This is not the same as Interpolation, since we do not require the material of \overline{X} to occur in both T and (U, V, w).

l+P erm  is equivalent to l+Cut + {x ⇒ (y•x)/y, or ; x ⇒ y/(y/x), or ; ...  }

Example where l is l^{1,/,•,\,...} or l_{ϵ}^{1,/,•,\,...},

l+W eak is equivalent to l+Cut + {x ⇒ x/y, x ⇒ y\x, or ; x ⇒ 1, or ; ... }

Example where l is l^{1,/,•,\,...} or l_{ϵ}^{1,/,•,\,...},

l+Contr is equivalent to l+Cut+{x ⇒ y/(x\x\y), x ⇒ (y/x/x)\x, or ; x ⇒ x•x, or ; ... }

We note here the the proof in the case of permutation, choosing the first formulation of the ‘permutation’ axiom. From right to left it suffices to note that the ‘permutation’ axiom is derivable in l + Perm. From left to right, it clearly suffices to show that U, a, V ⇒ w implies a, U, V ⇒ w, and this we have, given Lemma 1, by the derivation:

a ⇒ (\overline{X}•a)/\overline{X} \overbrace{U, \overline{X}, V ⇒ w T ⇒ \overline{X}}^{U, T, V ⇒ w}/L,•L (\overline{X}•a)/\overline{X}, U, V ⇒ wCut a, U, V ⇒ w

3.1 Axiom Schemes to Polymorphic Categories

In [Emms, 1993c], in proving that there are 2nd order Lambek grammars for the permutation closure of any CF language, it was shown how one can in a certain sense, trade an axiom scheme expressing permutation for a polymorphic category. We recap briefly the essentials of the argument made there. All the ‘permutation’ axiom does is allow one to convert a to (y•a)/y, for any y, and in each derivation of π(a_{1}, …, a_{n}) ⇒ w from a_{1}, …, a_{n} ⇒ w, we need to apply the ‘permutation’ axiom scheme just once to each antecedent. It is clear then that if a lexical item categorised as a, could also be categorised as (y•a)/y, for all y then that lexical item could be moved to the front of any construction in which it appears grammatically. This is out of the reach of the Lambek calculus, as we can only assign finitely many categories lexically, and there is no valid conversion from a to (y•a)/y. However, this is within reach of a polymorphic grammar, simply by assigning all a-items also the category ∀X.(X•a)/X. It should not be a surprise that when this is done to every lexical item, the enlarged grammar generates all permutations of strings recognised by the previous grammar. Let x ⇒ p(x, y) be any permutation axiom, i.e p(x, y) might be (y•x)/y, or y/(y/x), or w/(y\w)/(y/x). Then one can show that if G is an L lexicon, and G′ expands by adding ∀Y.p(a, Y), for each G-entry am then perm(lang(G)) ⊆ lang(G′). The special case of this was proved in [Emms, 1993c], with p(a, y) = w/(y\w)/(y/a), as part of the proof that there are l^{(/,\,∀)} grammars for the permutation closure of any CF language.

What is noticeable here is that although l^{(/,\,∀)} grammars for the permutation closure of a CF language are obtained, it is not the case that Permutation is a derivable rule in l^{(/,\,∀)}. In other words, one can get permutation closures when one had no right to expect that one would. This is symptomatic of an embedding of a stronger logic into a weaker one. Given the fact that each structural rule matches up with an axiom scheme, there is reason to think that there may in fact be ways to embed the structurally more relaxed logics into the polymorphic calculus. This is born out in the following section.

3.2 Structural Rules to Polymorphic Categories

In [Lincoln et al, 1995] there is a proof of such an embedding of a structurally more relaxed into a structurally stricter logic. The target logic of the embedding is IMLL2 (= l_{ϵ}^{1,/,•,∀} + Perm), and the source is LJ2 (= l_{ϵ}^{1,/,•,∀} + Contr + Weak + Perm). They note that certain quantified formulae seem to describe the action of the Contraction and Weakening rules. Let us refer to ∀X.(X•X)/X as C, and ∀X.1/X as W (note the connection with the above mentioned ‘contraction’ and ‘weakening’ axioms). As is quickly seen, the presence of an antecedent C licenses a single application of Contraction in the sense that: if IMLL2 |− U, x, x, V ⇒ w is derivable, then IMLL2 |− C, U, x, V ⇒ w is derivable, and likewise an antecedent W licenses a single application of Weakening: if IMLL2 |− U, V ⇒ w is derivable, then IMLL2 |− U, x, V ⇒ w is derivable. Expressed as it is by a formula of a linear calculus, IMLL2, such a license to apply a structural rule is gone as soon as it has been used — in contrast to formulae marked with linear logic’s exponentials, for which the repeated application of structural rules is licensed. However, the surprising fact pointed out in [Lincoln et al, 1995] is that when C, C, C, W is prefixed to a sequence T, one has license to apply Contraction and Weakening to T indefinitely often. We show this for the Contraction case below:

‘Contraction’ C, C, C, W, U, a, a, V ⇒ x•L C, C, C, W, U, a•a, V ⇒ x a ⇒ a∀L,/L C, C, C, W, U, C, a, V ⇒ x Perm C, C, C, C, W, U, a, V ⇒ x •L,•L, •L (C•C)•(C•C), W, U, a, V ⇒ x  C ⇒ C C ⇒ C•R C, C ⇒ C•C∀L,/L C, C, C, W, U, a, V ⇒ x (1)

This is the key to the embedding proved in [Lincoln et al, 1995] of LJ2 into IMLL2. We will carry this strategy of rexpresssing structural rules polymorphically one step further, moving the target logic for the embedding from IMLL2, which has Permutation, to l_{ϵ}^{1,/,•,\,∀}, which has no Permutation. Let us define P as ∀X∀Y.(X•Y)/X/Y. Then we observe P licenses left-ward shift, in the sense that where l is any of the l_{ϵ}^{1,/,•,\,∀,...} calculi if l |− U, a, V ⇒ w, then l |− P, a, U, V ⇒ w also. Given Lemma 1, this is established by the following derivation scheme:

\overbrace{_{\overline{X}, a, V ⇒ w•L \overline{X}•a, V ⇒ w}  U ⇒ \overline{X}}^{U, a, V ⇒ w}/L (\overline{X}•a)/\overline{X}, U, V ⇒ w  a ⇒ a/L (\overline{X}•a)/\overline{X}/a, a, U, V ⇒ w∀L \underbrace{∀X∀Y.(X•Y)/X/Y}_{P}, a, U, V ⇒ w

Clearly, where T is a sequence of formulae of length n, any permutation, π(T), can be generated from T by applying n leftward shifts:

Lemma 2 where P = ∀X.∀Y.(X•Y)/X/Y, l any of the l_{ϵ}^{1,/,•,\,∀,...} calculi, the following is a derivable rule of l

\begin{matrix}x_{1}, …, x_{n} ⇒ w \\ \underbrace{P, …, P}_{n times}, π(x_{1}, …, x_{n}) ⇒ w \end{matrix}

A useful lemma concerning the structural rule encoding formulae, C, W and P is the following:

Lemma 3 where l is any of the l_{ϵ}^{1,/,•,\,∀,...} calculi, weakening in l is admissible for x ∈ {C, W, P }.

Proof: by the following derivation schemes:

U, V ⇒ w •L, 1L, 1L U, 1•1, V ⇒ w ⇒ 1/L U,(1•1)/1,V ⇒ w ∀L U, \underbrace{∀X.X•X/X}_{C}, V ⇒ w  U, V ⇒ w 1L U, 1, V ⇒ w ⇒ 1/L U,1/1,V ⇒ w ∀L U, \underbrace{∀X.1/X}_{W}, V ⇒ w  U, V ⇒ w •L, 1L, 1L U, 1•1, V ⇒ w ⇒ 1 ⇒ 1/L,/L U,(1•1)/1/1,V ⇒ w  ∀L U, \underbrace{∀X∀Y.(X•Y)/X/Y}_{P}, V ⇒ w

End of proof

Our strategy to obtain an embedding of LJ2 into l_{ϵ}^{1,/,•,\,∀} will be parallel to that used in [Lincoln et al, 1995]. We will show that for a sequent with a C, C, C, W, P prefix (abbreviated as PRE), contraction, weakenings and permutations on material after the prefix is admissible in any of the

any of the l_{ϵ}^{1,/,•,\,∀,...} calculi.

Lemma 4 where l is any of the any of the l_{ϵ}^{1,/,•,\,∀,...} calculi, the following ‘post-prefix’ permutation, weakening, and contraction rules are admissible in l:

PRE, U ⇒ x PRE, π(U) ⇒ x  PRE, U, V ⇒ x PRE, U, a, V ⇒ x  PRE, U, a, a, V ⇒ x PRE, U, a, V ⇒ x

A remark before we give the proof of this. In (1), which establishes the corresponding cases of ‘post-CCCW ’ contraction in IMLL2, more than ‘post-CCCW ’ permutation was used, moving a C formula to where it is needed. At many other places in Lincoln et al’s embedding proof this is also the case. Now, because for l_{ϵ}^{1,/,•,\,∀} we can at best obtain ‘post-PRE’ permutation, it may seem that it will not be possible to also establish ‘post-PRE’ contraction (and to carry through other cases in the induction). Part of the solution to this lies in the fact that the PRE block can be doubled, so that the formulae in the second occurrence of the prefix are then post-PRE. The other part of the solution is the fact noted in Lemma 3, that weakening is already derivable for x ∈ {C, W, P }, which allows the discard of any surplus C’s,W ’s or P ’s which result from such doublings. Proof of Lemma 4 By the following derivation schemes:

‘post-prefix Perm’  PRE, U ⇒ x  use n P ’s to Perm, by Lemma 2 PRE, P^{1}, …, P^{n}, π(U) ⇒ x Apply Lemma 3 PRE, PRE^{1}, …, PRE^{n}, π(U) ⇒ xuse n C’s to Contr on n PRE’s C^{1}, …, C^{n}, PRE, π(U) ⇒ xrepeatedly use one C to Contr on C, C PRE, π(U) ⇒ x

‘post-prefix Weak’  PRE, U, V ⇒ x use W to Weak on a PRE, U, W, a, V ⇒ xuse ‘post-prefix Perm’ PRE, W, U, a, V ⇒ x apply Lemma 3 PRE, PRE^{1}, U, a, V ⇒ xuse 1 C to Contr on PRE C, PRE, U, a, V ⇒ xuse 1 C to Contr on C, C PRE, U, a, V ⇒ x

‘post-prefix Contr’  PRE, U, a, a, V ⇒ xuse C to Contr on a PRE, U, C, a, V ⇒ xuse ‘post-prefix Perm’ PRE, C, U, a, V ⇒ x apply Lemma 3 PRE, PRE^{1}, U, a, V ⇒ xuse one C to Contr PRE C, PRE, U, a, V ⇒ xuse one C to Contr on C, C PRE, U, a, V ⇒ x

End of Proof

We can now prove an embedding of LJ2 (= l_{ϵ}^{1,/,•,∀} + Contr + W eak + P erm) into l_{ϵ}^{1,/,•,\,∀} as follows:

Theorem 1 where U, x is any sequence of formulae from L(1, /, •, ∀), LJ2 |− U ⇒ x iff l_{ϵ}^{1,/,•,\,∀} |− C, C, C, W, P, U ⇒ x

Proof of Theorem 1 \underline{Left to Right}: by induction on the size of the LJ2 proof of U ⇒ x. If U ⇒ y is an LJ2 axiom, then clearly U ⇒ y is an l_{ϵ}^{1,/,•,\,∀} axiom, and by Lemma 3, adding the prefix, PRE, will preserve derivability. So for induction suppose for some n that we have the property for all LJ2 proofs of size < n, and consider an LJ2 proof of size n. Lemma 4 clearly suffices to establish the claim for those cases in the induction where the last step of the supposed LJ2 proof is Permutation, Weakening or Contraction. In the case where the supposed LJ2 proof ends in the application of single premise rule, it suffices to apply the inductive hypothesis to the premise, and then apply the same rule in l_{ϵ}^{1,/,•,\,∀}. There are two possibilities for an LJ2 proof to end in a two premise rule: Case: the last step is •R. The lefthand proof below is the supposed LJ2 proof, and the righthand proof is the l_{ϵ}^{1,/,•,\,∀} derivation establishing the claim. The derivability of the premises of the right-hand derivation follows by induction given the left-hand proof.

U ⇒ a V ⇒ b•R U, V ⇒ a•b  PRE, U ⇒ a PRE, V ⇒ b•R PRE, U, PRE, V ⇒ a•buse ‘post-prefix Perm PRE, PRE, U, V ⇒ a•bUse C to Contr on PRE C, PRE, U, V ⇒ a•b PRE, U, V ⇒ a•b

Case: last step is /L. Similar to the above, with reference the following derivations:

U, a, V ⇒ x T ⇒ b/L U, a/b, T, V ⇒ x  PRE, U, a, V ⇒ x PRE, T ⇒ b/L PRE, U, a/b, PRE, T, V ⇒ xuse ‘post-prefix Perm’ PRE, PRE, U, a/b, T, V ⇒ xUse C to Contr on PRE C, PRE, U, a/b, T, V ⇒ x PRE, U, a/b, T, V ⇒ x

\underline{Right to Left} First we note that for x ∈ {C, W, P }, LJ2 |− ⇒ x:

⇒ 1 Weak X ⇒ 1/R ⇒ 1/X ∀R ⇒ ∀X.1/X  X ⇒ X X ⇒ X•R X, X ⇒ X•XContr X ⇒ X•X /R ⇒ (X•X)/X ∀R ⇒ ∀X.(X•X)/X  X ⇒ X Y ⇒ Y •R X, Y ⇒ X•Y Perm Y, X ⇒ X•Y /R,/R ⇒ (X•Y)/X/Y ∀R ⇒ ∀X∀Y.(X•Y)/X/Y

Therefore, if we can show that l_{ϵ}^{1,/,•,\,∀} |− T ⇒ x implies LJ2 |− T ⇒ x, where T, x is a sequence of formulae from L(1, /, •, ∀), then C, C, C, W, P, U ⇒ x can serve as a premise in the following Cut based LJ2 proof of U ⇒ x.

⇒ C ⇒ C ⇒ C ⇒ W ⇒ P C, C, C, W, P, U ⇒ xCut 5 times U ⇒ x

Hence we need l_{ϵ}^{1,/,•,\,∀} |− T ⇒ x implies LJ2 |− T ⇒ x, where T, x is a sequence of formulae from L(1, /, •, ∀). We cannot prove this by straightforward induction on the size of the proof, because the premises of a l_{ϵ}^{1,/,•,\,∀} proof of T ⇒ x may feature formulae not confined to L(1, /, •, ∀): specifically when the last step is ∀L, the premise may feature \. Instead we prove a stronger claim concerning sequents over L(1, /, \, •, ∀). Let f be the obvious directionality collapsing map from L(1, /, \, •, ∀) to L(1, /, •, ∀). We show that where T, x is a sequence of formulae over L(1, /, \, •, ∀) that l_{ϵ}^{1,/,•,\,∀} |− T ⇒ x implies LJ2 |− f(T) ⇒ f(x), which entails what we need.

Clearly when T ⇒ x is an l_{ϵ}^{1,/,•,\,∀} axiom, f(T ⇒ x) is an LJ2 axiom. Furthermore when a l_{ϵ}^{1,/,•,\,∀} proof of T ⇒ x ends in 1L, /L,/R,•L, •R, ∀L, ∀R, f(T ⇒ x) follows by the corresponding rule in LJ2 from the images of the premises (note for the quantifier case f(x[y/X]) = (fx)[fy/X]). We give the remaining cases, where the lefthand derivation is the supposed l_{ϵ}^{1,/,•,\,∀} proof, and the righthand derivation is the LJ2 proof establishing the claim, the derivability of whose premises follows by induction:

T ⇒ x U, y, V ⇒ w\L U, T, x\y, V ⇒ w  fU, fy, fV ⇒ fw fT ⇒ fx/L fU, fy/fx, fT, fV ⇒ fwPerm fU, fT, fy/fx, fV ⇒ fw

x, T ⇒ y\R T ⇒ x\y  fx, fT ⇒ fyPerm fT, fx ⇒ fy/R fT ⇒ fy/fx

End of Proof of Theorem 1 As a corollary we obtain:

Theorem 2 l_{ϵ}^{1,/,•,\,∀} is undecidable

Remarks Given the [Lincoln et al, 1995] embedding of LJ2 into IMLL2, one might ask we do not obtain the undecidability of l_{ϵ}^{1,/,•,\,∀} by embedding IMLL2 into it. Note, however, to obtain unlimited post-prefix permutation, we used the contraction block of formulae, to generate duplicates of the permutation formula. There is no obvious way therefore to give an embedding from IMLL2 – which has no contraction, but unlimitted permutation – to l_{ϵ}^{1,/,•,\,∀}– which has no contraction, and no permutation. It seems likely to be the case we can use quantified formulae to simulate a structural rule only if we simulate contraction at the same time. It also deserves mention that sequents with an empty sequence of antecedents were used widely in the proof. It is not the case for example, that when empty antecedents are not admitted, that Lemma 3 holds, allowing weakening on x ∈ {C, W, P }. For example, although a/b, b ⇒ a is derivable, a/b, b, x ⇒ a is not, where x ∈ {C, W, P }. Since the work reported here was completed, Kanovich has announced an undecidability proof, by different means, of l^{1,/,\,•,∀} – see concluding section.

4 Polymorphic Reconstruction of Connectives

Prawitz first noted the higher order definability of certain connectives of 2nd order intuitionistic logic in terms of implication and quantification, in the context of a logic with all the structural rules. There are analogue definability results for IMLL2, which lacks the structural rules of Weakening and Contraction. In IMLL2, there is definability of 1, •, and ∃ in terms of ∀ and /, via:

\begin{aligned}1^{∗} & = & ∀X.X/X \\ (a•b)^{∗} & = & ∀X.X/(X/a^{∗}/b^{∗}) \\ (∃X.x)^{∗} & = & ∀Y.(Y/(∀X.(Y/x^{∗})) \end{aligned}

Also the additive connectives 0 and ⊤ are IMLL2 definable in terms of ∀ and /:

\begin{aligned}0^{∗} & = & ∀X.X \\ ⊤^{∗} & = & (∃X.X)^{∗} \end{aligned}

The further additive connectives of linear logic are not definable within IMLL2. Is there a corresponding result when the Permutation rule is jettisoned ? One might expect this not be the case because in no sense are 1, a•b, ∃X.x, 0 or ⊤ left or right looking. Yet a proposed definition in terms of ∀ and /,\, if it uses /, or \ at all, will have a particular directionality. Nonetheless, there is an embedding:

Theorem 3 Where U, x is any sequence of formulae from L(1, 0, ⊤, /, •, \, ∀, ∃), l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} |−U ⇒ x iff l_{ϵ}^{(/,\,∀)} |−U^{#} ⇒ x^{#}, where ·^{#} is defined:

x^{#} = x, where x is a variable
(x/y)^{#} = x^{#}/y^{#}
(y\x)^{#} = y^{#}\x^{#},
1^{#} = ∀X.X/X,
0^{#} = ∀X.X
⊤^{#} = (∃X.X)^{#}
(a•b)^{#} = ∀X.X/(b^{#}\a^{#}\X)
(∃X.x)^{#} = ∀Y.Y/(∀X.(x^{#}\Y)) (where Y binds no variable in x)

A remark before we give the proof. The intuition that the proposed translations should have no particular directionality is born out by the fact that where the above proposed translation has a principal ‘/’ connective (after quantifiers are stripped away), this translation is equivalent to another which has a principal ‘\’ connective

\begin{aligned}l_{ϵ}^{(/,\,∀)} |− & ∀X.X/X & ⇔ & ∀X.X\X \\ l_{ϵ}^{(/,\,∀)} |− & ∀X.X/(b\a\X) & ⇔ & ∀X.(X/b/a)\X \\ l_{ϵ}^{(/,\,∀)} |− & ∀Y.Y/(∀X.(x\Y)) & ⇔ & ∀Y.((∀X.(Y/x)\Y) \end{aligned}

Proof \underline{Left to Right} By induction on the size of the l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} proof. For x ⇒ x axioms of l_{ϵ}^{1,0,⊤,/,•,\,∀,∃}, we clearly have x^{#} ⇒ x^{#} is a l_{ϵ}^{(/,\,∀)} axiom. The other three axiom schemes of l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} are ⇒ 1, U, 0, V ⇒ w, and U ⇒ ⊤, and we give derivations of the images of these below:

X ⇒ X/R ⇒ X/X ∀R ⇒ ∀X.X/X  U^{#} ⇒ U^{#} w^{#} ⇒ w^{#} V^{#} ⇒ V^{#}\L,/L U^{#}, U^{#}\w^{#}/V^{#}, V^{#} ⇒ w∀L U^{#}, ∀X.X, V^{#} ⇒ w^{#}  U^{#} ⇒ \overline{X} Y ⇒ Y ∀L,\L U^{#}, ∀X(X\Y) ⇒ Y /R U^{#} ⇒ Y/∀X(X\Y) ∀R U^{#} ⇒ ∀Y.Y/∀X(X\Y)

Note in the final case, some \overline{X} must be found such that l_{ϵ}^{(/,\,∀)} |− U^{#} ⇒ \overline{X}. Such an \overline{X} is Y/(U^{#}\Y). So for induction suppose for some n we have the claim for all l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} proofs of size < n, and consider an arbitrary proof of size n. We give pairs of derivations below, where the lefthand derivations trace through all remaining possibilities for the supposed l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} proof, and the righthand derivation is the l_{ϵ}^{(/,\,∀)} proof establishing the claim, making frequent use of Lemma 1.

• active category is 1

1L  U V ⇒ w 1 U 1 V ⇒ w  ⇝ \overbrace{U^{#}, \overline{X} ⇒ w^{#} V^{#} ⇒ \overline{X}}^{U^{#}, V^{#} ⇒ w^{#}} ; U^{#}, ∀X.X/X, V^{#} ⇒ w^{#}

• active category is a•b

•R U ⇒ a V ⇒ b U V ⇒ a•b  ⇝ U^{#} ⇒ a^{#} V^{#} ⇒ b^{#} X ⇒ X\L\L U^{#}, V^{#}, (b^{#}\a^{#}\X) ⇒ X ∀R,/R U^{#}, V^{#} ⇒ ∀X.X/(b^{#}\a^{#}\X)

•L U a b V ⇒ w•L U a•b V ⇒ w  ⇝ \overbrace{_{U^{#}, \overline{X}, V^{#} ⇒ w^{#}  a^{#}, b^{#} ⇒ \overline{X} /R ⇒ (b^{#}\a^{#}\\overline{X})∀L,/L U^{#}, ∀X.X/(b^{#}\a^{#}\X), V^{#} ⇒ w^{#}}}^{U^{#}, a^{#}, b^{#}, V^{#} ⇒ w^{#}}

• active category is ∃X.x

∃R U ⇒ x[y/X]∃R U ⇒ ∃X.x  ⇝ U^{#} ⇒ x^{#}[y^{#}/X] Y ⇒ Y \L U^{#}, x^{#}[y^{#}/X]\Y ⇒ Y ∀L U^{#}, ∀X.(x^{#}\Y) ⇒ Y ∀R,/R U^{#} ⇒ ∀Y.(Y/∀X.(x^{#}\Y))

∃L For the righthand derivation, note that the \overline{Y} whose existence we infer by Lemma 1 has free variables from (U, V, w)^{#}, which can therefore be assumed distinct from X.

U, x, V ⇒ w ∃R U, ∃X.x, V ⇒ w  ⇝ \overbrace{_{U^{#}, \overline{Y} , V^{#} ⇒ w^{#}  x^{#} ⇒ \overline{Y} ∀R,\R ⇒ ∀X.((x^{#}\\overline{Y})∀L,/L U^{#}, ∀Y.Y/∀X(x^{#}\Y), V^{#} ⇒ w^{#}}}^{U^{#}, x^{#}, V^{#} ⇒ w^{#}}

• active category is a/b: trivial

• active category is ∀X.y: trivial \underline{Right to Left}

Suppose l_{ϵ}^{(/,\,∀)} |− U^{#} ⇒ x^{#}, where U, x is any sequence of formulae from L(1, 0, ⊤, /, •, \, ∀, ∃). The l_{ϵ}^{(/,\,∀)} proof is also a l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} proof, and hence l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} |− U^{#} ⇒ x^{#}. Therefore if we have l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} |− U ⇒ U^{#}, and l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} |− x^{#} ⇒ x we have the following proof l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} + Cut proof U ⇒ x, which implies the existence of a Cut-free l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} proof:

U ⇒ U^{#} U^{#} ⇒ x^{#} x^{#} ⇒ x Cut U ⇒ x^{#}  Cut U ⇒ x

Hence it suffices to show l_{ϵ}^{1,0,⊤,/,•,\,∀,∃} |− x ⇔ x^{#}, for all x ∈ L(1, 0, ⊤, /, •, \, ∀, ∃), which we show by induction on the complexity of x. When x is atomic and ∉ {1, 0, ⊤}, then x = x^{#}, and the claim is trivial. The remaining zero complexity cases are established by:

X ⇒ X 1L 1, X ⇒ X ∀R,/R 1 ⇒ ∀X.X/X  1 ⇒ 1 ⇒ 1/L 1/1 ⇒ 1 ∀ L ∀X.X/X ⇒ 1

0 ⇒ ∀X.X  0 ⇒ 0 ∀L ∀X.X ⇒ 0

U^{#} ⇒ \overline{X} Y ⇒ Y ∀L,\L U^{#}, ∀X(X\Y) ⇒ Y /R U^{#} ⇒ Y/∀X(X\Y) ∀R U^{#} ⇒ ∀Y.Y/∀X(X\Y)  ∀Y.Y/∀X(X\Y) ⇒ ⊤

So for induction, suppose for some n, we have the property for formulae of complexity < n, and consider an arbitrary formula, x, of complexity n. All possibilities are traced through below.

• x = a•b

a ⇒ a^{#} b ⇒ b^{#} X ⇒ X\L,\L a, b, b^{#}\a^{#}\X ⇒ X ∀R,/R a, b ⇒ ∀X.X/(b^{#}\a^{#}\X)•L a•b ⇒ ∀X.X/(b^{#}\a^{#}\X)  \overbrace{_{\overline{X} ⇒ a•b a^{#}, b^{#} ⇒ \overline{X}\R,\R ⇒ b^{#}\a^{#}\\overline{X}∀L,/L ∀X.X/(b^{#}\a^{#}\X) ⇒ a•b}}^{a^{#} ⇒ a b^{#} ⇒ b•R a^{#}, b^{#} ⇒ a•b}

• x is ∃X.x. In the righthand derivation, note that the \overline{Y} we infer by Lemma 1 contains only the free variables of ∃X.x, and therefore, ∀X does not bind variables of \overline{Y} in ∀X.(x^{#}\\overline{Y}).

x ⇒ x^{#} Y ⇒ Y ∀L,\L x, ∀X.(x^{#}\Y) ⇒ Y ∀R, /R, ∃R ∃X.x ⇒ ∀Y/(∀X(x^{#}\Y))  \overbrace{_{\overline{Y} ⇒ ∃X.x x^{#} ⇒ \overline{Y} ∀R,\R ⇒ ∀X(x^{#}\\overline{Y})/L \overline{Y} /∀X(x^{#}\\overline{Y}) ⇒ ∃X.x ∀L ∀Y.Y/(∀X.(x^{#}\Y)) ⇒ ∃X.x}}^{x^{#} ⇒ x ∃L x^{#} ⇒ ∃X.x}

• x is a/b: trivial

• x is ∀X.y: trivial

End of Proof It is clear from the proof that is also possible to do embeddings in which only one connective is defined away at a time. That is, where c is a connective in {1, 0, ⊤, •, ∃}, and c⃗ a sequence of connectives from {1, 0, ⊤, •, ∃} not featuring c, there is an embedding from l^{/,\,∀,c,c⃗} into l^{/,\,∀,c⃗}, using the map ·^{#} defined in Theorem 3.

Besides showing that l_{ϵ}^{(/,\,∀)} in a certain sense contains 1, 0, ⊤, • and ∃, we can put together the embedding of LJ2 into l_{ϵ}^{1,/,•,\,∀}, with an embedding l_{ϵ}^{1,/,•,\,∀} into l_{ϵ}^{(/,\,∀)}and obtain a stronger undecidability result^{3} :

Theorem 4 l_{ϵ}^{(/,\,∀)} is undecidable

Remarks: these embeddings of logics with more connectives into logics with fewer assume that sequents with an empty LHS are permitted in both source and target logics. What is the situation when then this assumption no longer holds ? We have not explored all the possibilities here, but some observations can quickly be made. One possibility is that the source logic does allow empty antecedents, but the target logic does not. Clearly then the proposed embedding translation cannot work for the case of a logic with 1 or ⊤, because the images of the valid source logic sequents ⇒ 1, and ⇒ ⊤, will not be possible sequents of the target logic. It is an open question whether there are other connective-eliminating embeddings in this case. Another possibility is that both source and target logics disallow sequents with an empty LHS. It is still the case that the proposed embedding does not work. For example, in the absence of empty antecedents, it no longer holds in any of the l^{/,\,∀,...} calculi that ∀X.X/X ⇔ ∀X.X\X, and a reflex of this that the image of the sequent Y, 1 ⇒ Y, which is valid in any of the l^{/,\,∀,1,...} calculi, is not valid in the l^{/,\,∀,...} that lack 1. We claim (see Appendix) that the absence of empty antecedents also affects the possibility to define away the • connective in terms of /,\ and ∀, for there are •-free sequents which are derivable in l^{/,•,\,∀}, which are not derivable in l^{(/,\,∀)}, such as a/d/c, ∀X.X/(X\b)/X, c, d, d\c\b ⇒ a, where a, b, c and d are distinct variables.

3Alternatively, we could start with LJ2 already restricted to implications and universal quantification and prove the embedding into l_{ϵ}^{(/,\,∀)} directly.

5 Concluding Remarks, Open Questions

The undecidability result for l_{ϵ}^{1,/,•,\,∀} and l_{ϵ}^{(/,\,∀)} fits into an overall picture of undecidability results for second order logics as follows. The undecidability of full second order linear logic (with multiplicatives, additives and exponentials) was known since [Girard, 1987], by an embedding of LJ2, using the exponentials. [Lincoln et al, 1995] prove undecidability for IMLL2, also by embedding LJ2, and we prove undecidability for the permutation-free version, again by embedding LJ2. [Lafont, 1995a] proves undecidability of classical (i.e. multiple conclusioned), second order linear logic, with multiplicatives and additives, by an adaption of a technique originally due to [Kanovich, 1995a], for the encoding of two counter machines. An embedding of the classical version of LJ2 is of no use because this is decidable. [Lafont and Scedrov, 1995] refines this technique to prove undecidability of classical second order linear logic with just the multiplicatives. [Kanovich, 1995b] adapts the technique further to prove undecidability of classical permutation-free second order linear logic with just the multiplicatives. The proof entails also the result reported here. [Kanovich, 1995c] addresses the logic with the restriction to non-empty antecedents, and using again an encoding of two counter machines, proves undecidability of l^{/,•,\,∀}. It is also claimed in [Kanovich, 1995c] that one can eliminate •, and prove thereby undecidability of the purely implicational second order Lambek calculus. However, as noted at the end of the preceding section, we claim that • cannot be eliminated from l^{/,•,\,∀}, and claim that therefore the undecidability of l^{/,\,∀} remains an open question.

We consider now what the reaction to our undecidability result for l_{ϵ}^{1,/,•,\,∀}, and l_{ϵ}^{(/,\,∀)}should be. The strongest possible reaction would be to conclude that these calculi should now be ruled out as playing a part in the linguist’s toolkit for describing languages. In response to this, one should note that this undecidability result places l_{ϵ}^{(/,\,∀)} in some rather respectable company. [Lincoln et al, 1992] prove purely propositional linear logic (i.e quantifier-free) to be undecidable. [Schieber, 1986] and [Johnson, 1988], each with respect to their own notion of feature-structure based grammars, prove that the universal recognition problem is undecidable: there can be no algorithm which, given a feature-structure based grammar and a string, decides whether the string belongs to the language generated by the grammar. It neither of these cases has this undecidability stifled interest in the systems. It is also germane to note examples of decidable but provably intractable systems which are in wide spread use, such as the type-checking algorithm for the polymorphic functional programming language ML [Mairson, 1990]. In these cases, the continuing interest in the systems involved reflects a switch of emphasis from the general situation to some restriction of it. Such a move seems the apt reaction to the undecidability for the 2nd order Lambek calculus, with an investigation of decidable fragments moving onto the agenda. [Emms, 1993a] contains a preliminary investigation of this, in which a subset of all possible sequents is considered which have the property that, however a proof is unfolded, a set of subproblems is generated having the form of (i) in the Unknown Elimination lemma above. This forms the basis of a decision procedure for such sequents. Sequents involving the polymorphic categories that have been proposed to have linguistic applications (eg. ∀X.X/(a\X) (quantification), ∀X.X\X/X (coordination), ∀X∀Y.c/(X\a)/(X/b) (extraction)) have this nature, and their derivability can be decided. It is interesting to note that of all the polymorphic formulae involved in the above embeddings, all but the formula expressing Contraction have this nature as well. Clearly the question of decidable fragments is one requiring further attention. The decidability of one oft-mooted candidate, namely a fragment allowing only outermost quantifers, remains an open question.

The structural rule embeddings, besides allowing a proof of undecidability, also point up potentially interesting new linguistic applications of polymorphism, in which a subcategorisation can indicate which resource management regime is permitted. For example, a x/CCCP subcategorisation indicates that material is needed which derives an x, with repeated access to Contraction and Permutation if need be, whilst a x/P P subcategorisation indicates that material is needed which derives an x, with at most 2 permutations. As far as I am aware no other categorial system in the literature allows for such specifications. A further line of investigation is a comparison with the work of [Kurtonina and Moortgat, 1994], [Kurtonina and Moortgat, 1995], who also consider embeddings between logics with differing associated structural rules. The logics studied are all based on l^{/,•,\}, and then vary according to (i) their inclusion of particular structural rules and (ii) the inclusion of, and axioms for, the so-called pure-residuation modalites. Of note is the fact that the embeddings are all amongst what have been termed substructural logics, in which the structural rule package never includes Weakening or Contraction. In this respect at least, the embeddings are of a different kind to those studied in the present paper, and suggest directions for further extensions of the present line of study. For example, [Kurtonina and Moortgat, 1995] consider embeddings between pairs of logics which differ according to whether they adopt an Associativity structural rule. As with the other structural rules considered in this paper, associativity can be reintroduced via axioms and Cut, and so there is reason to think that we may in a similar fashion be able to use polymorphism to give an embedding of LJ2 into the non-associative variant of l_{ϵ}^{(/,\,∀)}, thereby proving undecidability. For the moment, however, this remains a conjecture.

References

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

  ftp from ftp.cis.uni-muenchen.de/pub/incoming/emms/parsing.dvi.Z

[Emms, 1993b] Martin Emms. Some Applications of Categorial Polymorphism. In dyana Deliverable R1.3.A, 1993. available from ILLC, University of Amsterdam

[Emms, 1993c] 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 available via anonymous ftp from

  ftp.cis.uni-muenchen.de/pub/incoming/emms/recog.dvi.Z

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

  ftp.cis.uni-muenchen.de/pub/leiss/lambek.cut.dvi.gz

[Emms, 1994a] Martin Emms. Movement in Labelled and Polymorphic Calculi. in Proceedings of the 1st Rome Workshop on Linear Logic and Categorial Grammar. available via anonymous ftp

  ftp.cis.uni-muenchen.de/incoming/emms/Roma/movement.dvi.Z

[Emms, 1994b] Martin Emms. Completeness Results for Polymorphic Lambek Calculus. in dyana Deliverable R1.1.B, 1994. Available from ILLC, University of Amsterdam.

[Gabbay, 1981] Dov Gabbay. Semantical investigations in Heyting’s intuitionistic logic, Reidel, Dordrecht, 1981.

[Girard, 1987] J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50:1–102, 1987 [Hudelmaier and Shroeder-Heister, 1994] Jörg Hudelmaier and Peter Shroeder-Heister. Classical

Lambek Logic. Proceedings Linear Logic and Lambek Calculus Workshop, Rome. available via

anonymous ftp from ftp.let.ruu.nl/pub/users/moortgat/CompSem/Hudelmaier.ps

[Johnson, 1988] Mark Johnson. Attribute-Value Logic and the Theory of Grammar CSLI Lecture Note Series, Chicago University Press, Chicago, 1986

[Kanovich, 1995a] Max Kanovich. The Direct Simulation of Minsky machines in Linear Logic. To appear in Advances in Linear Logic, J.-Y.Girard, Y.Lafont and L.Regnier (eds.), London Mathematical Society Lecture Note Series, Cambridge University Press. 1995

[Kanovich, 1995b] Max Kanovich. Undecidability of Non-Commutative Second Order Multiplicative Linear Logic. Result announced on the Linear Logic mailing list

[Kanovich, 1995c] Max Kanovich. Undecidability of the Second Order Lambek Calculus. Result announced on the Linear Logic mailing list

[Lafont, 1995a] Yves Lafont. The undecidability of second order linear logic without exponentials. to appear in Journal of Symbolic Logic available via anonymous ftp from lmd.univ-mrs.fr

[Lafont and Scedrov, 1995] Yves Lafont and Andre Scedrov. The undecidability of second order multiplicative linear logic. available via anonymous ftp from lmd.univ-mrs.fr

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

[Lambek, 1961] Joachim Lambek. On the calculus of syntactic types. in R. Jakobson, ed., Structure of Language and its Mathematical Aspects, pp 166–178.

[Lincoln et al, 1992] Lincoln, Mitchell, Scedrov and Shankar. Decision Problems For Propositional Linear Logic. Annals of Pure and Applied Logic, 56:239–311, 1992

[Lincoln et al, 1995] Lincoln, Scedrov and Shankar. ecision Problems For Second-Order Linear Logic. to appear in Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS’95).

[Löb, 1976] M.H.Löb. Embedding first-order predicate logic in fragments of intuitionistic logic. Journal of Symbolic Logic,41:705–718, 1976.

[Mairson, 1990] Harry Mairson. Deciding ML Typability is Complete for Deterministic Exponential Time In Proceedings POPL 90.

[Kurtonina and Moortgat, 1994] Kurtonina and Moortgat. Controlling Resource Management. In dyana Deliverable R1.1.B, 1994. Available from ILLC, University of Amsterdam.

[Kurtonina and Moortgat, 1995] Kurtonina and Moortgat. Structural Control. This Volume, and to appear in Logic, Structures and Syntax, Blackburn and de Rijke (eds.) 1995.

[Pentus, 1992] Mati Pentus. Lambek Grammars are Context Free. ms. Dept of Mathematical Logic, Moscow University, 1992

[Schieber, 1986] Stuart Schieber. An introduction to Unification-based approaches to grammar CSLI Lecture Note Series, Chicago University Press, Chicago, 1986

[Tait, 1966] W.W.Tait. A non-constructive proof of Gentzen’s Hauptsatz for second-order logic Bulletin of the American Mathematical Society, 72: 980–983, 1966.

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

Appendix

The following sequent is derivable in l^{/,•,\,∀}, but not in l^{/,\,∀}, where a, b, c, d are distinct atoms.

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

We must first show 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 (whose proofs are here omitted). 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. It is clear that no atomic \overline{X} can be a solution. It also clear that the principal connective of \overline{X} cannnot be ‘/’, for this will not solve 1., and cannot be ‘\’, as this will not solve 2. This leaves just the possibility that \overline{X} is quantified. So assume \overline{X} has the form ∀Y_{1} … ∀Y_{n}.y, where y is either atomic or has a slash as principal connective. In case y is atomic, it is clear \overline{X} is not a solution for 3. So suppose y has a slash as principal connective. Clearly the proofs of 1 and 2 must end with a succession of n (∀L) 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

In order to solve 1′, y_{1} must have a principal left slash, and in order to solve 2′, y_{2} must have a principal right slash, but both y_{1} and y_{2} must also have the same principal slash as y. In this way we have eliminated all possibilities for \overline{X}. □