The Complexity of Multiplicative-Additive Lambek Calculus: 25 Years Later

Abstract

The Lambek calculus was introduced as a mathematical description of natural languages. The original Lambek calculus is NP-complete (Pentus), while its product-free fragment with only one implication is polynomially decidable (Savateev). We consider Lambek calculus with the additional connectives: conjunction and disjunction. It is known that this system is PSPACE-complete (Kanovich, Kanazawa). We prove, in contrast with the polynomial-time result for the product-free Lambek calculus with one implication, that the derivability problem is still PSPACE-complete even for a very small fragment $(\mathop {\backslash }, \wedge )$, including one implication and conjunction only. PSPACE-completeness is also provided for the $(\mathop {\backslash }, \vee )$ fragment, which includes only one implication and disjunction. Categorial grammars based on the original Lambek calculus generate exactly the class of context-free languages (Gaifman, Pentus). The class of languages generated by Lambek grammars extended with conjunction is known to be closed under intersection (Kanazawa), and therefore includes all finite intersections of context-free languages and, moreover, images of such intersections under alphabetic homomorphisms. We show that the same closure under intersection holds for Lambek grammars extended with disjunction, even for our small $(\mathop {\backslash }, \vee )$ fragment.

1 Introduction

Lambek calculus has been invented to analyze natural and artificial languages by means of categorial grammars [4, 17, 19, 20]. Though the original Lambek calculus can describe only context-free languages [23], it has been proven to be NP-complete [24], even if we confine ourselves to the product-free Lambek calculus equipped only with the left implication and the right implication [27]. On the contrary, the product-free Lambek calculus, with only one implication, is known to be decidable in polynomial time [26], see also [15]. It is known [2, 3] that already the fragment with only one implication is sufficient to generate all context-free languages.

This paper is focused on the complexity issues for Lambek calculus extended with two additional connectives: additive conjunction and disjunction. This calculus is presented on Table 1 in the form of a sequent calculus. Notice that antecedents of sequents are linearly ordered sequences of formulae, not sets or multisets.

Table 1. The Inference rules of Lambek calculus with conjunction and disjunction

As shown above on the example of the Lambek calculus without additive connectives, there are two different ways of measuring complexity for extensions of the Lambek calculus. The first one is the standard notion of algorithmic complexity of the derivability problem for the calculus in question. For the Lambek calculus with additive connectives, 25 years ago, Kanovich [10] and Kanazawa [9] show that its derivability problem is PSPACE-complete. Here we strengthen this result and prove PSPACE-hardness for the smallest possible fragments, with only two connectives: $\mathcal{L}(\mathop {\backslash }, \wedge )$, with only one implication and additive conjunction, and $\mathcal{L}(\mathop {\backslash }, \vee )$, with one implication and disjunction. The first result is presented in Sect. 2. The second result is similar, so we give only a sketch of the proof, in Appendix A. The upper PSPACE bound is known for the whole Lambek calculus with additive connectives [9, 10, 13, Sect. 8] and therefore inherited by its fragments, $\mathcal{L}(\mathop {\backslash }, \wedge )$ and $\mathcal{L}(\mathop {\backslash }, \vee )$.

The other complexity measure is the expressive power of categorial grammars based on a given calculus. A categorial grammar $\mathcal {G}$ is a triple $\langle \varSigma , \triangleright , H \rangle$, where $\varSigma$ is a finite alphabet, $\triangleright$ is a finite binary correspondence between letters of $\varSigma$ and Lambek formulae (these formulae could also include additive connectives), and H is a formula. A non-empty word $w = a_1 \ldots a_n$ over $\varSigma$ is accepted by $\mathcal {G}$, if there exist formulae $A_1$, ..., $A_n$ such that $a_i \triangleright A_i$ ($i = 1, \ldots , n$) and $A_1, \ldots , A_n \vdash H$ is a derivable sequent. The language generated by $\mathcal {G}$ is the set of all accepted words.

For Lambek grammars extended with conjunction, Kanazawa [8] proves that, in addition to context-free languages, they can generate finite intersections of such languages and images of such intersections under alphabetic homomorphisms (i.e., homomorphisms which map letters to letters). In Sect. 3 we prove the dual result, that Lambek grammars enriched with disjunction have the same property. Namely, we show that $\mathcal{L}(\mathop {\backslash },\vee )$, the product-free fragment with only one implication and disjunction, is already sufficient to generate finite intersections of such languages and images of such intersections under alphabetic homomorphisms.

2 PSPACE-Hardness of the Fragment $\mathcal{L}(\backslash , \wedge )$

Within our fragment $\mathcal{L}(\backslash , \wedge )$, we intend to encode quantified Boolean statements of the form:

$$\begin{aligned} \exists x_1 \forall x_2 \exists x_3 \forall x_4\dots \exists x_{2n-1} \forall x_{2n}\, (C_1\vee C_2\vee \cdots \vee C_m) \end{aligned}$$

(1)

Here $(C_1\vee C_2\vee \cdots \vee C_m)$ is a DNF over the Boolean variables $x_1$, $x_2$, ...$x_{2n}$.

Definition 1

We express validity of (1) in terms of the winning strategy given by a binary tree of height $2n\!+\! 1$, the nodes of which are labelled as follows.

The root is labelled by “ $\exists x_{1}$” and has only one outgoing edge the end of which is labelled by “ $\forall x_{2}$”. In its turn, this node has two outgoing edges the ends of which are labelled by the same “ $\exists x_{3}$”.

By induction, for $1\le k\le n$, each of the nodes on the level $2k\!-\!1$ is labelled by “ $\exists x_{2k-1}$”, and each of the nodes on the level 2k is labelled by “ $\forall x_{2k}$”.

At the node “ $\exists x_{2k-1}$”, the choice move of the proponent is to label the unique outgoing edge either by $t_{2k-1}$, meaning $x_{2k-1}$ be true, or by $f_{2k-1}$, meaning $x_{2k-1}$ be false. Being at the next node, “ $\forall x_{2k}$”, the opponent responds by labeling two outgoing edges by $t_{2k}$ and $f_{2k}$, resp.

Lastly, on the final level $2n\!+\!1$, each terminal node v is labelled by some $C_\ell$ so that, collecting the sequence of $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$ that label the respective edges along the branch leading from the root “ $\exists x_{1}$” to this leaf v, we get:

$$\begin{aligned} C_\ell (\alpha _1,\alpha _2,\dots ,\alpha _{2n-1},\alpha _{2n}) = \top \end{aligned}$$

(2)

We illustrate the challenges we have to answer to with Example 1.

Example 1

We consider the following statement (which is invalid):

$$\begin{aligned} \exists x_1 \forall x_2 \, (C_1\vee C_2) = \exists x_1 \forall x_2 \, ((x_1 \wedge \lnot x_2)\vee (\lnot x_1 \wedge x_2)) \end{aligned}$$

(3)

To provide (2), we express $C_1$ and $C_2$ as the formulas $E_1$ and $E_2$, resp.

$$\begin{aligned} E_1= & {} {(f_2 \backslash \, {(t_1 \backslash \, \top )})} \ \equiv \ {((t_1\cdot \,f_2) \backslash \, \top )} \end{aligned}$$

(4)

$$\begin{aligned} E_2= & {} {(t_2 \backslash \, {(f_1 \backslash \, \top )})} \ \equiv \ {((f_1\cdot \,t_2) \backslash \, \top )} \end{aligned}$$

(5)

Following [9, 10], we intend to express the “choice move” $\exists x_1$ as $(t_1 \wedge f_1)$, and the “branching move” $\forall x_2$ as $(t_2 \vee f_2)$, resulting in the following encoding sequent:

$$\begin{aligned} (t_1 \wedge f_1),\ (t_2 \vee f_2),\ (E_1\wedge E_2) \vdash \, \top \end{aligned}$$

(6)

Taking $(t_1 \wedge f_1),\ (t_2 \vee f_2)$ as a sequence, we assume that these formulas should be executed in the natural order. Starting with $(t_1 \wedge f_1)$, we have to prove either

$$\begin{aligned} t_1,\ (t_2 \vee f_2),\ (E_1\wedge E_2) \vdash \, \top \end{aligned}$$

(7)

or

$$\begin{aligned} f_1,\ (t_2 \vee f_2),\ (E_1\wedge E_2) \vdash \, \top \end{aligned}$$

(8)

Since both sequents are not derivable, we might have concluded that (6) was not derivable and, hence, it was in a proper correlation with the invalid (3).

However, if we first apply $(t_2 \vee f_2)$, the related sequents turn out to be derivable

$$\begin{aligned}&(t_1\wedge f_1),\ t_2,\ (E_1\wedge E_2) \vdash \, \top&\end{aligned}$$

(9)

$$\begin{aligned}&(t_1\wedge f_1),\ f_2,\ (E_1\wedge E_2) \vdash \, \top&\end{aligned}$$

(10)

which shows that in fact (6) is derivable and, hence, fails to express the invalid (3).

The intuitive remedy proposed by [9, 10, 18] is to force the correct order of actions by means of “leading” $q_i$. E.g., here we can express the “choice move” $\exists x_1$ and the “branching move” $\forall x_2$ as the following formulas adjusted

$$\begin{aligned}&{(q_0 \backslash \, ((t_1\cdot \,q_1) \wedge (f_1\cdot \,q_1)))}&\end{aligned}$$

(11)

$$\begin{aligned}&{(q_1 \backslash \, ((t_2\cdot \,q_2) \vee (f_2\cdot \,q_2)))}&\end{aligned}$$

(12)

resulting in the correct non-provable encoding sequent, something like that

$$\begin{aligned} q_0,\ {(q_0 \backslash \, ((t_1\cdot \,q_1) \wedge (f_1\cdot \,q_1)))},\ {(q_1 \backslash \, ((t_2\cdot \,q_2) \vee (f_2\cdot \,q_2)))},\ {(q_2 \backslash \, (E_1\wedge E_2))} \vdash \, \top \end{aligned}$$

(13)

The challenge of implementing this approach within $\mathcal{L}(\backslash , \wedge )$ consists of two parts:

(a):

get rid off the disjunctions, in the absence of the full duality of $\wedge$ and $\vee$;

(b):

get rid off the positive products of the form ${(A \backslash \, (B_1\cdot \,B_2))}$

2.1 The Relative Negation and Double Negation (Non-commutative)

Definition 2

In our encodings we will use the following abbreviation. We fix an atomic proposition b, and define ‘relative negation’ $A^b$ by: $A^b = {(A \backslash \, b)}$.

Our relative negation can be seen as a non-commutative analogue of the linear logic negation [5], which is defined by .

As for the relative “double negation”, the novelty of our approach is that we are in favour of the “asymmetric” $A^{bb} = {({(A \backslash \, b)} \backslash \, b)}$, because of its nice properties proven in Lemma 1.

We use also the following notation for the towers of double negations:

$$\begin{aligned} A^{[0]} = A,\quad A^{[k+1]} = {(A^{[k]} \backslash \, b)} \end{aligned}$$

(14)

Remark 1

The “double negation” in the symmetrical form: $^{b}\!A^{b} = (b / ({A}\backslash {b}))$, has received recognition as being appropriate and logical within a non-commutative linear logic framework (see [1]).

E.g., the natural $A \vdash \, ^{b}\!A^{b}$ is valid, in contrast to our $A^{bb}$, see Lemma 1(e).

However, the crucial Lemma 1(a) is destroyed with $^{b}\!A^{b}$, which is the reason for our “non-logical” choice of $A^{bb}$.

For a sequence $\varGamma = A_1, A_2,.., A_s$, by $\varGamma ^{bb}$ we denote the sequence $A_1^{bb}, A_2^{bb},..,A_s^{bb}$.

Lemma 1

($\mathbf {a}$) The following rules are derivable in Lambek calculus, $s\ge 1$:

(15)

(b):

Though $\vee$ and $\wedge$ are not fully dual: , the following equivalence fits our purposes:

$$\begin{aligned} A^{b} \wedge B^{b}\vdash (A \vee B)^{b} \quad \text {and} \quad (A \vee B)^{b}\vdash A^{b} \wedge B^{b} \end{aligned}$$

(16)

(c):

To simulate branching, we will use the derivable rule:

(17)

(d):

With $G_i = {(q_{i-1} \backslash \, B)}$, the crucial rule of “leading” $q_{i-1}$ is given by:

(18)

(e):

Essential complications are caused by the fact that $A \vdash A^{bb}$ is not valid.

Lemma 2

If c does not occur in $A_1, \ldots , A_n, B$, then the sequent $A_1^{cc}, \ldots , A_n^{cc} \vdash B^{cc}$ is equiderivable with $A_1, \ldots , A_n \vdash B$.

Proof

The right-to-left direction is due to Lemma 1(i). For the left-to-right direction, we use the reversibility of $\mathbf {R}\mathop {\backslash }$:

$$ B \mathop {\backslash }c, (A_1 \mathop {\backslash }c) \mathop {\backslash }c, \ldots , (A_n \mathop {\backslash }c) \mathop {\backslash }c \vdash c. $$

By induction on k, let us show derivability of

$$ A_{n-k}, \ldots , A_n, B \mathop {\backslash }c, (A_1 \mathop {\backslash }c) \mathop {\backslash }c, \ldots , (A_{n-k-1} \mathop {\backslash }c) \mathop {\backslash }c \vdash c. $$

Induction base ($k=0$) is given above. For the induction step, apply Lemma 11 below, which yields derivability of

$$ A_{n-k}, \ldots , A_n, B \mathop {\backslash }c, (A_1 \mathop {\backslash }c) \mathop {\backslash }c, \ldots , (A_{n-k-2} \mathop {\backslash }c) \mathop {\backslash }c \vdash A_{n-k-1} \mathop {\backslash }c $$

and reverse the $\mathbf {R} \mathop {\backslash }$ rule. Finally, we get $A_1, \ldots , A_n, B \mathop {\backslash }c \vdash c,$ and one more application of Lemma 11 yields the necessary $A_1, \ldots , A_n \vdash B$.

2.2 Complexity of the fragment $\mathcal{L}(\backslash , \wedge )$

Remark 2

Because of Lemma 1, for the sake of readability, here we will conceive of the formula ${((A \cdot \,B) \backslash \, C)}$ as abbreviation for ${(B \backslash \, {(A \backslash \, C)})}$. In particular, $(A \cdot \,B)^{b}$ is abbreviation for ${(B \backslash \, {(A \backslash \, b)})}$. The formula $(A\vee B)^b$ is conceived of as abbreviation for $({(A \backslash \, b)}\wedge {(B \backslash \, b)})$.

Theorem 1

The fragment $\mathcal{L}(\backslash , \wedge )$ is PSPACE-hard.

Proof

The direction from winning trees to derivable sequents is provided by Corollary 1.

By running from the leaves of the winning tree, labelled by some $C_\ell$, to its root “ $\exists x_{1}$”, we have to address the following issues:

• (a) With one and the same sequent of polynomial size, deal with the exponential number of branches and their sequences of $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$ that label the respective edges along the branch leading from the root to some leaf v.

• (b) In particular, verify “polynomially” the corresponding equalities (2).

Remark 3

To guarantee the proper order of the inference rules applied, we use the “leading” $q_0$, $q_1$, ..., $q_{2n-1}$, $q_{2n}$, and $c_{\ell ,2n}$, $c_{\ell ,2n-1}$,..., $c_{\ell ,2}$, $c_{\ell ,1}$, $c_{\ell ,0}$. The latter $c_{\ell ,i}$ is used to keep one and the same $C_\ell$ in the process of verifying (2).

2.3 Verifying the Equality (2)

We start with (b), assuming that the sequence $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$ is fixed.

Definition 3

Let $F_{\ell }$ denote: $(q_{2n} \backslash \, c_{\ell ,2n})$, and $H_{\ell }$ denote: $(c_{\ell ,0} \backslash \, {(e_0 \backslash \, e_0)})$.

For $1\le i\le 2n$, let $E_{\ell ,i}$ denote the formula: $(c_{\ell ,i} \backslash \, {(t_i \backslash \, c_{\ell ,i-1})})$, if the conjunct $C_\ell$ contains the variable $x_i$; and $E_{\ell ,i}$ denote the formula: $(c_{\ell ,i} \backslash \, {(f_i \backslash \, c_{\ell ,i-1})})$, if the conjunct $C_\ell$ contains the variable $\lnot x_i$; and $E_{\ell ,i}$ denote the formula:

$({(c_{\ell ,i} \backslash \, {(t_i \backslash \, c_{\ell ,i-1})})}\wedge {(c_{\ell ,i} \backslash \, {(f_i \backslash \, c_{\ell ,i-1})})})$, if $C_\ell$ contains neither $x_i$, nor $\lnot x_i$.

We introduce their “closed” versions:

$$\begin{aligned} \displaystyle { \widetilde{F} = \bigwedge _{\ell =1}^{m} F_{\ell } }, \quad \displaystyle { \widetilde{H} = \bigwedge _{\ell =1}^{m} H_{\ell } }, \quad \displaystyle { \widetilde{E_{i}} = \bigwedge _{\ell =1}^{m} E_{\ell ,i} } \end{aligned}$$

(19)

Lemma 3

In case (2) holds, a sequent of the specific form is derivable:

$$\begin{aligned} e_0^{bb}, \alpha _1^{bb}, \alpha _2^{bb}, \dots , \alpha _{2n-2}^{bb}, \alpha _{2n-1}^{bb}, (\alpha _{2n}\cdot \,q_{2n})^{bb},\ \varDelta _{n}^{bb}\ \vdash \ e_0^{bb} \end{aligned}$$

(20)

where $\varDelta _{n}$ is a sequence of formulas: $\varDelta _{n} = \widetilde{F}, \widetilde{E}_{2n}, \widetilde{E}_{2n-1}, \dots , \widetilde{E_{2}}, \widetilde{E_{1}}, \widetilde{H}$.

NB: Notice that $\varDelta _{n}$ does not depend on particular $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$.

Proof

Since $\alpha _{i-1}, \alpha _{i}, c_{\ell ,i},\,E_{\ell ,i,\alpha _{i}} \ \vdash \ (\alpha _{i-1} \cdot \,\, c_{\ell ,i-1})$, by a simple inverse induction on i, we can “consume” all of the $\alpha _{i}, c_{\ell ,i}$ with getting the sequents derivable:

$$e_0, \alpha _1, \alpha _2, \dots , \alpha _{2n}, q_{2n}, F_{\ell }, E_{\ell ,2n}, E_{\ell ,2n-1}, \dots E_{\ell ,2}, E_{\ell ,1}, H_{\ell }\ \vdash \ e_0 $$

and (see the rule L$\wedge$)

$$\begin{aligned} e_0, \alpha _1{}, \alpha _2{}, \dots , \alpha _{2n-2}{}, \alpha _{2n-1}{}, \alpha _{2n}, q_{2n}{},\ \varDelta _{n}{}\ \vdash \ e_0{} \end{aligned}$$

resulting in (20) with the help of Lemma 1.

2.4 Simulating the Opponent’s and Proponent’s Moves

Now we are ready to simulate the moves in the play.

Lemma 4

For any sequence $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$, labeling the branch that leads from the root to “ $\forall x_{2n}$”, the opponent move at “ $\forall x_{2n}$” is to label two outgoing edges by $t_{2n}$ and $f_{2n}$ resp. We simulate the move by the derivable sequent:

$$\begin{aligned} e_0^{[6]}, \alpha _1^{[6]}, \alpha _2^{[6]}, \dots , \alpha _{2n-2}^{[6]}, \ (\alpha _{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]},\ G_{2n}^{[2]},\ \varDelta _{n}^{[6]}\ \vdash \ e_0^{[6]} \end{aligned}$$

(21)

where

$$\begin{aligned} G_{2n} = {(q_{2n-1} \backslash \, \bigl ((t_{2n}\cdot \,q_{2n})^{[3]}\wedge (f_{2n}\cdot \,q_{2n})^{[3]}\bigr )^{[1]})} \end{aligned}$$

(22)

Proof

Having got two sequences at hand

$$ \alpha _1, \alpha _2, \dots , \alpha _{2n-1}, t_{2n},$$

and

$$ \alpha _1, \alpha _2, \dots , \alpha _{2n-1}, f_{2n},$$

by Lemma 3 we have

$$\begin{aligned} e_0^{[2]}, \alpha _1^{[2]}, \alpha _2^{[2]}, \dots , \alpha _{2n-2}^{[2]}, \alpha _{2n-1}^{[2]}, (t_{2n}\cdot \,q_{2n})^{[2]},\ \varDelta _{n}^{[2]}\ \vdash \ e_0^{[2]} \end{aligned}$$

(23)

and

$$\begin{aligned} e_0^{[2]}, \alpha _1^{[2]}, \alpha _2^{[2]}, \dots , \alpha _{2n-2}^{[2]}, \alpha _{2n-1}^{[2]}, (f_{2n}\cdot \,q_{2n})^{[2]},\ \varDelta _{n}^{[2]}\ \vdash \ e_0^{[2]} \end{aligned}$$

(24)

by Lemma 1(c) we produce

$$ e_0^{[4]}, \alpha _1^{[4]}, \alpha _2^{[4]}, \dots , \alpha _{2n-2}^{[4]}, \alpha _{2n-1}^{[4]}, \biggl ((t_{2n}\cdot \,q_{2n})^{[3]}\wedge (f_{2n}\cdot \,q_{2n})^{[3]}\biggr )^{[1]},\ \varDelta _{n}^{[4]}\ \vdash \ e_0^{[4]} $$

and conclude, Lemma 1(d), with the sequent (21) where $G_{2n}$ is given by (22).

Lemma 5

For the shorter sequence $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, labeling the one-edge shorter branch that leads from the root to “ $\exists x_{2n-1}$”, the proponent move at “ $\exists x_{2n-1}$” is to label the outgoing edge by $\alpha _{2n-1}$.

We simulate the move by the derivable sequent:

$$\begin{aligned} e_0^{[8]}, \alpha _1^{[8]}, \alpha _2^{[8]}, \dots , \alpha _{2n-3}^{[8]}, \ (\alpha _{2n-2}^{[6]}\cdot \,q_{2n-2})^{[2]},\ G_{2n-1}^{[2]}, G_{2n}^{[4]}, \ \varDelta _{n}^{[8]}\ \vdash \ e_0^{[8]} \end{aligned}$$

(25)

where

$$\begin{aligned} G_{2n-1} = {(q_{2n-2} \backslash \, \bigl ((t_{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]}\wedge (f_{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]}\bigr ))} \end{aligned}$$

(26)

Proof

Lemma 4 provides

$$\begin{aligned} e_0^{[6]}, \alpha _1^{[6]}, \alpha _2^{[6]}, \dots , \alpha _{2n-2}^{[6]}, \ (\alpha _{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]},\ G_{2n}^{[2]},\ \varDelta _{n}^{[6]}\ \vdash \ e_0^{[6]} \end{aligned}$$

and, hence,

$$\begin{aligned} e_0^{[6]}, \alpha _1^{[6]}, \alpha _2^{[6]}, \dots , \alpha _{2n-2}^{[6]}, \ \biggl ((t_{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]}\wedge (f_{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]}\biggr ),\ G_{2n}^{[2]},\ \varDelta _{n}^{[6]}\ \vdash \ e_0^{[6]} \end{aligned}$$

By Lemma 1(d) we conclude with the desired (25).

Corollary 1

If the statement (1) is valid then the following sequent is derivable in Lambek:

$$\begin{aligned} (e_0^{[6n]}\cdot \,q_0)^{[2]}, G_1^{[2]}, G_2^{[4]}, \dots , G_{2n-1}^{[4n-2]}, G_{2n}^{[4n]},\ \varDelta _{n}^{[6n+2]}\ \vdash \ e_0^{[6n+2]} \end{aligned}$$

(27)

where

$$\begin{aligned} G_1= & {} {(q_0 \backslash \, \bigl ((t_{1}^{[6n-2]}\cdot \,q_{1})^{[2]}\wedge (f_{1}^{[6n-2]}\cdot \,q_{1})^{[2]}\bigr ))} \end{aligned}$$

(28)

$$\begin{aligned} G_2= & {} {(q_{1} \backslash \, \bigl ((t_{2}^{[6n-6]}\cdot \,q_{2})^{[3]}\wedge (f_{2}^{[6n-6]}\cdot \,q_{2})^{[3]}\bigr )^{[1]})} \end{aligned}$$

(29)

$$\begin{aligned}&...&\nonumber \\ G_{2n-1}= & {} {(q_{2n-2} \backslash \, \bigl ((t_{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]}\wedge (f_{2n-1}^{[4]}\cdot \,q_{2n-1})^{[2]}\bigr ))} \end{aligned}$$

(30)

$$\begin{aligned} G_{2n}= & {} {(q_{2n-1} \backslash \, \bigl ((t_{2n}\cdot \,q_{2n})^{[3]}\wedge (f_{2n}\cdot \,q_{2n})^{[3]}\bigr )^{[1]})} \end{aligned}$$

(31)

Proof

By the bottom-up induction following the previous lemmas.

The direction from derivable sequents to winning trees is provided by Lemma 6.

Lemma 6

If the sequent (27) is derivable in Lambek then the statement (1) is valid.

Proof Sketch. Being derivable in Lambek calculus, the sequent (27) is derivable in linear logic. Replacing b with $\bot$, we get that $A^{bb}\equiv A$, resulting in that we can confine ourselves to Horn-like formulas, similar to (11) and (12), with the leading propositions from Remark 3. In its turn, such a Horn-like derivation can be transformed into a Horn-like tree program (see [11, 12, 18]), which in fact happens to be a winning strategy for the statement (1).

This concludes the proof of Lemma 6 and thereby the proof of Theorem 1.

In fact, we have proved a more general result.

Corollary 2

Let L be a calculus that includes $\mathcal{L}(\backslash ,\wedge )$, with or without Lambek’s restriction, and is in turn included in linear logic. Then the fragment of L, which uses only one implication and conjunction, is PSPACE-hard.

Proof

Given an instance of quantified Boolean formula (1), we take the sequent (27) and prove that there exists a winning tree if and only if (27) is derivable in L. Namely, if there is a winning tree, that sequent is derivable in $\mathcal{L} (\backslash , \wedge )$ with Lambek’s restriction, and thereby in the corresponding fragment of L. On the other hand, if that sequent is derivable in L, then, repeating proof of Lemma 6 for the derivation in linear logic, we conclude that there exists a winning tree.

We can also modify this technique to establish PSPACE-hardness for the fragment $\mathcal{L}(\backslash ,\vee )$, which includes only one implication and disjunction.

Theorem 2

The fragment $\mathcal{L}(\backslash , \vee )$ is PSPACE-hard.

We give a proof sketch in Appendix A.

3 Grammars Based on the Lambek Calculus with Disjunction

Theorem 3

For any fragment of the Lambek calculus with conjunction and disjunction, which includes at least one division operation, $\mathop {\backslash }$, and disjunction, $\vee$, the class of languages generated by categorial grammars based on this calculus (in particular, the class of languages generated by $\mathcal{L}(\mathop {\backslash }, \vee )$-grammars) is closed under finite intersections.

This theorem immediately yields the following corollary.

Corollary 3

Grammars based on $\mathcal{L}(\mathop {\backslash },\vee )$ can generate arbitrary finite intersections of context-free languages.

Moreover, $\mathcal{L}(\mathop {\backslash },\vee )$ also captures images of such intersections under alphabetic homomorphisms. A alphabetic homomorphism is a mapping $h :\varSigma _1^+ \rightarrow \varSigma _2^+$ of words over one alphabet to words of another one, such that $h(\varSigma _1) \subseteq \varSigma _2$ and $h(uv) = h(u) \, h(v)$ for any $u,v \in \varSigma _1^+$. The class of languages generated by $\mathcal{L}(\mathop {\backslash },\vee )$-grammars is closed under alphabetic homomorphisms. Indeed, if the grammar $\mathcal {G}= \langle \varSigma _1, \triangleright , H \rangle$ generates language M, then $\mathcal {G}_h = \langle \varSigma _2, \triangleright _h, H \rangle$, where $a \triangleright _h A$ iff $b \triangleright A$ for some $b \in h^{-1}(a)$, generates h(M). This yields the following stronger corollary.

Corollary 4

Grammars based on $\mathcal{L}(\mathop {\backslash },\vee )$ can generate all language of the form $h(M_1 \cap \ldots \cap M_k)$, where $M_1$, ..., $M_k$ are context-free and h is a alphabetic homomorphism.

Notice that this extension of Corollary 3 is non-trivial, since $h(M_1 \cap M_2)$ is not always equal to $h(M_1) \cap h(M_2)$. There is an example by Păun [22] of a language which is not a finite intersection of context-free languages, but can be obtained from such an intersection by applying a alphabetic homomorphism: $\{a^{2n^2} \mid n \ge 1 \} = h(\{(a^n b^n)^n \mid n \ge 1\}),$ where $h(a) = h(b) = a$.

Before proving Theorem 3, we establish several technical lemmata. The first one is a simplified version of Kanazawa’s [9] Lemma 13.

Definition 4

Let the set of variables include two disjoint subsets, $\mathrm {Var}_1$ and $\mathrm {Var}_2$. A formula is called a $P_i$-formula if it includes only variables from $\mathrm {Var}_i$ ($i = 1, 2$).

Lemma 7

Let $\varGamma$ and $\varDelta$ sequences consisting of $P_1$-formulae and $P_2$-formulae, in an arbitrary order. Let B be a $P_2$-formula and C be a $P_1$-formula. Then the sequent $\varGamma , B, \varDelta \vdash C$ is not derivable.

Proof

Induction on a cut-free derivation. The sequent in question could not be in axiom, because then $B = C$, and $P_1$-formulae and $P_2$-formulae do not intersect.

Now consider the last rule applied in the derivation. If it is a one-premise rule, i.e., one of $\mathbf {L} \cdot$, $\mathbf {R}{\mathop {/}}$, $\mathbf {R} {\mathop {\backslash }}$, $\mathbf {L} {\wedge }$, $\mathbf {R} {\vee }$, then its premise also satisfies the conditions of the lemma, and such a sequent, by induction hypothesis, could not be derivable. Contradiction. The same happens with $\mathbf {L}{\vee }$ and $\mathbf {R}{\wedge }$, where both premises are not derivable by induction hypothesis. For $\mathbf {R}{\cdot }$, induction hypothesis yields non-derivability of the premise into which the B formula goes.

The most tricky cases are $\mathbf {L} {\mathop {\backslash }}$ and $\mathbf {L} {\mathop {/}}$. We consider the former; the latter is dual. Recall that $\mathbf {L} {\mathop {\backslash }}$ is a rule of the form

Now the question is where comes B. There are three possible cases.

• Case 1: B is in $\varSigma _1$ or $\varSigma _2$. In this case, the right premise satisfies the condition of the lemma, and is therefore not derivable by induction hypothesis.

• Case 2: B is in $\varPhi$. In this case, let us consider $E \mathop {\backslash }F$, which is either a $P_1$-formula or a $P_2$-formula. If $E \mathop {\backslash }F$ is a $P_1$-formula, then so is E, and the left premise, $\varPhi \vdash E$, satisfies the condition of the lemma and is not derivable by induction. If $E \mathop {\backslash }F$ is a $P_2$-formula, then so is F, and now the right premise $\varSigma _1, F, \varSigma _2 \vdash C$, satisfies the condition of the lemma, and induction hypothesis yields its non-derivability.

• Case 3: $B = E \mathop {\backslash }F$. The right premise satisfies the condition of the lemma (F is a $P_2$-formula and C is a $P_1$-formula), and is therefore not derivable my induction hypothesis.

The next 4 lemmas are proved by straightforward induction on derivation. We put their proofs in Appendix B.

Definition 5

Define the notion of strictly positive occurrence of a subformula inside a formula:

• A is strictly positive in itself;

• C occurs strictly positively in $A \mathop {\backslash }B$ if and only if it occurs strictly positively in B; the same for $B \mathop {/}A$;

• C occurs strictly positively in $A \cdot B$ if and only if if occurs strictly positively in A or in B; the same for $A \vee B$ and $A \wedge B$.

Lemma 8

(Disjunctive Property). Let $F_1$ and $F_2$ be arbitrary formulae, and $E_1, \ldots , E_n$ be formulae without $\wedge$ in which subformulae of the form $A \vee B$ do not occur strictly positively. Then the derivability $E_1, \ldots , E_n \vdash F_1 \vee F_2$ implies the derivability of $E_1, \ldots , E_n \vdash F_i$ for $i = 1$ or 2.

Lemma 9

If $F_1, \ldots , F_n$ do not include variable b, then $F_1, \ldots , F_n \vdash b$ is not derivable.

Lemma 10

If $F_1, \ldots , F_\ell , E_1 \mathop {\backslash }b, \ldots , E_k \mathop {\backslash }b, b \vdash b$ is derivable and $F_1, \ldots , F_\ell$ do not include b, then $k = \ell = 0$.

Lemma 11

If $F_1,\ldots , F_\ell , E_1 \mathop {\backslash }b, \ldots , E_k \mathop {\backslash }b \rightarrow b$ is derivable and $F_1, \ldots , F_\ell$ do not include b, then $F_1, \ldots , F_\ell , E_1 \mathop {\backslash }b, \ldots , E_{k-1} \mathop {\backslash }b \rightarrow E_k$ is derivable.

The following lemma is the key one for the proof of Theorem 3.

Lemma 12

Let $A_1, \ldots , A_n, C$ be $P_1$-formulae, $B_1, \ldots , B_n, D$ be $P_2$-formulae, and let b be a fresh variable, $b \notin \mathrm {Var}_1 \cup \mathrm {Var}_2$. Also suppose that no formula of the form $E \vee F$ occurs in $A_1$, ..., $A_n$, $B_1$, ..., or $B_n$ strictly positively. Then the sequent

$$ ((A_1 \mathop {\backslash }b) \vee (B_1 \mathop {\backslash }b)) \mathop {\backslash }b, \ldots , ((A_n \mathop {\backslash }b) \vee (B_n \mathop {\backslash }b)) \mathop {\backslash }b \vdash ((C \mathop {\backslash }b) \vee (D \mathop {\backslash }b)) \mathop {\backslash }b $$

is derivable if and only if so are $A_1, \ldots , A_n \vdash C$ and $B_1, \ldots , B_n \vdash D$.

In the notations of Subsect. 2.1, the first sequent of this lemma can be shortly written as $(A_1^b \vee B_1^b)^b, \ldots , (A_n^b \vee B_n^b)^b \vdash (C^b \vee D^b)^b.$ Though $(A^b \vee B^b)^b$ is not equivalent to $A \wedge B$, and even not equivalent to $(A \wedge B)^{bb}$, this sequent happens to be equiderivable with $A_1 \wedge B_1, \ldots , A_n \wedge B_n \vdash C \wedge D$, which Kanazawa [9] used for his intersection construction with additive conjunction.

Proof

The “if” part is straightforwardly established by direct derivation.

For the “only if” part we first use the reversibility of $\mathbf {R} {\mathop {\backslash }}$ and $\mathbf {L} {\vee }$, which yields derivability of the following two sequents:

$$\begin{aligned}&C \mathop {\backslash }b, ((A_1 \mathop {\backslash }b) \vee (B_1 \mathop {\backslash }b)) \mathop {\backslash }b, \ldots , ((A_n \mathop {\backslash }b) \vee (B_n \mathop {\backslash }b)) \mathop {\backslash }b \vdash b\\&D \mathop {\backslash }b, ((A_1 \mathop {\backslash }b) \vee (B_1 \mathop {\backslash }b)) \mathop {\backslash }b, \ldots , ((A_n \mathop {\backslash }b) \vee (B_n \mathop {\backslash }b)) \mathop {\backslash }b \vdash b. \end{aligned}$$

Let us analyze the derivation of the first sequent. We claim derivability of $K_1, \ldots , K_n, C \mathop {\backslash }b \vdash b$, where each $K_i$ is either $A_i$ or $B_i$. In order to prove it, consider a more general statement, the derivability of

$$K_{n-k}, \ldots , K_n, C \mathop {\backslash }b, (A_1^b \vee B_1^b)^b, \ldots , (A_{n-k-1}^b \vee B_{n-k-1}^b)^b \vdash b.$$

This statement is proved by induction on k. Indeed, for $k=0$ derivability of this sequent was shown above. For the induction step, suppose that

$$K_{n-k}, \ldots , K_n, C \mathop {\backslash }b, (A_1^b \vee B_1^b)^b, \ldots , (A_{n-k-1}^b \vee B_{n-k-1}^b)^b \vdash b$$

is derivable and apply Lemma 11, which yields derivability of

$$ K_{n-k}, \ldots , K_n, C \mathop {\backslash }b, (A_1^b \vee B_1^b)^b, \ldots , (A_{n-k-2}^b \vee B_{n-k-2}^b)^b \vdash A_{n-k-1}^b \vee B_{n-k-1}^b. $$

Now apply the Disjunctive Property (Lemma 8) and obtain derivability of

$$ K_{n-k}, \ldots , K_n, C \mathop {\backslash }b, (A_1^b \vee B_1^b)^b, \ldots , (A_{n-k-2}^b \vee B_{n-k-2}^b)^b \vdash K_{n-k-1} \mathop {\backslash }b, $$

where $K_{n-k-1}$ is either $A_{n-k-1}$ or $B_{n-k-1}$. Reversion of $\mathbf {L} {\mathop {\backslash }}$ yields the necessary

$$ K_{n-(k+1)}, K_{n-k}, \ldots , K_n, C \mathop {\backslash }b, (A_1^b \vee B_1^b)^b, \ldots , (A_{n-k-2}^b \vee B_{n-k-2}^b)^b \vdash b. $$

In the end of the induction, for $k = n-1$, we get $K_1, \ldots , K_n, C \mathop {\backslash }b \vdash b$, and one more application of Lemma 11 yields $K_1, \ldots , K_n \vdash C$.

Now recall that C is a $P_1$-formula, and each of $K_1, \ldots , K_n$ is a $P_1$-formula or a $P_2$-formula. If $K_i = B_i$ for some i, i.e., it is a $P_2$-formula, then $K_1, \ldots , K_n \vdash C$ is not derivable by Lemma 7. Thus, for all i we have $K_i = A_i$, and obtain the needed sequent $A_1, \ldots , A_n \vdash C$.

The same reasoning applied to $D \mathop {\backslash }b, (A_1^b \vee B_1^b)^b, \ldots , (A_n^b \vee B_n^b)^b \vdash b$ yields $B_1, \ldots , B_n \vdash D$.

Lemma 12, together with Lemma 2 of Subsect. 2.1, yield the following corollary:

Corollary 5

Let $A_1, \ldots , A_n, C$ be $P_1$-formulae, $B_1, \ldots , B_n, D$ be $P_2$-formulae, and let b and c be fresh variables ($b,c\notin \mathrm {Var}_1 \cup \mathrm {Var}_2$, $b \ne c$). Then the sequent

$$ ((A_1^{cc})^b \vee (B_1^{cc})^b)^{b}, \ldots , ((A_n^{cc})^b \vee (B_1^{cc})^b)^b \vdash ((C^{cc})^b \vee (D^{cc})^b)^b $$

is derivable if and only if so are $A_1, \ldots , A_n \vdash C$ and $B_1, \ldots , B_n \vdash D.$

Proof

The only strictly positive subformula or $A_i^{cc}$ and $B_j^{cc}$ is c. Thus, there is no strictly positive subformula the form $E \vee F$, and we can apply Lemma 12. This lemma yields the fact that

$$ ((A_1^{cc})^b \vee (B_1^{cc})^b)^{b}, \ldots , ((A_n^{cc})^b \vee (B_1^{cc})^b)^b \vdash ((C^{cc})^b \vee (D^{cc})^b)^b $$

is derivable if and only if so are $A_1^{cc}, \ldots , A_n^{cc} \vdash C^{cc}$ and $B_1^{cc}, \ldots , B_n^{cc} \vdash D^{cc}.$ For these two sequents, we apply Lemma 2 and replace these sequents with equiderivable ones, $A_1, \ldots , A_n \vdash C$ and $B_1, \ldots , B_n \vdash D$.

Now we are ready to prove the main result of this section.

Proof

(of Theorem 3). Consider two categorial grammars over the same alphabet, $\mathcal {G}_1 = \langle \varSigma , \triangleright _1, H_1 \rangle$ and $\mathcal {G}_2 = \langle \varSigma , \triangleright _2, H_2 \rangle$. Without loss of generality we can suppose that all formulae of $\mathcal {G}_i$ are $P_i$-formulae (otherwise just rename the variables). Construct the new grammar $\mathcal {G}= \langle \varSigma , \triangleright , H \rangle$, where, for each $a \in \varSigma$ we postulate $a \triangleright ((A^{cc})^b \vee (B^{cc})^b)^b$ for any A and B such that $a \triangleright _1 A$ and $a \triangleright _2 A$; $H = ((H_1^{cc})^b \vee (H_2^{cc})^b)^b$. Here b and c are fresh variables: b and c are distinct and do not occur in $\mathcal {G}_1$ or $\mathcal {G}_2$. By Corollary 5 a word $a_1, \ldots a_n$ is accepted by $\mathcal {G}$ if and only if it is accepted by both $\mathcal {G}_1$ and $\mathcal {G}_2$. Therefore, the language generated by $\mathcal {G}$ is exactly the intersection of languages generated by $\mathcal {G}_1$ and $\mathcal {G}_2$.

4 Concluding Remarks

In this paper we have proved two refined results on the complexity of the Lambek calculus enriched either with conjunction or disjunction. Namely, we have established PSPACE-completeness for small fragments $\mathcal{L} (\mathop {\backslash }, \wedge )$ and $\mathcal{L}(\mathop {\backslash }, \vee )$. Notice that the encoding used in this paper is more involved than the encodings from [6, 8, 10, 18], because here we were not allowed to use the product (multiplicative conjunction) and one of the divisions. Besides, we have proved that $\mathcal{L}(\mathop {\backslash },\vee )$-grammars generate all finite intersections of context-free languages and images of such intersections under alphabetic homomorphisms.

There are some questions left for future work. First, we see that in our constructions for proving PSPACE-hardness involve formulae of unbounded implication depth. On the other hand, for the original Lambek calculus without additive connectives, which is NP-complete, Pentus [25], nevertheless, a polynomial time decision procedure for the case where the order (a complexity measure similar to implication depth) of formulae is bounded by a constant d, fixed in advance. The degree of the polynomial, of course, depends on d. For the Lambek calculus with additives, we plan to show that it is not the case. Following the basic ideas of our encoding, with the formulas of the implication nesting depth bounded by some constant, we intend to simulate at least co-NP-hardness of our small fragment $\mathcal{L}(\backslash , \wedge )$ with one implication and conjunction.

Another open question is to describe the class of languages generated by Lambek grammars with additive connectives. In particular, Kuznetsov and Okhotin [14, 16] show that such grammars can generate languages described by conjunctive grammars [21]. Such grammars can be quite powerful, for example, can generate $\{a^{4^n} \mid n \ge 1 \}$ [7]. It is yet unknown whether all such languages can be generated by $\mathcal{L}(\backslash ,\vee )$-grammars.

Appendices

A PSPACE-completeness of the fragment $\mathcal{L}(\backslash , \vee )$

In this section we will modify Sect. 2 to establish PSPACE-completeness for the fragment $\mathcal{L}(\backslash ,\, \vee \,)$, which includes only one implication and disjunction.

Remark 4

For the sake of readability, we conceive of the formula ${((A \cdot \,B) \backslash \, C)}$ as abbreviation for ${(B \backslash \, {(A \backslash \, C)})}$. In particular, $(A \cdot \,B)^{b}$ is abbreviation for ${(B \backslash \, {(A \backslash \, b)})}$. Because of Lemma 1, the formula $(A^b\wedge B^b)$ is conceived of as abbreviation for ${((A\vee B) \backslash \, b)}$ within this section.

Theorem 4

The fragment $\mathcal{L}(\backslash , \vee )$ is PSPACE-complete.

Proof Sketch. We start with the equality (2), assuming that $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$ are given.

To prove Lemma 14, the “disjunction analog” of Lemma 3, we modify the basic material given in the “conjunction” Definition 3 by means of Definitions 6 and 7 working within the $\mathcal{L}(\backslash , \vee )$ fragment.

Definition 6

For $1\le i\le 2n$, let $E_{\ell ,i,\beta }$ denote the formula: $(c_{\ell ,i} \backslash \, {(\beta \backslash \, c_{\ell ,i-1})})$.

Let $F_{\ell }$ denote: $(q_{2n} \backslash \, c_{\ell ,2n})$, and $H_{\ell }$ denote: $(c_{\ell ,0} \backslash \, {(e_0 \backslash \, e_0)})$.

Lemma 13

The following “verifying” sequent is derivable in Lambek calculus

$$e_0, \alpha _1, \alpha _2, \dots , \alpha _{2n}, q_{2n}, F_{\ell }, E_{\ell ,2n,\alpha _{2n}}, E_{\ell ,2n-1,\alpha _{2n-1}}, \dots E_{\ell ,2,\alpha _{2}}, E_{\ell ,1,\alpha _{1}}, H_{\ell }\ \vdash \ e_0 $$

Proof

By the inverse induction on i: $\alpha _{i-1}, \alpha _{i}, c_{\ell ,i},\, E_{\ell ,i,\alpha _{i}} \ \vdash \ (\alpha _{i-1} \cdot \,\, c_{\ell ,i-1})$

Definition 7

We introduce the following formulas:

$$\begin{aligned} \left\{ \begin{array}{c}{} \displaystyle { \widetilde{F} = \biggl (\bigvee _{\ell =1}^{m} (F_{\ell })^{b}\biggr )^{b} }, \quad \displaystyle { \widetilde{H} = \biggl (\bigvee _{\ell =1}^{m} (H_{\ell })^{b}\biggr )^{b} } \\[2ex] \displaystyle { \widetilde{E_{i}} = \biggl (\bigvee _{1\le \ell \le m,\ E_{\ell ,i,\beta }\in \mathcal{E}_{\ell ,i}} (E_{\ell ,i,\beta })^{b}\biggr )^{b} } \end{array}\right. \end{aligned}$$

(32)

where a one- or two-element set of formulas, $\mathcal{E}_{\ell ,i}$, is defined as follows:

• (1) $\mathcal{E}_{\ell ,i} = \{\, E_{\ell ,i,t_i}\, \}$, if the conjunct $C_\ell$ contains the variable $x_i$,

• (2) $\mathcal{E}_{\ell ,i} = \{\, E_{\ell ,i,f_i}\, \}$, if the conjunct $C_\ell$ contains $\lnot x_i$,

• (3) $\mathcal{E}_{\ell ,i} = \{\, E_{\ell ,i,t_i},\ E_{\ell ,i,f_i}\, \}$, if $C_\ell$ contains neither $x_i$, nor $\lnot x_i$.

By applying (2) and Lemma 1, we get the desired verification:

Lemma 14

The following sequent is derivable in Lambek

$$e_0^{bb}, \alpha _1^{bb}, \alpha _2^{bb}, \dots , \alpha _{2n-1}, (\alpha _{2n}\cdot \,\, q_{2n})^{bb},\ \varDelta _{n}\ \vdash \ e_0^{bb} $$

where $\varDelta _{n}$ is a sequence of formulas: $\varDelta _{n} = \widetilde{F}, \widetilde{E}_{2n}, \widetilde{E}_{2n-1}, \dots , \widetilde{E_{2}}, \widetilde{E_{1}}, \widetilde{H}$

Corollary 6

It suffices to follow the line of reasoning in Sect. 2 to find appropriate $G_1$, $G_2$, ..., $G_{2n-1}$, $G_{2n}$, such that the following sequent is derivable in Lambek calculus if and only if the statement (1) is valid:

$$\begin{aligned} (e_0^{[4n]}\cdot \,q_0)^{[2]}, G_1^{[2]}, G_2^{[4]}, \dots , G_{2n-1}^{[4n-2]}, G_{2n}^{[4n]}, \ \varDelta _{n}^{[4n]}\ \vdash \ e_0^{[4n+2]} \end{aligned}$$

(33)

B Proofs of Technical Lemmas for Section 3

Proof

(of Lemma 8). Induction on derivation. The sequent in question could not be an axiom, since the antecedent of $F_1 \vee F_2 \vdash F_1 \vee F_2$ includes $F_1 \vee F_2$ in a strictly positive position. Consider the last rule applied in the derivation. It could be $\mathbf {L} {\mathop {\backslash }}$, $\mathbf {L} {\mathop {/}}$, $\mathbf {L} \cdot$, or . Rules with $\wedge$ cannot be used, since there are no $\wedge$’s in the antecedent, and the main connective of the succedent is $\vee$. If the last rule is , we immediately reach our goal.

If the derivation ends with an application of $\mathbf {L} {\cdot }$:

then we apply the induction hypothesis, get $E_1, \ldots , E'_i, E''_i, \ldots , E_n \vdash F_i$ ($i = 1$ or 2) and apply $\mathbf {L} {\cdot }$ to this sequent, which yields our goal.

For $\mathbf {L} {\mathop {\backslash }}$, we get the following

and notice that the antecedent of the right premise still satisfies the conditions of the lemma, thus we can apply induction hypothesis. The induction hypothesis yields $E_1, \ldots , E_i, E''_j, \ldots , E_n \vdash F_i$. Applying $\mathbf {L} {\mathop {/}}$ with the same left premise, $E_{i+1}, \ldots , E_{j-1} \vdash E'_j$, yields our goal.

The $\mathbf {L} {\mathop {/}}$ case is symmetric.

Proof

(of Lemma 9). Induction on derivation. The axiom should be of the form $b \vdash b$, which violates the condition. For each inference rule, we apply the induction hypothesis for the premise from which the succedent b comes.

Proof

(of Lemma 10). Induction on derivation. Induction base is axiom $b \vdash b$. Consider the last rule applied. If it is one of the one-premise rules, then we use the induction hypothesis for the only premise. For applications of $\mathbf {L}{\mathop {/}}$ or $\mathbf {L}{\mathop {\backslash }}$, if the rightmost occurrence of b goes to the right premise, we again directly use the induction hypothesis. Notice that for $\mathbf {L}{\mathop {\backslash }}$ this is always the case. The other rule, $\mathbf {L}{\mathop {/}}$, however, can decompose one of the $F_i$ and take the rightmost b to the left premise:

The right premise, however, now is not derivable by Lemma 9. Contradiction.

Proof

(of Lemma 11). Induction on derivation again. Any one-premise rule applied for one of the $F_i$, as well as $\mathbf {L} {\mathop {/}}$ or $\mathbf {L} {\mathop {\backslash }}$ which keeps $E_k \mathop {\backslash }b$ in the right premise, is handled by directly using the induction hypothesis and applying the same rule. The situation where $\mathbf {L} {\mathop {/}}$ takes $E_k \mathop {\backslash }b$ to the left premise leads to contradiction with Lemma 9, exactly as in the proof of the previous lemma.