The Lambek Calculus with Iteration: Two Variants

Abstract

Formulae of the Lambek calculus are constructed using three binary connectives, multiplication and two divisions. We extend it using a unary connective, positive Kleene iteration. For this new operation, following its natural interpretation, we present two lines of calculi. The first one is a fragment of infinitary action logic and includes an omega-rule for introducing iteration to the antecedent. We also consider a version with infinite (but finitely branching) derivations and prove equivalence of these two versions. In Kleene algebras, this line of calculi corresponds to the *-continuous case. For the second line, we restrict our infinite derivations to cyclic (regular) ones. We show that this system is equivalent to a variant of action logic that corresponds to general residuated Kleene algebras, not necessarily *-continuous. Finally, we show that, in contrast with the case without division operations (considered by Kozen), the first system is strictly stronger than the second one. To prove this, we use a complexity argument. Namely, we show, using methods of Buszkowski and Palka, that the first system is $\varPi _1^0$-hard, and therefore is not recursively enumerable and cannot be described by a calculus with finite derivations.

This work is supported by the Russian Science Foundation under grant 16-11-10252.

1 The Infinitary Lambek Calculus with Positive Iteration

The Lambek calculus $\mathbf {L}$ [12] deals with formulae that are built using three connectives, $\cdot$ (product), $\mathop {\backslash }$, and $\mathop {/}$ (left and right divisions). These connectives enjoy a natural interpretation as operations on formal languages (completeness shown by Pentus [17]). There are, however, also other interesting and well-respected operations on formal languages, and it is quite natural to try to extend $\mathbf {L}$ by adding these operations as new connectives.

One of the most common of such operations is iteration, or Kleene star: for a language M over an alphabet $\varSigma$ its iteration is defined as follows:

$$M^* = \{ u_1 \dots u_n \mid n \ge 0, u_i \in M \}.$$

As one can notice, $M^*$ always includes the empty word, $\varepsilon$. The original Lambek calculus, however, obeys so-called Lambek’s non-emptiness restriction, that is, the empty sequence is never allowed in $\mathbf {L}$ (this restriction is motivated by linguistic applications; from the algebraic point of view, this means that we’re considering residuated semigroups instead of residuated monoids). Therefore, throughout this paper we consider a modified version of Kleene star, called positive iteration:

$$M^+ = \{ u_1 \dots u_n \mid n \ge 1, u_i \in M \} = M^* - \{ \varepsilon \}.$$

In this paper, we introduce several extensions of the Lambek calculus with this new connective, establish connections between them, and prove some complexity bounds.

Formulae of the Lambek calculus with positive iteration, usually called types, are built from a countable set of variables (primitive types) $\mathrm {Pr}= \{ p_1, p_2, p_3, \dots \}$ using three binary connectives, $\cdot$, $\mathop {\backslash }$, and $\mathop {/}$, and one unary connective, ${}^+$ (written in the postfix form, $A^+$). The set of all types is denoted by $\mathrm {Tp}$. Types are denoted by capital Latin letters; capital Greek letters stand for finite linearly ordered sequences of types.

Derivable objects are sequents of the form $\varPi \rightarrow A$, where $A \in \mathrm {Tp}$ and $\varPi$ is a non-empty finite sequence of types.

Now let’s define the first calculus for positive iteration, $\mathbf {L}^{\!+}_{\omega }$. The axioms and the rules for $\cdot$, $\mathop {\backslash }$, and $\mathop {/}$ are the same as in the original Lambek calculus $\mathbf {L}$:

For ${}^+$, this calculus includes a countable set of right rules:

and one left rule

This rule is an $\omega$ -rule, or an infinitary rule. Application of such a rule makes the proof tree infinite. This is somewhat unpleasant from the computational point of view, but, as we show later on, it appears to be inevitable.

The rules $(\rightarrow {}^+)_n$ and $({}^+\rightarrow )_\omega$ come from the rules for iteration in infinitary action logic, $\mathbf {ACT}_{\omega }$ [4]. Our system $\mathbf {L}^{\!+}_{\omega }$ differs from $\mathbf {ACT}_{\omega }$ in the following two points.

• 1. $\mathbf {L}^{\!+}_{\omega }$ enriches the “pure” (multiplicative) Lambek calculus $\mathbf {L}$, while $\mathbf {ACT}_{\omega }$ is based on the full Lambek calculus $\mathbf {FL}$, including also additive conjunction ($\wedge$) and disjunction ($\vee$). This means that complexity lower bounds for $\mathbf {L}^{\!+}_{\omega }$ are stronger results than lower bounds for $\mathbf {ACT}_{\omega }$.

• 2. In contrast to $\mathbf {ACT}_{\omega }$, in $\mathbf {L}^{\!+}_{\omega }$ we have Lambek’s non-emptiness restriction, and therefore use positive iteration instead of Kleene star.

The cut rule of the form

is admissible in $\mathbf {L}^{\!+}_{\omega }$. This fact is proved by the same transfinitary cut-elimination procedure, as presented by Palka [14] for $\mathbf {ACT}_{\omega }$ (for a restricted fragment of $\mathbf {L}^{\!+}_{\omega }$ cut elimination was independently shown by Ryzhkova [21]).

The admissibility of $(\mathrm {cut})$ yields the fact that the rules $(\rightarrow \mathop {\backslash })$, $(\rightarrow \mathop {/})$, $(\cdot \rightarrow )$, and, most interestingly, $({}^+\rightarrow )_\omega$ are invertible.

The Lambek calculus $\mathbf {L}$, defined by axioms $(\mathrm {ax})$ and rules $(\rightarrow \mathop {\backslash })$, $(\mathop {\backslash }\rightarrow )$, $(\rightarrow \mathop {/})$, $(\mathop {/}\rightarrow )$, $(\rightarrow \cdot )$, and $(\cdot \rightarrow )$, is a conservative fragment of $\mathbf {L}^{\!+}_{\omega }$. Cut elimination for $\mathbf {L}$ was known already by Lambek [12].

The calculus $\mathbf {L}^{\!+}_{\omega }$ defined in this section is sound with respect to the intended interpretation on formal languages, where ${}^+$ is interpreted as positive iteration:

$$ M^+ = \{ u_1 \dots u_n \mid n \ge 1, u_i \in M \}, $$

and the Lambek connectives are interpreted in the same way as for $\mathbf {L}$:

$$\begin{aligned} M \cdot N&= \{ uv \mid u \in M, v \in N \},\\ M \mathop {\backslash }N&= \{ u \in \varSigma ^+ \mid (\forall v \in M) \, vu \in N \}, \\ N/M&= \{ u \in \varSigma ^+ \mid (\forall v \in M) \, uv \in N \}. \end{aligned}$$

The arrow, $\rightarrow$, is interpreted as the subset relation.

Completeness with respect to this interpretation is an open problem.

2 $\varPi _1^0$-completeness of $\mathbf {L}^{\!+}_{\omega }$

In this section we prove that derivability in $\mathbf {L}^{\!+}_{\omega }$ is $\varPi _1^0$- (co-r.e.-) hard. Basically, we follow the same strategy as Buszkowski [4], namely, encoding the totality problem for context-free grammars. Our construction, however, is more involved: instead of embedding context-free grammars into the Lambek environment as Ajdukiewicz – Bar-Hillel basic categorial grammars, we use another translation by Safiullin [22] which yields a categorial grammar that assigns exactly one type to each letter of the alphabet. This trick allows us to avoid using additive operations, and prove the complexity lower bound for the extension of the original, purely multiplicative Lambek calculus $\mathbf {L}$. For the purely multiplicative fragment of $\mathbf {ACT}_{\omega }$, the lower complexity bound was left as an open problem by Buszkowski in [4]. Here we solve not that problem exactly, but its version with Lambek’s restriction.

Throughout this paper, all languages do not contain the empty word. Accordingly, all context-free grammars do not contain $\varepsilon$-rules. By $\textsc {total}^+$ we denote the set of all context-free grammars $\mathcal {G}$ such that the language generated by $\mathcal {G}$ is the set of all non-empty words, $\varSigma ^+$. The problem $\textsc {total}^+$ is $\varPi _1^0$-hard. Indeed, as shown in [4], $\textsc {total}$, the totality problem for context-free grammars possibly using the empty word, reduces to $\textsc {total}^+$. In its turn, $\textsc {total}$ itself is known to be undecidable, and standard proofs of this fact actually yield more: they reduce a well-known $\varSigma _1^0$- (r.e.-) complete problems, e.g., Post’s correspondence problem [7, Theorem 9.22] or halting problem for Turing machines [5, Example 5.43], to the complement of $\textsc {total}$. This makes $\textsc {total}$ and $\textsc {total}^+$ themselves $\varPi _1^0$-complete.

We can further restrict ourselves to context-free grammars over a two-letter alphabet, $\{ b, c \}$. Denote the $\varepsilon$-free totality problem over $\{ b, c\}$ by $\textsc {total}^+_2$. The original problem $\textsc {total}^+$ is reduced to $\textsc {total}^+_2$ in the following way. Let $\mathcal {G}$ be a context-free grammar that defines a language $\mathcal {L}(\mathcal {G})$ over $\varSigma = \{ a_0, a_1, \dots , a_n \}$. The homomorphism $h :a_i \mapsto b^{i} c$ is a one-to-one correspondence between $\varSigma ^+$ and $\{ u \in \{ b,c \}^+ \mid u \text { ends on } c \text { and doesn't contain } b^{n+1} \text { as a subword} \}$. Now we can computably transform $\mathcal {G}$ into a new context-free grammar $\mathcal {G}'$ for the language $h(\mathcal {L}(\mathcal {G})) \cup \{ u \in \{b,c\}^+ \mid u \text { ends on }$b$\text { or contains } b^{n+1} \text { as a subword} \}$ over $\{b,c\}$. Clearly, $\mathcal {G}\in \textsc {total}^+ \iff \mathcal {G}' \in \textsc {total}_2^+$. This establishes the necessary reduction and $\varPi _1^0$-hardness of $\textsc {total}_2^+$.

Finally, we consider the alternation problem for context-free grammars over $\{ b, c \}$, denoted by $\textsc {alt}_2$. A context-free grammar $\mathcal {G}$ belongs to $\textsc {alt}_2$ if the language it generates includes the language $(\{b\}^+ \{c\}^+)^+ = \{ b^{m_1} c^{k_1} \ldots b^{m_n} c^{k_n} \mid n \ge 1, m_i \ge 1, k_j \ge 1 \}$ (as a subset). Clearly, $\textsc {alt}_2$ is also $\varPi _1^0$-hard by reduction of $\textsc {total}_2^+$, since $M = \{ b, c \}^+ \iff \{b\} \cdot M \cdot \{c\} \supseteq (\{b\}^+ \{c\}^+)^+$.

Now we need an encoding of context-free grammars in the Lambek calculus. A Lambek categorial grammar with unique type assignment over the alphabet $\{ a_1, \dots , a_n \}$ consists of $(n+1)$ types (without the $^+$ connective) $A_1, \dots , A_n, H$ (H is called the target type), and a word $w = a_{i_1} \dots a_{i_m}$ belongs to the language generated by this grammar iff the sequent $A_{i_1}, \dots , A_{i_m} \rightarrow H$ is derivable in $\mathbf {L}$. These grammars have the same expressive power as context-free grammars (without $\varepsilon$-rules).

Theorem 1

(A. Safiullin, 2007). For every context-free language there exists, and can be effectively constructed from the original context-free grammar, a Lambek categorial grammar with unique type assignment [22].

The inverse translation, from Lambek categorial grammars to context-free grammars, is also available due to Pentus [15] (in this paper we don’t need it). In order to make this paper logically self-contained, we revisit Theorem 1 and give its full proof in the Appendix (in Safiullin’s paper [22], the proof is only briefly sketched).

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

Theorem 2

The derivability problem for $\mathbf {L}^{\!+}_{\omega }$ is $\varPi _1^0$-complete.

Proof

The fact that this problem belongs to class $\varPi _1^0$ (the upper bound) is established by the same argument as for $\mathbf {ACT}_{\omega }$ in [14].

To prove $\varPi _0^1$-hardness of the derivability problem in $\mathbf {L}^{\!+}_{\omega }$ (the lower bound), we encode $\textsc {alt}_2$. For every context-free grammar $\mathcal {G}$ over $\{b,c\}$ we algorithmically construct an $\mathbf {L}^{\!+}_{\omega }$-sequent $E \rightarrow H$ such that

$$\mathcal {G}\in \textsc {alt}_2 \iff E \rightarrow H \text { is derivable in } \mathbf {L}^{\!+}_{\omega }.$$

First we apply Theorem 1 to $\mathcal {G}$ and obtain a Lambek categorial grammar with unique type assignment. In this case, it consists of three types, B, C, and H. Next, let $E = (B^+ \cdot C^+)^+$.

Now, since the $(\cdot \rightarrow )$ and $({}^+\rightarrow )$ rules are invertible, the sequent $E \rightarrow H$ is derivable in $\mathbf {L}^{\!+}_{\omega }$ iff for any positive natural numbers n, $m_1$, ..., $m_n$, $k_1$, ..., $k_n$ the sequent $B^{m_1}, C^{k_1}, \dots , B^{m_n}, C^{k_n} \rightarrow H$ is derivable in $\mathbf {L}^{\!+}_{\omega }$, and, since it doesn’t contain $^{+}$, by conservativity also in the Lambek calculus $\mathbf {L}$. By definition of Lambek grammar, this is equivalent to $b^{m_1} c^{k_1} \dots b^{m_n} c^{k_n} \in \mathcal {L}(\mathcal {G})$. Therefore, $E \rightarrow H$ is derivable iff the language generated by $\mathcal {G}$ includes all words of the form $b^{m_1} c^{k_1} \dots b^{m_n} c^{k_n}$, i.e., $\mathcal {G}\in \textsc {alt}_2$.

3 The Calculus with Infinite Derivation Branches

In this section we define $\mathbf {L}^{\!+}_{\infty }$, another infinitary calculus that extends $\mathbf {L}$ with positive iteration, in the spirit of sequent systems with non-well-founded derivations for other logics [2, 13, 24]. Compared to $\mathbf {L}^{\!+}_{\omega }$, $\mathbf {L}^{\!+}_{\infty }$ has a finite number of rules and each rule has a finite number of premises. The tradeoff is that now derivation trees are allowed to have infinite depth.

The Lambek part (rules for $\mathop {\backslash }$, $\mathop {/}$, and $\cdot$) is taken from $\mathbf {L}$. The rules for positive iteration are as follows:

As said before, we allow infinitely deep derivations. For the cut-free version, any trees with possibly infinite paths are allowed, but for the calculus with $(\mathrm {cut})$ one has to be extremely cautious. Clearly, allowing arbitrary infinite proofs would yield dead circles without actually using rules for $^+$:

Such “derivations” should be ruled out. There are, however, trickier cases like the following:

Here in the only infinite path we can see an infinite number of $({}^+\rightarrow )$ applications. However, the resulting sequent, $p^+ \rightarrow p$, is not valid under the formal language interpretation (e.g., $\{a\}^+ \not \subseteq \{a\}$) and therefore should not be derivable.

For the calculus with $(\mathrm {cut})$, we impose the following constraint on the infinite derivation tree: in each infinite path there should be an infinite number of applications of $({}^+\rightarrow )_{\mathrm {L}}$ with the same active occurrence of $A^+$ (the occurrence is tracked by individuality from bottom to top), cf. [2, Definition 5.5].

In our example that “derives” $p^+ \rightarrow p$, the occurrence of $p^+$ that is active in the lower application of $({}^+\rightarrow )_\mathrm {L}$ tracks to the left premise, and the $p^+$ that goes further to the infinite path is another occurrence generated by cut. For the cut-free system, this constraint holds automatically.

Also notice that the rules in $\mathbf {L}^{\!+}_{\infty }$ are asymmetric: we don’t introduce the rules where A appears to the right of $A^+$. Yet, this calculus is equivalent to the symmetric system $\mathbf {L}^{\!+}_{\omega }$ (Proposition 1). A motivation for this asymmetry is explained in the end of Sect. 4.

We generalize both $\mathbf {L}^{\!+}_{\infty }$ and $\mathbf {L}^{\!+}_{\omega }$ by adding the additive disjunction, $\vee$, governed by the following rules:

and denote the extensions by $\mathbf {L}^{\!+}_{\infty }(\vee )$ and $\mathbf {L}^{\!+}_{\omega }(\vee )$ respectively.

The cut-free calculi $\mathbf {L}^{\!+}_{\omega }(\vee )$ and $\mathbf {L}^{\!+}_{\infty }(\vee )$ (and, therefore, their conservative fragments $\mathbf {L}^{\!+}_{\omega }$ and $\mathbf {L}^{\!+}_{\infty }$) are equivalent.

Proposition 1

A sequent is derivable in $\mathbf {L}^{\!+}_{\omega }(\vee )$ iff it is derivable in $\mathbf {L}^{\!+}_{\infty }(\vee )$.

Proof

(sketch of). The “only if” part is trivial: the $\omega$-rule is derivable in $\mathbf {L}^{\!+}_{\infty }(\vee )$ and so are the $(\rightarrow {}^+)_n$ rules. All other rules are the same.

For the “if” part, we make use of the $*$-elimination result by Palka [14]. We consider the n-th negative mapping that replaces any negative occurrence of $A^+$ (polarity is defined as usual) by $A \vee A^2 \vee \ldots \vee A^n$ and show that if a sequent is derivable in $\mathbf {L}^{\!+}_{\infty }(\vee )$, than all its negative mappings are also derivable. In the negative mapping, however, there are no negative occurrences of $^+$, and therefore its cut-free derivation doesn’t have infinite branches. Moreover, we replace each $(\rightarrow {}^+)_\mathrm {L}$ rule application with the following subderivation:

The sequent $A, A^+ \rightarrow A^+$ is derivable in $\mathbf {L}^{\!+}_{\omega }(\vee )$, using the $\omega$-rule. Thus, the negative mapping of the original is derivable in $\mathbf {L}^{\!+}_{\omega }(\vee )$ using cut, and, by cut elimination, has a cut-free derivation. Then we go backwards and show, following the argument of Palka [14], that the original sequent is derivable in $\mathbf {L}^{\!+}_{\omega }(\vee )$.

4 The Cyclic Calculus

Now let’s consider the following example:

We see that actually we don’t have to develop the derivation tree further, since the sequent $p, (p \mathop {\backslash }p)^+ \rightarrow p$ on top already appears lower in the derivation, and now this tree can be built up to an infinite one in a regular way.

We define the notion of cyclic proof as done in [24, 25] (for GL, the Gödel – Löb logic) and call this system $\mathbf {L}^{\!+}_{\mathrm {circ}}$. In contrast to the situation with GL, however, here $\mathbf {L}^{\!+}_{\mathrm {circ}}$ is strictly weaker than $\mathbf {L}^{\!+}_{\omega }$ ($\mathbf {L}^{\!+}_{\infty }$) due to complexity reasons. Indeed, $\mathbf {L}^{\!+}_{\omega }$ is $\varPi _1^0$-hard, while in $\mathbf {L}^{\!+}_{\mathrm {circ}}$ derivations are finite and the derivability problem is recursively enumerable (belongs to $\varSigma _1^0$). This is true even in the signature without $\vee$.

For the extension of $\mathbf {L}^{\!+}_{\mathrm {circ}}$ with additive disjunction, we show that the cyclic system $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ is equivalent to the corresponding variant of action logic considered by Pratt [19], Kozen [10], and Jipsen [9]. The difference is due to Lambek’s non-emptiness restriction and the use of positive iteration instead of Kleene star.

Formally, cyclic derivations are defined as follows. The system $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ has the same axioms and rules as $\mathbf {L}^{\!+}_{\infty }(\vee )$, but infinite derivations are not allowed. Instead, for each application of the $({}^+\rightarrow )_{\mathrm {L}}$ rule that yields $\varGamma , A^+, \varDelta \rightarrow B$ we trace the active occurrence of $A^+$ upwards and are allowed to stop if we again get the same sequent, $\varGamma , A^+, \varDelta \rightarrow B$ with the same occurrence of $A^+$. This sequent is backlinked to the original one, forming a cycle. The cut rule is also allowed. Note that in the bottom of each cycle we always have the $({}^+\rightarrow )_{\mathrm {L}}$ rule with the active occurrence of $A^+$ which is traced through the cycle, thus satisfying the constraint needed for infinite derivations with cut. Clearly, every cyclic derivation can be expanded into an infinite one. On the other hand, the cyclic system $\mathbf {L}^{\!+}_{\mathrm {circ}}$ is not equivalent to $\mathbf {L}^{\!+}_{\infty }$ due to complexity reasons.

This system $\mathbf {L}^{\!+}_{\mathrm {circ}}$ appears to have much in common with various coinductive proof systems [1, 8, 11, 18, 20]. These connections are worth further investigation.

The cyclic system $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ happens to be equivalent to a non-sequential calculus $\mathbf {ACT}^+$ defined below, which is the positive iteration variant of the axioms for action algebras by Pratt [19]:

$$ A \rightarrow A \qquad (A \cdot B) \cdot C \rightarrow A \cdot (B \cdot C) \qquad A \cdot (B \cdot C) \rightarrow (A \cdot B) \cdot C $$

The rules for $\mathop {\backslash }$, $\mathop {/}$, and $\cdot$ correspond to the non-sequential formulation of the Lambek calculus [12].

Lemma 1

The following rule is admissible in $\mathbf {ACT}^+$:

This lemma is actually a modification of a well-known alternative formulation of the calculus for action logic (connecting it to Kleene algebra). The difference, again, is in using positive iteration instead of Kleene star.

Proof

The second premise yields $A \rightarrow C \mathop {\backslash }C$, and since $(C \mathop {\backslash }C) \cdot (C \mathop {\backslash }C) \rightarrow C \mathop {\backslash }C$ is derivable, we get $A \vee ((C \mathop {\backslash }C) \cdot (C \mathop {\backslash }C)) \rightarrow C \mathop {\backslash }C$, and therefore $A^+ \rightarrow C \mathop {\backslash }C$ and then $C \rightarrow C{\mathop {/}}A^+$. By transitivity with $A \rightarrow C$ this yields $A \rightarrow C{\mathop {/}}A^+$, and therefore $A \cdot A^+ \rightarrow C$. Combining this with $A \rightarrow C$, we get $A \vee (A \cdot A^+) \rightarrow C$, and it is sufficient to show $A^+ \rightarrow A \vee (A \cdot A^+)$. Denote $A \vee (A \cdot A^+)$ by B. We have $A \rightarrow B$ and also $B \cdot B \rightarrow B$. Indeed, using distributivity conditions: $(E \vee F) \cdot G \leftrightarrow (E \cdot G) \vee (E \cdot G)$ and $G \cdot (E \vee F) \leftrightarrow (G \cdot E) \vee (G \cdot F)$, that are derivable in $\mathbf {ACT}^+$, we replace $B \cdot B$ with $(A \cdot A) \vee (A \cdot A \cdot A^+) \vee (A \cdot A^+ \cdot A) \vee (A \cdot A^+ \cdot A \cdot A^+)$, and applying the axiom for ${}^+$ and monotonicity, we see that all four disjuncts here yield $A \cdot A^+$, and therefore B. Hence, by the rule for ${}^+$, we obtain $A^+ \rightarrow B$.

Lemma 2

The following rule is admissible in $\mathbf {ACT}^+$:

Lemma 2 is essential for emulating cyclic reasoning in the non-sequential calculus $\mathbf {ACT}^+$. The k parameter corresponds to the number of $({}^+\rightarrow )_\mathrm {L}$ applications in the cycle.

Proof

First we prove that

$$A^+ \rightarrow A \vee A^2 \vee \ldots \vee A^k \vee (A^k)^+ \vee (A^k)^+ \cdot A \vee \ldots \vee (A^k)^+ \cdot A^{k-1}$$

is derivable in this calculus. We denote the right-hand side of this formula by B and show $A \rightarrow B$ and $B \cdot A \rightarrow B$ (this yields $A^+ \rightarrow B$ by Lemma 1). The first is trivial. For the second, using distributivity conditions, we replace $B \cdot A$ with

$$A^2 \vee A^3 \vee \ldots \vee A^k \vee A^{k+1} \vee (A^k)^+ \cdot A \vee (A^k)^+ \cdot A^2 \vee \ldots \vee (A^k)^+ \cdot A^k \vee (A^k)^+ \cdot A^{k+1}.$$

All types in this long disjunction, except $A^{k+1}$ and $(A^k)^+ \cdot A^{k+1}$, belong to the disjunction B (and therefore yield B). For the two exceptions we have the following: $A^{k+1} \rightarrow (A^k)^+ \cdot A$ and $(A^k)^+ \cdot A^{k+1} \rightarrow (A^k)^+ \cdot A$.

Now we prove the lemma itself by deriving $B \rightarrow C$. To do this, we need to show $H \rightarrow C$ for any disjunct H in B. For $H = A$, ..., $H = A^k$ this is stated in the premises. Since that $(C{\mathop {/}}C) \cdot (C{\mathop {/}}C) \rightarrow C{\mathop {/}}C$ is derivable and $A^k \rightarrow C{\mathop {/}}C$ follows from the last premise, we get $A^k \vee ((C{\mathop {/}}C) \cdot (C{\mathop {/}}C)) \rightarrow (C{\mathop {/}}C)$, and therefore $(A^k)^+ \rightarrow C{\mathop {/}}C$. Thus, $(A^k)^+ \cdot C \rightarrow C$, then $C \rightarrow (A^k)^+ \mathop {\backslash }C$, and by transitivity with $A^i \rightarrow C$ we get $(A^k)^+ \cdot A^i \rightarrow C$ for any $i = 1, \dots , k-1$. It remains to show $(A^k)^+ \rightarrow C$. We have $(A^k)^+ \cdot A^k \rightarrow C$ and also $A^k \rightarrow C$ as a premise. One can easily prove $(A^k)^+ \rightarrow A^k \vee ((A^k)^+ \cdot A^k)$ and thus establish $(A^k)^+ \rightarrow C$.

Finally, by transitivity from $A^+ \rightarrow B$ and $B \rightarrow C$ we obtain $A^+ \rightarrow C$.

Theorem 3

A sequent (of the form $E \rightarrow F$) is derivable in $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ iff it is derivable in $\mathbf {ACT}^+$.

Proof

The “if” part is easier. The rules operating Lambek connectives ($\cdot$, $\mathop {/}$, and $\mathop {\backslash }$) can be emulated in the sequential calculus due to Lambek [12]. The rules for $\vee$ in $\mathbf {ACT}^+$ directly correspond to the rules for $\vee$ in $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$.

The following cyclic derivation yields $A^+ \rightarrow B$ from $A \rightarrow B$ and $B, B \rightarrow B$, thus establishing the rule for $^+$ from $\mathbf {ACT}^+$:

The track of $A^+$ goes through the cycle, and the $({}^+\rightarrow )_\mathrm {L}$ rule is applied to it at every round.

Finally, for $A^+ \cdot A^+ \rightarrow A^+$, we first derive $A \cdot A^+ \rightarrow A^+$ (using $(\rightarrow ^+)_{\mathrm {L}}$ and $(\cdot \rightarrow )$), and then, following Pratt [19], transform it into $A^+ \cdot A^+ \rightarrow A^+$:

In this derivation we’ve used other rules of $\mathbf {ACT}^+$, which were previously shown to be valid in $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$. Together with $A \rightarrow A^+$ (derivable using $(\rightarrow {}^+)_1$), this yields the last axiom of $\mathbf {ACT}^+$, $A \vee (A^+ \cdot A^+) \rightarrow A^+$.

For “only if” part, we first replace all cycles in the $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ derivation by applications of the rule from Lemma 2. We proceed by induction on the number of cycles. For the induction step, let the derivation end with an application of $(^{}+\rightarrow )_\mathrm {L}$, involved in a cycle. Let k be the number of applications of $({}^+\rightarrow )_{\mathrm {L}}$ to the active occurrence of $A^+$ that is tracked along this cycle. Let the goal sequent be $\varGamma , A^+, \varDelta \rightarrow B$; the same sequent appears on top of the cycle:

Let $C = \varGamma \mathop {\backslash }B{\mathop {/}}\varDelta$ (if $\varGamma$ or $\varDelta$ contains more than one formula, we add $\cdot$’s between them; if $\varGamma$ or $\varDelta$ is empty, we omit the corresponding division). The sequent $\varGamma , C, \varDelta \rightarrow B$ is derivable in the Lambek calculus. Then we go down the cycle path, replacing the active $A^+$ with $A^i, C$. We start with $i = 0$ and increase i each time we come across $({}^+\rightarrow )_{\mathrm {L}}$ applied to the active $A^+$. After this substitution, this application becomes trivial: instead of

we get

and actually forget about the left premise of the rule. All other rules remain valid. In the end, this gives us $\varGamma , A^k, C, \varDelta \rightarrow B$, or $A^k \cdot C \rightarrow C$. Moreover, the derivation of this sequent was obtained by substitution and cutting some branches from the original derivation, and therefore contains less cycles. By induction, we can suppose that $A^k \cdot C \rightarrow C$ was derived without cycles, using the rule from Lemma 2.

Next, for an arbitrary j from 1 to k, we go upwards along the trace of the active $A^+$ and find the j-th application of $({}^+\rightarrow )_{\mathrm {L}}$:

Now we cut off the right (cyclic) derivation branch and replace $A^+$ in the goal with A. Next, we trace it down back to the original sequent, replacing $A^+$ with $A^i$. The index i starts from 1 and gets increased each time we pass through the $({}^+\rightarrow )_{\mathrm {L}}$ rule with the active $A^+$. Again, these applications trivialize, all other rules remain valid. In the end, we get $\varGamma , A^j, \varDelta \rightarrow B$ derivable with a less number of cycles. This yields $A^j \rightarrow C$.

Finally, having $A \rightarrow C$, $A^2 \rightarrow C$, ..., $A^k \rightarrow C$, and $A^k \cdot C \rightarrow C$, we apply Lemma 2 and obtain $A^+ \rightarrow C$. Using cut, we invert $(\cdot \rightarrow )$, $(\rightarrow \mathop {/})$, and $(\rightarrow \mathop {\backslash })$, decompose C and arrive at the original goal sequent $\varGamma , A^+, \varDelta \rightarrow B$.

This finishes the non-trivial part of the proof: now we have a normal, non-cyclic derivation, and it remains to show that other rules of $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ used in it are admissible in $\mathbf {ACT}^+$. (Formally speaking, the languages of $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ and $\mathbf {ACT}^+$ are different. In $\mathbf {ACT}^+$, instead of sequents of the form $A_1, \dots , A_n \rightarrow B$, we consider $A_1 \cdot \ldots \cdot A_n \rightarrow B$.)

The rules for Lambek connectives ($\mathop {\backslash }$, $\mathop {/}$, and $\cdot$), and also the cut rule, are admissible in $\mathbf {ACT}^+$ due to Lambek [12]. The rules for $\vee$ correspond directly. Finally, the $(\rightarrow {}^+)_1$ and $(\rightarrow {}^+)_{\mathrm {L}}$ are validated as follows (here we use previously validated Lambek rules):

Note that, despite the fact that the calculus for $\mathbf {ACT}^+$ is symmetric, the asymmetry in the rules of $\mathbf {L}^{\!+}_{\mathrm {circ}}(\vee )$ is essential for our reasoning, because if we allow both left and right rules for ${}^+$, the rule from Lemma 2, that is used to emulate cyclic derivation, would transform into

and for this rule we don’t know whether it is admissible in $\mathbf {ACT}^+$.

5 Further Work and Open Questions

In this section we summarize the questions that are still (to the author’s best knowledge) unsolved.

• 1. Though we don’t claim cut elimination for $\mathbf {L}^{\!+}_{\infty }$ in this paper, it looks plausible that it could be proven using continuous cut elimination (cf. [13, 23]). For $\mathbf {L}^{\!+}_{\mathrm {circ}}$, however, the problem looks harder, since if one unravels the cyclic derivation into an infinite one and eliminates cut, the resulting derivation could be not cyclic anymore.

• 2. In this paper we use complexity arguments to show that $\mathbf {L}^{\!+}_{\omega }$ is strictly more powerful than any its subsystem with finite derivations. This doesn’t yield any examples of concrete sequents derivable in $\mathbf {L}^{\!+}_{\omega }$ and not derivable, say, in $\mathbf {L}^{\!+}_{\mathrm {circ}}$. Constructing such examples is yet an open problem.

• 3. We don’t know whether the rule in the end of Sect. 4 is admissible if $\mathbf {ACT}^+$. If yes, we could allow both left and right rules for ${}^+$ is cyclic derivations, and this system would be still equivalent to $\mathbf {ACT}^+$.

• 4. Safiullin’s construction (see Appendix) essentially uses Lambek’s non-emptiness restriction. The question whether any context-free language can be generated by a categorial grammar with unique type assignment, based on the variant of the Lambek calculus allowing empty left-hand sides of sequents, is still open. From our perspective, a positive answer to this question (maybe, by modification of Safiullin’s construction) would immediately yield $\varPi _1^0$-hardness of the Lambek calculus allowing empty left-hand sides of sequents, enriched with Kleene star (but without additive conjunction and disjunction), thus solving a problem posed by Buszkowski [4].

• 5. An open (and, in the view of the sophisticatedness of Pentus’ completeness proof [17], very hard) question is the completeness of $\mathbf {L}^{\!+}_{\omega }$ w.r.t. language interpretation (see Sect. 1). A partial completeness result, for the fragment where $^+$ is allowed only in the denominators of $\mathop {\backslash }$ and $\mathop {/}$, was obtained by Ryzhkova [21], using Buszkowski’s canonical model construction [3].

Appendix: Safiullin’s Construction Revisited

Theorem 1 by Safiullin is a crucial component of our $\varPi _1^0$-hardness proof for $\mathbf {L}^{\!+}_{\omega }$. Unfortunately, Safiullin’s paper [22] is very brief and, moreover, includes this theorem (which is probably the most interesting result of that paper) as a side-effect of a more complicated construction. This makes it very hard to follow Safiullin’s ideas and arrive at a complete proof. Therefore, in this Appendix we present Safiullin’s proof clearly and in detail.

In this Appendix, the ${}^+$ connective is never used, and $\mathrm {Tp}$ stands for the set of types constructed from primitive ones using $\cdot$, $\mathop {\backslash }$, and $\mathop {/}$.

Define the top of a Lambek type in the following way: ${\mathrm {top}(q) = q \text { for } q \in \mathrm {Pr}}$; ${\mathrm {top}(A \mathop {\backslash }B)= \mathrm {top}(B{\mathop {/}}A) = \mathrm {top}(B).}$ Note that the $A \cdot B$ case is missing. Thus, not every type has a top.

For types with tops, the $(\rightarrow \cdot )$ rule is invertible (proof by induction):

Lemma 3

If all types of $\varPi$ have tops and $\varPi \rightarrow A_1 \cdot \ldots \cdot A_n$ is derivable in $\mathbf {L}$, then $\varPi = \varPi _1, \dots , \varPi _n$ and $\varPi _i \rightarrow A_i$ is derivable for every $i = 1, \ldots , n$.

If a sequent of the form $\varPi \rightarrow q$, $q \in \mathrm {Pr}$, has a cut-free derivation in $\mathbf {L}$, trace the occurrence of q back to the axiom of the form $q \rightarrow q$, and then trace the left q back to its occurrence in $\varPi$. This occurrence of q will be called the principal occurrence (for different derivations, the principal occurrences could differ).

Lemma 4

The principal occurrence has the following properties:

• 1. if all types in $\varPi$ have tops, then the principal occurrence is one of them;

• 2. if in a derivation of $\varPi , q, \varPhi \rightarrow q$ the occurrence of q between $\varPi$ and $\varPhi$ is principal, then $\varPi$ and $\varPhi$ are empty;

• 3. if in a derivation of $\varPi , q{\mathop {/}}A, \varPhi \rightarrow q$ the occurrence of q in $q{\mathop {/}}A$ is principal, then $\varPi$ is empty;

• 4. if in a derivation of $\varPi , A \mathop {\backslash }q, \varPhi \rightarrow q$ the occurrence of q in $A \mathop {\backslash }q$ is principal, then $\varPhi$ is empty.

Proof

For statement 1, proceed by induction on derivation. For statements 2–4, suppose the contrary and also proceed by induction on derivation.

Lemma 5

If all types of $\varPi$ have tops, and these tops are not q, then $\varPi \rightarrow q{\mathop {/}}q$ is not derivable in $\mathbf {L}$.

Proof

Since $(\rightarrow \mathop {/})$ is invertible, we get $\varPi , q \rightarrow q$, and by Lemma 4 $\varPi$ should be empty. But $\rightarrow q{\mathop {/}}q$ is not derivable due to Lambek’s restriction.

Lemma 6

If in a derivation of $q{\mathop {/}}A, \varPhi \rightarrow q$ the leftmost occurrence of q is principal or in a derivation of $\varPhi , A \mathop {\backslash }q \rightarrow q$ the rightmost occurrence of q is principal, then $\varPhi \rightarrow A$ is derivable.

Proof

Induction on the derivation.

Lemma 7

If $\varPi , q{\mathop {/}}q, \varPhi \rightarrow q{\mathop {/}}q$ is derivable in $\mathbf {L}$, all types from $\varPi$ and $\varPhi$ have tops, and these tops are not q, then $\varPi$ and $\varPhi$ are empty.

Proof

Again, by inverting $(\rightarrow \mathop {/})$ we get $\varPi , q{\mathop {/}}q, \varPhi , q \rightarrow q$. The rightmost q cannot be principal, because otherwise $\varPi , q{\mathop {/}}q, \varPhi$ is empty (Lemma 4). The second possibility is the top of $q{\mathop {/}}q$. Then, again by Lemma 4, $\varPi$ is empty, and by Lemma 6 $\varPhi , q \rightarrow q$ is derivable. Since tops of $\varPhi$ are not q, the rightmost occurrence of q is principal. By Lemma 4, $\varPhi$ is empty.

By $\mathbb {F}$ we denote the free group generated by the set of primitive types $\mathrm {Pr}$. For every $A \in \mathrm {Tp}$ we define its interpretation in this free group, $[\![A]\!]$, as follows: $[\![q]\!] = q \text { for } q \in \mathrm {Pr}$; $[\![A \cdot B]\!] = [\![A]\!] [\![B]\!]$; $[\![A \mathop {\backslash }B]\!] = [\![A]\!]^{-1} [\![B]\!]$; $[\![B{\mathop {/}}A]\!] = [\![B]\!] [\![A]\!]^{-1}$. If $[\![A]\!]$ is the unit of $\mathbb {F}$, A is called a zero-balance type.

The primitive type count, $\#_q(A)$, for $q \in \mathrm {Pr}$ and $A \in \mathrm {Tp}$, is defined as follows: $\#_q(q) = 1$; $\#_q(q') = 0$, if $q' \in \mathrm {Pr}$ and $q' \ne q$; $\#_q(A \cdot B) = \#_q(A) + \#_q(B)$; $\#_q(A \mathop {\backslash }B) = \#_q(B{\mathop {/}}A) = \#_q(B) - \#_q(A)$. Notice that if A is a zero-balance type, then $\#_q(A) = 0$ for every $q \in \mathrm {Pr}$.

If the sequent $A_1, \dots , A_n \rightarrow B$ is derivable in $\mathbf {L}$, then it is balanced, namely, $\#_q(B) = \#_q(A_1) + \ldots + \#_q(A_n)$ for every $q \in \mathrm {Pr}$, and $[\![A_1]\!] \ldots [\![A_n]\!] = [\![B]\!]$.

Theorem 4

(M. Pentus, 1994). If $[\![A_1]\!] = [\![A_2]\!] = \ldots = [\![A_n]\!]$, then there exists such $B \in \mathrm {Tp}$, that all sequents $A_1 \rightarrow B$, $A_2 \rightarrow B$, ..., $A_n \rightarrow B$ are derivable in $\mathbf {L}$ [16].

For a set of zero-balance types $\mathcal {U}= \{ A_1, \dots , A_n \}$, we construct an ersatz of their additive disjunction, $A_1 \vee \ldots \vee A_n$, in the following way. In the notations for types, we sometimes omit the multiplication sign, $\cdot$, if this doesn’t lead to misunderstanding. Let u, t, and s be fresh primitive types, not occurring in $A_i$. By Theorem 4, there exist such types F and G that the following sequents are derivable for all $i = 1, \ldots , n$:

$$ (t{\mathop {/}}t) A_i (t{\mathop {/}}t) \ldots (t{\mathop {/}}t) A_n (t{\mathop {/}}t) \rightarrow F, \qquad (t{\mathop {/}}t) A_1 (t{\mathop {/}}t) \ldots (t{\mathop {/}}t) A_i (t{\mathop {/}}t) \rightarrow G. $$

Now let

$$ E = (t{\mathop {/}}t) A_1 (t{\mathop {/}}t) A_2 (t{\mathop {/}}t) \ldots (t{\mathop {/}}t) A_n (t{\mathop {/}}t), $$

$$ B = E\, (((u{\mathop {/}}F) \mathop {\backslash }u) \mathop {\backslash }(t{\mathop {/}}t)), \qquad C = ((t{\mathop {/}}t) \mathop {/}(u{\mathop {/}}(G \mathop {\backslash }u))) \, E. $$

We omit the multiplication sign, $\cdot$, if this doesn’t lead to misunderstanding.

Finally, $\mathrm {is}(\mathcal {U}) = ((s{\mathop {/}}E) \cdot B) \mathop {\backslash }s{\mathop {/}}C.$

Lemma 8

For each $A_i \in \mathcal {U}$, the sequent $A_i \rightarrow \mathrm {is}(\mathcal {U})$ is derivable in $\mathbf {L}$.

Proof

The derivation is straightforward.

Lemma 9

If the sequent $\varPi \rightarrow \mathrm {is}(\mathcal {U})$ is derivable in $\mathbf {L}$, all types in $\varPi$ have tops, and these tops are not s or t, then for some $A_j \in \mathcal {U}$ the sequent $B_2, \varPi , C_1 \rightarrow A_j$, where $B_2$ is either empty or is a type such that $B = B_2$ or $B = B_1 \cdot B_2$ for some $B_1$, and $C_1$ is either empty or is a type such that $C = C_1$ or $C = C_1 \cdot C_2$ for some $C_2$ (up to associativity of $\cdot$).

Using the invertibility of $(\cdot \rightarrow )$, we replace $\cdot$’s in $B_2$ and $C_1$ by commas, and thus consider them as sequences of types that have tops. Actually, we want them to be empty, and it will be so in our final construction.

Proof

Let $\varPi \rightarrow \mathrm {is}(\mathcal {U})$ be derivable. Then one can derive $(s{\mathop {/}}E), B, \varPi , C \rightarrow s$, and then by Lemma 6 we get $B, \varPi , C \rightarrow E$ (since the leftmost s is the only top s, and it is the principal occurrence). Recall that $E = (t{\mathop {/}}t) A_1 \dots (t{\mathop {/}}t) A_n (t{\mathop {/}}t)$ and apply Lemma 3. It is sufficient so show that, after decompositon, the whole $\varPi$ comes to one part of the left-hand side of the sequent. Suppose the contrary, then locate the principal occurrence of t (it should be in B). Then proceed by induction: finally we run out of t’s in B and get a contradiction.

Proof

(of Theorem 1 ). Given a context-free grammar $\mathcal {G}$ without $\varepsilon$-rules, we need to construct an equivalent Lambek grammar with unique type assignment. Let $\varSigma = \{ a_1, \dots , a_\mu \}$ be the alphabet, $\mathcal {N}= \{ N_0, N_1, N_2, \dots , N_\nu \}$ be the set of non-terminal symbols of $\mathcal {G}$, $N_0$ is the starting symbol.

First we algorithmically transform $\mathcal {G}$ into Greibach normal form [6] with rules of the following three forms: $N_i \Rightarrow a_j N_k N_\ell$, $N_i \Rightarrow a_j N_k$, or $N_i \Rightarrow a_j$.

Now we construct the Lambek grammar. Let $\mathrm {Pr}$ include distinct primitive types p, $p_1, \dots , p_\nu$, r, u, t, and s. For each $i = 0, \dots , \nu$ let $H_i = p{\mathop {/}}((p_i{\mathop {/}}p_i) \cdot p)$ (this type corresponds to the non-terminal $N_i$). Next, for each $j = 1, \dots , \mu$, we form a set $\mathcal {U}_j$ in the following way:

$$\begin{aligned} \text {add } K_{i,k,\ell } = r{\mathop {/}}\bigl ( ( H_k \cdot H_\ell \cdot (p_i{\mathop {/}}p_i)) \mathop {\backslash }r \bigr )&\text { for each rule } N_i \Rightarrow a_j N_k N_\ell ,\\ \text {add } K_{i,k} = r{\mathop {/}}\bigl ( ( H_k \cdot (p_i{\mathop {/}}p_i)) \mathop {\backslash }r \bigr )&\text { for each rule } N_i \Rightarrow a_j N_k,\\ \text {add } K_i = r{\mathop {/}}\bigl ( (p_i{\mathop {/}}p_i) \mathop {\backslash }r \bigr )&\text { for each rule } N_i \Rightarrow a_j. \end{aligned}$$

Now let $D_j = \mathrm {is}(\mathcal {U}_j)$ and $A_j = p{\mathop {/}}(D_j \cdot p)$ be the type corresponding to $a_j$. For the target type H we take $H_0$. Our claim is that $a_{i_1} \dots a_{i_n} \in \mathcal {L}(\mathcal {G})$ iff the sequent $A_{i_1}, \dots , A_{i_n} \rightarrow H_0$ is derivable in $\mathbf {L}$.

For the easier “only if” part, we prove a more general statement: if $\gamma \in (\mathcal {N}\cup \varSigma )^+$ can be generated from $N_m$ in $\mathcal {G}$, then the sequent $\varGamma \rightarrow H_m$ is derivable in $\mathbf {L}$, where $\varGamma$ is a sequence of types corresponding to letters of $\gamma$, $A_j$ for $a_j \in \varSigma$ and $H_i$ for $N_i \in \mathcal {N}$. To establish this, it is sufficient to prove that the following sequents are derivable (each step of the context-free generation maps to a $(\mathrm {cut})$ with the corresponding sequent):

$$\begin{aligned} A_j, H_k, H_\ell \rightarrow H_i&\text { for each rule } N_i \Rightarrow a_j N_k N_\ell ,\\ A_j, H_k \rightarrow H_i&\text { for each rule } N_i \Rightarrow a_j N_k,\\ A_j \rightarrow H_i&\text { for each rule } N_i \Rightarrow a_j. \end{aligned}$$

Consider sequents of the first type (the second and the third types are handled similarly). Since $D_j = \mathrm {is}(\mathcal {U}_j)$ and $K_{i,k,\ell } = r{\mathop {/}}\bigl ( ( H_k \cdot H_\ell \cdot (p_i{\mathop {/}}p_i)) \mathop {\backslash }r \bigr ) \in \mathcal {U}_j$, we have $K_{i,k,\ell } \rightarrow D_j$ by Lemma 8. Then the derivation is as follows:

For the “if” part, let $A_{i_1}, \dots , A_{i_n} \rightarrow H_i$ be derivable and proceed by induction on the cut-free derivation (i is arbitrary here for induction; in the end $i = 0$). Since $H_i = p{\mathop {/}}((p_i{\mathop {/}}p_i) \cdot p)$ and $(\rightarrow \mathop {/})$ and $(\cdot \rightarrow )$ are invertible, we get $A_{i_1}, \dots , A_{i_n}, p_i{\mathop {/}}p_i, p \rightarrow p$. Locate the principal occurrence of p. By Lemma 4, it is the p in $A_{i_1} = p{\mathop {/}}(D_{i_1} \cdot p)$, and by Lemma 6 the sequent $A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i, p \rightarrow D_{i_1} \cdot p$ is derivable. Let $j = i_1$. Since all our types have tops, apply Lemma 3.

Case 1 (good). The sequent decomposes into $A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i \rightarrow D_j$ and $p \rightarrow p$. Consider the former sequent. Tops on the left side are p and $p_i$, we can apply Lemma 9 and get $B_2, A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i, C_1 \rightarrow K$ for some $K \in \mathcal {U}_j$.

Let’s prove that $B_2$ and $C_1$ in this case are empty. Suppose $K = K_{i',k,\ell }$ (the cases of $K_{i',k}$ and $K_{i'}$ are handled similarly). Then, by invertibility of $(\rightarrow \mathop {/})$, we get $B_2, A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i, C_1, (H_k \cdot H_\ell \cdot (p_{i'}{\mathop {/}}p_{i'})) \mathop {\backslash }r \rightarrow r$. Now locate the principal occurrence of r.

Subcase 1.1. The principal occurrence of r is the rightmost one. By Lemma 6, we get $B_2, A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i, C_1 \rightarrow H_k \cdot H_\ell \cdot (p_{i'}{\mathop {/}}p_{i'})$. Apply Lemma 3. First, by Lemma 5, $i = i'$, otherwise there’s no $p_i$ in tops of the left-hand side. Next, the part of the left-hand side that yields $(p_i{\mathop {/}}p_i)$, by Lemma 7, contains only $(p_i{\mathop {/}}p_i)$. Therefore, $C_1$ is empty. Now, for some part $\varPi$ we have $\varPi \rightarrow H_k$, and, decomposing $H_k$, we get $\varPi , p_i{\mathop {/}}p_i, p \rightarrow p$. By Lemma 4, the principal occurrence of p is not the rightmost one. Since $B_2$ doesn’t have p in tops, $\varPi$ should include also some of the $A_{i_2}, \dots$, and the principal p is the top of one of them. But, since $A_m$ is of the form $p{\mathop {/}}\dots$, by Lemma 4 the part to the left of this $A_m$, and, therefore, $B_2$ should be empty.

Subcase 1.2. The principal occurrence of r is somewhere in $B_2$ or $C_1$, in a type $K \in \mathcal {U}_j$. By Lemma 4, it is then the leftmost occurrence of r, because K has the form $r\mathop {/}\ldots$. This rules out the possibility of it being in $C_1$ (we definitely have $p_i{\mathop {/}}p_i$ to the left of it). If it is in $B_2$, again by Lemma 6, we get $B'_2, A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i, C_1 \rightarrow H_{k'} \cdot H_{\ell '} \cdot (p_i{\mathop {/}}p_i)$ ($H_{k'}$ and $H_{\ell '}$ are optional), and we’re in the same situation, as Subcase 1.1. Thus, $B'_2$ and $C_1$ should be empty. However, $B'_2$ now should contain the last type of B, $(((u{\mathop {/}}F)\mathop {\backslash }u){\mathop {/}}(t \mathop {/}t))$. Contradiction. Subcase 1.2 impossible.

Now we have $A_{i_2}, \dots , A_{i_n}, p_i{\mathop {/}}p_i \rightarrow H_k \cdot H_\ell \cdot (p_i{\mathop {/}}p_i)$ (the only choice for the principal r now is the rightmost one, and we’ve applied Lemma 6). By Lemma 3, we get $A_{i_2}, \dots , A_{i_z} \rightarrow H_k$, $A_{i_{z+1}}, \dots , A_{i_n} \rightarrow H_\ell$, $p_i{\mathop {/}}p_i \rightarrow p_i{\mathop {/}}p_i$ (the last left side is $p_i{\mathop {/}}p_i$ alone by Lemma 7).

Apply induction hypothesis. In the context-free grammar, we now have $N_k \Rightarrow ^* a_{i_2} \dots a_{i_z}$ and $N_\ell \Rightarrow ^* a_{i_{z+1}} \dots a_{i_n}$. Since $i' = i$, we also have the rule $N_i \Rightarrow a_j N_k N_\ell$ ($N_k$ and $N_\ell$ are optional) in the grammar (since the corresponding K type was in $\mathcal {U}_j$). Thus, $N_i \Rightarrow a_j a_{i_2} \dots a_{i_z} a_{i_{z+1}} \dots a_{i_n}$. Recall that $j = i_1$.

Case 2 (bad). The sequent decomposes in another way, yielding $A_{i_2}, \dots , A_{i_z} \rightarrow D_j$ and $\dots , p_i{\mathop {/}}p_i, p \rightarrow p$. Again, by Lemma 9, we get $B_2, A_{i_2}, \dots , A_{i_z}, C_1 \rightarrow K$ for some $K \in \mathcal {U}_j$, and further $B_2, A_{i_2}, \dots , A_{i_z}, C_1, (H_k \cdot H_\ell \cdot (p_{i'}{\mathop {/}}p_{i'})) \mathop {\backslash }r \rightarrow r$. Now we locate the principal occurrence of r and proceed as in Case 1. The only difference, however, is that now there is no $p_i{\mathop {/}}p_i$ in the left-hand side, and for that reason derivation fails by Lemma 5. Thus, Case 2 is impossible.