Lambek Calculus: Recognizing Power and Complexity

Makoto Kanazawa

Abstract

I survey known results and results that easily follow from known results about the recognizing power and complexity of various fragments of the Lambek calculus.

Contents

1 Complexity and recognizing power of logics 2 2 Lambek calculus 3 3 Multiplicative-exponential Lambek calculus 5 4 Multiplicative-additive Lambek calculus 8 5 Multiplicative Lambek calculus 12

1 Complexity and recognizing power of logics

We first have to explain what we mean by the complexity and the recognizing power of a logic. To most people, the former notion should be familiar, but the latter may sound novel.

We assume that a logic K is presented in the form of a sequent calculus, which is the favorite format for substructural logics. A sequent is an expression of the form

A_{1}, …, A_{m} − B_{1}, …, B_{n}

where m, n ≥ 0 and A_{1}, …, A_{m}, B_{1}, …, B_{n} are formulas.^{1} We denote the set of well-formed formulas of K by Form_{K} and the set of sequents of K by Seq_{K}.

Any logic K determines the set Prov_{K} of provable sequents. Members of Prov_{K} are expressions made up from a finite stock of symbols, so Prov_{K} is a language in the sense of formal language theory. The complexity of K is defined to be the complexity-theoretic characteristic of this language Prov_{K}. We can be said to have determined the complexity of K if we have succeeded in locating Prov_{K} precisely in the space of complexity classes as we know it today. Thus, if we know that Prov_{K} is, say, PSPACE-complete, we know the complexity of K, in which case we also say that K is PSPACE-complete.

The complexity of a logic K is the property of a single language associated with K. In contrast, the recognizing power of K has to do with a class of languages. Given a fixed alphabet Σ, K is said to recognize a language L ⊆ Σ^{+} if there exist some finite subset A of Form_{K}, some B ∈ Form_{K}, and some relation R ⊆ Σ × A such that

L = { w ∈ Σ^{+} | ∃Γ(w R̃ Γ ∧ Γ − B ∈ Prov_{K}) },

where R̃ ⊆ Σ∗ × Form∗_{K} is the extension of R to a relation between strings of symbols and strings of formulas:

w R̃ Γ ⇔ w = Γ = ϵ ∨

∃c ∈ Σ ∃v ∈ Σ∗ ∃A ∈ Form_{K} ∃Δ ∈ Form∗_{K}

(w = cv ∧ Γ = AΔ ∧ c R A ∧ v R̃ Δ).

Then Rec_{K} is defined to be the class of all languages (over Σ) recognized by K. Note that in this definition, the empty string is disregarded, so that languages recognized consist of non-empty strings. This is for the sake of simplifying some results. Henceforth, when we talk about recognizing power, we simply say ‘language’ to mean ‘language without the empty string’. We know the recognizing power of K when we can characterize Rec_{K} in terms of familiar notions from formal language theory, e.g., when we know that Rec_{K} is the class of all context-free languages (i.e., context-free languages that do not include the empty string).

1Sometimes one-sided sequents of the form

− A_{1}, …, A_{n} are used, but we use the more general two-sided format.

The notion of recognizing power has its origin in the Lambek calculus, where a pair ⟨R, B⟩ with R ⊆ Σ×A for some finite A is viewed as a grammar. Yet the notion applies to any logic presented in the form of a sequent calculus. When G = ⟨R, B⟩, where R and B are as above, we say that G is a K-grammar, and write L(G) for the language { w ∈ Σ^{+} | ∃Γ(w R̃ Γ ∧ Γ − B ∈ Prov_{K}) }.

There are some properties of Rec_{K} that do not depend on any specific choice of K. For instance, Rec_{K} is always closed under strictly alphabetic morphisms, homomorphisms that are length-preserving. Also, if K_{2} is a conservative extension of K_{1}, one has Rec_{K_{1}} ⊆ Rec_{K_{2}}.

Some connections between Prov_{K} and Rec_{K} are apparent. For instance, if Prov_{K} is recursive, then all languages in Rec_{K} are recursive, and likewise, if Prov_{K} is in NP, Rec_{K} is a subclass of NP. An additional interest of investigating Rec_{K} lies in the fact that it sometimes admits of a natural language-theoretic characterization which cannot be captured by a rough complexity-theoretic measure, and which sometimes provides valuable additional information about the logic in question.

2 Lambek calculus

We are interested in a family of logics related to the system first presented in Lambek 1958, 1961. In modern terms, they are systems of noncommutative intuitionistic propositional linear logic. In these systems, sequents are of the form

A_{1}, …, A_{m} − B

having exactly one succedent formula. Lambek also required that m ≥ 1, but we choose not to do so here. So the antecedent of a sequent can be empty. This choice is significant in just one place.

There are six propositional connectives: ⊗, {− \atop ∘}, ∘−, &, ⊕, and !. The systems we consider here differ only in which of these connectives are used. The connectives ⊗, {− \atop ∘}, and ∘− are called multiplicatives, and & and ⊕ are called additives. The connective ! is the exponential connective. This terminology is borrowed from linear logic. The multiplicatives of the Lambek calculus are usually written •, \, /, but here we use different notations to emphasize the connection with linear logic. Some people have used these notations from linear logic for the Lambek calculus.

As in other logics, axioms of the Lambek calculus are sequents of the form

A − A,

where A is any well-formed formula. Rules of inference associated with the different connectives are listed in Figure 1. Here as elsewhere, upper-case Greek letters stand for finite sequences of formulas and upper-case Roman letters stand for formulas. In (− !), !Γ stands for the result of prefixing ! to each formula in Γ.

{Γ, A, B, Δ − C \atop Γ, A ⊗ B, Δ − C} (⊗ −)  \begin{matrix}Γ − A & Δ − B \\ Γ, Δ − A ⊗ B \end{matrix} (− ⊗)
\begin{matrix}Γ − A & Δ, B, Π − C \\ Δ, Γ, A {− \atop ∘} B, Π − C \end{matrix} ({− \atop ∘} −)  {A, Γ − B \atop Γ − A {− \atop ∘} B} (− {− \atop ∘})
\begin{matrix}Γ − A & Δ, B, Π − C \\ Δ, B ∘− A, Γ, Π − C \end{matrix} (∘− −)  {Γ, A − B \atop Γ − B ∘− A} (− ∘−)
{Γ, A, Δ − C \atop Γ, A & B, Δ − C} (& −_{1})  \begin{matrix}Γ − A & Γ − B \\ Γ − A & B \end{matrix} (− &)
{Γ, B, Δ − C \atop Γ, A & B, Δ − C} (& −_{2})
\begin{matrix}Γ, A, Δ − C & Γ, B, Δ − C \\ Γ, A ⊕ B, Δ − C \end{matrix} (⊕ −)  {Γ − A \atop Γ − A ⊕ B} (− ⊕_{1})
{Γ − B \atop Γ − A ⊕ B} (− ⊕_{2})
{Γ, A, Δ − C \atop Γ,!A, Δ − C} (! −)  {!Γ − C \atop !Γ − !C} (− !)
{Γ, Δ − C \atop Γ,!A, Δ − C} !W  {Γ,!A, Δ,!A, Π − C \atop Γ,!A, Δ, Π − C} !C_{1}
{Γ,!A, Δ,!A, Π − C \atop Γ, Δ,!A, Π − C} !C_{2}

Figure 1: Rules of inference of the Lambek calculus.

The Lambek calculus has just one structural rule, namely Cut, which is eliminable.

\begin{matrix}Γ − A & Δ, A, Π − C \\ Δ, Γ, Π − C \end{matrix} Cut

Note that not only do formulas of the form !A in the antecedent of a sequent undergo weakening and contraction, but also they can be moved anywhere within the antecedent. The following rules are derivable using !W, !C_{1}, and !C_{2}:

{Γ,!A, Δ, Π − C \atop Γ, Δ,!A, Π − C} !E_{1} {Γ, Δ,!A, Π − C \atop Γ,!A, Δ, Π − C} !E_{2}

Formulas not of this restricted form do not undergo any of the usual structural rules, not even Exchange.

We will consider the multiplicative Lambek calculus (MLC), the calculus which has only the multiplicatives as its logical connectives; the multiplicativeadditive Lambek calculus (MALC), which has the mulitplicatives and the additives but not the exponential; and the multiplicative-exponential Lambek calculus (MELC), which has the mulitplicatives and the exponential. The full Lambek calculus with all the connectives mentioned so far has the same recognizing power and complexity as the multiplicative-exponential fragment. What is known about the recognizing power and complexity of the three calculi is summarized in Table 1. The complexity of MLC and the recognizing power of MALC have not been precisely characterized. In the following sections, we will review these results in turn, starting with MELC.

recognizing power  complexity
MLC = CFL ∈ NP
MALC ⊃ finite intersections of CFLs  PSPACE-complete
MELC  = r.e.  undecidable (r.e.-complete)

Table 1: Recognizing power and complexity of various fragments of the Lambek calculus.

3 Multiplicative-exponential Lambek calculus

Lincoln et al. (1992) show that MELC is undecidable by a reduction from semi-Thue systems. Their proof is given in the one-sided cyclic format for noncommutative linear logic, but the idea is even more transparent with the two-sided intuitionistic format adopted here. The proof provides an exact characterization of the complexity of MELC: it is complete for the r.e. sets (under computable many-one reductions). It also shows that MELC recognizes all r.e. languages.

The main idea is coding of MLC theories in MELC formulas. Since MLC provability in a theory, even for the fragment MLC(⊗) with ⊗ as the only connective, is quite easily shown to be undecidable, the coding can be used to show the undecidability of MELC (or MELC(⊗, {− \atop ∘},!)—{− \atop ∘} is necessary for the coding purpose).^{2}

A K theory is just a finite subset of Seq_{K}. If T is a K theory, a sequent of K is provable in K + T if there is a derivation of it which is just like a proof in K (possibly with applications of Cut) except that sequents in T may appear at some leaves.

The following lemma about MLC may be proved using standard cut elimination techniques.

Lemma 1. Let T be an MLC theory. If an MLC sequent t is provable in MLC + T, then there is a proof of t in MLC + T where every application of Cut involves an axiom in T as one of its premises.

For any theory T = {t_{1}, …, t_{l}}, its translation [T] is defined to be the sequence

![t_{1}], …,![t_{l}],

where for any sequent A_{1}, …, A_{n} − B, [A_{1}, …, A_{n} − B] is the formula

(A_{1} ⊗ ⋯ ⊗ A_{n}) {− \atop ∘} B.

2We sometimes denote a calculus with a restricted set of connectives by displaying the connectives, as we do here.

Lemma 2. Let T be an MLC theory, and let Π − D be an MLC sequent. Then the following are equivalent:

(i) Π − D is provable in MLC + T. (ii) [T], Π − D is provable in MELC.

Proof. (i) ⇒ (ii). By induction on the depth of proof, noting that if A_{1}, …, A_{n} − B ∈ T,

[T], A_{1}, …, A_{n} − B

is provable in MELC.

(ii) ⇒ (i). Remove all occurrences of formulas of the form !t from a proof of [T], Π − D. All applications of rules for the mulitplicatives remain applications of the same rule. Applications of !W, !C_{1}, and !C_{2} become repetitions of the same sequent, so just delete one of the two occurrences. Applications of (! −) change as follows:

⋮ ; Γ, [A_{1}, …, A_{n} − B], Δ − C ; Γ,![A_{1}, …, A_{n} − B], Δ − C ⇝ ⋮ ; Γ′, [A_{1}, …, A_{n} − B], Δ′ − C ; Γ′, Δ′ − C

Then we can change all such parts simultaneously as follows:

\begin{aligned}A_{1}, …, A_{n} − B ; ⋮ . ; − [A_{1}, …, A_{n} − B] & ⋮ ; Γ′, [A_{1}, …, A_{n} − B], Δ′ − C \\ & Γ′, Δ′ − C \end{aligned} Cut

making the resulting figure a proof of Π − D in MLC + T. ⊣

Note that in the above proof it is crucial to allow a sequent to have an empty antecedent.

We now describe a reduction from type 0 grammars of Chomsky to MELC(⊗, {− \atop ∘},!). A type 0 grammar G is a quadruple ⟨Σ, N, S, P ⟩, where Σ is a finite alphabet, N is a finite set of nonterminals disjoint from Σ, S is a designated member of N, and P is a finite set of rewriting rules of the form

α → β,

where α ∈ (Σ ∪ N)^{+} and β ∈ (Σ ∪ N)∗. The ‘rewrites’ relation ⇒∗_{G} associated with G is defined by the following axioms and rule:

α ⇒∗ α for α ∈ (Σ ∪ N)^{+}  α ⇒∗ β for α → β ∈ P  \begin{matrix}α ⇒∗ β & γ ⇒∗ δ α σ \\ γ ⇒∗ δ β σ \end{matrix}

α ⇒∗_{G} β is defined to hold if α ⇒∗ β is derivable using the above axioms and rule. This definition of ⇒∗_{G} is diffrent from, but equivalent to, the standard definition. The language generated by G, denoted L(G), is defined to be { w ∈

Σ∗ | S ⇒∗_{G} w }.

Given a type 0 grammar G = ⟨Σ, N, S, P ⟩, we define an MLC theory T_{G} as follows. Suppose Σ = {c_{1}, …, c_{m}} and let N = {D_{1}, …, D_{n}}. We put Σ ∪ N = {c_{1}, …, c_{m}} ∪ {D_{1}, …, D_{n}} into a one-one correspondence π with a set {p_{1}, …, p_{m+n}} of atomic formulas. For any expression of the form

X_{1} … X_{i} ⇒∗ Y_{1} … Y_{j},

where X_{1}, …, X_{i}, Y_{1}, …, Y_{j} ∈ Σ ∪ N and i ≥ 1, we associate the following sequent as its translation τ(X_{1} … X_{i} ⇒∗ Y_{1} … Y_{j}):

q_{1}, …, q_{j} − r_{1} ⊗ ⋯ ⊗ r_{i},

where q_{1}, …, q_{j} and r_{1}, …, r_{i} are atomic formulas that correspond to Y_{1}, …, Y_{j} and X_{1}, …, X_{i}, respectively, by π (note the flip-flop of the two sides). Let

T_{G} = { τ(α ⇒∗ β) | α → β ∈ P }.

We have the following:

Lemma 3. For any α ∈ (Σ ∪ N)^{+} and β ∈ (Σ ∪ N)∗, α ⇒∗_{G} β holds if and only if τ(α ⇒∗ β) is provable in MLC + T_{G}.

The proof is straightforward, given our definition of ⇒∗_{G}.

By Lemmas 2 and 3, we get

Lemma 4. Let G = ⟨Σ, N, S, P ⟩ be a type 0 grammar. For any w ∈ Σ∗, w ∈ L(G) if and only if

[T_{G}], Γ − q

is provable in MELC, where Γ − q = τ(S ⇒∗ w).

Since the question ‘w ∈ L(G)?’ is undecidable, we get

Theorem 5 (Lincoln et al.). Provability in MELC is undecidable.

In fact, since type 0 grammars generate all r.e. sets, it follows that the set Prov_{MELC} is complete for the r.e. sets.

Also, note that

[T_{G}], Γ − D

is provable if and only if

Γ − ⨂[T_{G}] {− \atop ∘} D

is, where ⨂(A_{1}, …, A_{n}) is A_{1} ⊗ ⋯ ⊗ A_{n}. Then Lemma 4 implies

Theorem 6. MELC recognizes all r.e. languages.

The present reduction uses only the connectives ⊗, {− \atop ∘}, and !, so the above results hold of MELC(⊗, {− \atop ∘},!). Kanovich (1993) shows that MELC({− \atop ∘}, ∘−,!) is undecidable by a reduction from a two-counter machine. In fact, Buszkowski (1982) has shown that provability in MLC({− \atop ∘}) theories is undecidable by a reduction from type 0 grammars. Since we can use A_{n} {− \atop ∘}(… {− \atop ∘}(A_{1} {− \atop ∘} B) …) in place of (A_{1} ⊗ ⋯ ⊗ A_{n}) {− \atop ∘} B in Lemma 2 and Theorem 6, it follows that MELC({− \atop ∘},!) already has the same complexity and recognizing power as the full (multiplicative-additive-exponential) Lambek calculus.

As noted above, it is crucial to allow sequents with empty antecedent to capture provability in MLC theories by provability in MELC. To the best of my knowledge, there is no published proof that the MELC with Lambek’s nonempty antecedent requirement has the same complexity and recognizing power as the MELC without the requirement.^{3}

4 Multiplicative-additive Lambek calculus

Lincoln et al. (1992) show that multiplicative-additive linear logic is PSPACEcomplete by reducing quantified Boolean formula satisfiability (QBF). Adapting their proof, we can show the same for multiplicative-additive Lambek calculus (MALC). (I arrived at this proof in ignorance of Kanovich 1994, where a similar proof is provided.) The key observation here is that satisfiability of closed quantified Boolean formulae whose quantifier-free matrix is in disjunctive normal form (DNF) is already PSPACE-complete. This enables us to do away with the Exchange rule which was necessary in Lincoln et al.’s encoding. Linear negation also turns out to be unnecessary.

Let {x_{1}, x_{2}, x_{3}, … } be the set of propositional variables. Without loss of generality, we can assume that a closed quantified Boolean formula is of the form

Q_{1}x_{1} … Q_{n}x_{n}(D_{1} ∨ ⋯ ∨ D_{m}),  (1)

where for each i, Q_{i} is either ∀ or ∃ and D_{i} is a conjunction of literals from {x_{1}, …, x_{n}, ¬x_{1}, …, ¬x_{n}} such that for every j, at most one of x_{j} and ¬x_{j} occurs in D_{i}. Satisfiability of such formulas is PSPACE-complete. This follows from the well-known fact that satisfiability of quantified Boolean formulae with conjunctive normal form (CNF) matrix is PSPACE-complete and the fact that PSPACE = co-PSPACE.

We first show how the quantifer-free matrix M = D_{1} ∨⋯∨D_{m} of (1) can be encoded in MALC. Corresponding to the literals in M, the MALC encoding uses atomic formulas x_{1}, x̄_{1}, …, x_{n}, x̄_{n}. Each disjunct is translated as follows:

[[D_{i}]] = y_{1} ⊗ ⋯ ⊗ y_{n},

3In personal communication (1996), Max Kanovich informed me that MELC with Lambek’s requirement is undecidable.

where

y_{j} = \begin{cases}x_{j} & if x_{j} occurs in D_{i}, \\ x̄_{j} & if ¬x_{j} occurs in D_{i}, \\ (x_{j} ⊕ x̄_{j}) & otherwise. \end{cases}

Note that in the translation of D_{i}, the propositional variables appear in the sorted order. Then the translation of the DNF matrix is given by

[[D_{1} ∨ ⋯ ∨ D_{m}]] = [[D_{1}]] ⊕ ⋯ ⊕ [[D_{m}]].

If I is an assignment of truth values to propositional variables x_{1}, …, x_{n}, then we let

[[I]] = y_{1}, …, y_{n}

where

y_{j} = \begin{cases}x_{j} & if I(x_{j}) = true, \\ x̄_{j} & if I(x_{j}) = false. \end{cases}

The following lemma is straightforward.

Lemma 7. Let M be a DNF formula in propositional variables x_{1}, …, x_{n}, and let I be an assignment of truth values to x_{1}, …, x_{n}. Then I ⊧ M if and only if [[I]] − [[M]] is provable in MALC.

To translate quantified formulas, we introduce new atomic formulas q_{0}, q_{1}, …, q_{n}. We translate each quantifier as follows:

[[∀x_{i}]] = q_{i−1} {− \atop ∘}((x_{i} ⊗ q_{i}) ⊕ (x̄_{i} ⊗ q_{i})),
[[∃x_{i}]] = q_{i−1} {− \atop ∘}((x_{i} ⊗ q_{i}) &(x̄_{i} ⊗ q_{i})).

This is the ‘lock-and-key’ method for simulating quantifier dependencies introduced by Lincoln et al. (1992).

Lemma 8. Let M be a DNF formula in propositional variables x_{1}, …, x_{n}, and let I be an assignment of truth values to x_{1}, …, x_{i} (0 ≤ i ≤ n). Then I ⊧ Q_{i+1}x_{i+1} … Q_{n}x_{n}M if and only if

[[I]], q_{i}, [[Q_{i+1}x_{i+1}]], …, [[Q_{n}x_{n}]] − [[M]] ⊗ q_{n}

is provable in MALC.

As a special case, we have

Corollary 9. Let M be a DNF formula in propositional variables x_{1}, …, x_{n}. Then ⊧ Q_{1}x_{1} … Q_{n}x_{n}M if and only if

q_{0}, [[Q_{1}x_{1}]], …, [[Q_{n}x_{n}]] − [[M]] ⊗ q_{n}

is provable in MALC.

This is a polynomial-time reduction from QBF satisfiability to provability in MALC. As in the case of mulitiplicative-additive linear logic, MALC is in PSPACE, so we have

Theorem 10. Provability in MALC is PSPACE-complete.

In contrast, the recognizing power of MALC has not been precisely characterized. There is a known lower bound, however, due to Kanazawa (1992).

Theorem 11. Rec_{MALC({− \atop ∘},&)} properly includes the class of finite intersections of context-free languages.

Theorem 11 is a consequence of the following lemma and Lemma 15 below.

Lemma 12. Rec_{MALC(...,&)} (with any selection of connectives including &) is closed under intersection.

Proof. We give a more streamlined proof than Kanazawa 1992. Let G_{1} = ⟨↦_{1}, D_{1}⟩ and G_{2} = ⟨↦_{2}, D_{2}⟩ be MALC(…, &)-grammars. Let P_{1} and P_{2} be the sets of atomic formulas used in G_{1} and G_{2}, respectively. Without loss of generality, we can assume that P_{1} ∩ P_{2} = ∅. Let G = ⟨↦, D_{1} & D_{2}⟩, where

↦ = { ⟨c, A & B⟩ | c ↦_{1} A, c ↦_{2} B }.

It suffices to prove L(G) = L(G_{1}) ∩ L(G_{2}). This follows from the following claim. Below, formulas built exclusively from atomic formulas in P_{i} are called P_{i}-formulas, for i = 1, 2.

Claim If A_{1}, …, A_{n} are P_{1}-formulas and B_{1}, …, B_{n} are P_{2}-formulas, then the following are equivalent:

(i) A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1} & D_{2} is provable in MALC. (ii) A_{1}, …, A_{n} − D_{1} and B_{1}, …, B_{n} − D_{2} are both provable in MALC.

Proof of the claim. (ii) ⇒ (i). This direction is easy:

\begin{matrix}{A_{1}, …, A_{n} − D_{1} \atop A_{1} & B_{1}, …, A_{n} − D_{1}} ; ⋮ . ; A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1} & {B_{1}, …, B_{n} − D_{2} \atop A_{1} & B_{1}, …, B_{n} − D_{2}} ; ⋮ . ; A_{1} & B_{1}, …, A_{n} & B_{n} − D_{2} \\ A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1} & D_{2} \end{matrix}

(i) ⇒ (ii). Assume (i). We show that A_{1}, …, A_{n} − D_{1} is provable in MALC. By symmetry, the same holds for B_{1}, …, B_{n} − D_{2}.

First, note that A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1} is provable:

\begin{matrix}A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1} & D_{2} & {D_{1} − D_{1} \atop D_{1} & D_{2} − D_{1}} \\ A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1} \end{matrix} Cut

Since Cut is eliminable in MALC, we get a cut-free proof P of A_{1} & B_{1}, …, A_{n} & B_{n} − D_{1}. There are three possible ways in which a negative occurrence of A_{i} & B_{i} can originate in a cut-free proof in MALC:

(1) It originates in an axiom:

A_{i} & B_{i} − A_{i} & B_{i}

(2) It originates in the conclusion of (& −): a.

{…, A_{i}, … − … \atop …, A_{i} & B_{i}, … − …}

b.

{…, B_{i}, … − … \atop …, A_{i} & B_{i}, … − …}

We will show that in P, each A_{i} & B_{i} originates in the way indicated in (2a). If this is so, by skipping the applications of (& −) that introduce A_{i} & B_{i} (for i = 1, …, n), we can transform P into a proof of A_{1}, …, A_{n} − D_{1}.

Since there is no positive occurrence of A_{i} & B_{i} in P, (1) is clearly excluded. We can show that (2b) is also impossible in P by two lemmas.

Lemma 13. Let Γ and Δ be sequences consisting of P_{1}-formulas, P_{2}- formulas, and formulas of the form A & B, where A is a P_{1}-formula and B is a P_{2}-formula. Let D be a P_{1}-formula, and C be a P_{2}-formula. Then Γ, C, Δ − D is not provable in MALC.

Proof. By induction on the depth of cut-free proof. ⊣

Lemma 14. In P, the succedent of every sequent is a P_{1}-formula.

Proof. Suppose there is a sequent in P with a P_{2}-formula as its succedent. Since the succedent of the endsequent is a P_{1}-formula, the lowest such sequent must be the left premise of an applicatoin of ({− \atop ∘} −) or (∘− −). Then the right premies violates Lemma 13. ⊣

This concludes the proof of the claim and Lemma 12. ⊣

Lemma 15. There is no calculus K such that Rec_{K} equals the class of finite intersections of context-free languages.

Proof. It suffices to point out that the class of finite intersections of contextfree languages is not closed under strictly alphabetic morphisms (Păun 1980). Consider the following context-free languages.

L_{0} = { a^{i}b^{i} | i ≥ 1 }
L_{1} = L∗_{0}
L_{2} = { b^{i}a^{i} | i ≥ 1 }
L_{3} = ⋃_{n≥1} a^{n}L_{2}^{n−1}b^{+}

Then

L_{1} ∩ L_{3} = { (a^{n}b^{n})^{n} | n ≥ 1 }.

Let h be a strictly alphabetic morphism such that h(a) = h(b) = a. Then

h(L_{1} ∩ L_{2}) = { a^{2n^{2}} | n ≥ 1 },

which is not regular and hence cannot be a finite intersection of context-free languages, since all context-free subsets of a∗ are regular. ⊣

Here are some open questions in view of Theorems 10 and 11:

• Does MALC recognize all context-sensitive languages?

• Does MALC recognize any PSPACE-complete languages? (Note that any finite intersection of context-free languages is in P.)

• Is MALC({− \atop ∘}, &) PSPACE-complete?

5 Multiplicative Lambek calculus

The recognizing power of the mulitplicative Lambek calculus MLC (or even the smaller fragment MLC({− \atop ∘})) had been the most outstanding open question about the mathematics of the Lambek calculus until 1992, when Mati Pentus announced a proof of the so-called ‘Chomsky conjecture’ (Pentus 1993):

Theorem 16 (Pentus). Rec_{MLC} is precisely the class of all context-free languages.

Pentus’s proof shows that given any Lambek grammar, one can effectively find an equivalent context-free grammar. Given Γ − C, let A be { A | A is not longer than the longest formula in Γ − C and contains only atomic formulas in Γ − C }. The main step of the proof is to show that if Γ − C is provable in MLC, then Γ − C is provable from the following set by Cut alone:

{ A_{1} − A_{2} ∈ Prov_{MLC} | A_{1}, A_{2} ∈ A } ∪
{ A_{1}, A_{2} − A_{3} ∈ Prov_{MLC} | A_{1}, A_{2}, A_{3} ∈ A }

It is not known whether the construction of this set can be carried out in polynomial time, so it does not follow that Prov_{MLC} is in P, although once the set is constructed, provability by Cut alone can be checked by reduction to universal context-free recognition, which is in P. Prov_{MLC} is clearly in NP, but nobody has shown that it is in P or is NP-hard.

Pentus’s theorem shows that for any finite set A of MLC formulas and any MLC formula B, the set

Prov_{MLC}^{A,B} = Prov_{MLC} ∩ { Γ − B | Γ ∈ A∗ }

is a context-free language. Could Prov_{MLC} be a context-free language? If so, this would of course imply that Prov_{MLC} is in P. It is easy to see, however, that the answer is no, even over a finite set of atomic formulas.^{4} A more interesting question to ask would be whether there is an easily computable function f that reduces Prov_{MLC} to a context-free set.

It is also worth mentioning that another result of Pentus’s (1994) implies that the symmetric transitive closure of the ‘− relation’ between formulas

{ ⟨A, B⟩ | A − B ∈ Prov_{MLC} }

is in P. In fact, there is an easy transformation [[·]] (Pentus’s ‘free group’ interpretation) that makes the set

{ [[A − B]] | A − B ∈ Prov_{MLC} }

context-free, and this constitutes a reduction of the relation in question.

Another interesting consequence of Pentus’s (1993) theorem is that the following question is decidable.^{5}

STRONG DEDUCIBILITY IN MLC.

INSTANCE: a finite set {A_{1}, …, A_{n}} of MLC formulas and an MLC formula B. QUESTION: Is there a finite sequence Γ ∈ {A_{1}, …, A_{m}}∗ such that Γ − B is provable in MLC?

This is decidable since non-emptyness of context-free languages is decidable.

One might find the decidability of strong deducibility in MLC puzzling since it looks very similar to the question of whether a sequent of the form

!A_{1}, …,!A_{n} − B,

where A_{1}, …, A_{n}, B are MLC formulas, is provable in MELC; the latter question is undecidable by the proof of Theorem 5. In fact, the linear logic counterparts of the two questions are equivalent (see Ono 1998). This is not so in the Lambek calculus. The following simple example shows that the two questions are not equivalent.

{p_{1}, p_{2}, p_{3} − p_{1} ⊗ p_{2} ⊗ p_{3} \atop p_{1},!p_{2}, p_{3} − p_{1} ⊗ p_{2} ⊗ p_{3}} ; ⋮ . ; p_{1}, p_{3},!p_{2} − p_{1} ⊗ p_{2} ⊗ p_{3} ; p_{1} ⊗ p_{3},!p_{2} − p_{1} ⊗ p_{2} ⊗ p_{3} ; !(p_{1} ⊗ p_{3}),!p_{2} − p_{1} ⊗ p_{2} ⊗ p_{3}

As the above proof shows, the sequent !(p_{1} ⊗ p_{3}),!p_{2} − p_{1} ⊗ p_{2} ⊗ p_{3} is provable, but there is no sequence Γ ∈ {p_{1}⊗p_{3}, p_{2}}∗ such that Γ − p_{1}⊗p_{2}⊗p_{3} is provable.

p_{0} {− \atop ∘}(p_{1} {− \atop ∘}(… {− \atop ∘} p_{m}) …) − q_{0} {− \atop ∘}(q_{1} {− \atop ∘}(… {− \atop ∘} q_{n}) …)

4A sequent of the form:

is provable if and only if m = n and p_{i} = q_{i} for i = 0, …, m.

5The term strong reducibility is from Ono 1998. This was called ∗-derivability by van Benthem (1991).

Note also that the above result about the recognizing power of MALC (Theorem 11) implies that MALC has an undecidable strong deducibility problem, in contrast to MLC. This follows from the fact that the question of whether given two context-free languages have a non-empty intersection is undecidable. Here we see that a language-theoretic characterization of the recognizing power of a logic can help to settle more standard questions about the logic.

References

van Benthem, J. 1991. Language in Action. Amsterdam: North-Holland. (Second edition 1995, MIT Press.)

Buszkowski, W. 1982. Some decision problems in the theory of syntactic categories. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 28, 539–548.

Kanazawa, M. 1992. The Lambek calculus enriched with additional connectives. Journal of Logic, Language and Information 1, 141–171.

Kanovich, M. I. 1993. The expressive power of modalized purely implicational calculi. CSLI Report. Center for the Study of Language and Information, Stanford University.

Kanovich, M. I. 1994. Horn fragments of non-commutaive logics with additives are PSPACE-complete. In Proceedings 1994 Annual Conference of the European Association for Computer Science Logic. Kazimierz, Poland.

Lambek, J. 1958. The mathematics of sentence structure. American Mathematical Monthly 65, 154–170.

Lambek, J. 1961. On the calculus of syntactic types. In R. Jakobson, ed., Structure of Language and Its Mathematical Aspects, pp. 161–178. American Mathematical Society.

Lincoln, P., J. Mitchell, A. Scedrov, and N. Shankar. 1992. Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56, 239–311.

Ono, H. 1998. Decidability and finite model property of substructural logics. In J. Ginzburg, Z. Khasidashvili, C. Vogel, J.J. Lévy, and E. Vallduví, eds., The Tbilisi Symposium on Logic, Language and Computation: Selected Papers. Stanford, Calif.: CSLI Publications.

Păun, G. 1980. A note on the intersection of context-free languages. Fundamenta Informticae 3, 135–139.

Pentus, M. 1993. Lambek grammars are context free. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 429– 433.

Pentus, M. 1994. Equivalent types in Lambek calculus and linear logic. Journal of Logic, Language and Information 3, 121–140.

Pentus, M. 1997. Product-free Lambek calculus and context-free grammars. Journal of Symbolic Logic 62, 648–660.