The Cut-Elimination Theorem for the Second Order Lambek Calculus

Martin Emms and Hans Leiß

                   {emms,leiss}@cis.uni-muenchen.de

Universität München, CIS

June 24, 1993

Abstract

A second order extension of Lambek’s sequent calculus for categorial grammars is presented. We show that sequents provable with the Cut-rule can be proved without the Cut-rule as well.

1 Introduction

We will be concerned with a second order extension of Lambek’s [7] sequent calculus for categorial grammars and the issue of Cut Elimination. Therefore, it is convenient to begin with a description of the Lambek calculus.

To build syntactic types or categories, Lambek [7] uses the binary connectives ‘/’ and ‘\’, first proposed by Bar-Hillel[1].^{1} He refers to categorial reductions as sequents and defines the accepted categorial reductions by a close variant of Gentzen’s sequent calculus for implicational propositional logic. This is Lambek’s calculus, l^{(/,\)}:

(Ax)  \overline{x ⇒ x}

(/L) \frac{U, y, V ⇒ z  T ⇒ x}{U, y/x, T, V ⇒ z}  (/R) \frac{T, x ⇒ y}{T ⇒ y/x}

(\L) \frac{U, y, V ⇒ z  T ⇒ x}{U, T, x\y, V ⇒ z}  (\R) \frac{x, T ⇒ y}{T ⇒ x\y}

Here U, T, V are sequences of categories (U,V possibly empty), w, x, y are categories. With regard to the names of the rules, ‘L’ and ‘R’ stand for left and right.

l^{(/,\)}stands out amongst other categorial grammars that make the same choice of connectives for several mathematical and practical reasons. For example, there are soundness and completeness results for the ‘standard interpretation’ of categories x as sets [[x]] ⊆ A^{∗} of strings over an alphabet A, and connectives inrerpreted as [[x/y]] = {a : a ∈ A^{∗}, a · b ∈ [[x]] for each b ∈ [[y]]}, and correspondingly for \, where · is concatenation of strings. Buszkowski[2] showed that for this (and similar) interpretations, we get l^{(/,\)} |− x_{1}, …, x_{n} ⇒ y if and only if [[x_{1}]]· . . . ·[[x_{n}]] ⊆ [[y]] using · as elementwise concatenation. Another interesting aspect is that via the Curry-Howard isomorphism, an operational, semantic significance can be given to each proof of the calculus, where differing proofs of a single sequent can have a differing operational meanings. This has the practical benefit (potentially at least) to solve the linguistic puzzle of scope ambiguities that are not accompanied by syntactic ambiguities.

1In common with several authors, we omit Lambek’s product connective (denoting concatenation) and use the name Lambek calculus for what is really the product-free calculus.

However, certain aspects of linguistic coverage have eluded all those who have proposed purely Lambek grammars. One is full coverage of extraction constructions, with Lambek grammars always failing to cover non-peripheral extractions (eg. the (man)_{i} who Dave told e_{i} to leave). Second, only the scope-ambiguities of peripheral quantifiers are covered (eg. every student made one mistake). Third, there is no purely Lambek grammar account of cross-categorial coordination, and other constructs that need schematic categories. The standard approach is to add a coordination (axiom) schema to the grammar, such as x, and, x ⇒ x, with a pure Lambek grammar being used to assign some category to the strings to be coordinated.

Given the completeness result for l^{(/,\)}, a categorial grammar solution to these problems can only be reached by restricting the possible interpretations using further axioms and rules and possibly an expansion of the categorial language.^{2} Moortgat[8] has, for example, proposed a connective that would deal with non-peripheral extraction, and a further connective to deal with the quantifier problems. Emms[3] proposed a single, simple generalisation of l^{(/,\)} to a polymorphic calculus that enables all of the above problems to be solved. The reader is refered to [4] for demonstrations and arguments why it constitutes a better solution to the above problems of linguistic coverage than others that have been proposed.

In this polymorphic extension of the calculus, added to the categorial vocabulary are category variables and the possibility of their quantification. For example, we will have such categories as ∀X(X/X) that could be used as the category of a negation operation working uniformly for all categories X. Then added to l^{(/,\)}, are left and right rules for ∀, to give what will be called l^{(/,\,∀)}:^{3}

(∀L) \frac{U, x[y/Y], V ⇒ z}{U, ∀Y x, V ⇒ z} (∀R) \frac{T ⇒ x}{T ⇒ ∀Y.x[Y/Z]}, if Z is not free in T and Y is not free in ∀Z.x

In the premise of the (∀L) rule, a category y is substituted for a variable. Whether this y may contain quantifiers is a parameter that may be varied in the definition of the calculus. The paper will be concerned with the calculus that results when no restriction is placed on y.

The calculus extended with both universal and existential quantifiers will also be called ‘Second Order Lambek Calculus’, because of its connection to second order propositional logic.

1.1 Cut Elimination and Categorisation

The concern of this paper is not a linguistic, but a technical one: whether there is a Cut Elimination theorem for the second order calculus. The question is whether any new sequents would be derivable if the following ‘Cut’ rule were added to the calculus:

2There are solutions to these problems that are not in any sense categorial, and an ever present obligation is to find reasons to favour categorial over non-categorial solutions.

3In addition to [3], existential quantification will be also considered in later sections.

(Cut) \frac{U, x, V ⇒ z  T ⇒ x}{U, T, V ⇒ z}

The fact that no new sequents are derivable by the addition of Cut is called the Cut Elimination property. In logical calculi, this is an important property because it says that the use of lemmata in reasoning, useful to structure and shorten proofs, can in principle be avoided in favour of ‘direct’ proofs – although typically at the price of a blow-up in proof size.

In Lambek calculi, Cut Elimination has a similar relevance, reducing indirect to direct ways of parsing – even without an increase in proof length. Parsing here is done with respect to the following definition of syntactical categorisation for a sequent categorial grammar.

Where L is a sequent calculus, we might define ‘grammar’ and ‘categorisation’ as follows. A grammar, G, is an assumed or ‘lexical’ assignment of (finitely many) categories to words. Reading G |− s : y as ‘according to G, s has category y’, one would say G |− s : y, if (i) s is lexically assigned y, or (ii) s is the concatenation s_{1} ⋯ s_{n} of n ≥ 1 words s_{i} with G |− s_{i} : x_{i}, and L |− x_{1}, …, x_{n} ⇒ y.^{4} Call x_{1}, …, x_{n} ⇒ z a ‘categorising sequent’ for s_{1} ⋯ s_{n} if the x_{i} are lexically assigned to the s_{i}.

Given this definiton of categorisation, one can show that Cut Elimination means that for any grammar G, the decidability of categorisation (the question whether G |− s : x) reduces to the decidability of sequent provability (the question whether L |− r).

A quick illustration of this follows. Consider deciding whether G |− s_{1}s_{2} : z, where s_{1} and s_{2} are lexically assigned the categories x and y. One can first check whether the categorising sequent is provable, that is whether L |− x, y ⇒ z. If it is, then G |− s_{1}s_{2} : z, and the parse tree would be that in (1 a). However, if L |− / x, y ⇒ z, that does not immediately imply that G |− / s_{1}s_{2} : z. For if there are x′ and y′ such that x ⇒ x′, y ⇒ y′, and x′, y′ ⇒ z were L-derivable, then G |− s_{1}s_{2} : z. The associated parse tree is shown in (1 b). Call this latter route to categorising s_{1}s_{2} as z a ‘non-flat’ categorisation strategy.

a s_{1} x s_{2} y z  b s_{1} x s_{2} y x′ y′ z (1)

So parsing with respect to the natural definition of categorisation requires one to decide whether the ‘non-flat’ categorisation strategy will succeed. However, there is a problem in deciding this in a straightforward way because there are infinitely many x′ and y′ such that L |− x ⇒ x′, y ⇒ y′. This would appear to open up a gap between the decidability of sequent provability and the decidability of categorisation.

The Cut Elimination theorem^{5} closes this gap in the following way. If the string can be categorised with the non-flat strategy, then there is a Cut-based proof of the categorising sequent. For example, the parse tree (1 b) implies the existence of the following Cut based proof of x, y ⇒ z:

4Taking [[x]] to be the set of strings assigned category x, soundness of L would give [[x_{1}]] ⋯ [[x_{n}]] ⊆ [[y]].

5The completeness of the Cut-free calculus with respect to the interpretation of categories as sets of strings offers an alternative argument why the ‘non-flat’ strategy is not needed.

⋮  _{⋮}  _{⋮}_{y ⇒ y′}  _{x′, y′ ⇒ z}_{Cut}_{x′, y ⇒ z}_{x ⇒ x′}  _{Cut}_{x, y ⇒ z} (2)

But given Cut Elimination, a Cut-based proof of the categorising sequent implies the existence of a Cut-free proof of the same sequent. This means that to decide the categorisation question for a given string, it is sufficient to check simply the derivability of the categorising sequent, and thus the decidability of categorisation is reduced to the decidability of sequent provability.

1.2 Degree of a Cut versus Proof Size

Before giving our proof of Cut Elimination, we note some difficulties for straightforward attempts at a proof. These explain why section 2 begins by redefining the calculus somewhat.

Using L as neutral between l^{(/,\)}and l^{(/,\,∀)} (these formulated as Cut free), one can say that Cut Elimination will hold if we can show:

If L |− U, x, V ⇒ w and L |− T ⇒ x, then L |− U, T, V ⇒ w.  (3)

To obtain a proof of Cut Elimination for l^{(/,\)}, Lambek basically adapted Gentzen’s proof for propositional logic. This involves showing the above by induction on ♯(U, x, V, w, T), where ♯(y) is the complexity of y as measured by a count of connectives.

With the second order Lambek calculus, induction on ♯(U, x, V, w, T) runs into a difficulty in the case where the main connective of x is introduced in the last steps of the proofs of both T ⇒ x and U, x, V ⇒ w. If x contains a quantifier, say x ≡ ∀Y z, we would be considering a pair of sequents with proofs

⋮ U, z[y/Y], V ⇒ w (∀L) U, ∀Y z, V ⇒ w  ⋮ T ⇒ z (∀R), (Y not free in T) T ⇒ ∀Y z

and attempting to show that (3) holds for these two sequents, assuming (3) for all cases of complexity strictly less than n = ♯(U, ∀Y z, V, w, T). The natural move is to consider the substitution throughout T ⇒ z of y for Y, and show substitution for free variables preserves derivability. Given that Y is not free in T, this would be the sequent T ⇒ z[y/Y] and this, together with the assumed provable U, z[y/Y], V ⇒ w, forms a pair instantiating the pattern that (3) concerns. So if ♯(U, z[y/Y], V, w, T) < n, we would have by induction, a proof of U, T, V ⇒ w. However, this requires that ♯(z[y/Y]) < ♯(∀Y z), which does not hold in cases like y ≡ ∀X(X/X) and z ≡ X/X.

(As an aside, we note that for the restricted version of the calculus where quantifiers are not allowed but for universal ones in prefix position, the straightforward extension of Lambek’s method will actually yield a proof of Cut Elimination. In this case, y above is quantifier-free and so ♯(z[y/Y]) < ♯(∀Y z) will hold if quantifier-rank is made the essential part of the complexity.)

In spite of the above set back to Lambek’s method, one can show that (3) actually holds for the unrestricted second order calculus. The tactic is to do so not by induction on ♯(U, x, V, w, T), but by induction on the size of the proofs of U, x, V ⇒ w and T ⇒ x, with the size of a proof taken to be the number of nodes in it. Looking back at the above case, one can see that there will be no block just as long as substitution for free variables not only preserves derivability, but also preserves size.

However, in showing that substitutions preserve proof size one apparently needs that changes of bound variables preserve proof size as well. But changes of bound variables will not be size preserving for the calculus as presented. For example, ∀X(X/X) ⇒ ∀X(X/X) has a proof of size 1. By a change of bound variables we obtain ∀X(X/X) ⇒ ∀Y (Y/Y), which has proofs of size larger than 1 only. (One cannot simply avoid this by requiring axioms to be quantifier-free, since then substitutions of quantified formulas into axioms will not be size preserving.) We see three ways to escape from this difficulty:

1. An obvious way to get around it would be to consider categories as equivalence classes modulo renaming of bound variables. For doing the cut-elimination proof, we prefer a simpler syntactic notion of category.

2. Change of bound variables preserves provability, so it can be added as derivable rule, CBV. Ignore CBV nodes in proof size. Then, concerning l^{(/,\,∀)}+ CBV, show that substitution is proof size preserving. This will allow a proof of Cut Elimination for l^{(/,\,∀)}+ CBV, which together with the eliminability of CBV, entails Cut elimination for l^{(/,\,∀)}. The details have been checked, but will not be given here.

3. Reformulate the calculus so that bound and free variables are always distinct, making thereby the definition of substitution simpler. A proof of size preserving substitution is then possible, leading to a proof of Cut Elimination. This is the way taken in sections 2 and 3. It has the advantage that one can easily give a bound on the size of the cut-free proof in terms of the proof at hand.

In the final section of the paper we demonstrate that the Cut Elimination proof for the reformulated calculus entails Cut Elimination for the calculus as formulated above.

2 The Second Order Lambek Calculus

To avoid renaming of bound variables during substitutions, we assume two disjoint infinite lists of variables. We use FV (x) for the set of variables occuring in x that are taken from the first list (of free) variables –ranged over by Y and Z–, and BV (x) for the variables occuring in x that come from the second list (of bound variables) –ranged over by X. The result of replacing all occurrences of the free variable Z in x by the bound variable X is denoted by x[X/Z]. The variable clashes this may lead to are excluded by clause (iii) of the following definition.

Definition 1 Formulas (or syntactic categories) are inductively defined as follows:

i) Each free variable Z is a formula.

ii) If x and y are formulas, so are (x/y) and (x\y).

iii) ∀Xx̃ and ∃Xx̃ is a formula, if x is a formula and x̃ ≡ x[X/Z], where X is a bound and Z a free variable such that Z ∉ FV (QXz) for each subformula QXz of x with Q ∈ {∀, ∃}.

Henceforth we write QX.x[X/Z] for the formula QXz with z ≡ x[X/Z]; in particular Z then does not occur in subformulas ∃Xy and ∀Xy of x.

Note that if X is from the list of bound variables, x[X/Z] need not be a formula, as it may have occurences of the ‘bound’ variable X that are not in the scope of a quantifier ∃X or ∀X. Let us call such an expression a pseudo-formula.

For a pseudo-formula x and a formula y, we always have FV (y) ∩ BV (x) = ∅, so that substitution x[y/Y] of the free variable Y in x by y can be defined without change of bound variables:

\begin{matrix}Y [y/Y]  ≡ & y & Z[y/Y]  ≡ & Z for Z ≢ Y \\ (x/z)[y/Y] ≡ & (x[y/Y]/z[y/Y]) & (x\z)[y/Y] ≡ & (x[y/Y]\z[y/Y]) \\ (∀Xz)[y/Y] ≡ & ∀X.z[y/Y] & (∃Xz)[y/Y] ≡ & ∃X.z[y/Y] \end{matrix}

Here we used Z for both free and bound variables. Since z in the quantified formulas in general is not a formula, we have to define substition x[y/Y] for pseudo-formulas x.

Definition 2 The rules of the second order Lambek Calculus are the following. We use x, y and z for formulas, X for bound and Y and Z for free variables, U and V for arbitrary and T for nonempty lists of formulas.

\begin{matrix}(Ax) & \overline{x ⇒ x} & (Cut) & \frac{U, x, V ⇒ z  T ⇒ x}{U, T, V ⇒ z} \\ (/L) & \frac{U, y, V ⇒ z  T ⇒ x}{U, y/x, T, V ⇒ z} & (/R) & \frac{T, x ⇒ y}{T ⇒ y/x} \\ (\L) & \frac{U, y, V ⇒ z  T ⇒ x}{U, T, x\y, V ⇒ z} & (\R) & \frac{x, T ⇒ y}{T ⇒ x\y} \\ (∀L) & \frac{U, x[y/Y], V ⇒ z}{U, ∀X.x[X/Y], V ⇒ z} & (∀R) & \frac{T ⇒ x}{T ⇒ ∀X.x[X/Z]} Z! \\ (∃L) & \frac{U, x, V ⇒ z}{U, ∃X.x[X/Z], V ⇒ z} Z! & (∃R) & \frac{T ⇒ x[z/Z]}{T ⇒ ∃X.x[X/Z]} \end{matrix}

The side condition Z! means that Z must not be free in the lower sequent.

3 Preservation of Proof Size under Substitution

By ⊢^{n} T ⇒ w we mean that T ⇒ w has a derivation with at most n nodes in the proof tree.

Lemma 1 For every number n, sequent T ⇒ w, formula y and free variable Y,

⊢^{n} T ⇒ w  ⇒  ⊢^{n} T [y/Y] ⇒ w[y/Y].

Proof by induction on the number n of nodes in the derivation of T ⇒ w. The claim is obvious for n = 1, since axioms x ⇒ x are allowed not only for atomic, but also for complex formulas x.

Suppose it is shown for n, and let a derivation of T ⇒ w with n + 1 nodes be given, denoted by

\begin{matrix}⋮ & n+1 \\ T ⇒ w. \end{matrix}

Since the other cases are obvious by induction, we only consider the cases where the last step in this derivation uses one of the quantifier rules. First note that where Z̃ ∉ FV (x, y, Y),

(QX.x[X/Z])[y/Y] ≡ QX.x[Z̃/Z][y/Y][X/Z̃]  (4)

Case (∀L): We have a derivation

(∀L) \frac{\begin{matrix}⋮ & n \\ U, x[z/Z], V ⇒ w \end{matrix}}{U, ∀X.x[X/Z], V ⇒ w} .

By induction, there is a derivation

\begin{matrix}⋮ & n \\ U[y/Y], x[z/Z][y/Y], V [y/Y] ⇒ w[y/Y]. \end{matrix}

Choose Z̃ ∉ FV (x, y, Y). We then have

x[z/Z][y/Y] ≡ x[Z̃/Z][y/Y][z[y/Y]/Z̃]  (5)

and hence we can add a (∀L) step to the above derivation to get:

(∀L) \frac{\begin{matrix}⋮ & n \\ U[y/Y], x[z/Z][y/Y], V [y/Y] ⇒ w[y/Y] \end{matrix}}{U[y/Y], ∀X.x[Z̃/Z][y/Y][X/Z̃], V [y/Y] ⇒ w[y/Y]},

which establishes the claim using (4). Case (∃R): (Similar to (∀L).) We have a derivation

(∃R) \frac{\begin{matrix}⋮ & n \\ T ⇒ x[z/Z] \end{matrix}}{T ⇒ ∃X.x[X/Z]}.

By induction, there is a derivation

\begin{matrix}⋮ & n \\ T [y/Y] ⇒ x[z/Z][y/Y]. \end{matrix}

Choosing Z̃ ∉ FV (x, y, Y), we have (5) again, and hence we can add a (∃R) step to get:

(∃R) \frac{\begin{matrix}⋮ & n \\ T [y/Y] ⇒ x[z/Z][y/Y] \end{matrix}}{T [y/Y] ⇒ ∃X.x[Z̃/Z][y/Y][X/Z̃]},

which establishes the claim by (4). Case (∀R): We have a derivation

(∀R) \frac{\begin{matrix}⋮ & n \\ T ⇒ x \end{matrix}}{T ⇒ ∀X.x[X/Z]} Z!

Choose Z̃ ∉ FV (T, x, y, Y). By induction there is a derivation

\begin{matrix}⋮ & n \\ T [Z̃/Z][y/Y] ⇒ x[Z̃/Z][y/Y] \end{matrix}

of T [y/Y] ⇒ x[Z̃/Z][y/Y], using that Z ∉ FV (T). By the choice of Z̃, we can add a (∀R) step to the above derivation to get:

(∀R) \frac{\begin{matrix}⋮ & n \\ T [y/Y] ⇒ x[Z̃/Z][y/Y] \end{matrix}}{T [y/Y] ⇒ ∀X.x[Z̃/Z][y/Y][X/Z̃]} Z̃!,

which establishes the claim by (4).

Case (∃L): (Similar to (∀R).) We have a derivation

(∃L) \frac{\begin{matrix}⋮ & n \\ U, x, V ⇒ w \end{matrix}}{U, ∃X.x[X/Z], V ⇒ w} Z!

Choose Z̃ ∉ FV (U, x, V, w, y, Y). By induction there is a derivation

\begin{matrix}⋮ & n \\ U[Z̃/Z][y/Y], x[Z̃/Z][y/Y], V [Z̃/Z][y/Y] ⇒ w[Z̃/Z][y/Y] \end{matrix}

of U[y/Y], x[Z̃/Z][y/Y], V [y/Y] ⇒ w[y/Y], using that Z ∉ FV (U, V, w). By the choice of Z̃, we can add a (∃L) step to the above derivation to get:

(∃L) \frac{\begin{matrix}⋮ & n \\ U[y/Y], x[Z̃/Z][y/Y], V [y/Y] ⇒ w[y/Y] \end{matrix}}{U[y/Y], ∃X.x[Z̃/Z][y/Y][X/Z̃], V [y/Y] ⇒ w[y/Y]} Z̃!,

which establishes the claim by (4). □

4 The Cut-Elimination Theorem

We are now ready to prove the Cut Elimination property. As motivated in the introduction, we proceed by induction on the proof sizes of the premises of a cut.

Theorem 1 If a sequent is provable using (Cut), it can also be proved without using (Cut).

Let ⊢_{k}^{n} denote provability with a derivation with at most n nodes and exactly k applications of (Cut). The first lemma is an instance of (3), claiming that cuts can be eliminated when their premises have cut-free proofs. It’s statement also mentiones a bound on the size of the cut-free proof in terms of the size of the original proof using (Cut). This is not just for external reasons, but actually needed in establishing the lemma, since the induction hypothesis has to be used twice in one of the cases (see case 5, subcvase v ≡ x/y below).

Lemma 2 If ⊢_{0}^{m} Γ, v, Π ⇒ w and ⊢_{0}^{n} Δ ⇒ v, then ⊢_{0}^{m+n} Γ, Δ, Π ⇒ v.

The second lemma says that removing an application of (Cut) will also remove a node in the derivation tree. Hence, adding the (Cut)-rule does not reduce the minimal proof sizes of provable sequents.

Lemma 3 If ⊢_{k}^{n} Γ ⇒ w, then ⊢_{0}^{n−k} Γ ⇒ w.

The cut-elimination theorem follows immediately from Lemma 3. Proof of Lemma 3: If k > 0, choose a topmost application of (Cut) in the given derivation of Γ ⇒ w, i.e. one whose upper sequents are derived without using (Cut). Using Lemma 2, replace this subderivation of the lower sequent by a cut-free derivation. This gives a new derivation of Γ ⇒ w which shows ⊢_{k−1}^{n−1} T ⇒ w. By induction, the remaining cuts can be reduced similiarly. □

Proof of Lemma 2. The proof is by induction on m + n. By ⋮ ^{n}_{Γ ⇒ w} we here denote a cut-free derivation of Γ ⇒ w with at most n ≥ 1 nodes. Assume

\begin{matrix}⋮ & m \\ Γ, v, Π ⇒ w \end{matrix}  and  \begin{matrix}⋮ & n \\ Δ ⇒ v \end{matrix} ,

in order to show

\begin{matrix}⋮ & m+n \\ Γ, Δ, Π ⇒ w. \end{matrix}

We distinguish several cases. Case 1: m = 1. Then Γ, v, Π ⇒ w is obtained by (Ax), so Γ = Π = ∅, v ≡ w, and the second

assumption ⋮ ^{n}_{Δ ⇒ v} is used as ⋮ ^{m+n}_{Γ,Δ,Π ⇒ w.} Case 2: n = 1. Then Δ ⇒ v is obtained by an application of (Ax), so Δ ≡ v and we can use

⋮ ^{m}_{Γ,v,Π ⇒ w} as ⋮ ^{m+n}_{Γ,Δ,Π ⇒ w}.

Case 3: m, n > 1 and the last step of ⋮ ^{n}_{Δ ⇒ v} does not introduce the main connective of v.

Then the last step of ⋮ ^{n}_{Δ ⇒ v} uses a left-rule, which is one of the following: Subcase (/L): We have derivations

\begin{matrix}⋮ & m \\ Γ, v, Π ⇒ w \end{matrix}  and  (/L) \frac{\begin{matrix}⋮ & n_{1} \\ U, y, V ⇒ v \end{matrix}  \begin{matrix}⋮ & n_{2} \\ T ⇒ x \end{matrix}}{U, y/x, T, V ⇒ v} .
By induction on m + n_{1} < m + n, there is ⋮ ^{m+n_{1}}_{Γ,U,y,V,Π ⇒ w} and hence by an application of (/L)

(/L) \frac{\begin{matrix}⋮ & m+n_{1} \\ Γ, U, y, V, Π ⇒ w \end{matrix} \begin{matrix}⋮ & n_{2} \\ T ⇒ x \end{matrix}}{Γ, U, y/x, T, V, Π ⇒ w} .

Note that this is a derivation of Γ, Δ, Π ⇒ w with at most m + n_{1} + n_{2} + 1 = m + n nodes. Subcase (\L): Similar.

Subcase (∀L): We have

\begin{matrix}⋮ & m \\ Γ, v, Π ⇒ w \end{matrix}  and  (∀L) \frac{\begin{matrix}⋮ & n−1 \\ U, x[y/Y], V ⇒ v \end{matrix}}{U, ∀X.x[X/Y], V ⇒ v.}

By induction on m + (n − 1) < m + n, we get

(∀L) \frac{\begin{matrix}⋮ & m+n−1 \\ Γ, U, x[y/Y], V, Π ⇒ w \end{matrix}}{Γ, U, ∀X.x[X/Y], V, Π ⇒ w} .

Subcase (∃L): We have derivations

\begin{matrix}⋮ & m \\ Γ, v, Π ⇒ w \end{matrix}  and  (∃L) \frac{\begin{matrix}⋮ & n−1 \\ U, x, V ⇒ v \end{matrix}}{U, ∃X.x[X/Z], V ⇒ v} Z!

Choose Z̃ ∉ FV (Γ, Π, w, U, ∃X.x[X/Z], V, v), so that x ≡ x[Z̃/Z][Z/Z̃]. By Lemma 1, there is a (cut-free) derivation

\begin{matrix}⋮ & n−1 \\ U[Z̃/Z], x[Z̃/Z], V [Z̃/Z] ⇒ v[Z̃/Z] \end{matrix}

of U, x[Z̃/Z], V, ⇒ v, whence by induction on m + (n − 1) < m + n there is

\begin{matrix}⋮ & m+n−1 \\ Γ, U, x[Z̃/Z], V, Π ⇒ w \end{matrix} .

Since ∃X.x[Z̃/Z][X/Z̃] ≡ ∃X.x[X/Z] and Z̃ is not free in Γ, U, ∃X.x[X/Z], V, Π ⇒ w, we obtain

(∃L) \frac{\begin{matrix}⋮ & m+n−1 \\ Γ, U, x[Z̃/Z], V, Π ⇒ w \end{matrix}}{Γ, U, ∃X.x[X/Z], V, Π ⇒ w} .

Case 4: m, n > 1 and the last step of ⋮ ^{m}_{Γ,v,Π ⇒ w} does not introduce the main connective of v.

Subcase a) The last step is a right rule. For some connective ∘ we then have derivations

(∘R) \frac{\begin{matrix}⋮ & m−1 \\ Γ′, v, Π′ ⇒ w′ \end{matrix}}{Γ, v, Π ⇒ w}  and  \begin{matrix}⋮ & n \\ Δ ⇒ v. \end{matrix}

By induction on (m − 1) + n < m + n, there is a derivation

(∘R) \frac{\begin{matrix}⋮ & m−1+n \\ Γ′, Δ, Π′ ⇒ w′ \end{matrix}}{Γ, Δ, Π ⇒ w} .

In case ∘ is ∀ and w ≡ ∀X.x[X/Z], we can assume that the side condition on the variable Z is satisfied for this new application of (∀R): otherwise, if Z ∈ FV (Δ), choose a fresh variable Z̃ such that x[X/Z] ≡ x[Z̃/Z][X/Z̃] and first apply [Z̃/Z] to the derivation of Γ, v, Π ⇒ w. Subcase b) The last step is an application of a left-rule. We then have, for some connective ∘ ∈ {/, \, ∀, ∃}, two derivations

(∘L) \frac{\begin{matrix}⋮ & m_{1} \\ Γ′, v, Π′ ⇒ w \end{matrix}  [\begin{matrix}⋮ & m_{2} \\ T ⇒ x \end{matrix}]}{Γ, v, Π ⇒ w}  and  \begin{matrix}⋮ & n \\ Δ ⇒ v \end{matrix} ,

where the subderivation in brackets is missing for ∘ ∈ {∀, ∃}. By induction on m_{1} + n < m + n, there is

(∘L) \frac{\begin{matrix}⋮ & m_{1}+n \\ Γ′, Δ, Π′ ⇒ w \end{matrix}  [\begin{matrix}⋮ & m_{2} \\ T ⇒ x \end{matrix}]}{Γ, Δ, Π ⇒ w}.

If ∘ is ∃, we can satisfy the side condition on the quantified variable as in the previous case.

Case 5: m, n > 1 and the last steps of ⋮ ^{m}_{Γ,v,Π ⇒ w} and ⋮ ^{n}_{Δ ⇒ v} introduce the main connective of v. Then these last steps are corresponding left- and right-rules for one of the four connectives. Subcase v ≡ y/x: We have

(/L) \frac{\begin{matrix}⋮ & m_{1} \\ U, y, V ⇒ w \end{matrix}  \begin{matrix}⋮ & m_{2} \\ T ⇒ x \end{matrix}}{U, y/x, T, V ⇒ w}  and  (/R) \frac{\begin{matrix}⋮ & n−1 \\ Δ, x ⇒ y \end{matrix}}{Δ ⇒ y/x} .

By induction on m_{1} + (n − 1) < m + n there is

\begin{matrix}⋮ & m_{1}+n−1 \\ U, Δ, x, V ⇒ w, \end{matrix}

and since m_{1} + m_{2} + n − 1 < m + n, we can use induction again to get

\begin{matrix}⋮ & m_{1}+m_{2}+n−1 \\ U, Δ, T, V ⇒ w. \end{matrix}

Subcase v ≡ x\y: Similar. Subcase v ≡ ∀X.x[X/Z]: For some Y and x̃ with x̃[X/Y] ≡ x[X/Z] we have derivations

(∀L) \frac{\begin{matrix}⋮ & m−1 \\ U, x̃[y/Y], V ⇒ w \end{matrix}}{U, ∀X.x̃[X/Y], V ⇒ w}  and  (∀R) \frac{\begin{matrix}⋮ & n−1 \\ Δ ⇒ x \end{matrix}}{Δ ⇒ ∀X.x[X/Z]} Z!

Lemma 1 applied to the second assumption yields

\begin{matrix}⋮ & n−1 \\ Δ ⇒ x[y/Z]. \end{matrix}

Since x[X/Z] ≡ x̃[X/Y] gives x[y/Z] ≡ x̃[y/Y], by induction on (m − 1) + (n − 1) < m + n we get

\begin{matrix}⋮ & m−1+n−1 \\ U, Δ, V ⇒ w. \end{matrix}

Subcase v ≡ ∃X.x[X/Z]: For some Y and x̃ with x[X/Z] ≡ x̃[X/Y] we have

(∃L) \frac{\begin{matrix}⋮ & m−1 \\ Γ, x, Π ⇒ w \end{matrix}}{Γ, ∃X.x[X/Z], Π ⇒ w} Z!  and  (∃R) \frac{\begin{matrix}⋮ & n−1 \\ Δ ⇒ x̃[z/Y] \end{matrix}}{Δ ⇒ ∃X.x̃[X/Y]}.

By Lemma 1 we get a derivation

\begin{matrix}⋮ & m−1 \\ Γ[z/Z], x[z/Z], Π[z/Z] ⇒ w[z/Z] \end{matrix}

of Γ, x[z/Z], Π ⇒ w. Since x[X/Z] ≡ x̃[X/Y] implies x[z/Z] ≡ x̃[z/Y], by induction on (m − 1) + (n − 1) < m + n there is a derivation

\begin{matrix}⋮ & m−1+n−1 \\ Γ, Δ, Π ⇒ w. \end{matrix}

□

5 Relation to the Simpler Presentation of the Calculus

The purpose of this section is compare the system just considered with the simpler system of the introduction based on just one infinite list of variables rather than two. The systems will be henceforth referred to as L_{1} and L_{2}.

Definition 1 Formulas (or syntactic categories) of L_{1} are inductively defined as follows:

i) Each variable X is a formula.

ii) If x and y are formulae, so are x/y and (x\y).

iii) If x is a formula and X is a variable, then ∀Xx and ∃Xx are formulae.

The rules for L_{1} were given in section 1, with the omission of the (∃L) and (∃R), which rules should be clear from the corresponding L_{2} rules. The notions of free and bound variables for L_{1} and the definition of substitution are the usual ones, with substitution involving a renaming of bound variables (with respect to a given enumeration of the variables) to avoid clashes.^{6}

Definition 2 (Substitution)

1. X[a/X] = a

2. (b_{1}/b_{2})[a/X] = b_{1}[a/X]/b_{2}[a/X], correspondingly for ‘\’

6See Hindley and Seldin[6]

3. (∀Xb)[a/X] = ∀Xb

4. (∀Y b)[a/X] = ∀Y (b[a/X]) if Y ∉ F V (a) or X ∉ F V (b)

5. (∀Y b)[a/X] = ∀Z(b[Z/Y][a/X]) if Y ∈ F V (a) and X ∈ F V (b), where Z is the ‘first’ variable not occurring free in b or a

Where x contains an occurrence of ∀X.z, and x′ is the replacement in x of ∀X.z by ∀Y.z[Y/X], Y ∉ F V (z), we shall say x′ comes from x by a change of bound variable, notated x ∼_{1} x′. Then x ∼ x′ if x′ comes from x by a finite, possible empty, series of ∼_{1} steps. For reference purposes we note the following, where X, Y and Z are distinct variables:^{7}

(i) Z ∉ F V (a) implies a[Z/X][b/Z] ∼ a[b/X]

(ii) Y ∉ F V (b) implies a[c/Y][b/X] ∼ a[b/X][c[b/X]/Y]

(iii) a ∼ a′, b ∼ b′ implies a[b/X] ∼ a′[b′/X]

(iv) if x[X/Y] ∼ y then for some x′, x ∼ x′, y = x′[X/Y]

(v) ∼ is an equivalence relation

L_{1}^{0} will be used to refer a restriction of L_{1} that allows only zero-complexity axioms. We have the following three lemmas:

Lemma 4 (Basic axioms)

(i) L_{1} |− T ⇒ x implies L_{1}^{0} |− T ⇒ x, (ii) L_{1} + Cut |− T ⇒ x implies L_{1}^{0} + Cut |− T ⇒ x

Lemma 5 (Preservation of derivability under ∼)

(i) if L_{1} |− r, then for any r′, r ∼ r′, L_{1} |− r′, (ii) if L_{1} + Cut |− r, then for any r′, r ∼ r′, L_{1} + Cut |− r′

Lemma 6 (Preservation of derivability under substitution) For any category, a, for any variable Z,

i) if L_{1} |− T ⇒ x, then L_{1} |− T [a/Z] ⇒ x[a/Z] (ii) if L_{1} + Cut |− T ⇒ x, then L_{1} + Cut |− T [a/Z] ⇒ x[a/Z]

The Basic Axioms lemma is very easily shown. For the proofs of the other two lemmas see the Appendix. They can be used in showing an equivalence between L_{1} and L_{2}.

We will identify the BV (resp. F V) set of L_{2} variables with the even (resp. odd) L_{1} variables. We will say concerning L_{1} sequents that s ⇝ s′ if s′ comes from s by changes of bound variable and substitutions of fresh (i.e. not all ready present) variables for variables. When the bound variables of a sequent are even and the free variables are odd, we will call it clean. We have the following (for proof see Appendix):

Lemma 7 (L_{1} and L_{2} equivalence) Where s and s′ are L_{1} and L_{2} sequents such that s ⇝ s′,

(i) L_{1} |− s iff L_{2} |− s′ (ii) L_{1} + Cut |− s iff L_{2} + Cut |− s′

This lemma together with Cut Elimination for L_{2} entails Cut Elimination for L_{1}. For suppose L_{1} + Cut |− s. Then for some s′, such that s ⇝ s′, L_{2} + Cut |− s′, so L_{2} |− s′, so L_{1} |− s.

7when no variable bound in a is free in Z, b, c, (i) – (ii) become identities

6 Concluding Remarks and Problems

1. It is easily seen that the cut elimination theorem also holds if we allow the associative product connective · to build formulas, together with the proof rules

(· L) \frac{U, x, y, V ⇒ z}{U, x · y, T, V ⇒ z}  (· R) \frac{U ⇒ x,  V ⇒ y}{U, V ⇒ x · y} .

2. The question whether a given sequent is provable in the second order Lambek calculus remains open. By the Cut elimination result, decidability of provability for the calculus including (Cut) is reduced to the same question for the calculus without (Cut). In contrast to the first-order case, cut elimination seems not to guarantee a finite search space for proofs, since apparently there is no useful ‘subterm property’ because of (∀L) and (∃R).

Note that Gabbay[5] proved the undecidability of second order intuitionistic propositional logic. However, this does not directly apply to the second order Lambek calculus with its different quantifier rules and missing structural rules.

3. A particularly interesting fragment of the second order calculus is the one where all quantifiers in formulas must be universal ones in prefix position. Cut-elimination for this fragment apparently does not follow from Theorem 1, because in a cut-free proof of a sequent of the fragment, formulas quantified away in the (∀L) and (∃R) rules need not belong to the the fragment. However, it is easily checked that its proof works as well for this fragment, — even the straightforward extension of Lambek’s proof by induction on the complexity of Cuts does. Again, the question whether decidability of provability holds for this fragment is left open.

4. We have not discussed semantics of the quantifiers. The ‘standard semantics’ using sets of strings as the value of categories can be extended by interpreting ∀ and ∃ via intersection and union, or least upper and greatest lower bound in residuated partially ordered groups (c.f. Buszkowski[2]). However, there is some doubt whether arbitrary intersection and union give the right denotations from a linguistic point of view. We leave a treatment of the semantics to further investigations.

Acknowledgement

We thank Robert Stärk for proposing to do the proof via Lemma 2 and 3, and for several discussions on how to deal best with renaming of bound variables.

7 Appendix

7.1 Proof of Change of Bound Variable

Proof For part (i) of the lemma, it suffices to show that c.b.v.’s preserve derivability in L_{1}^{0}, which we show by induction on the number of nodes. A proof of size 1 must be x ⇒ x, where x has zero complexity, and then x bears the relation ∼ only to itself, so there is nothing to show. So now suppose the statement is true for all proofs of size less than some h, and consider some arbitrary proof, γ of size h, with root r, and some x chosen in r as the category to undergo the c.b.v.

We can make a first division into cases according to whether the category, x, in r is the active category. In the case that x is not the active category, then r is concluded by some rule R, from some r_{1}, containing x, and possibly one further sequent, r_{2}. See proof (6a) below:

a ⋮1 ⋮2 r_{1}[x] r_{2}R r[x]  b  ⋮1′  ⋮2 r_{1}[x′/x] r_{2}R r[x′/x] (6)

1) is of size less than h, and so by induction there is an L_{1}^{0} proof, 1′), of r_{1}[x′/x] for any x′ ∼ x. The rule R will allow the deduction of the desired r[x′/x] from r_{1}[x′/x] and r_{2}. See proof (6b) above.

Now suppose that x is the active category. We make a division into cases according to the particular inference introducing the main connective of x. The cases for the slash connectives are trivial, so we consider just the quantifier cases, and of these just the ∀ cases, as the ∃ cases are parallel.

• x = ∀X.y and x is an antecedent. We have for γ, a proof of the following form, of size h:

⋮1 U, y[a/X], V ⇒ w∀L U, ∀X.y, V ⇒ w

We must consider all z such that ∀X.y ∼ z, for which the following observation is necessary:

if ∀X.y ∼ z then z = ∀X′.y′[X′/X], where y ∼ y′ and X′ ∉ F V (∀X.y)

Proof of the observation: By induction on the length of the sequence of ∼_{1} steps linking ∀X.y to z. There are two cases to be considered for a 1-step c.b.v. on ∀X.y, according to whether the bound variable undergoing the change is bound by a quantifier in y, or is bound by the outermost quantifier, ∀X.

Inner: ∀X.y ∼_{1} ∀X.y′, where y ∼_{1} y′. Clearly ∀X.y′ is of the desired form. Outer: ∀X.y ∼_{1} ∀X′.y[X′/X], if X′ ∉ F V (y). Because y ∼ y, ∀X′.y[X′/X] is of the desired form if X′ ∉ F V (∀X.y), which follows from X′ ∉ F V (y).

So now suppose that for sequences of ∼_{1} steps of length < n, any z derived from ∀X.y by such a sequence is of the desired form, and consider an arbitrary sequence of length n. So at the penultimate step we have a z_{n−1} of the form ∀X′.y′[X′/X], where y ∼ y′,and X′ ∉ F V (∀X.y). We consider the two possibilities for the nth step:

Inner: ∀X′.y′[X′/X] ∼_{1} ∀X′.Φ, where y′[X′/X] ∼_{1} Φ. Therefore for some y′′. y′ ∼ y′′, Φ = y′′[X′/X]. By the transitivity of ∼, y ∼ y′′. Therefore, ∀X′.Φ, i.e. ∀X′.y′′[X′/X], is of the desired form. Outer: ∀X′.y′[X′/X] ∼_{1} ∀X′′.y′[X′/X][X′′/X′], where X′′ ∉ F V (y′[X′/X]). Now X′ ∉ F V (∀X.y) implies y′[X′/X][X′′/X′] ∼ y′[X′′/X]. So for some y′′, y′ ∼ y′′, y′[X′/X][X′′/X′] = y′′[X′′/X]. So, ∀X′′.y′[X′/X][X′′/X′], i.e. ∀X′′.y′′[X′′/X] will be of the desired form if X′′ ∉ F V (∀X.y). We have X′′ ∉ F V (y′[X′/X]), which implies X′′ ∉ F V (y[X′/X]). Unless X′′ = X, this implies X′′ ∉ F V (y), which is sufficient for X′′ ∉ F V (∀X.y). If X′′ = X, then clearly also X′′ ∉ F V (∀X.y)

End of proof of the observation The proof establishing the claim then is:

⋮1′ U, y′[X′/X][a/X′], V ⇒ w∀L U, ∀X′.y′[X′/X], V ⇒ w

The inductive hypothesis guarantees the upper proof, using y[X′/X][a/X′] ∼ y[a/X] (because X′ ∉ F V (∀X.y)).

• x = ∀X.y and x is an succedent. We have a proof of the following form, of size h:

⋮1 T ⇒ y  ∀R T ⇒ ∀X′.y[X′/X] X ∉ F V (T), X′ ∉ F V (∀X.y)

We must consider all z such that ∀X′.y[X′/X] ∼ z, where X′ ∉ F V (∀X.y), for which we use the following observation:

if ∀X′.y[X′/X] ∼ z, where X′ ∉ F V (∀X.y), then z = ∀X′′.y′[X′′/X], y ∼ y′, X′′ ∉

F V (∀X.y).

This follows from the observation that was made in the preceding case. The proof which establishes the claim is:

⋮1′ T ⇒ y′  ∀R T ⇒ ∀X′′.y′[X′′/X] X ∉ F V (T), X′′ ∉ F V (∀X.y′)

The existence of the upper subproof is given by induction. That X′′ ∉ F V (∀X.y′), follows from X′′ ∉ F V (∀X.y).

To show part (ii) of the lemma, it is sufficient to show that c.b.v’s preserve derivability in L_{1}^{0} + Cut, the proof for which will be exactly like that above with the addition of the case for Cut, which will be trivial.

End of Proof

We have shown that c.b.v’s preserve derivability in L_{1} (and L_{1} + Cut). Therefore, the addition of a CBV rule to L_{1} (or L_{1} + Cut) would yield no new sequents. The other rules of L_{1} will be referred to as its ‘logical’ rules.

7.2 Proof of Substitution

Proof For part (i) of the lemma, it suffices to show the corresponding property for L_{1} + CBV, which we do by induction on the size of the proof, this time defining size to ignore CBV steps. It turns out to be necessary to prove that size is preserved in the substitution. L_{1} + CBV will be referred to as L_{1}^{CBV}.

Proofs of size 1 can consist only of a possibly empty series of CBV steps leading from an axiom form sequent, x ⇒ x. First consider the case that there are no CBV steps. Then we simply observe that x[a/Z] ⇒ x[a/Z] is still an axiom form sequent, and has a size 1 proof. Now suppose for some n, we have preservation of derivability under substitution for proofs consisting of an axiom followed by less than n CBV steps. Consider a proof, of r_{n}, consisting of n CBV steps leading from an axiom. We seek a proof of r_{n}[a/Z]. Call the sequent from which r_{n} is obtained r_{n−1}. We have r_{n−1} ∼ r_{n}. Therefore r_{n−1}[a/Z] ∼ r_{n}[a/Z], and so if we had a proof of r_{n−1}[a/Z], we could obtain a proof of r_{n}[a/Z] by adding one CBV step. But we have a proof of r_{n−1}, so by induction we have a proof of r_{n−1}[a/Z], of size 1.

So now suppose that for all proofs of size less than some h, the root remains provable, and with the same size, after a substitution throughout for a free variable. We take some arbitrary proof of size h, and consider what its last possible step could be. As the other cases are trivial we consider just the quantifier cases, and of these just the ∀ cases, because the ∃ cases are parallel.

• Last step is (∀L). We have an L_{2} proof, of size h:

⋮1 U, y[b/X], V ⇒ w∀L U, ∀X.y, V ⇒ w

Choose X′ ∉ F V (a, y, Z). The proof establishing the claim is:

⋮ ; U[a/Z], y[b/X][a/Z], V [a/Z] ⇒ w[a/Z]  CBV U[a/Z], y[X′/X][a/Z][b[a/Z]/X′], V [a/Z] ⇒ w[a/Z]∀L U[a/Z], ∀X′(y[X′/X][a/Z]), V [a/Z] ⇒ w[a/Z]CBV U[a/Z], (∀X.y)[a/Z], V [a/Z] ⇒ w[a/Z]

The upper proof is given under the inductive hypothesis. For the lower CBV step we use where X′ is a variable ∉ F V (a, y, Z):

(∀X.y)[a/Z] ∼ (∀X′.y[X′/X])[a/Z] ≡ (∀X′.y[X′/X][a/Z])

and for the upper:

y[b/X][a/Z] ∼ y[X′/X][b/X′][a/Z] ∼ y[X′/X][a/Z][b[a/Z]/X′]

• Last step is ∀R. So we have a proof of the following form, with size h:

⋮1 T ⇒ y  ∀R T ⇒ ∀X′.y[X′/X] X ∉ F V (T), X′ ∉ F V (∀X.y)

Let X′′ be a variable ∉ F V (T, y, a, Z, X′). The proof establishing the claim is:

⋮1′ T [a/Z] ⇒ y[X′′/X][a/Z] ∀R T [a/Z] ⇒ (∀X′′.y[X′′/X])[a/Z]CBV T [a/Z] ⇒ (∀X′.y[X′/X])[a/Z]

The upper proof is obtained by two applications of the inductive hypothesis, for the substitutions [X′′/X] and [a/Z]. For the (∀R) step, note that ∀X′′(y[X′′/X][a/Z]) = (∀X′′.y[X′′/X])[a/Z], and that X′′ ∉ F V (T [a/Z]). For the CBV step we use:

∀X′.y[X′/X] ∼ ∀X′′.y[X′/X][X′′/X]

y[X′/X][X′′/X′] ∼ y[X′′/X]

• Last step is CBV. This last CBV step may be preceded by n other CBV steps.

When the number of preceding CBV steps is zero, r is proved from a sequent r_{0}, which itself has a proof of size h, whose last step is not CBV. This is a case already considered, and so there is a proof r_{0}[a/Z]. Since r_{0}[a/Z] ∼ r[a/Z], adding a last CBV step will give the desired proof.

For the case where the number of preceding CBV steps is non-zero, we reason exactly as we did in the corresponding case concerning size 1 proofs.

For part (ii) of the lemma, including Cut, it again suffices to show the corresponding property for L_{1} + Cut + CBV. The proof of this will be exactly as above, with addition of a case for Cut, which is trivial.

End of Proof

7.3 Proof of Equivalence of L_{1} and L_{2}

To prove this lemma we use the preceding lemmas for change of bound variable and substitution in L_{1}. Besides these we assume (a) a change of bound variable lemma for L_{2}, and (b) that in L_{1}^{CBV}, when a proof ends with a logical step, followed by a CBV, the order of these may be interchanged, and without changing the size of the proof. For substitution according to the L_{1} or L_{2} definitions we will use [z/Z]_{1} or [z/Z]_{2}.

Proof For part (i) of the lemma, first note that for L_{1}, for any s, s′ such that s ⇝ s′, L_{1} |− s iff L_{1} |− s′. So it will suffice to show, for all clean s, L_{1} |− s iff L_{2} |− s.

\underline{Left to Right}

Since L_{1} is equivalent to L_{1}^{CBV}, it will suffice to show L_{1}^{CBV} |−s implies L_{2} |−s, which will be shown by induction on the size of the L_{1}^{CBV} proof, ignoring CBV steps in the size.

A size 1 proof is an axiom, followed by m CBV steps (m ≥ 0). When m = 0, we have just an axiom in L_{1} and this is an axiom also in L_{2}. As at all stages of the CBV sequence there are only two categories to which a c.b.v. can be applied, it is sufficient to consider CBV sequences of length ≤ 2. When m = 1, we have a proof of s by CBV from some axiom x ⇒ x. Because s is clean, so is x ⇒ x. So L_{2} derives x ⇒ x, and by c.b.v in L_{2}, L_{2} derives s. When m = 2, the root is x′ ⇒ x′′, where x ∼ x′, and x ∼ x′′. Because x′ is clean, L_{2} derives x′ ⇒ x′. x′′ is also clean, and because x′ ∼ x′′, by c.b.v. in L_{2}, L_{2} derives x′ ⇒ x′′.

Suppose the claim for all proofs of size less than n, and consider an L_{1}^{CBV} proof of size n. The cases where the last step is a Slash rule are trivial, so we consider just the remaining cases. First note that where x, y, Z are clean, x[y/Z]_{1} ≡ x[y/Z]_{2}.

• (∀L) is the last step. The proof introduces a category ∀X.y. For some clean y′, Z, Z not in the scope of ∀X in y′, y = y′[X/Z]_{1}(= y′[X/Z]_{2}). We have a L_{1}^{CBV} proof of size n:

⋮ ; U, y′[X/Z]_{1}[x/X]_{1}, V ⇒ w

∀L

U, ∀Xy′[X/Z]_{1}, V ⇒ w Let x′ be derived from x by ‘cleaning’ bound variables. As y′[X/Z]_{1}[x/X]_{1} ∼ y′[X/Z]_{1}[x′/X]_{1}, we have (in L_{1}^{CBV}):

⋮ ; U, y′[X/Z]_{1}[x/X]_{1}, V ⇒ w

CBV

U, y′[X/Z]_{1}[x′/Z]_{1}, V ⇒ w

For each X′ ∈ fv(x′) such that X occurs in the scope of ∀X′ in y, pick an odd X̃′ ∉ fv(U, y, x, V, w, X), and substitute for X′ in x′. Call the result x̃′. From the above, there is a L_{1}^{CBV} proof, size n − 1 of U[X̃′/X′]_{1}, y′[X/Z]_{1}[x′/X]_{1}[X̃′/X′]_{1}, V [X̃′/X′]_{1} ⇒ w[X̃′/X′]_{1}. Because y′[X/Z]_{1}[x′/X]_{1}[X̃′/X′] ∼ y′[X/Z]_{1}[x̃′/X]_{1}, there is a L_{1}^{CBV} proof, size n − 1:

⋮ ; U[X̃′/X′]_{1}, y′[X/Z]_{1}[x̃′/X]_{1}, V [X̃′/X′]_{1} ⇒ w[X̃′/X′]_{1}

of U[X̃′/X′]_{2}, y′[x̃′/Z]_{2}, V [X̃′/X′]_{2} ⇒ w[X̃′/X′]_{2}. Because all the categories are clean, we have by induction a proof of the same sequent in L_{2}. We may add a step of (∀ L) to get an L_{2} proof:

⋮ ; U[X̃′/X′]_{2}, y′[x̃′/Z]_{2}, V [X̃′/X′]_{2} ⇒ w[X̃′/X′]_{2} ∀L U[X̃′/X′]_{2}, ∀Xy′[X/Z]_{2}, V [X̃′/X′]_{2} ⇒ w[X̃′/X′]_{2}

of U[X̃′/X′]_{2}, (∀Xy′[X/Z]_{2})[X̃′/X′]_{2}, V [X̃′/X′]_{2} ⇒ w[X̃′/X′]_{2}. Subsitution throughout this will give the desired sequent, so there will be an L_{2} proof of it

• (∀R) is the last step. We have a L_{1}^{CBV} proof of size n:

⋮ ; T ⇒ y  ∀ R T ⇒ ∀X′y[X′/X]  {X ∉ fv(T), \atop X′ ∉ fv(∀Xy)}

For some clean y′, Z, Z not in the scope of ∀X′ in y′, we have y[X′/X]_{1} = y′[X′/Z]_{1} = y′[X′/Z]_{2}. We seek an L_{2} proof of T ⇒ ∀X′y′[X′/Z]_{2}. We can assume Z ∉ fv(T). There exists a L_{1}^{CBV} proof:

⋮ ; T ⇒ y[Z/X]_{2}

CBV T ⇒ y′

The subproof is given by the substitution [Z/X], and for the CBV step we use that y′ ∼ y[Z/X]. Therefore the L_{2} proof establishing the claim is:

⋮ ; T ⇒ y′  ∀ R T ⇒ ∀X′y′[X′/Z]_{2} Z ∉ fv(T)

The upper proof is given by induction.

• The proof ends in a CBV sequence. Some logical step immediately precedes the CBV sequence. We use the fact that a logical step and a CBV step can be interchanged and without change of size. Therefore proofs of size n ending in a CBV sequence imply the existence of proofs of size n ending in a logical step, which is then a case already considered.

\underline{Right to Left}

All but the quantifier cases are trivial.

• (∀L) is the last step. We have an L_{2} proof, of size n:

⋮ ; U, y[z/Z]_{2}, V ⇒ w ∀L U, ∀Xy[X/Z]_{2}, V ⇒ w

y is clean, and Z does not occur in the scope of ∀X. By induction we have an L_{1}^{CBV} proof of U, y[z/Z]_{1}, V ⇒ w. Because X ∉ fv(y), and no variable free in z is bound in y, y[X/Z]_{1}[z/X]_{1} = y[z/Z]_{1}. Therefore the proof establishing the claim is

⋮ ; U, y[X/Z]_{1}[z/X]_{1}, V ⇒ w

∀L

U, ∀Xy[X/Z]_{1}, V ⇒ w

• (∀R) is the last step. We have an L_{2} proof of size n:

⋮ ; T ⇒ y  ∀ R T ⇒ ∀Xy[X/Z]_{2}  Z ∉ fv(T)

As usual Z is assumed not in the scope of ∀X in y. For some Z̃ ∉ fv(T, y, Z), let ỹ = y[Z̃/Z]_{2}. By the substitution lemma for L_{2}, we have an L_{2} proof, size n − 1 of T [Z̃/Z]_{2} ⇒ y[Z̃/Z]_{2}, which is in fact a proof of T ⇒ ỹ. By induction this may be also proved in L_{1}^{CBV}. Then because y[X/Z]_{1} = ỹ[X/Z̃]_{1}, by the choice of Z̃, the proof establishing the claim is

⋮ ; T ⇒ y  ∀ R T ⇒ ∀Xỹ[X/Z̃]_{1}  Z̃ ∉ fv(T)

The second part of the lemma, concerning the versions of the calculi with Cut, involves the same proof as above with the addition of a case for Cut, which is a trivial case.

End of Proof

References

[1] Y. Bar-Hillel. A quasi-arithmetical notation for syntactic description. Language, 29:47–58, 1953.

[2] W. Buszkowski. Completeness results for Lambek syntactic calculus. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 32:13–28, 1986.

[3] M. Emms. Polymorphic quantifiers. In M. S. L. Torenvliet, editor, Seventh Amsterdam Colloquium, pages 139–163. Center for Cognitive Science, University of Edinburgh, 1989.

[4] M. T. Emms. Logical Ambiguity. PhD thesis, University of Edinburgh, 1992.

[5] D. M. Gabbay. Semantical Investigations in Heyting’s Intuitionistic Logic, volume 148 of Synthese Library. D. Reidel, Dordrecht, 1981.

[6] R. Hindley and J. P. Seldin. Introduction to Combinators and λ-Calculus. Cambridge University Press, Cambridge, 1986.

[7] J. Lambek. The mathematics of sentence structure. American Mathematical Monthley, 65:154– 170, 1958.

[8] M. Moortgat. The logic of discontinuous type constructors (draft). Tilburg Symposium on Discontinuous Constituents, 1990.