Lambek Semantics

Herman Hendriks

… ‘oδòς ’άνω κάτω μία καὶ ‘ωυτή.

… [the] way up [and] down [is] one and [the] same.

Heraclitus, Diels–Kranz 22 B 60

When Lambek (1958) introduced his syntactic calculus, he showed that it is equivalent to a sequent axiomatization, the Lambek-Gentzen sequent calculus (henceforth: L). The calculus L defines a general notion of derivability in the following sense: an expression consisting of the lexical items e_{1}, …, e_{n} of respective categories c_{1}, …, c_{n} is parsed as belonging to a certain category c if and only if the statement ‘c_{1}, …, c_{n} is a c’ (written as a so-called sequent c_{1}, …, c_{n} ⊢ c) can be derived as a theorem of the system. Thus, grammatical derivations are reduced to logical deductions, giving rise to the slogan ‘parsing as deduction’. The calculus L contains, among other rules, the so-called Cut rule. By proving that the set of theorems of L is not increased by adding Cut, Lambek established the decidability of L: for an arbitrary sequent the proof procedure is guaranteed to answer the question whether the sequent is valid after a finite number of steps. The proof of this fact is constructive: Lambek defined an algorithm which enables one to eliminate all occurrences of Cut in proofs.

The semantic interpretation procedure of Moortgat (1988) for productfree L is a sequent implementation of Van Benthem’s term construction algorithm for the natural deduction formulation of L (1986, Chapter 7; 1991). In this semantics, the interpretations of a grammatical expression (derivable sequent) are directly determined by the proofs of its validity in the syntactic calculus. The present paper provides an alternative formulation of the Van Benthem/Moortgat semantics for L (which is introduced in Section 1) and uses it to prove the following results. Section 2 contains a straightforward proof of a semantic version of Lambek’s Cut elimination theorem which entails that L is semantically decidable as well: the result of applying Lambek’s Cut elimination algorithm is a derivation which is semantically equivalent to the original derivation. Section 3 is devoted to further normalization of L, resulting in a sequent calculus L* which is put to use in the subsequent sections. First, we show in Section 4 that L* provides a solution to the so-called ‘spurious ambiguity problem’ – the problem that different proofs of a given sequent may yield one and the same semantic interpretation. In L*, each interpretation of a sequent corresponds to exactly one proof. In Section 5, we use L* to prove that an explicit elaboration of the suggestions in Moortgat’s ‘Unambiguous Proof Representations for the Lambek Calculus’ (1990) leads to representations of L-proofs of sequents with atomic goal categories which ‘summarize’ L* derivations and are, hence, indeed ‘unambiguous’, i.e., devoid of spurious ambiguity. A comparison of L* with the proof nets proposed in Roorda (1991), on the other hand, shows that every L* proof corresponds to a non-singleton set of proof nets. Finally, with the help of L* we are able to show in Section 6 that syntactic recognition within L can be mimicked using one basic category only, thus extending a result of Ponse (1988) for LP, the Lambek calculus with permutation, to L proper.

1 Introduction

We will employ the following definitions of the notions of category and sequent:

Let atom be some finite set of atomic categories (none of which is of the form (a/b) or (b\a)). Then cat, the set of categories based on atom, is the smallest set such that (i) atom ⊆ cat, and (ii) if a ∈ cat and b ∈ cat, then (a/b) ∈ cat and (b\a) ∈ cat.

(1)

A sequent is an expression T ⊢ c, where T is a finite non-empty sequence of categories and c ∈ cat. (So, T = c_{1}, …, c_{n}, where n > 0 and for all i, 1 ≤ i ≤ n: c_{i} ∈ cat.)

(2)

Outermost brackets of categories will be omitted. The sequence of categories c_{1}, …, c_{n} will be called the left-hand side of a sequent c_{1}, …, c_{n} ⊢ c, and the single category c its right-hand side or goal.

The product-free Lambek-Gentzen sequent calculus L consists of a set of axioms plus five inference rules: /L, \L, /R, \R and Cut. The axioms and rules are listed in (3) and (4), respectively. In (4), a, b, and c denote arbitrary categories and T, U, and V arbitrary finite sequences of categories, of which T is non-empty.

(3) axiom, the set of axioms of L, is the set {c ⊢ c | c ∈ cat}.

\begin{aligned}& T ⊢ b U, a, V ⊢ c [/L] U, a/b, T, V ⊢ c & T ⊢ b U, a, V ⊢ c [\L] U, T, b\a, V ⊢ c \\ (4) \end{aligned}

T, b ⊢ a [/R] T ⊢ a/b  b, T ⊢ a [\R] T ⊢ b\a

T ⊢ a U, a, V ⊢ c [Cut] U, T, V ⊢ c

Moortgat (1988) proposes a semantics for L in which every category occurrence c in a derivation is assigned some typed lambda term γ. The type of γ depends on c. For categories c ∈ atom, some type assignment type(c) is assumed, and the function type is extended to non-atomic categories by the stipulation that type(a/b) = type(b\a) = (type(b), type(a)). In this semantics, which is given in (5) below, the axioms of L correspond to identity, the rules /L and \L to functional application, the rules /R and \R to lambda abstraction, and the Cut rule to substitution.^{1} The respective assignment of terms γ_{1}, …, γ_{n}, γ to categories c_{1}, …, c_{n}, c in a derivable sequent c_{1}, …, c_{n} ⊢ c is usually written as c_{1} :γ_{1}, …, c_{n}:γ_{n} ⊢ c:γ.

syntax:  semantics:

(5)

c ⊢ c [axiom]  γ ⊢ γ
T ⊢ b U, a, V ⊢ c [/L] U, a/b, T, V ⊢ c  T′ ⊢ β U′, ϕ(β), V′ ⊢ γ U′, ϕ, T′, V′ ⊢ γ

T ⊢ b U, a, V ⊢ c [\L] U, T, b\a, V ⊢ c  T′ ⊢ β U′, ϕ(β), V′ ⊢ γ U′, T′, ϕ, V′ ⊢ γ

T, b ⊢ a [/R] T ⊢ a/b  {T′, v ⊢ α \atop T′ ⊢ λv.α}

b, T ⊢ a [\R] T ⊢ b\a  {v, T′ ⊢ α \atop T′ ⊢ λv.α}

T ⊢ a U, a, V ⊢ c [Cut] U, T, V ⊢ c  T′ ⊢ α U′, α, V′ ⊢ γ U′, T′, V′ ⊢ γ

1Viz., the substitution of T′ (which yields α) for α in U′, α, V′ ⊢ γ.

In (5), only the terms of the ‘active’ categories are indicated separately. The expression v denotes a variable of type type(b), while α, β, γ and ϕ denote terms of type type(a), type(b), type(c), and (type(b), type(a)), respectively. The expressions T′, U′ and V′ refer to the sequences of terms assigned to the sequences of ‘inactive’ categories T, U, and V. Thus, the terms assigned to the categories in T, U, V are identical in premise and conclusion.

The interpretation which a proof with conclusion c_{1} :γ_{1}, …, c_{n}:γ_{n} ⊢ c:γ assigns to a sequence of lexical expressions e_{1}, …, e_{n} of categories c_{1}, …, c_{n} with interpretations e′_{1}, …, e′_{n} is obtained by performing the simultaneous substitution [γ_{1} :=e′_{1}, …, γ_{n}:=e′_{n}] in the term γ assigned to the goal of the conclusion sequent: γ[γ_{1} :=e′_{1}, …, γ_{n}:=e′_{n}].

For example: let the lexical expressions someone, bores and everyone be assigned the categories (s/n)\s, (n\s)/n and (s/n)\s, as well as the interpretations λP.∃z P (z), bore and λP.∀z P (z) of type ((e, t), t), (e, (e, t)) and ((e, t), t), respectively. Then the following derivation shows that Someone bores everyone is of category s:

(6) _{\begin{matrix}\begin{matrix}n ⊢ n & ^{n ⊢ n s ⊢ s [\L] n, n\s ⊢ s} & [/L] & n, (n\s)/n, n ⊢ s \\ [/R] \\ n, (n\s)/n ⊢ s/n \end{matrix} & s ⊢ s & [\L] & n, (n\s)/n, (s/n)\s ⊢ s \\ [\R] \\ (n\s)/n, (s/n)\s ⊢ n\s \end{matrix} s ⊢ s [/L] s/(n\s), (n\s)/n, (s/n)\s ⊢ s}

An interpretation of derivation (6) is given in (7), where u, v, w, x, and y represent variables of type e, e, ((e, t), t), (e, (e, t)) and ((e, t), t), respectively:

\begin{matrix}u ⊢ u & x(v)(u) ⊢ x(v)(u) & v ⊢ v & u, x(v) ⊢ x(v)(u) & u, x, v ⊢ x(v)(u) & u, x ⊢ λv.x(v)(u) & y(λv.x(v)(u)) ⊢ y(λv.x(v)(u)) & u, x, y ⊢ y(λv.x(v)(u)) & x, y ⊢ λu.y(λv.x(v)(u)) & w(λu.y(λv.x(v)(u))) ⊢ w(λu.y(λv.x(v)(u))) & w, x, y ⊢ w(λu.y(λv.x(v)(u))) \\ (7) \end{matrix}

Performing the simultaneous substitution (8) in w(λu.y(λv.x(v)(u))), the term assigned to the conclusion goal in (7), supplies the sentence Someone bores everyone with an interpretation equivalent to ∃u∀v bore(v)(u).

{[w:=λP.∃z P (z), x:=bore, y:=λP.∀z P (z)] \atop (8)}

Note, first, that semantics (5) needs to be supplemented with at least the following condition, which guarantees that the abstractions introduced by \R and /R bind only one variable occurrence:

If T:T′ ⊢ c:λv.γ is the conclusion of a \R or /R inference, then v does not occur freely in T′.

(9)

For instance, if – violating this condition but in keeping with (5) – all occurrences of v in (7) are replaced by u, then the conclusion goal of (6) is assigned the term w(λu.y(λu.x(u)(u))), which results in the incorrect interpretation ∃u∀u bore(u)(u), ‘Everyone bores himself’, for Someone bores everyone.

And, second, note that simultaneous substitution is not always welldefined for semantics (5), which allows complex terms and different occurrences of the same term in the left-hand side of sequents. For (i) it is unclear what is meant by a substitution of a term for a complex term (this requires at least some extension of the notion of ‘free occurrence of’ to terms other than variables), and (ii) simultaneous substitution does not make sense when the same term is to be substituted twice. The problem reappears at deeper levels, e.g., when a left-hand side category c_{i} is assigned a term γ_{i} which also occurs as a subterm of a term γ_{j} assigned to another left-hand side category c_{j}. Moreover, this substitution problem causes a complication in the proof of ‘semantic Cut elimination’.^{2}

2Consider Moortgat’s treatment (1990, p. 151) of the crucial case 5 of Lambek’s Cut elimination algorithm (cf. section 2 below), in which:

[A]T, d:v ⊢ b:β [/R] T ⊢ b/d:λv.β ^{V_{1} ⊢ d:δ ^{[B]}U, b:[λv.β](δ), V_{2} ⊢ c:γ [/L] U, b/d:λv.β, V_{1}, V_{2} ⊢ c:γ} [Cut] U, T, V_{1}, V_{2} ⊢ c:γ is replaced by:

V_{1} ⊢ d:δ^{^{[A′]}T, d:δ ⊢ b:β[v:=δ] ^{[B′]}U, b:β[v:=δ], V_{2} ⊢ c:γ[[λv.β](δ):=β[v:=δ]] [Cut] U, T, d:δ, V_{2} ⊢ c:γ[[λv.β](δ):=β[v:=δ]]} [Cut] U, T, V_{1}, V_{2} ⊢ c:γ[[λv.β](δ):=β[v:=δ]] (The terms assigned to U, T, V_{1} and V_{2} have been omitted.) In order to be able to make the transition from [A] and [B] to [A′] and [B′], respectively, Moortgat needs something

These considerations suggest that it is more natural to have a semantics which always yields proofs of sequents c_{1} : v_{1}, …, c_{n} : v_{n} ⊢ c: γ where the terms v_{1}, …, v_{n} constitute a sequence of different variables. Therefore, the alternative semantics (10) which will be used in the following sections is based on the same category-to-type assignment as semantics (5), but differs from (5) as regards the terms it assigns to the categories in a derivable sequent c_{1}, …, c_{n} ⊢ c. For the left-hand side categories c_{i} (1 ≤ i ≤ n), this interpretation is some variable v_{i} of type type(c_{i}), whereas for the righthand side category c, it is a (possibly complex) term γ of type type(c): c_{1} :v_{1}, …, c_{n}:v_{n} ⊢ c:γ.

In (10), u, v, x and w represent variables of type type(a), type(b), type(c) and (type(b), type(a)); α, β and γ denote terms of type type(a), type(b) and type(c); and T′, U′ and V′ refer to the sequences of variables assigned to the sequences of categories T, U and V. Again, only the terms of the active categories are indicated separately, and the terms of other categories are identical in premise and conclusion. The expression γ[u:=α]

like: ($) If π[U:U′, a:α, V :V′ ⊢_{(5)} c:γ], then for all terms α′ of type type(a):

π[U:U′, a:α′, V :V′ ⊢_{(5)} c:γ[α:=α′]].

(We let π[c_{1} :γ_{1}, …, c_{n}:γ_{n} ⊢_{(5)} c:γ] represent that semantics (5) assigns the respective terms γ_{1}, … γ_{n}, γ to the categories c_{1}, …, c_{n}, c in the conclusion sequent c_{1}, …, c_{n} ⊢ c of π. Note that [α:=α′] is more than mere substitution for free variable occurrences; it also involves replacement of compound terms – cf. the transition from [B] to [B′].) But such a lemma is not available, as can be seen from the following derivations – where α, α′, β and γ are terms of type type(a), type(a), type((a\b)/a) and (type(a), type(a)), respectively:

(i)  a:α ⊢ a:α ^{a:γ(α) ⊢ a:γ(α) b:β(α)(γ(α)) ⊢ b:β(α)(γ(α)) [/L] b/a:β(α), a:γ(α) ⊢ b:β(α)(γ(α))} [\L] a:α, a\(b/a):β, a:γ(α) ⊢ b:β(α)(γ(α))

(ii) a:α′ ⊢ a:α′ ^{a:γ(α) ⊢ a:γ(α) b:β(α′)(γ(α)) ⊢ b:β(α′)(γ(α)) [/L] b/a:β(α′), a:γ(α) ⊢ b:β(α′)(γ(α))} [\L] a:α′, a\(b/a):β, a:γ(α) ⊢ b:β(α′)(γ(α))

Since no variable-binding operator is present, it seems plausible to assume that both occurrences of α in the term assigned to the conclusion goal of derivation (i) are free and that, hence, [β(α)(γ(α))][α:=α′] is the term β(α′)(γ(α′)). But, refuting ($), the term assigned to the conclusion goal of (ii) is β(α′)(γ(α)).

If, however, condition (9) is met, then in every sequent T : T′ ⊢ c: γ the sequence T′ of left-hand side terms has the same free variables as γ, and the following can be established (where v is a variable and α is a term, both of type type(a)):

(#) If π[T :T′ ⊢_{(5)} c:γ], then π[T :T′[v:=α] ⊢_{(5)} c:γ[v:=α]].

denotes the result of substituting term α for all free occurrences of u in γ.

syntax:  semantics:

(10)

c ⊢ c [axiom]  x ⊢ x
T ⊢ b U, a, V ⊢ c [/L] U, a/b, T, V ⊢ c  T′ ⊢ β  U′, u, V′ ⊢ γ U′, w, T′, V′ ⊢ γ[u:=w(β)]

T ⊢ b U, a, V ⊢ c [\L] U, T, b\a, V ⊢ c  T′ ⊢ β  U′, u, V′ ⊢ γ U′, T′, w, V′ ⊢ γ[u:=w(β)]

T, b ⊢ a [/R] T ⊢ a/b  {T′, v ⊢ α \atop T′ ⊢ λv.α}

b, T ⊢ a [\R] T ⊢ b\a  {v, T′ ⊢ α \atop T′ ⊢ λv.α}

T ⊢ a U, a, V ⊢ c [Cut] U, T, V ⊢ c  T′ ⊢ α U′, u, V′ ⊢ γ U′, T′, V′ ⊢ γ[u:=α]

In the context of a proof, we will assume that all variables x and w assigned to axiom instances or introduced in the conclusions of /L or \L inferences are different. Observe that, consequently, (i) the variables v_{1}, … v_{n} assigned to the left-hand side of a sequent c_{1}, …, c_{n} ⊢ c are all different; (ii) these variables v_{1}, … v_{n} make up the free variables of the term γ assigned to the goal c; and (iii) each variable v_{1}, … v_{n} occurs exactly once in γ.

Note that semantics (10) is more ‘compositional’ than (5), in that the complexity of the term γ assigned to the goal of a sequent c_{1}, …, c_{n} ⊢ c increases with the length of the proof of that sequent. This property makes semantics (10) more perspicuous, which facilitates proving things about it. In semantics (5), on the other hand, we see that the rule /L assigns a term ϕ to its conclusion category a/b which is less complex than the term ϕ(β) assigned to the category a in its right-hand side premise. (The same holds for \L.) Moreover, semantics (10) is easier to use in practice, since it entails considerably less duplication of semantic information than (5), witness its interpretation of derivation (6):

(11) \begin{matrix}\begin{matrix}v ⊢ v & ^{u ⊢ u z ⊢ z u, z′ ⊢ z′(u)} & u, x, v ⊢ x(v)(u) \\ u, x ⊢ λv.x(v)(u) \end{matrix} & z′′ ⊢ z′′ & u, x, y ⊢ y(λv.x(v)(u)) \\ x, y ⊢ λu.y(λv.x(v)(u)) \end{matrix} z′′′ ⊢ z′′′ w, x, y ⊢ w(λu.y(λv.x(v)(u)))

Still, to the extent that semantics (5) is well-behaved, it is essentially the same as semantics (10), on account of the following relationship. Suppose that the assignment of terms by (5) is restricted by condition (9), and, for i ∈ {5, 10}, let π[c_{1} :γ_{1}, …, c_{n}:γ_{n} ⊢_{(i)} c:γ] represent that semantics (i) assigns the respective terms γ_{1}, …, γ_{n}, γ to the categories c_{1}, …, c_{n}, c in the conclusion sequent c_{1}, …, c_{n} ⊢ c of proof π. Then the following holds:

π[c_{1} :v_{1}, …, c_{n}:v_{n} ⊢_{(10)} c:γ] if and only if
π[c_{1} :γ_{1}, …, c_{n}:γ_{n} ⊢_{(5)} c:γ[v_{1} :=γ_{1} …, v_{n}:=γ_{n}]] .

(12)

From (12), which is proven by induction on the length of π (where fact (#)

– see footnote 2 – is needed as a lemma for the cases \R and /R), it follows that if the terms γ_{1}, …, γ_{n} of the left-hand side categories c_{1}, …, c_{n} in the conclusion sequent c_{1}, …, c_{n} ⊢ c of π constitute a sequence v_{1}, …, v_{n} of different variables, then semantics (10) assigns a term to the goal category c which is syntactically identical to the term assigned by semantics (5).

2 Cut Elimination and Semantics

Van Benthem (1986) proved that the number of distinct readings for an L-derivable sequent is finite. However, in addition one would like to have an effective method for generating all readings. The availability of such a method could serve practical purposes by providing a solution to the ‘parsing problem’, which is:

… to find all readings for a given string. This is a necessary step if one wants to give a satisfactory parsing algorithm for L. It should be noticed, however, that it is not at all clear which members of the infinite set of derivations for a sentence S in L lead to different readings, and thus, finding all possible readings seems to be problematic to begin with, let alone finding them efficiently. (Bouma (1989))

A possible way of solving this problem is to prove that the result of applying Lambek’s Cut elimination algorithm is a derivation which is semantically equivalent to the original derivation. Then for every derivation of an Lderivable sequent there is a Cut-free derivation with the same interpretation, and we can safely restrict our attention to the (finite number of) Cut-free derivations. Each of the inference rules /L, \L, /R and \R derives its conclusion from one or more premises with a strictly smaller number of occurrences of / and \. Hence establishing the derivability of the premise(s) is more simple than establishing the derivability of the conclusion, and it follows that every sequent has only finitely many Cut-free derivations.

Adapting the proof of Lambek (1958), we will show in this section that sequents in the proof of which the Cut inference rule has been used can also be derived without using Cut, while keeping their semantics the same. That is, Cut is a derived rule of inference which does not yield new theorems, nor new interpretations. This is done in a constructive way: it is possible to transform every proof which makes use of the Cut rule into a Cut-free proof which determines the same interpretation as the original one.

The two base cases of this transformation procedure (case 1 and 2 below) involve Cut inferences where one of the premises is an instance of the axiom scheme c ⊢ c. Here the conclusion coincides with the other premise, and the Cut inference can be eliminated immediately. The recursive cases of the procedure (case 3, 4 and 5 below) work by reduction of what is called the ‘degree’ of the Cut inference. Degree is defined as follows:

(i) The degree d(c) of a category c is defined inductively:
d(c) = 0 for c ∈ atom; d(a/b) = d(b\a) = d(a) + d(b) + 1.
(ii) The degree d(c_{1}, …, c_{n}) of a finite sequence of categories
c_{1}, …, c_{n} equals d(c_{1}) + … + d(c_{n}).
(iii) The degree d(T ⊢ c) of a sequent T ⊢ c equals d(T) + d(c).
(iv) The degree d(α) of a Cut inference α =

T ⊢ a U, a, V ⊢ c U, T, V ⊢ c
equals d(T) + d(U) + d(V) + d(a) + d(c).

(13)

Thus, the degree of a category, a sequence of categories and a sequent is equal to the number of slashes it contains.

Any Cut inference of which at least one premise has been proven without Cut can be turned into one or two new Cut inferences of strictly smaller degree. Since the minimal degree of an inference is zero, these proof transformations will ultimately converge on the base case.

We will now prove

1. that in any application of Cut,

T ⊢ a U, a, V ⊢ c [Cut], U, T, V ⊢ c

of which at least one premise has been proven without Cut,

(a) either the conclusion is identical with one of the premises so that the application of Cut can be eliminated,

(b) or the application of Cut can be replaced by one or two applications of Cut of smaller degree; and

2. that execution of this Cut elimination procedure always leads to semantically equivalent proofs.

There are five main cases:

1: T ⊢ a is an axiom; then T = a and the conclusion coincides with the premise U, a, V ⊢ c.

a ⊢ a U, a, V ⊢ c [Cut] U, a, V ⊢ c  u′ ⊢ u′ U′, u, V′ ⊢ γ [Cut] U′, u′, V′ ⊢ γ[u:=u′]

Cut can be eliminated, for note that the variable u′ does not occur in γ. Hence we also have the interpretation U′, u′, V′ ⊢ γ[u:=u′] for (the subproof of) the premise U, a, V ⊢ c, due to the following fact (which is proven by a straightforward induction on the length of π):

If π[U:U′, a:u, V :V′ ⊢ c:γ] and u′ is a variable of type type(a)
not occurring in γ, then π[U:U′, a:u′, V :V′ ⊢ c:γ[u:=u′] ].

2: U, a, V ⊢ c is an axiom; then U and V are empty, c = a, and the conclusion coincides with the premise T ⊢ a. Cut can be eliminated because the terms α and u[u:=α] assigned to the coinciding premise and conclusion coincide as well:

\begin{matrix}T′ ⊢ α & u ⊢ u & [Cut] & T′ ⊢ u[u:=α] \\ T ⊢ a & a ⊢ a & [Cut] & T ⊢ a \end{matrix}

3: The last step in the proof of T ⊢ a uses a rule but does not introduce the main connective of a. Then T ⊢ a is derived by /L (or \L) from two sequents, one of which has the form T′ ⊢ a, with d(T′) < d(T). Hence we can reverse the order of the rules /L (or \L) and Cut, resulting in a new Cut inference which has smaller degree than the old one. We only consider /L. (\L is analogous.) Then T = P, b/d, Q, R, and we can replace:

Q ⊢ d P, b, R ⊢ a [/L] P, b/d, Q, R ⊢ a U, a, V ⊢ c [Cut] U, P, b/d, Q, R, V ⊢ c

by:

Q ⊢ d ^{P, b, R ⊢ a U, a, V ⊢ c [Cut] U, P, b, R, V ⊢ c} [/L] U, P, b/d, Q, R, V ⊢ c

Semantically, this amounts to replacing:

Q′ ⊢ δ  P′, v, R′ ⊢ α [/L] P′, w, Q′, R′ ⊢ α[v:=w(δ)] U′, u, V′ ⊢ γ [Cut] U′, P′, w, Q′, R′, V ⊢ γ[u:=α[v:=w(δ)]]

by:

Q′ ⊢ δ ^{P′, v, R′ ⊢ α U′, u, V′ ⊢ γ [Cut] U′, P′, v, R′, V′ ⊢ γ[u:=α]}[/L] U′, P′, w, Q′, R′, V′ ⊢ [γ[u:=α]][v:=w(δ)]

The terms γ[u:=α[v:=w(δ)]] and [γ[u:=α]][v:=w(δ)] are identical because v does not occur in γ; hence this replacement of Cut preserves interpretation.

4: The last step in the proof of U, a, V ⊢ c uses one of the rules /L, \L, /R, \R, but does not introduce the main connective of a. Then U, a, V ⊢ c is inferred from one or two sequents, one of which has the form U′, a, V′ ⊢ c′ with d(U′)+d(V′)+d(c′) < d(U)+d(V)+d(c) (since the inference introduces one occurrence of a connective). Again, we can reverse the order of the rules; the new Cut inference has smaller degree than the given one. We only consider \L and \R. (/L and /R are analogous.) 4.1: U, a, V ⊢ c is obtained by \L. Then U, a, V = P, Q, d\b, R. Note that a and d\b are distinct category occurrences (for \L does not introduce the main connective of a). Therefore, there are three possibilities: a is part of P, Q or R (The last subcase, which is analogous to the first one, will not be treated.) 4.1.a: The category a is part of P, so P = P_{1}, a, P_{2}. Replace:

T ⊢ a ^{Q ⊢ d P_{1}, a, P_{2}, b, R ⊢ c [\L] P_{1}, a, P_{2}, Q, d\b, R ⊢ c} [Cut] P_{1}, T, P_{2}, Q, d\b, R ⊢ c

by:

Q ⊢ d ^{T ⊢ a P_{1}, a, P_{2}, b, R ⊢ c [Cut] P_{1}, T, P_{2}, b, R ⊢ c} [\L] P_{1}, T, P_{2}, Q, d\b, R ⊢ c

On the semantic side, this entails the replacement of:

T′ ⊢ α ^{Q′ ⊢ δ  P′_{1}, u, P′_{2}, v, R′ ⊢ γ [\L] P′_{1}, u, P′_{2}, Q′, w, R′ ⊢ γ[v:=w(δ)]} [Cut] P′_{1}, T′, P′_{2}, Q′, w, R′ ⊢ [γ[v:=w(δ)]][u:=α]

by:

Q′ ⊢ δ ^{T′ ⊢ α P′_{1}, u, P′_{2}, v, R′ ⊢ γ [Cut] P′_{1}, T′, P′_{2}, v, R′ ⊢ γ[u:=α]}[\L] P′_{1}, T′, P′_{2}, Q′, w, R′ ⊢ [γ[u:=α]][v:=w(δ)]

The terms [γ[v:=w(δ)]][u:=α] and [γ[u:=α]][v:=w(δ)] are identical, because u and v are different variables, u does not occur in w(δ), and v does not occur in α. 4.1.b: The category a is part of Q, so Q = Q_{1}, a, Q_{2}. Replace:

T ⊢ a ^{Q_{1}, a, Q_{2} ⊢ d P, b, R ⊢ c [\L] P, Q_{1}, a, Q_{2}, d\b, R ⊢ c} [Cut] P, Q_{1}, T, Q_{2}, d\b, R ⊢ c

by:

T ⊢ a Q_{1}, a, Q_{2} ⊢ d [Cut] Q_{1}, T, Q_{2} ⊢ d P, b, R ⊢ c [\L] P, Q_{1}, T, Q_{2}, d\b, R ⊢ c

This entails a semantic replacement of:

T′ ⊢ α ^{Q′_{1}, u, Q′_{2} ⊢ δ  P′, v, R′ ⊢ γ [\L] P′, Q′_{1}, u, Q′_{2}, w, R′ ⊢ γ[v:=w(δ)]} [Cut] P′, Q′_{1}, T′, Q′_{2}, w, R′ ⊢ [γ[v:=w(δ)]][u:=α]

by:

T′ ⊢ α Q′_{1}, u, Q′_{2} ⊢ δ [Cut] Q′_{1}, T′, Q′_{2} ⊢ δ[u:=α] P′, v, R′ ⊢ γ [\L] P′, Q′_{1}, T′, Q′_{2}, w, R′ ⊢ γ[v:=w(δ[u:=α])]

Again, the terms [γ[v:=w(δ)]][u:=α] and γ[v:=w(δ[u:=α])] are identical, for u does not occur in γ, and u and w are different variables. 4.2: U, a, V ⊢ c is obtained by \R. Then c = d\b, and we can replace:

T ⊢ a ^{d, U, a, V ⊢ b [\R] U, a, V ⊢ d\b} [Cut] U, T, V ⊢ d\b

by:

T ⊢ a d, U, a, V ⊢ b [Cut] d, U, T, V ⊢ b [\R] U, T, V ⊢ d\b

This is reflected in the semantic replacement of:

T′ ⊢ α ^{v, U′, u, V′ ⊢ β [\R] U′, u, V′ ⊢ λv.β} [Cut] U′, T′, V′ ⊢ [λv.β][u:=α]

by:

T′ ⊢ α v, U′, u, V′ ⊢ β [Cut] v, U′, T′, V′ ⊢ β[u:=α] [\R] U′, T′, V′ ⊢ λv.[β[u:=α]]

Since u and v are different variables, the term [λv.β][u:=α] is identical to λv.[β[u:=α]].

5: The last steps in the proofs of both T ⊢ a and U, a, V ⊢ c introduce the main connective, / or \, of a. So a = b/d or a = d\b. (Only the /-case is treated here.) We can replace:

T, d ⊢ b [/R] T ⊢ b/d ^{V_{1} ⊢ d U, b, V_{2} ⊢ c [/L] U, b/d, V_{1}, V_{2} ⊢ c} [Cut] U, T, V_{1}, V_{2} ⊢ c

by:

V_{1} ⊢ d ^{T, d ⊢ b U, b, V_{2} ⊢ c [Cut] U, T, d, V_{2} ⊢ c} [Cut] U, T, V_{1}, V_{2} ⊢ c

Semantically, this involves a replacement of:

T′, v ⊢ β [/R] T′ ⊢ λv.β ^{V′_{1} ⊢ δ  U′, u, V′_{2} ⊢ γ [/L] U′, w, V′_{1}, V′_{2} ⊢ γ[u:=w(δ)]} [Cut] U′, T′, V′_{1}, V′_{2} ⊢ [γ[u:=w(δ)]][w:=λv.β]

by:

V′_{1} ⊢ δ ^{T′, v ⊢ β U′, u, V′_{2} ⊢ γ [Cut] U′, T′, v, V′_{2} ⊢ γ[u:=β]} [Cut] U′, T′, V′_{1}, V′_{2} ⊢ [γ[u:=β]][v:=δ]

Because w does not occur in γ, the term [γ[u:=w(δ)]][w:=λv.β] is identical to γ[u:=[w(δ)][w:=λv.β]]. The latter term is identical to γ[u:=[λv.β](δ)], because w does not occur in δ. Since the free variables V′_{1} of δ do not occur in β, they are free for v in β and we can apply β-conversion, with the result [γ[u:=β[v:=δ]]].^{3} As v does not occur in γ, this is the same term as [γ[u:=β]][v:=δ]. □

3 Further Normalization

We have shown that if c_{1} : v_{1}, …, c_{n}: v_{n} ⊢ c: γ is derivable in L, then there is a Cut-free L derivation of c_{1} :v_{1}, …, c_{n}:v_{n} ⊢ c:γ′ such that γ and γ′ are equivalent. Consequently, we only have to consider the Cut-free derivations of a sequent to obtain all its semantic interpretations. But in spite of the fact that a given sequent has only finitely many Cut-free derivations, Cut-less L still suffers from what has been called the ‘spurious ambiguity problem’ (König (1989)), viz., the problem that different proofs of a given sequent may yield one and the same semantic interpretation. When the calculus is actually used for parsing and interpreting expressions, this may entail superfluous work: interpretations will be computed n times instead of once. For example, the sequent c/c, c/c, c ⊢ c has two semantically equivalent Cutfree proofs, viz., (14) and (15), in which the symbol ^{♯} is used to keep track of the active category:

3Thus, case 5 does not involve identity of terms, but equivalence under β-conversion (also called λ-conversion): [λv.γ′](γ′′) = γ′[v:=γ′′] if γ′′ is free for v in γ′.

It takes an induction on the length of the derivation to see that terms γ assigned to conclusion goals in Cut-free proofs are always in β-normal form, i.e., they do not have subterms of the form [λv.γ′](γ′′).

\begin{aligned}& ^{c ⊢ c c ⊢ c [/L] c/c^{♯}, c ⊢ c} c ⊢ c [/L] c/c^{♯}, c/c, c ⊢ c & _{^{x ⊢ x u ⊢ u [/L] y, x ⊢ y(x)} v ⊢ v [/L] z, y, x ⊢ z(y(x))} \\ (14) \end{aligned}

\begin{aligned}& c ⊢ c ^{c ⊢ c c ⊢ c [/L] c/c^{♯}, c ⊢ c} [/L] c/c, c/c^{♯}, c ⊢ c & _{x ⊢ x ^{u ⊢ u v ⊢ v [/L] z, u ⊢ z(u)} [/L] z, y, x ⊢ z(y(x))} \\ (15) \end{aligned}

Of course, not all ambiguity in L is spurious. Some sequents are really ambiguous. The sequent s/(n\s), (n\s)/n, (s/n)\s ⊢ s, for example, has six Cut-free derivations, which are not all equivalent. These derivations are listed below. Each derivation is followed by the interpretation it assigns to its conclusion sequent s/(n\s), (n\s)/n, (s/n)\s ⊢ s:

\begin{matrix}\begin{matrix}\begin{matrix}n ⊢ n & ^{n ⊢ n s ⊢ s [\L] n, n\s^{♯} ⊢ s} & [/L] & n, (n\s)/n^{♯}, n ⊢ s \\ [/R] \\ n, (n\s)/n ⊢ s/n^{♯} \end{matrix} & s ⊢ s & [\L] & n, (n\s)/n, (s/n)\s^{♯} ⊢ s \\ [\R] \\ (n\s)/n, (s/n)\s ⊢ n\s^{♯} \end{matrix} & s ⊢ s & [/L] & s/(n\s)^{♯}, (n\s)/n, (s/n)\s ⊢ s \\ (16) \end{matrix}

u, v, w ⊢ u(λu′.w(λw′.v(w′)(u′)))

(17) \begin{matrix}^{n ⊢ n n\s ⊢ n\s [/L] (n\s)/n^{♯}, n ⊢ n\s} & s ⊢ s & [/L] & s/(n\s)^{♯}, (n\s)/n, n ⊢ s \\ [/R] \\ s/(n\s), (n\s)/n ⊢ s/n^{♯} \end{matrix} s ⊢ s [\L] s/(n\s), (n\s)/n, (s/n)\s^{♯} ⊢ s

u, v, w ⊢ w(λw′.u(v(w′)))

\begin{matrix}\begin{matrix}^{n ⊢ n \begin{matrix}n ⊢ n & s ⊢ s & [\L] & n, n\s^{♯} ⊢ s \\ [\R] \\ n\s ⊢ n\s^{♯} \end{matrix} [/L] (n\s)/n^{♯}, n ⊢ n\s} & s ⊢ s & [/L] & s/(n\s)^{♯}, (n\s)/n, n ⊢ s \\ [/R] \\ s/(n\s), (n\s)/n ⊢ s/n^{♯} \end{matrix} & s ⊢ s & [\L] & s/(n\s), (n\s)/n, (s/n)\s^{♯} ⊢ s \\ (18) \end{matrix}

u, v, w ⊢ w(λw′.u(λu′.v(w′)(u′)))

\begin{matrix}\begin{matrix}\begin{matrix}n ⊢ n & ^{n ⊢ n s ⊢ s [\L] n, n\s^{♯} ⊢ s} & [/L] & n, (n\s)/n^{♯}, n ⊢ s \\ [\R] \\ (n\s)/n, n ⊢ n\s^{♯} \end{matrix} & s ⊢ s & [/L] & s/(n\s)^{♯}, (n\s)/n, n ⊢ s \\ [/R] \\ s/(n\s), (n\s)/n ⊢ s/n^{♯} \end{matrix} & s ⊢ s & [\L] & s/(n\s), (n\s)/n, (s/n)\s^{♯} ⊢ s \\ (19) \end{matrix}

u, v, w ⊢ w(λw′.u(λu′.v(w′)(u′)))

(20) \begin{matrix}n ⊢ n & ^{n\s ⊢ n\s s ⊢ s [/L] s/(n\s)^{♯}, n\s ⊢ s} & [/L] & s/(n\s), (n\s)/n^{♯}, n ⊢ s \\ [/R] \\ s/(n\s), (n\s)/n ⊢ s/n^{♯} \end{matrix} s ⊢ s [\L] s/(n\s), (n\s)/n, (s/n)\s^{♯} ⊢ s

u, v, w ⊢ w(λw′.u(v(w′)))

\begin{matrix}\begin{matrix}n ⊢ n & ^{\begin{matrix}n ⊢ n & s ⊢ s & [\L] & n, n\s^{♯} ⊢ s \\ [\R] \\ n\s ⊢ n\s^{♯} \end{matrix} s ⊢ s [/L] s/(n\s)^{♯}, n\s ⊢ s} & [/L] & s/(n\s), (n\s)/n^{♯}, n ⊢ s \\ [/R] \\ s/(n\s), (n\s)/n ⊢ s/n^{♯} \end{matrix} & s ⊢ s & [\L] & s/(n\s), (n\s)/n, (s/n)\s^{♯} ⊢ s \\ (21) \end{matrix}

u, v, w ⊢ w(λw′.u(λu′.v(w′)(u′)))

The terms assigned to the conclusions of the derivations (18), (19) and (21) are identical. Moreover, because the subterm λu′.v(w′)(u′) of the term w(λw′.u(λu′.v(w′)(u′))) assigned to the conclusion goal of these derivations is equivalent to v(w′) by η-conversion,^{4} the interpretation of these conclusions is equivalent to u, v, w ⊢ w(λw′.u(v(w′))), the interpretation assigned to the conclusions of (17) and (20). So, five of the six Cut-free derivations of the sequent s/(n\s), (n\s)/n, (s/n)\ ⊢ s are semantically equivalent.

However, the interpretation u(λu′.w(λw′.v(w′)(u′))) of the conclusion of derivation (16) is not equivalent to the interpretation of the other conclusions. This can be seen as follows. If the expressions someone, bores and everyone are assigned categories and translations as in (22), then performing the simultaneous substitution (23) in the term of the conclusion goal in (16) supplies the sentence Someone bores everyone with the wide scopesubject interpretation ∃x∀y bore(y)(x), whereas performing this substitution in the terms of the conclusion goals in (17) through (21) yields the wide scope-object interpretation ∀y∃x bore(y)(x).

expression category interpretation
someone  s/(n\s)  λP.∃x P (x)
bores  (n\s)/n  bore
everyone  (s/n)\s  λP.∀y P (y)

(22)

4By η-conversion, the following equivalence is meant: λv.γ′(v) = γ′, provided that v does not occur freely in γ′. A term γ is in η-normal form iff it does not have subterms of the form λv.γ′(v). Equivalence in typed λ-calculus amounts to identity of βη-normal forms in the following sense: for every term γ there is a unique term γ^{βη} which is in βη-normal form (i.e., it is both in β-normal form and in η-normal form) and which can be obtained from γ by performing a finite number of β-conversions and η-conversions (where renaming of bound variables – i.e., the replacement of subterms λv.α by λv′.[α[v:=v′]] if v′ is free for v in α – is allowed), and two terms γ and δ are equivalent iff their βη-nfs γ^{βη} and δ^{βη} are syntactically identical (again modulo renaming bound variables).

{[u:=λP.∃x P (x), v:=bore, w:=λP.∀y P (y)] \atop (23)}

This example gives a nice illustration of what spurious ambiguity comes down to: the wide scope-subject interpretation is derived only once, but the wide-scope-object interpretation is associated with five derivations. Clearly, if we want to put the calculus L to use in parsing and interpreting expressions, this is going to be a problem: the latter interpretation will be computed five times instead of once.

König (1989) is the first attempt to solve the problem, but it does not succeed completely. For instance, König’s system allows the two derivations (14) and (15) for the unambiguous sequent c/c, c/c, c ⊢ c. In the sequel we will show how this problem can be solved for L by further restricting the Cut-free calculus. The resulting system L*, which is equivalent to the system which was indepently proposed by Hepple (1990), is a solution to the spurious ambiguity problem: it provides exactly one proof per interpretation.

The ‘non-spuriously ambiguous’ calculus L* which will be presented below is based on the following three observations:

A: First, each non-atomic axiom instance a/b ⊢ a/b and b\a ⊢ b\a can be decomposed into a proof with two less complex axiom premises, a ⊢ a and b ⊢ b. For instance, axioms b\a ⊢ b\a with interpretation w ⊢ w can be replaced by:

\begin{matrix}b ⊢ b & a ⊢ a & [\L] & b, b\a ⊢ a \\ [\R] \\ b\a ⊢ b\a \end{matrix}  \begin{aligned}u ⊢ u & v ⊢ v & [\L] & u, w ⊢ w(u) \\ & [\R] \\ w ⊢ λu.w(u) \end{aligned}

Due to η-conversion, the term λu.w(u) is equivalent to w. (Axioms a/b ⊢ a/b can be treated analogously.)

B: Second, if a \R or /R inference yields the right-hand side premise of a /L or \L inference, we can always reverse the order of the rules, whereas the semantics remains the same. We only consider the ⟨/R, /L⟩-case, where the rules involved are /R and /L, respectively. (The cases ⟨/R, \L⟩, ⟨\R, /L⟩ and ⟨\R, \L⟩ are analogous.) We can replace:

(24) T ⊢ d ^{U, c, V, b ⊢ a [/R] U, c, V ⊢ a/b} [/L] U, c/d, T, V ⊢ a/b

by:

T ⊢ d U, c, V, b ⊢ a [/L] U, c/d, T, V, b ⊢ a [/R] U, c/d, T, V ⊢ a/b

Semantically, this entails a replacement of:

T′ ⊢ δ ^{U′, z, V′, y ⊢ α [/R] U′, z, V′ ⊢ λy.α}[/L] U′, v, T′, V′ ⊢ [λy.α][z:=v(δ)]

by:

T′ ⊢ δ  U′, z, V′, y ⊢ α [/L] U′, v, T′, V′, y ⊢ α[z:=v(δ)] [/R] U′, v, T′, V′ ⊢ λy.[α[z:=v(δ)]]

The terms [λy.α][z:=v(δ)] and λy.[α[z:=v(δ)]] are identical, since z and y are different variables.

C: Third, whenever a \L or /L inference yields the right-hand side premise of another \L or /L inference, and both inferences have different active categories,^{5} we can reverse the order of the inferences and shift the latter inference to the left-hand side premise (cf. (25)) or to the right-hand side premise (cf. (26)) of the former one. We only treat the ⟨/L, \L⟩-case. (The cases ⟨/L, /L⟩, ⟨\L, /L⟩ and ⟨\L, \L⟩ are analogous.)

Suppose that the conclusion X, W, d\c, Z ⊢ e has been derived by applying \L to left-hand side premise W ⊢ d and right-hand side premise X, c, Z ⊢ e, and that the right-hand side premise X, c, Z ⊢ e is the result of applying /L with an active category a/b different from c – that is: X, c, Z = P, a/b, Q, R, and the category a/b occurs in X or Z:

5The notions ‘same’ and ‘different’ active category are defined as follows: in a structure

T_{2} ⊢ b_{2} ^{T_{1} ⊢ b_{1} U, a, V ⊢ c [$L] T_{3} ⊢ c} [#L] T_{4} ⊢ c (where $ and # ∈ {\, /}), the inferences $L and #L have the same active category iff

(i)  $ = \, # = \, T_{3} = U, T_{1}, b_{1}\a, V and T_{4} = U, T_{1}, T_{2}, b_{2}\(b_{1}\a), V; or

(ii) $ = \, # = /, T_{3} = U, T_{1}, b_{1}\a, V and T_{4} = U, T_{1}, (b_{1}\a)/b_{2}, T_{2}, V; or

(iii) $ = /, # = \, T_{3} = U, a/b_{1}, T_{1}, V and T_{4} = U, T_{2}, b_{2}\(a/b_{1}), T_{1}, V; or

(iv) $ = /, # = /, T_{3} = U, a/b_{1}, T_{1}, V and T_{4} = U, (a/b_{1})/b_{2}, T_{2}, T_{1}, V; otherwise, the inferences $L and #L have different active categories.

W ⊢ d ^{Q ⊢ b P, a, R ⊢ e [/L] X, c, Z ⊢ e} [\L] X, W, d\c, Z ⊢ e

Then there are three possibilities: c occurs in Q (see (25)), or c does not occur in Q, and then c occurs in P (see (26)) or in R (analogous to (26)). In all cases we can reverse the order of the rules while keeping the same semantics. If c occurs in Q, then Q = Q_{1}, c, Q_{2}, and we can replace:

(25) W ⊢ d ^{Q_{1}, c, Q_{2} ⊢ b P, a, R ⊢ e [/L] P, a/b, Q_{1}, c, Q_{2}, R ⊢ e} [\L] P, a/b, Q_{1}, W, d\c, Q_{2}, R ⊢ e

by:

W ⊢ d Q_{1}, c, Q_{2} ⊢ b [\L] Q_{1}, W, d\c, Q_{2} ⊢ b P, a, R ⊢ e [/L] P, a/b, Q_{1}, W, d\c, Q_{2}, R ⊢ e

Semantically, this entails the replacement of:

W′ ⊢ δ ^{Q′_{1}, z, Q′_{2} ⊢ β  P′, x, R′ ⊢ ϵ [/L] P′, y, Q′_{1}, z, Q′_{2}, R′ ⊢ ϵ[x:=y(β)]}[\L] P′, y, Q′_{1}, W′, v, Q′_{2}, R′ ⊢ [ϵ[x:=y(β)]][z:=v(δ)]

by:

W′ ⊢ δ  Q′_{1}, z, Q′_{2} ⊢ β [\L] Q′_{1}, W′, v, Q′_{2} ⊢ β[z:=v(δ)] P′, x, R′ ⊢ ϵ [/L] P′, y, Q′_{1}, W′, v, Q′_{2}, R′ ⊢ ϵ[x:=y(β[z:=v(δ)])]

The terms [ϵ[x:=y(β)]][z:=v(δ)] and ϵ[x:=y(β[z:=v(δ)])] are identical, because z does not occur in ϵ and z and y are different variables.

If c occurs in P, then P = P_{1}, c, P_{2} and we can replace:

(26) W ⊢ d ^{Q ⊢ b P_{1}, c, P_{2}, a, R ⊢ e [/L] P_{1}, c, P_{2}, a/b, Q, R ⊢ e} [\L] P_{1}, W, d\c, P_{2}, a/b, Q, R ⊢ e

by:

Q ⊢ b ^{W ⊢ d P_{1}, c, P_{2}, a, R ⊢ e [\L] P_{1}, W, d\c, P_{2}, a, R ⊢ e} [/L] P_{1}, W, d\c, P_{2}, a/b, Q, R ⊢ e

In the semantics, this amounts to the replacement of:

W′ ⊢ δ ^{Q′ ⊢ β  P′_{1}, z, P′_{2}, x, R′ ⊢ ϵ [/L] P′_{1}, z, P′_{2}, y, Q′, R′ ⊢ ϵ[x:=y(β)]}[\L] U′, P′_{1}, v, P′_{2}, y, Q′, R′ ⊢ [ϵ[x:=y(β)]][z:=v(δ)]

by:

Q′ ⊢ β ^{W′ ⊢ δ  P′_{1}, z, P′_{2}, x, R′ ⊢ ϵ [\L] P′_{1}, W′, v, P′_{2}, x, R′ ⊢ ϵ[z:=v(δ)]}[/L] P′_{1}, W′, v, P′_{2}, y, Q′, R′ ⊢ [ϵ[z:=v(δ)]][x:=y(β)]

The terms [ϵ[x:=y(β)]][z:=v(δ)] and [ϵ[z:=v(δ)]][x:=y(β)] are identical, since x and z are different variables, x does not occur in v(δ), and z does not occur in y(β).^{6}

Observation A entails that for every proof of a sequent, there is a semantically equivalent proof π in which all axiom instances are atomic: at ⊢ at. For note that each non-atomic axiom instance can be decomposed in the way sketched above, and that every decomposition strictly decreases the sum of the degrees of the axiom instances. Hence every proof can be transformed into such an equivalent proof π after finitely many decompositions.

6Note (i) that transformation (26) cannot arise when the right-hand side premise of the first inference is an axiom, because the left-hand side of P_{1}, c, P_{2}, a, R ⊢ e contains at least the two categories c and a; and (ii) that if transformation (26) is executed in a configuration such as the one indicated below, where on the left-hand side @L and $L have the same active category and $L and #L have different active categories, then on the right-hand-side @L and #L (as well as #L and $L) have different active categories:

T_{5} ⊢ c ^{T_{3} ⊢ b ^{T_{1} ⊢ a T_{2} ⊢ d [@L] T_{4} ⊢ d} [$L] T_{6} ⊢ d} [#L] T_{7} ⊢ d ⇝_{(26)} T_{3} ⊢ b ^{T_{5} ⊢ c ^{T_{1} ⊢ a T_{2} ⊢ d [@L] T_{4} ⊢ d} [#L] T′_{6} ⊢ d} [$L] T_{7} ⊢ d

Moreover, given such a π, we can use observations B and C for obtaining a further normalized proof π′′ in which (i) no major (right-hand side) premise of a \L or /L inference is the conclusion of a \R or /R inference (this corresponds to B);^{7} and (ii) the same left-hand side category remains active whenever one goes down from axioms via major premises of \L and /L inferences (this corresponds to C).

In order to see this, we first define the notion ‘maximal major path’ (mmp) for Cut-free L proofs π: an mmp is a sequence ⟨σ_{0}, …, σ_{p}⟩ (p ∈ IN) of sequent occurrences in π, such that (i) σ_{0} is an axiom instance; (ii) for all i, 0 ≤ i < p, σ_{i+1} is the conclusion of an inference with sole (\R or /R) or major (\L or /L) premise σ_{i}; and (iii) σ_{p} is not the sole or major premise of an inference.^{8}

It is not hard to see that every sequent occurrence in a proof π is on exactly one mmp, and that every proof π contains as many mmps as it contains axiom instances, i.e., at least one.

Now, consider a proof π with n + 1 mmps, and focus on the main mmp μ = ⟨σ_{0}, …, σ_{p}⟩ which culminates in the final conclusion σ_{p} of π. Let q be the number of \L and /L inferences in μ, and r the number of \R and /R inferences in μ. So, σ_{p} = σ_{q+r}, some sequent T_{q+r} ⊢ c_{q+r}, and the sequent σ_{0} is an axiom c_{0} ⊢ c_{0}. Moreover, for 0 ≤ i ≤ q + r: (a) each σ_{i+1} obtained by \R or /R is concluded from a subproof π_{i} of π with conclusion σ_{i}, and (b) each σ_{i+1} obtained by \L or /L is concluded from two subproofs of π: π′_{j} (where 1 ≤ j ≤ q) and π_{i} (with conclusion σ_{i}):

(a) ..... π_{i} σ_{i} σ_{i+1}  (b) π′_{j}  σ_{i} σ_{i+1} ..... π_{i}

The left-hand side subproofs π′_{1} through π′_{q} have a total number of n mmps, which is one less than the number of mmps in the whole proof π.

Next, let k(μ) ≤ r · q be the number of pairs of sequents σ_{i} and σ_{j} in μ such that (i) 1 ≤ i < j ≤ q + r; (ii) σ_{i} is the conclusion of a \R or /R inference; and (iii) σ_{j} is the conclusion of a \L or /L inference.

Note that an application of transformation (24) to a \R or /R inference which yields the major premise of a \L or /L inference in an mmp ν always leads to an mmp ν′ which (i) has the same length, (ii) has the same σ_{q+r}, (iii) builds on the same left-hand side subproofs π′_{1},… π′_{q}, and (iv) assigns the same interpretation to σ_{q+r} as ν; but that k(ν′) = k(ν) − 1:

7Consequently, every major premise of a \L or /L inference must be an (atomic) axiom instance at ⊢ at or the conclusion of another \L or /L inference. Since \L and /L identify the goal categories of their major premise and conclusion, every \L and /L inference in π′′ necessarily derives a conclusion sequent with an atomic goal category: T ⊢ at.

8Therefore, σ_{p} must be either the minor (left-hand side) premise of a \L or /L inference, or the final conclusion of π.

π′_{j}  σ_{i} σ_{i+1} π^{i−1}  ⇝_{(24)}  π′j σ′_{i} σ_{i+1} π^{i−1}

So, after k(μ) applications of transformation (24) we obtain a semantically equivalent proof π′ of T_{q+r} ⊢ c_{q+r} such that in the main mmp μ′ of π′ no \R or /R inference precedes a \L or /L inference, i.e., k(μ′) = 0:

π′_{1} c_{0} ⊢ c_{0} [axiom] \L and /L \R and /R T′_{1} ⊢ c′_{1} π′_{q} ..... ......... T′_{q} ⊢ c′_{q} T′_{(q+r)−1} ⊢ c′_{(q+r)−1} T_{q+r} ⊢ c_{q+r}

Concentrate on the sequence ν = ⟨c_{0} ⊢ c_{0}, …, T′_{q} ⊢ c′_{q}⟩ which is the main mmp of the subproof of π′ with conclusion T′_{q} ⊢ c′_{q}, and consider the first inference $L in ν which has a different active category than the inference #L which yields the major premise of $L (where $ and # ∈ {\, /}). We can apply one of the proof transformations (25) and (26). If (26) is applicable, then inference $L reappears one place higher up in the main mmp, now yielding the major premise of #L, and again having a different active category than the inference which now yields its major premise (cf. footnote 6 (ii)):

π′j π′_{j+1}  σ_{i} [$L] σ_{i+1}  π^{i−1}[#L] ⇝_{(26)}  π{′ \atop j+1} π′_{j}  [#L] [$L] σ′_{i} σ_{i+1}  π^{i−1}

Observe that an application of transformation (26) to an mmp of length q always leads to an mmp with (i) the same length, (ii) the same σ_{q}, (iii) the same left-hand side subproofs π′_{1},… π′_{q} (though appearing in a different order), and (iv) the same interpretation for σ_{q}. Since the new situation is structurally the same as the old one, transformation (26) can be applied again and again, until transformation (25) is applicable – for $L yielding conclusion σ_{i} (2 ≤ i ≤ q), this happens after at most i steps: when $L yields σ_{2}, transformation (25) must be applied (cf. footnote 6 (i)).

Transformation (25) removes inference $L from the mmp and adds it, together with its left-hand side subproof π′_{j+1}, to the left-hand side subproof π′_{j} of #L, where the number of mmps in the newly created left-hand side subproof π′′_{j} is equal to the sum of the number of mmps in π′_{j} and π′_{j+1}:^{9}

π′j π′_{j+1}  σ_{i} [$L] σ_{i+1}  π^{i−1}[#L] ⇝_{(25)}  π{′ \atop j+1} π′′_{j}  π_{i−1} [#L] [$L] σ′_{i}  σ_{i+1} π′j

The resulting mmp ν′ is one sequent shorter than ν, but its last sequent σ′_{q−1} equals σ_{q} of ν, and receives the same interpretation. The same procedure can be reapplied to the first inference $L′ in ν′ which has a different active category than the inference #L′ which yields its major premise. If this is done s times, where 0 ≤ s ≤ q − 1 and s is the number of \L and /L inferences having a different active category than the first inference in ν, we obtain a semantically equivalent proof π′′ of T_{q+r} ⊢ c_{q+r} such that in μ′′, the main mmp of π′′, no application of \R or /R precedes an application of \L or /L, and all applications of \L and /L have the same active category:

π′′_{1} c_{0} ⊢ c_{0} [axiom] \L and /L: same active category \R and /R T′_{1} ⊢ c′_{1} π′′_{q−s} ..... ......... T′_{q} ⊢ c′_{q} T′_{(q+r)−1} ⊢ c′_{(q+r)−1} T_{q+r} ⊢ c_{q+r}

The finite procedure which led from π to π′′ can be repeated for the subproofs π′′_{1}, …, π′′_{q−s} of π′′. Moreover, the task of normalizing the proofs π′′_{1} through π′′_{q−s} involves less work than our initial task of normalizing π, because we started with a proof with n + 1 mmps, whereas the total number of mmps in π′′_{1} through π′′_{q−s} equals n.

The above considerations can be summarized in the form of the calculus L*, which is given in (27) below. This calculus introduces the symbol ‘*’ which controls the activity of categories in derivations. Unlike the symbol ‘^{♯}’, which was merely added to the L derivations (14) through (21) in order to enhance their readability, the symbol ‘*’ is a substantial ingredient of L* derivations, since there is a special rule which deals with its behaviour:

9So that the new series of left-hand side subproofs π′_{1},…,π′_{j−1},π′′_{j},π′_{j+2},…,π′_{q} of ν′ still has a total number of n mmps.

syntax:  semantics:

(27)

at* ⊢ at [axiom]  x ⊢ x
T ⊢ b* U, a*, V ⊢ at [/L] U, a/b*, T, V ⊢ at  T′ ⊢ β  U′, u, V′ ⊢ γ U′, w, T′, V′ ⊢ γ[u:=w(β)]

T ⊢ b* U, a*, V ⊢ at [\L] U, T, b\a*, V ⊢ at  T′ ⊢ β  U′, u, V′ ⊢ γ U′, T′, w, V′ ⊢ γ[u:=w(β)]

T, b ⊢ a* [/R] T ⊢ a/b*  {T′, v ⊢ α \atop T′ ⊢ λv.α}

b, T ⊢ a* [\R] T ⊢ b\a*  {v, T′ ⊢ α \atop T′ ⊢ λv.α}

{U, a*, V ⊢ at \atop U, a, V ⊢ at*}  U′, u, V′ ⊢ γ [ * ] U′, u, V′ ⊢ γ

The calculus in (27) observes the same conventions as regards categories, types, terms and variables as (10) above, with the exceptions that at represents an arbitrary atomic category, that γ refers to a term of type type(at), and that x denotes a variable of type type(at).

Important properties of the calculus L* are the following. Let γ′ = γ denote equivalence of terms γ′ and γ (we will use γ′ ≡ γ for syntactic identity of terms modulo renaming bound variables):

Theorem 1:

1. T ⊢_{L*} c* if and only if T ⊢_{L} c.

2. If T:T′ ⊢_{L*} c*:γ, then T:T′ ⊢_{L} c:γ.

3. If T:T′ ⊢_{L} c:γ, there is a γ′ such that γ′ = γ and T:T′ ⊢_{L*} c*:γ′.

Proof: We have seen that if T :T′ ⊢_{L} c:γ, then there is a Cut-free L proof π of T : T′ ⊢ c : γ′ such that γ′ = γ and π has the following properties:

(a) all axiom instances in π are atomic; (b) no major premise of a \L or /L inference in π is the conclusion of a \R or /R inference; and (c) the same category remains active whenever one goes down from axioms via major premises of \L and /L inferences in π.

But this is sufficient, for there is an L* proof π′ of T:T′ ⊢ c*:γ′ iff there is a Cut-free L proof π of T:T′ ⊢ c:γ′ with the properties (a) through (c):

Observe (a′) that L* axioms at* ⊢ at involve only atomic categories; (b′) that the major premise of a \L or /L inference in L* can only be an axiom or the conclusion of another \L or /L inference (the asterisk must be on the left-hand side); and (c′) that if a \L or /L inference yields the major premise of another \L or /L inference, then they have the same (asterisked) active left-hand side category. On account of (a′) through (c′), every Cutfree L proof π of a sequent T : T′ ⊢ c: γ′ having the properties (a) through (c) can be turned into an L* proof π′ of T : T′ ⊢ c* : γ′ by (i) adding an asterisk to the left-hand side category of every axiom instance; (ii) adding an asterisk to the active left-hand side category in every conclusion sequent of a \L, /L, \R and /R inference; and (iii) replacing every sequent of the form U : U′, a* : u, V : V′ ⊢ at : γ which is not the major premise of a \L or /L inference by the following inference:

\begin{matrix}U:U′, a*:u, V :V′ ⊢ at : γ & [ * ] & U:U′, a:u, V :V′ ⊢ at* : γ \\ (28) \end{matrix}

And, conversely, every L* proof π′ of T:T′ ⊢ c*:γ′ can be turned into a Cutfree L proof π of T:T′ ⊢ c:γ′ with properties (a) through (c) by (i) replacing every inference of the form (28) by the sequent U : U′, a: u, V : V′ ⊢ at : γ; and (ii) deleting all remaining asterisks. □

4 Spurious Ambiguity

In the present section we will show that L* is a solution to the spurious ambiguity problem: if π_{1} is an L* proof of T : T′ ⊢ c: γ and π_{2} is an L* proof of T : T′ ⊢ c: γ′ such that γ = γ′, then π_{1} = π_{2}.^{10} As γ = γ′ entails that λT′.γ = λT′.γ′, this claim is a corollary of the following:

10Above we merely required that in the context of an L (or L*) proof all variables x and w assigned to an axiom instance or introduced in the conclusion of a \L or /L inference be different. Accordingly, we will identify all derivations which differ only with respect to the particular variables they assign. Thus for sequents σ and τ, we let σ = τ iff σ = c_{1} : v_{1}, …, c_{n}: v_{n} ⊢ c: γ and τ = c_{1} : v′_{1}, …, c_{n}: v′_{n} ⊢ c: γ′; and for proofs π and ρ, we let π = ρ if and only if

• π = σ, ρ = τ, where σ and τ are (axiom) sequents such that σ = τ;

Theorem 2:

If π_{1} is an L* proof of T:T′ ⊢ c:γ′ and π_{2} is an L* proof of T:T′′ ⊢ c:γ′′ such that λT′.γ′ = λT′′.γ′′, then π_{1} = π_{2}.

Proof: Suppose π_{1} and π_{2} are two different proofs of the same conclusion T ⊢ c. Since axioms and non-axiom theorems in L* never have the same degree (cf. definition (13) (iii) above), no sequent can be both an axiom and a non-axiom theorem. This entails that there must be at least one non-axiom sequent T^{∘} ⊢ c^{∘} which is derived from different premises in π_{1} and π_{2}. Inspection of L* shows that the goal c^{∘} of this sequent cannot be of the form b\a* or a/b*, for the rules \R and /R which yield conclusions with such goals have the property that their conclusion sequents, T ⊢ b\a* and T ⊢ a/b*, completely determine the form of their premise sequents: b, T ⊢ a* and T, b ⊢ a*, respectively. So, c^{∘} must be (i) an asterisked atomic category at*; or (ii) a non-asterisked atomic category at.

(i) If c^{∘} = at*, then T^{∘} ⊢ c^{∘} must have been obtained with the * rule in both π_{1} and π_{2}. Hence T^{∘} = U, a, V, b, W and the situation is as follows in π_{1} and π_{2}:

U:U′, a*:u′, V :V′, b:v′, W:W′ ⊢ at :γ′ [ * ] and U:U′, a:u′, V :V′, b:v′, W:W′ ⊢ at*:γ′

U:U′′, a:u′′, V :V′′, b*:v′′, W:W′′ ⊢ at :γ′′ [ * ] U:U′′, a:u′′, V :V′′, b:v′′, W:W′′ ⊢ at*:γ′′

(29)

It turns out that λU′λu′λV′λv′λW′.γ′ and λU′′λu′′λV′′λv′′λW′′.γ′′ are nonequivalent terms (see Fact 1 below).

• π = {π′ \atop σ} , ρ = {ρ′ \atop τ} , π′ = ρ′ and σ = τ; or

• π = π′ π′′ σ , ρ = ρ′ ρ′′ τ , π′ = ρ′, π′′ = ρ′′ and σ = τ.

Alternatively, we could enforce one particular assignment of different variables to each derivation π, for instance by requiring (i) that the sequence of axiom leafs of π equal at_{1}* : v_{1} ⊢ at_{1} : v_{1}, …, at_{n}* : v_{n} ⊢ at_{n} : v_{n}, where for all i, 1 ≤ i ≤ n: v_{1} is the i-th variable of type type(at_{i}); and (ii) that for all instances of \L and /L in π the variable w be the i-th variable of type (type(b),type(a)) iff u is the i-th variable of type type(a).

Note that this would not restrict the semantic potential of the calculus, for it is easily checked that all π_{1} and π_{2} such that π_{1} = π_{2} in the sense just defined are semantically equivalent: if π_{1} = π_{2}, then π_{1} is a proof of c_{1} : v_{1}, …, c_{n}: v_{n} ⊢ c: γ and π_{2} is a proof of c_{1} : v′_{1}, …, c_{n}: v′_{n} ⊢ c: γ′ such that λv_{1}...λv_{n}.γ ≡ λv′_{1}...λv′_{n}.γ′ (and hence: λv_{1}...λv_{n}.γ = λv′_{1}...λv′_{n}.γ′). The more liberal option has been chosen since it links up better with the alternative approaches to be discussed in the next section.

(ii) If c^{∘} = at, then the left-hand side T^{∘} of T^{∘} ⊢ c^{∘} must contain one asterisked category d*. Because T^{∘} ⊢ c^{∘} is not an axiom, d* must be a non-atomic asterisked category a/b* (or b\a*), and, accordingly, T^{∘} ⊢ x^{∘} must have been obtained using /L (or \L) in both π_{1} and π_{2}. We only consider /L, since the \L case is analogous. Then d* equals a/b*; T^{∘} = U, a/b*, V, W, X, where W is a non-empty sequence of categories; and the situation is as follows in π_{1} and π_{2}:

V :V′ ⊢ b*:β′  U:U′, a*:u′, W:W′, X:X′ ⊢ at :γ′ [/L] and U:U′, a/b*:w′, V :V′, W:W′, X:X′ ⊢ at :γ′[u′:=w′(β′)]

V :V′′, W:W′′ ⊢ b*:β′′  U:U′′, a*:u′′, X:X′′ ⊢ at :γ′′ [/L] U:U′′, a/b*:w′′, V :V′′, W:W′′, X:X′′ ⊢ at :γ′′[u′′:=w′′(β′′)]

(30)

The term λU′λw′λV′λW′λX′.γ′[u′:=w′(β′)] can be shown to be non-equi-valent to λU′′λw′′λV′′λW′′λX′′.γ′′[u′′:=w′′(β′′)] (see Fact 2 below).

Consequently, the intermediate conclusion T^{∘} ⊢ c^{∘} gets non-equivalent interpretations in π_{1} and π_{2}.

Moreover, it can be shown that any non-equivalence of the terms which different proofs assign to some intermediate sequent is inherited by the terms assigned to the conclusions drawn from that sequent (see Fact 3 below). So, if the intermediate conclusion T^{∘} ⊢ c^{∘} has non-equivalent interpretations in π_{1} and π_{2}, then T ⊢ c, the final conclusion of both proofs, will receive non-equivalent interpretations in π_{1} and π_{2} as well. □

In footnote 3 it was observed that terms γ assigned to sequent goals in Cutfree L proofs are always in β-normal form, i.e., they do not have subterms of the form [λv.γ′](γ′′). In the proof of Theorem 1 we have seen that the terms assigned to sequent goals in L* proofs constitute a subset of the terms assigned to sequent goals in Cut-free L proofs and, hence, are in β-normal form as well. However, they also meet the stronger requirement of being in what we will call ‘βη̄-normal form’ (as can be seen by an easy induction on the length of L* derivations):

A term γ is in η̄-normal form (η̄-nf) iff every occurrence of a subterm γ′ ≢ λv.γ′′ of functional type (a, b) is applied to some term γ′′′ in γ, i.e., it occurs as γ′(γ′′′) in γ.^{11}

11Let η-expansion (‘η̄-conversion’) be defined as the replacement of a subterm occurrence

A term γ is in βη̄-nf iff γ is in β-nf and γ is in η̄-nf.

As was noted in footnote 4, equivalence in typed λ-calculus amounts to identity of βη-nfs, i.e., two terms γ and δ are equivalent (γ = δ) iff their βηnfs γ^{βη} and δ^{βη} are syntactically identical modulo renaming bound variables (γ^{βη} ≡ δ^{βη}). Together with the fact mentioned in footnote 11, this yields that γ = δ iff γ^{βη̄} ≡ δ^{βη̄}. Terms assigned to sequent goals in L* proofs are in βη̄-nf, so they are equivalent just in case they are identical, a fact which will be exploited in the corollaries of the following lemma. Let the function # count the number of arguments of c ∈ cat, i.e., #(at) = 0 and #(a/b) = #(b\a) = #(a) + 1.

Lemma:

If U:U′, c*:w, V :V′ ⊢ at : γ, then there are terms γ_{1}, …, γ_{#(c)} such that γ ≡ w(γ_{#(c)})...(γ_{1}) and w does not occur in γ_{1}, …, γ_{#(c)}.

Proof: by induction on the degree of c.

• If c ∈ atom, then #(c) = 0 and U : U′, c* : w, V : V′ ⊢ at : γ is an axiom sequent at*:w ⊢ at :w, so γ ≡ w.

• If c = a/b (or b\a), then U : U′, c* : w, V : V′ ⊢ at : γ is the conclusion of a /L (or, analogously, a \L) inference:

V_{1} :V′_{1} ⊢ b*:β  U:U′, a*:u, V_{2} :V′_{2} ⊢ at :γ [/L] U:U′, a/b*:w, V_{1} :V′_{1}, V_{2} :V′_{2} ⊢ at :γ[u:=w(β)]

Applying the induction hypothesis to γ, we know that there are terms γ_{1}, …, γ_{#(a)} such that γ ≡ u(γ_{#(a)})...(γ_{1}) and the variable u does not occur in γ_{1}, …, γ_{#(a)}. Note that #(a/b) = #(a)+1, and that the term γ[u:=w(β)] is identical to w(β)(γ_{#(a)})...(γ_{1}), where w, being different from the variables in β and γ, does not occur in γ_{1}, …, γ_{#(a)}, β. □

γ′ ≢ λv.γ′′ of functional type (a, b) which is not applied to any term γ′′′ by λv.γ′(v), where v does not occur freely in γ′. One can show that η-expansion is strongly normalizing and Church-Rosser: for every term γ there is a unique term γη̄ which is in η̄-normal form, and which can be obtained from γ by performing a finite number of η-expansions (where renaming of bound variables is allowed). This is established by induction on the complexity of (the type of) γ, using the facts that (i) variables of non-functional (atomic) type are in η̄-nf; (ii) η-expansion of variables of type (a, b) only introduces variables of less complex type; and (iii) η-expansion of complex terms λv.γ′ and γ′(γ′′) only involves η-expansion of less complex terms. As η-expansion respects β-normality, we have the following fact:

for every γ and δ: γ^{βη} ≡ δ^{βη} iff γ^{βη̄} ≡ δ^{βη̄}.

Let T′ be a sequence of variables v_{1}, …, v_{n}, and T a sequence of categories c_{1}, …, c_{n}. We will say that T′ is of type T iff for all i, 1 ≤ i ≤ n: v_{i} is of type type(c_{i}). If T′ = v′_{1}, …, v′_{n} is a sequence of different variables and T′′ = v′′_{1}, …, v′′_{n} is a sequence of variables of the same type as T′, then γ[T′:=T′′] denotes the result of performing the simultaneous substitution [v′_{1} :=v′′_{2}, …, v′_{n}:=v′′_{n}] in γ.

Note that for sequences T′, T′′ and T′′′ of different variables of the same type such that T′ and T′′ occur in γ′ and γ′′, respectively, and T′′′ occurs in γ′ nor γ′′, we have: λT′.γ′ ≡ λT′′.γ′′ iff γ′[T′:=T′′′] ≡ γ′′[T′′:=T′′′], since • λT′′′.[γ′[T′:=T′′′]] ≡ λT′′′.[γ′′[T′′:=T′′′]] iff γ′[T′:=T′′′] ≡ γ′′[T′′:=T′′′];

• λT′.γ′ ≡ λT′′′.[γ′[T′:=T′′′]] by renaming bound variables; and

• λT′′.γ′′ ≡ λT′′′.[γ′′[T′′:=T′′′]] by renaming bound variables.

Fact 1. Consider (29). By the above Lemma: γ′ ≡ u′(γ′_{#(a)})...(γ′_{1}) and γ′′ ≡ v′′(γ′′_{#(b)})...(γ′′_{1}). Let U′′′, u′′′, V′′′, v′′′, W′′′ be a sequence of different variables of type U, a, V, b, W which do not occur in γ′ and γ′′. Abbreviate U′, u′, V′, v′, W′ as S′; U′′, u′′, V′′, v′′, W′′ as S′′; and U′′′, u′′′, V′′′, v′′′, W′′′ as S′′′. Then λS′.γ′ ≢ λS′′.γ′′, since γ′[S′:=S′′′] ≡ [u′(γ′_{#(a)})...(γ′_{1})][S′:=S′′′] ≡ u′′′(γ′_{#(a)}[S′:=S′′′])...(γ′_{1}[S′:=S′′′]) ≢ v′′′(γ′′_{#(b)}[S′′:=S′′′])...(γ′′_{1}[S′′:=S′′′]) ≡ [v′′(γ′′_{#(b)})...(γ′′_{1})][S′′:=S′′′] ≡ γ′′[S′′:=S′′′]. Therefore, λS′.γ′ ≠ λS′′.γ′′.

Fact 2. Consider (30). Again, by the Lemma: γ′ ≡ u′(γ′_{#(a)})...(γ′_{1}) and γ′′ ≡ u′′(γ′′_{#(a)})...(γ′′_{1}), where u′ and u′′ do not occur in γ′_{1}, …, γ′_{#(a)} and γ′′_{1}, …, γ′′_{#(a)}, respectively. Hence γ′[u′:=w′(β′)] ≡ w′(β′)(γ′_{#(a)})...(γ′_{1}) and γ′′[u′′:=w′′(β′′)] ≡ w′′(β′′)(γ′′_{#(a)})...(γ′′_{1}). Since the sequence of categories W is non-empty, we have that W = W_{1}, c, W_{2}; W′ = W′_{1}, v′, W′_{2}; and W′′ = W′′_{1}, v′′, W′′_{2}. Note that for 1 ≤ i ≤ #(a): v′ occurs freely in some γ′_{i} but not in β′, whereas v′′ occurs freely in β′′ but not in any γ′′_{i}. Let U′′′, w′′′, V′′′, W′′′, X′′′ be a sequence of different variables of type U, a/b, V, W, X not occurring in γ′[u′:=w′(β′)] and γ′′[u′′:=w′′(β′)], and let W′′′ = W′′′_{1}, v′′′, W′′′_{2}. Denote U′, w′, V′, W′, X′ by S′; U′′, w′′, V′′, W′′, X′′ by S′′; and U′′′, w′′′, V′′′, W′′′, X′′′ by S′′′.

We now have that λS′.[γ′[u′:=w′(β′)]] ≢ λS′′.[γ′′[u′′:=w′′(β′′)]], since [γ′[u′:=w′(β′)]][S′:=S′′′] ≢ [γ′′[u′′:=w′′(β′′)]][S′′:=S′′′]:

• [γ′[u′:=w′(β′)]][S′:=S′′′] ≡ [w′(β′)(γ′_{#(a)})...(γ′_{1})][S′:=S′′′] ≡ w′′′(β′[S′:=S′′′])(γ′_{#(a)}[S′:=S′′′])...(γ′_{1}[S′:=S′′′]); • [γ′′[u′′:=w′′(β′′)]][S′′:=S′′′] ≡ [w′′(β′′)(γ′′_{#(a)})...(γ′′_{1})][S′′:=S′′′] ≡

w′′′(β′′[S′′:=S′′′])(γ′′_{#(a)}[S′′:=S′′′])...(γ′′_{1}[S′′:=S′′′]); and

• the variable v′′′ occupies the position of v′ in [γ′[u′:=w′(β′)]][S′:=S′′′] and of v′′ in [γ′′[u′′:=w′′(β′′)]][S′′:=S′′′], so v′′′ occurs freely in some γ′_{i}[S′:=S′′′] but not in β′[S′:=S′′′], and it occurs freely in β′′[S′′:=S′′′] but not in any γ′′_{i}[S′′:=S′′′].

Therefore: λS′.[γ′[u′:=w′(β′)]] ≠ λS′′.[γ′′[u′′:=w′′(β′′)]].

Fact 3. Consider the following two inferences:

T:T′ ⊢ b*:β′  U:U′, a*:u′, V :V′ ⊢ at :γ′ [/L] and U:U′, a/b*:w′, T:T′, V :V′ ⊢ at :γ′[u′:=w′(β′)]

T:T′′ ⊢ b*:β′′  U:U′′, a*:u′′, V :V′′ ⊢ at :γ′′ [/L] U:U′′, a/b*:w′′, T:T′′, V :V′′ ⊢ at :γ′′[u′′:=w′′(β′′)]

By the Lemma: γ′ ≡ u′(γ′_{#(a)})...(γ′_{1}), γ′[u′:=w′(β′)] ≡ w′(β′)(γ′_{#(a)})...(γ′_{1}), γ′′ ≡ u′′(γ′′_{#(a)})...(γ′′_{1}) and γ′′[u′′:=w′′(β′′)] ≡ w′′(β′′)(γ′′_{#(a)})...(γ′′_{1}). Let U′′′, w′′′, T′′′, V′′′ be a sequence of different variables of type U, a/b, T, V which do not occur in γ′[u′:=w′(β′)] and γ′′[u′′:=w′′(β′′)]. Abbreviate U′, w′, T′, V′ as S′; U′′, w′′, T′′, V′′ as S′′; and U′′′, w′′′, T′′′, V′′′ as S′′′.

Now, suppose that λS′.[γ′[u′:=w′(β′)]] ≡ λS′′.[γ′′[u′′:=w′′(β′′)]]. This entails that [γ′[u′:=w′(β′)]][S′:=S′′′] ≡ [γ′′[u′′:=w′′(β′′)]][S′′:=S′′′], that is: [w′(β′)(γ′_{#(a)})...(γ′_{1})][S′:=S′′′] ≡ [w′′(β′′)(γ′′_{#(a)})...(γ′′_{1})][S′′:=S′′′].

So, β′[S′:=S′′′] ≡ β′′[S′′:=S′′′] and for all i, 1 ≤ i ≤ #(a): γ′_{i}[S′:=S′′′] ≡ γ′′_{i}[S′′:=S′′′]. Since the variables U′, w′, V′ and U′′, w′′, V′′ do not occur in β′ and β′′, respectively, we have that β′[S′:=S′′′] ≡ β′[T′:=T′′′] and β′′[S′′:=S′′′] ≡ β′′[T′′:=T′′′]. So, λT′.β′ ≡ λT′′.β′′. Moreover, since the variables w′, T′ and w′′, T′′ do not occur in any γ_{i} and γ′′_{i}, respectively, we have that for all i: γ′_{i}[S′:=S′′′] ≡ γ′_{i}[U′, V′:=U′′′, V′′′] and γ′′_{i}[S′′:=S′′′] ≡ γ′′_{i}[U′′, V′′:=U′′′, V′′′]. Finally, since u′ and u′′ are different from the variables in γ′_{1}, …, γ′_{#(a)} and γ′′_{1}, …, γ′′_{#(a)}, respectively, we can conclude that λU′λu′λV′.u′(γ′_{#(a)})...(γ′_{1}) ≡ λU′′λu′′λV′′.u′′(γ′′_{#(a)})...(γ′′_{1}).

Consequently, if λT′.β′ ≠ λT′′.β′′ or λU′λu′λV′.γ′ ≠ λU′′λu′′λV′′.γ′′, then λU′λw′λT′λV′.[γ′[u′:=w′(β′)]] ≠ λU′′λw′′λT′′λV′′.[γ′′[u′′:=w′′(β′′)]].

Furthermore, note (i) that the \L case is analogous; (ii) that the semantics of the * rule is identity; and (iii) that the cases \R and /R are trival as well. So, non-equivalence of terms assigned to some sequent is always inherited by the terms assigned to the conclusions drawn from that sequent.

Returning to the examples treated earlier, it turns out that the unambiguous sequent c/c, c/c, c ⊢ c* is indeed derived only once in L*, whereas it has two Cut-free derivations, (14) and (15), in L:

\begin{matrix}\begin{matrix}^{c* ⊢ c [ * ] c ⊢ c*} & c* ⊢ c & [/L] & c/c*, c ⊢ c \\ [ * ] \\ c/c, c ⊢ c* \end{matrix} & c* ⊢ c & [/L] & c/c*, c/c, c ⊢ c \\ [ * ] \\ c/c, c/c, c ⊢ c* \end{matrix} ; (31)

Modulo * inferences, derivation (31) has the structure of (14). There is no L* proof with the structure of (15), for the main mmp of (15) contains two different active left-hand side categories.

The two-way ambiguous sequent s/(n\s), (n\s)/n, (s/n)\s ⊢ s which has the six Cut-free L derivations (16) through (21) is derived twice in L*, cf. (32) and (33) below. These derivations are structurally similar and semantically equivalent to (16) and (19), respectively. The remaining Cutfree L derivations of the sequent do not have L* counterparts: (17) and (20) because of a non-atomic axiom instance n\s ⊢ n\s; (18) due to a \R inference which yields the major premise of a /L inference; and (21) on account of an mmp with two different active left-hand side categories.

\begin{aligned}\begin{aligned}\begin{matrix}^{n* ⊢ n [ * ] n ⊢ n*} & ^{^{n* ⊢ n [ * ] n ⊢ n*} s* ⊢ s [\L] n, n\s* ⊢ s} & [/L] & n, (n\s)/n*, n ⊢ s \\ [ * ] \\ n, (n\s)/n, n ⊢ s* \end{matrix} ; [/R] ; n, (n\s)/n ⊢ s/n* & s* ⊢ s & [\L] & n, (n\s)/n, (s/n)\s* ⊢ s \\ & [ * ] \\ n, (n\s)/n, (s/n)\s ⊢ s* \end{aligned} ; [\R] ; (n\s)/n, (s/n)\s* ⊢ n\s* & s* ⊢ s & [/L] & s/(n\s)*, (n\s)/n, (s/n)\s ⊢ s \\ & [ * ] \\ s/(n\s), (n\s)/n, (s/n)\s ⊢ s* \end{aligned} ; (32)

\begin{aligned}\begin{aligned}\begin{matrix}^{n* ⊢ n [ * ] n ⊢ n*} & ^{^{n* ⊢ n [ * ] n ⊢ n*} s* ⊢ s [\L] n, n\s* ⊢ s} & [/L] & n, (n\s)/n*, n ⊢ s \\ [ * ] \\ n, (n\s)/n, n ⊢ s* \end{matrix} ; [\R] ; (n\s)/n, n ⊢ n\s* & s* ⊢ s & [/L] & s/(n\s)*, (n\s)/n, n ⊢ s \\ & [ * ] \\ s/(n\s), (n\s)/n, n ⊢ s* \end{aligned} ; [/R] ; s/(n\s), (n\s)/n ⊢ s/n* & s* ⊢ s & [\L] & s/(n\s), (n\s)/n, (s/n)\s* ⊢ s \\ & [ * ] \\ s/(n\s), (n\s)/n, (s/n)\s ⊢ s* \end{aligned} ; (33)

5 Partial Deduction and Proof Nets

In the present section we will discuss two alternative approaches to the problem of spurious ambiguity which were proposed in Moortgat (1990) and Roorda (1991). First, in Section 5.1, we give a formalization of the proposals in Moortgat (1990), and prove that the resulting proof representations ‘summarize’ L* derivations of sequents with atomic goal categories and are, hence, devoid of spurious ambiguity. Next, section 5.2 is devoted to a comparison of L* with the proof nets proposed in Roorda (1991). It is shown that every L* proof corresponds to a non-singleton set of proof nets.

5.1 Partial Deduction

Moortgat (1990) suggests that partial deduction offers a way of tackling the problem of spurious ambiguity for L. The basic idea of partial deduction is that theorem proving is preceded by a compilation of the lexicon, i.e., the set of categories which occur in the left-hand side of the sequents to be derived and interpreted. This set of categories serves as the basis for the generation of axioms and rules which are to replace the original axioms and rules of L.^{12} The idea is that since they have more internal structure than the rules of L, the new rules restrict the derivational freedom of the original system, thus eliminating spurious ambiguity.

12Moortgat says that ‘partial deduction of the lexicon adds non-trivial axioms to the trivial axioms and logical rules’ of L, such that the resulting system ‘can do without the original logical rules’ (1990, p. 388; small caps added, italics sic), but in the sequel we will see that the addition involves both axioms and rules.

Unfortunately, Moortgat (1990) does not contain a formal definition of partial deduction, let alone a proof that the method is sound and complete – i.e., that it eliminates all spurious ambiguity while preserving all L-derivable sequents and interpretations.

The paper only treats two examples, viz., the categories (a_{1}\a_{2})/a_{3} and (s/(n\s))\s, where a_{1}, a_{2}, a_{3}, n and s are atomic.

The first order^{13} category (a_{1}\a_{2})/a_{3} gives rise to a single derived inference rule:^{14}

T_{2} :T′_{2} ⊢ a_{3} :γ_{2}  T_{1} :T′_{1} ⊢ a_{1} :γ_{1} [(a_{1}\a_{2})/a_{3}] T_{1} :T′_{1}, (a_{1}\a_{2})/a_{3} :v_{0}, T_{2} :T′_{2} ⊢ a_{2} :v_{0}(γ_{2})(γ_{1})

(34)

The higher order category (s/(n\s))\s, on the other hand, results in a set consisting of two derived inference rules. One corresponds to the category (s/(n\s))\s itself, and the other to the (only) argument n\s of the (only) argument s/(n\s) of (s/(n\s))\s:

\begin{matrix}T_{1} :T′_{1}, n\s:v_{1} ⊢ s:γ_{1} & [(s/(n\s))\s] & T_{1} :T′_{1}, (s/(n\s))\s:v_{0} ⊢ s:v_{0}(λv_{1}.γ_{1}) \\ (35) \end{matrix}

T_{1} :T′_{1} ⊢ n:γ_{1}  [n\s] T_{1} :T′_{1}, n\s:v_{0} ⊢ s:v_{0}(γ_{1})

We will show that a formal definition can be given which (i) is consistent with the examples treated by Moortgat; and (ii) indeed solves the problem of spurious ambiguity for sequents with atomic goal categories.

First, we define two functions from categories to sets of categories. For c ∈ cat, A(c) is the set consisting of the arguments of c, while A^{A}(c) is the set consisting of the arguments of the arguments of c:

A(at) = ∅; A(a/b) = A(b\a) = {b} ∪ A(a);

A^{A}(at) = ∅; A^{A}(a/b) = A^{A}(b\a) = A(b) ∪ A^{A}(a).

13The order of a category c, o(c), is defined as follows: o(c) = 0 if c ∈ atom; o(a/b)

= o(b\a) = max(o(a),o(b) + 1). For example: o(n) = 0, o(n\s) = 1, o(s/(n\s)) = 2 and o((s/(n\s))\s) = 3, whereas o((s\(n/s))/s) = 1.

14Different from Moortgat (1990), but in keeping with our modification (10) of his semantics (5), the left-hand side categories (a_{1}\a_{2})/a_{3}, (s/(n\s))\s and n\s are assigned a variable v_{0} instead of a (possibly complex) term.

For a set of categories C, let C^{+} be the set which includes C and contains, for n ∈ IN, any argument of (an argument of an argument of)^{n} an argument of a category c ∈ C. More formally:

Let C ⊆ cat. C^{+} is the smallest set such that

(i) C ⊆ C^{+}, and (ii) for all c ∈ C^{+}: A^{A}(c) ⊆ C^{+}.

If C is the set of categories which appear in the left-hand side of sequents, then C^{+} is the set of categories from which new axioms and rules are derived.

That C^{+} is the required set can be seen from the examples (34) and (35). A derived inference rule associated with a category c deals with occurrences of c in the left-hand side of sequents: a category c consisting of n arguments c_{1}, … c_{n} and a (final) value at yields a derived inference rule consisting of a conclusion with left-hand side category c and goal category at, plus n premises with goal categories c_{1}, … c_{n} – that is: provided that c_{1}, … c_{n} are atomic categories, as in (34). If, as in (35), an argument category c_{i} of c itself consists of arguments c′_{1}, … c′_{m} and final value at′, then the relevant premise has at′ as its goal category, while the categories c′_{1}, … c′_{m} appear in its left-hand side. Now, the presence of arguments of arguments of c in the left-hand side of premises of the derived inference associated with c entails that these categories should be associated with a derived inference rule of their own.

For the example categories (a_{1}\a_{2})/a_{3} and (s/(n\s))\s, the above definitions yield the following:

A((a_{1}\a_{2})/a_{3}) = {a_{1}, a_{3}}; A^{A}((a_{1}\a_{2})/a_{3}) = ∅;

so {(a_{1}\a_{2})/a_{3}}^{+} = {(a_{1}\a_{2})/a_{3}}.

A((s/(n\s))\s) = {s/(n\s)}; A^{A}((s/(n\s))\s) = {n\s};

A(n\s) = {n}; A^{A}(n\s) = ∅;

so {(s/(n\s))\s}^{+} = {(s/(n\s))\s, n\s}.

Next, let f be the following function from interpreted sequents to interpreted sequents:^{15} f(T:T′ ⊢ at :γ) = T:T′ ⊢ at :γ f(T:T′ ⊢ a/b:λv.γ) = f(T:T′, b:v ⊢ a:γ); and f(T:T′ ⊢ b\a:λv.γ) = f(b:v, T:T′ ⊢ a:γ).

15Strictly speaking, f is a partial function, because terms assigned to goal categories a/b or b\a are not necessarily of the form λv.γ.

Below we will also employ the following straightforward extension of f to interpreted sequents with asterisked goal categories:

f(T :T′ ⊢ at* : γ) = T :T′ ⊢ at* : γ;

Syntactically, the function f peels off the argument categories from the goal category of the sequent to which it is applied. Semantically, it strips the term assigned to the goal category of its lambda abstractions. Together with the variables of the abstractions, these argument categories are added to the left-hand side of the sequent. An induction on #(c)^{16} shows that if a proof π of T:T′ ⊢ c:γ is of the form indicated below, where I_{1}, … I_{#(c)} ∈ {\R, /R}, then the conclusion of the subproof π′ of π is the sequent f(T:T′ ⊢ c:γ):

π′  [I_{1}] ....  [I_{#(c)}] T:T′ ⊢ c:γ

The function g assigns an axiom to every atomic category at and a derived inference rule to every compound category b\a and a/b:

g(at) = at :v_{0} ⊢ at :v_{0};

g(a/b) = f(T_{m+1} :T′_{m+1} ⊢ b:λv_{1}...λv_{#(b)}.γ_{m+1})  σ_{m} …  σ_{1} X, a/b:v_{0}, T_{m+1} :T′_{m+1}, Y ⊢ at :v_{0}(λv_{1}...λv_{#(b)}.γ_{m+1})(δ_{m})...(δ_{1})

and

g(b\a) = f(T_{m+1} :T′_{m+1} ⊢ b:λv_{1}...λv_{#(b)}.γ_{m+1})  σ_{m} …  σ_{1} X, T_{m+1} :T′_{m+1}, b\a:v_{0}, Y ⊢ at :v_{0}(λv_{1}...λv_{#(b)}.γ_{m+1})(δ_{m})...(δ_{1})

iff g(a) consists of the conclusion X, a : v_{0}, Y ⊢ at : v_{0}(δ_{m})...(δ_{1}) and the premises σ_{m}, …, σ_{1}. (Note that m = #(a).)

The expressions T_{1} : T′_{1}, …, T_{#(c)} : T′_{#(c)} occurring in a rule g(c) will range over non-empty finite sequences of pairs consisting of a category and a variable.^{17} As before, we will require that in the context of a proof all variables v_{0} assigned to an axiom instance or introduced in the conclusion of a derived inference rule be different.

f(T :T′ ⊢ a/b* : λv.γ) = f(T :T′, b:v ⊢ a*:γ); and

f(T :T′ ⊢ b\a* : λv.γ) = f(b:v, T :T′ ⊢ a*:γ).

Note that since the terms assigned to goal categories in L* derivations are in η̄-nf (see section 4 above), the restriction of f to L*-derivable interpreted sequents is a total function.

16Recall that the function # counts the number of arguments of c ∈ cat: #(at) = 0 and #(a/b) = #(b\a) = #(a) + 1.

Let us see what these definitions amount to for the example categories discussed above. We start with the category (a_{1}\a_{2})/a_{3}. Since #(a_{1}) = #(a_{3}) = 0:

f(T_{i}:T′_{i} ⊢ a_{1} :λv_{1}...λv_{#(a_{1})}.γ_{i}) = T_{i}:T′_{i} ⊢ a_{1} :γ_{i}; and

f(T_{i}:T′_{i} ⊢ a_{3} :λv_{1}...λv_{#(a_{3})}.γ_{i}) = T_{i}:T′_{i} ⊢ a_{3} :γ_{i}.

Since g(a_{2}) = a_{2} :v_{0} ⊢ a_{2} :v_{0}, we have:

g(a_{1}\a_{2}) =  T_{1} :T′_{1} ⊢ a_{1} :γ_{1}  , and T_{1}, a_{1}\a_{2} :v_{0} ⊢ a_{2} : v_{0}(γ_{1})

g((a_{1}\a_{2})/a_{3}) = T_{2} :T′_{2} ⊢ a_{3} :γ_{2}  T_{1} :T′_{1} ⊢ a_{1} :γ_{1} . T_{1} :T′_{1}, (a_{1}\a_{2})/a_{3}, T_{2} :T′_{2} ⊢ a_{2} :v_{0}(γ_{2})(γ_{1})

Note that g((a_{1}\a_{2})/a_{3}) is the same rule as (34). Now consider the second example, (s/(n\s))\s. Since #(s/(n\s)) = 1:

f(T_{i}:T′_{i} ⊢ s/(n\s):λv_{1}...λv_{#(s/(n\s))}.γ_{i}) = T_{i}:T′_{i}, n\s:v_{1} ⊢ s:γ_{i}.

Hence, and because g(s) = s:v_{0} ⊢ s:v_{0}:

g((s/(n\s))\s) =  T_{1} :T′_{1}, n\s:v_{1} ⊢ s:γ_{1}  . T_{1} :T′_{1}, (s/(n\s))\s:v_{0} ⊢ s:v_{0}(λv_{1}.γ_{1})

Since #(n) = 0:

f(T_{i}:T′_{i} ⊢ n:λv_{1}...λv_{#(n)}.γ_{i}) = T_{i}:T′_{i} ⊢ n:γ_{i}.

17Since the expressions T_{1} : T′_{1}, …, T_{#(c)} : T′_{#(c)} and γ_{1}, …, γ_{#(c)} are distinguished by their subscripts, each T_{i}: T′_{i} and γ_{i} can be instantiated independently. Strictly speaking, the variables v_{1}, … v_{#(b_{i})} and v_{1}, … v_{#(b_{j})} occurring in different premises σ_{i} and σ_{j} of a rule g(c), as well as their counterparts in the conclusion of g(c), should be distinguished for the same reason, for example in the following way:

v_{1}^{i}, … v_{#(b_{i})}^{i} and v_{1}^{j}, … v_{#(b_{j})}^{j}.

Readability considerations, however, restrained us from doing so.

Moreover, g(s) = s:v_{0} ⊢ s:v_{0}, so that:

g(n\s) =  T_{1} :T′_{1} ⊢ n:γ_{1}  . T_{1} :T′_{1}, n\s:v_{0} ⊢ s:v_{0}(γ_{1})

The rules g((s/(n\s))\s) and g(n\s) are identical to the ones in (35). Thus, our formal definition is consistent with the examples of Moortgat (1990).

Call an interpreted sequent c_{1} :v_{1}, … c_{n}:v_{n} ⊢ c:γ a PD (‘Partial Deduction’) theorem if and only if it is derivable using the axioms and rules in the set {g(c) | c ∈ {c_{1}, …, c_{n}}^{+} }.

Notice that all PD theorems have atomic goal categories. We will show that there exists a surjection h from L* proofs of sequents T : T′ ⊢ at* : γ with asterisked atomic goal categories to PD proofs of T:T′ ⊢ at :γ.

On account of Theorem 1 (see section 3 above), this entails that partial deduction preserves all (interpretations of) L-derivable sequents with atomic goal categories.

Moreover, on account of Theorem 2 (see section 4 above), the existence of h entails that partial deduction is devoid of spurious ambiguity in that it derives every interpretation only once. The function h is defined as follows. Let I_{1}, … I_{#(b)} ∈ {\R, /R}:

(a) h(at*:w ⊢ at :w [ * ] at :w ⊢ at*:w  ) = at :w ⊢ at :w;

(b) h(  π′  [I_{1}] ....  [I_{#(b)}] T:T′ ⊢ b*:β  π′′ [/L] U:U′, a/b*:w, T:T′, V :V′ ⊢ at :γ[v:=w(β)] [ * ] U:U′, a/b:w, T:T′, V :V′ ⊢ at*:γ[v:=w(β)]  )=

h(π′)  … π_{n}  π_{1} [g(a/b)] iff U:U′, a/b:w, T:T′, V :V′ ⊢ at :γ[v:=w(β)]

h(  π′′  [ * ] U:U′, a:v, V :V′ ⊢ at*:γ )= π_{n}  …  π_{1} [g(a)]; U:U′, a:v, V :V′ ⊢ at :γ

(c) h(  π′  [I_{1}] ....  [I_{#(b)}] T:T′ ⊢ b*:β  π′′ [\L] U:U′, T:T′, b\a*:w, V :V′ ⊢ at :γ[v:=w(β)] [ * ] U:U′, T:T′, b\a:w, V :V′ ⊢ at*:γ[v:=w(β)]  )=

h(π′)  … π_{n}  π_{1} [g(b\a)] iff U:U′, T:T′, b\a:w, V :V′ ⊢ at :γ[v:=w(β)]

h(  π′′  [ * ] U:U′, a:v, V :V′ ⊢ at*:γ )= π_{n}  …  π_{1} [g(a)]. U:U′, a:v, V :V′ ⊢ at :γ

On the level of proofs, the function h closely follows the pattern of the rule-building function g. Due to clause (a) of the definition of h, the most simple L* proofs π of sequents with asterisked atomic goal categories are mapped to PD proofs h(π) which instantiate the value of g for atomic categories. Moreover, clause (b) maps more complex L* proofs π of sequents with asterisked atomic goal categories to PD proofs h(π) in which the last rule applied is g(a/b), where a/b is a category occurring in the left-hand side of the conclusion sequent of π. The #(a/b) subproofs of h(π) which yield the premises of this application of the rule g(a/b) are determined by two subproofs – π′ and π′′ – of π: π′ is an L* proof of a sequent with asterisked atomic goal category, while π′′ extended with * (‘π′′ + *’) is an L* proof of a sequent with asterisked atomic goal category such that h(π′′ + *) is a PD proof in which the last rule applied is g(a). Now, given the way in which g(a/b) is defined (viz., in terms of g(a)), the conclusion of h(π′) plus the premises of g(a) in h(π′′ + *) can serve as the premises of an application of g(a/b) which infers the non-asterisked counterpart of the conclusion of π. (An isomorphic story can be told about clause (c).)

We will now prove the following facts: (1) for every L* proof π of a sequent Z: Z′ ⊢ at* : δ with asterisked atomic goal category, h(π) is a PD proof of Z: Z′ ⊢ at : δ; and (2) for every PD proof π, there is an L* proof π* such that h(π*) = π.

(1) That for every L* proof π of a sequent Z : Z′ ⊢ at* : δ with asterisked atomic goal, h(π) is a PD proof of Z:Z′ ⊢ at :δ is shown by induction on d, the degree of the conclusion Z:Z′ ⊢ at*:δ of π. Note that in view of its goal category at*, the sequent Z : Z′ ⊢ at* : δ, i.e., U : U′, c: w, W : W′ ⊢ at* : δ, must have been derived by the * rule from U:U′, c*:w, W:W′ ⊢ at :δ.

• d = 0. Then the sequent U:U′, c*:w, W:W′ ⊢ at :δ must be an L* axiom at*:w ⊢ at :w. This case is covered by clause (a) of the definition of h which states that h(π) = at :w ⊢ at :w, i.e., an application of g(at).

• d > 0. There are two possibilities: c = a/b or c = b\a. We only consider the former case. (The b\a case is analogous.) If c = a/b, then W : W′ = T : T′, V : V′ and δ ≡ γ[v:=w(β)], because U : U′, c* : w, W : W′ ⊢ at : δ, i.e., U : U′, a/b* : w, T : T′, V : V′ ⊢ at : γ[v:=w(β)], must have been inferred by /L from the premises (a) T:T′ ⊢ b*:β and (b) U:U′, a*:v, V :V′ ⊢ at :γ.

(a) As for the subproof of T :T′ ⊢ b*:β: such a sequent must have been inferred using * (if b = at), \R (if b = b′′\b′) or /R (if b = b′/b′′). Besides, premises of \R and /R inferences have asterisked goal categories as well. So this subproof must have the following form, where I_{1}, … I_{#(b)} ∈ {\R, /R}:

π′  π_{0}  [ * ] σ_{0}  [I_{1}] ....  [I_{#(b)}] T:T′ ⊢ b*:β

Note that since every I_{i} (1 ≤ i ≤ #(b)) adds an abstraction λu_{i} to the term assigned to the goal category of its premise, the term β must be of the form λu_{1}...λu_{#(b)}.β′. So, using the observation concerning f made above, we know that σ_{0} is the sequent f(T:T′ ⊢ b*:λu_{1} … λu_{#(b)}.β′). This sequent has an asterisked atomic goal and its degree is smaller than the degree of the conclusion of π. Hence we can apply the induction hypothesis to π′ and infer that h(π′) is a PD proof of f(T : T′ ⊢ b: λu_{1} … λu_{#(b)}.β′) – i.e., f(T:T′ ⊢ b*:λu_{1} … λu_{#(b)}.β′) minus asterisk.

(b) As for the subproof π′′ of U:U′, a*:v, V :V′ ⊢ at :γ: note that we can apply the Lemma of section 4 above: γ ≡ v(γ_{#(a)})...(γ_{1}), where v does not occur in γ_{1}, …, γ_{#(a)}. Moreover, the derivation π′′′ consisting of π′′ plus an additional * inference is an L* proof of a sequent with an asterisked atomic goal category:

π′′′ =  π′′ U:U′, a:v, V :V′ ⊢ at*:γ [ * ]

The degree of U : U′, a: v, V : V′ ⊢ at* : γ is smaller than the degree of the conclusion of π. Hence h(π′′′) is a PD proof of U:U′, a:v, V :V′ ⊢ at :γ by the induction hypothesis. Since γ ≡ v(γ_{#(a)})...(γ_{1}), we know that g(a) must be the last inference of h(π′′′), a proof which, therefore, has the following form:

h(π′′′) = π^{#(a)}  …  π^{1} U:U′, a:v, V :V′ ⊢ at :v(γ_{#(a)})...(γ_{1}) [g(a)]

Now, according to clause (b) of the definition of h,

h(π) =h(π′)  π^{#(a)}  …  π^{1} U:U′, a/b:w, T:T′, V :V′ ⊢ at :γ[v:=w(β)] [g(a/b)],

which is indeed a PD proof, for recall that

g(a/b)=f(T^{m+1} :T{′ \atop m+1} ⊢ b:λv^{1}...λv^{#(b)}.γ^{m+1})  σ^{#(a)} …  σ^{1} X, a/b:v_{0}, T_{m+1} :T′_{m+1}, Y ⊢ at :v_{0}(λv_{1}...λv_{#(b)}.γ_{m+1})(δ_{#(a)})...(δ_{1}) ,

where σ_{#(a)}, …, σ_{1} and X, a: v_{0}, Y ⊢ at : v_{0}(δ_{#(a)})...(δ_{1}) are the premises and conclusion of g(a), and note that

• apparently, the conclusions of the subproofs π_{#(a)}, …, π_{1} match the respective premises σ_{#(a)}, …, σ_{1} of the rule g(a) in such a way that at :v(γ_{#(a)})...(γ_{1}), U:U′, a:v and V :V′ match at :v_{0}(δ_{#(a)})...(δ_{1}), X, a:v_{0} and Y, respectively; and

• obviously, the conclusion f(T:T′ ⊢ b:λu_{1}...λu_{#(b)}.β′) of h(π′) matches the first premise f(T_{m+1} : T′_{m+1} ⊢ b : λv_{1}...λv_{#(b)}.γ_{m+1}) of the rule g(a/b) in such a way that T:T′ and λu_{1}...λu_{#(b)}.β′ match T_{m+1} :T′_{m+1} and λv_{1}...λv_{#(b)}.γ_{m+1}, respectively.

But this means that the conclusion of g(a/b) is matched by the sequent U : U′, a/b : w, T : T′, V : V′ ⊢ at : w(λu_{1}...λu_{#(b)}.β′)(γ_{#(a)})...(γ_{1}). Note, finally, that w(λu_{1} … λu_{#(b)}.β′)(γ_{#(a)})...(γ_{1}) ≡ γ[v:=w(β)], because γ ≡ v(γ_{#(a)})...(γ_{1}), the variable v does not occur in γ_{1}, …, γ_{#(a)}, and β ≡ λu_{1} … λu_{#(b)}.β′. □

(2) We show that for every PD proof π there is an L* proof π* such that h(π*) = π by induction on d, the degree of the conclusion Z: Z′ ⊢ at : δ of the proof π.

• d = 0. Then Z only contains atomic categories, so for c ∈ atom: π must match g(c) = at :v_{0} ⊢ at :v_{0}. Consequently, π = at :v ⊢ at :v, and:

at :v ⊢ at :v = h(at*:v ⊢ at :v [ * ] at :v ⊢ at*:v )

• d > 0. Then the conclusion of π must have been obtained by a derived inference rule g(c) such that the degree of c is greater than 0. So:

π = π_{#(a)+1} π_{#(a)} … π_{1} U:U′, b\a:w, W:W′ ⊢ at :δ [g(b\a)], or

π = π_{#(a)+1} π_{#(a)} … π_{1} U:U′, a/b:w, W:W′ ⊢at :δ [g(a/b)],

We will only consider the case of g(a/b). (The case of g(b\a) is analogous.) Then W:W′ = T:T′, V :V′ and γ ≡ w(λu_{1}...λu_{#(b)}.β′)(γ_{#(a)})...(γ_{1}), where (i) the conclusion of π_{#(a)+1} is f(T : T′ ⊢ b: λu_{1}...λu_{#(b)}.β′); and (ii) the conclusions of the subproofs π_{#(a)}, …, π_{1} match the respective premises σ_{#(a)}, …, σ_{1} of the rule g(a) in such a way that application of that rule to these sequents yields U:U′, a:v, V :V′ ⊢ at :v(γ_{#(a)})...(γ_{1}).

Since the degree of the sequents f(T : T′ ⊢ b : λu_{1}...λu_{#(b)}.β′) and U : U′, a : v, V : V′ ⊢ at : v(γ_{#(a)})...(γ_{1}) is smaller than the degree of the conclusion of π, we can apply the induction hypothesis to π_{#(a)+1} and ρ =

π_{#(a)}  …  π_{1} U:U′, a:v, V :V′ ⊢ at :v(γ_{#(a)})...(γ_{1}) [g(a)],

and conclude that there are L* proofs π_{#(a)+1}* and ρ* such that h(π_{#(a)+1}*) = π_{#(a)+1} and h(ρ*) = ρ.

Because π_{#(a)+1} and ρ are proofs of f(T : T ⊢ b : λu_{1}...λu_{#(b)}.β′) and U : U′, a: v, V : V′ ⊢ at : v(γ_{#(a)})...(γ_{1}), respectively, we know that π_{#(a)+1}* and ρ* are proofs of the asterisked sequents f(T : T ⊢ b* : λu_{1}...λu_{#(b)}.β′) and U:U′, a:v, V :V′ ⊢ at*:v(γ_{#(a)})...(γ_{1}), respectively.

As for π_{#(a)+1}*: it can be shown by induction on #(c) that any L* proof π* of f(T : T ⊢ c* : λu_{1}...λu_{#(c)}.β′) can be extended to an L* proof π*^{+} of T : T ⊢ c* : λu_{1}...λu_{#(c)}.β′ by adding #(c) \R and /R inferences to π*. Hence there exists such an L* proof π_{#(a)+1}*^{+} of T:T ⊢ b*:λu_{1}...λu_{#(b)}.β′.

As for ρ*: since U : U′, a: v, V : V′ ⊢ at* : v(γ_{#(a)})...(γ_{1}), the conclusion of ρ*, has an asterisked atomic goal which is assigned a term with leading variable v, we know (by the Lemma of section 4) that

ρ* =  ρ*′ U:U′, a:v, V :V′ ⊢ at*:v(γ_{#(a)})...(γ_{1}) [ * ],

where U:U′, a*:v, V :V′ ⊢ at :v(γ_{#(a)})...(γ_{1}) is the conclusion of ρ*′. Hence π*, the proof below, is an L* derivation, where I_{1}, …, I_{#(b)} ∈ {\R, /R}:

π_{#(a)+1}*  [I_{1}] ....  [I_{#(b)}] T:T′ ⊢ b*:λu_{1}...λu_{#(b)}.β′  π_{#(a)+1}*^{+}  ρ*′ [/L] U:U_{′}, a/b*:w, T:T_{′}, V :V_{′} ⊢ at :w(λu_{1}...λu_{#(b)}.β_{′})(γ_{#(a)})...(γ_{1}) [ * ] U:U′, a/b:w, T:T′, V :V′ ⊢ at*:w(λu_{1}...λu_{#(b)}.β′)(γ_{#(a)})...(γ_{1})

Finally, because h(ρ*) = ρ =

π_{#(a)}  …  π_{1} U:U′, a:v, V :V′ ⊢ at :v(γ_{#(a)})...(γ_{1}) [g(a)],

clause (b) of the definition of h tells us that h(π*) =

h(π_{#(a)+1}*)  π_{#(a)}  …  π_{1} U:U′, a/b:w, T:T′, V :V′ ⊢ at :w(λu_{1}...λu_{#(b)}.β′)(γ_{#(a)})...(γ_{1}) [g(a/b)]

And because h(π_{#(a)+1}*) = π_{#(a)+1}, we have that h(π*) =

π^{#(a)+1}  π^{#(a)}  …  π^{1} U:U′, a/b:w, T:T′, V :V′ ⊢ at :w(λu_{1}...λu_{#(b)}.β′)(γ_{#(a)})...(γ_{1}) [g(a/b)],

which is nothing else but π. □

By way of illustration, we return to the sample sequents c/c, c/c, c ⊢ c and s/(n\s), (n\s)/n, (s/n)\s ⊢ s treated in the previous sections. The categories c/c and c generate one rule and one axiom:

T_{1} :T′_{1} ⊢ c:γ_{1} c/c:v_{0}, T_{1} :T′_{1} ⊢ c:v_{0}(γ_{1}) [g(c/c)]

c:v_{0} ⊢ c:v_{0} [g(c)] These yield one PD derivation of c/c, c/c, c ⊢ c, viz., (36). Observe that (36) = h(31):

\begin{matrix}c:x ⊢ c:x & c/c:y, c:x ⊢ c:y(x) & [g(c/c)] & [g(c/c)] & c/c:z, c/c:y, c:x ⊢ c:z(y(x)) \\ (36) \end{matrix}

The categories s/(n\s), (s/n)\s and (n\s)/n generate the following rules and axiom:

n:v_{1}, T_{1} :T′_{1} ⊢ s:γ_{1}  [g(s/(n\s))] s/(n\s):v_{0}, T_{1} :T′_{1} ⊢ c:v_{0}(λv_{1}.γ_{1})

T_{1} :T′_{1}, n:v_{1} ⊢ s:γ_{1}  [g((s/n)\s)] T_{1} :T′_{1}, (s/n)\s:v_{0} ⊢ c:v_{0}(λv_{1}.γ_{1})

n:v_{0} ⊢ n:v_{0} [g(n)]

T_{2} :T′_{2} ⊢ n:γ_{2}  T_{1} :T′_{1} ⊢ n:γ_{1} [g((n\s)/n)] T_{1} :T′_{1}, (n\s)/n:v_{0}, T_{2} :T′_{2} ⊢ c:v_{0}(γ_{2})(γ_{1})

These yield two proofs of s/(n\s), (n\s)/n, (s/n)\s ⊢ s, viz., (37) and (38), where (37) = h(32) and (38) = h(33):

\begin{matrix}n:w′ ⊢ n:w′ & n:u′ ⊢ n:u′ & [g((n\s)/n)] & n:u′, (n\s)/n:v, n:w′ ⊢ s:v(w′)(u′) & [g((s/n)\s)] & n:u′, (n\s)/n:v, (s/n)\s:w ⊢ s:w(λw′.v(w′)(u′)) & [g(s/(n\s))] & s/(n\s):u, (n\s)/n:v, (s/n)\s:w ⊢ s:u(λu′.w(λw′.v(w′)(u′))) \\ (37) \end{matrix}

\begin{matrix}n:w′ ⊢ n:w′ & n:u′ ⊢ n:u′ & [g((n\s)/n)] & n:u′, (n\s)/n:v, n:w′ ⊢ s:v(w′)(u′) & [g(s/(n\s))] & s/(n\s):u, (n\s)/n:v, n:w′ ⊢ s:u(λu′.v(w′)(u′)) & [g((s/n)\s)] & s/(n\s):u, (n\s)/n:v, (s/n)\s:w ⊢ s:w(λw′.u(λu′.v(w′)(u′))) \\ (38) \end{matrix}

5.2 Proof Nets

Roorda (1991) introduces so-called proof nets – which were invented for linear logic by Girard (1987) – for the Lambek calculus. Proof nets are proposed as a solution to the problem of spurious ambiguity, in that they replace ‘inessential’ order of rule applications in sequent proofs by ‘parallellism’.

In the present section we will assess the merits of this proposal. We start with the definition of proof nets given in Roorda (1991), which is listed in (a) through (g) below. Next, an alternative, equivalent definition is presented in (a′) through (h′). While Roorda’s definition recursively introduces connectives, the alternative one proceeds by adding links. This different set-up has two advantages. First, it allows a direct, inductive definition of the semantic interpretation of proof nets – see the definition given in (a′′) through (h′′). And second, it brings out the correspondence between applying rules in L* and adding links to proof nets: there will turn out to be a one-many relationship between L* proofs and proof nets.

Basically, a proof net is a structure of linked signed categories. For the product-free Lambek calculus, the following links are distinguished:

at^{−} at^{+} ax at^{+} at^{−} ax  b^{+} a^{−} \2 b\a^{−}  a^{−} b^{+} /2 a/b^{−} a^{+} b^{−} \1 b\a^{+}  b^{−} a^{+} /1 a/b^{+}

(39)

Below, the expressions X, Y and Z will denote sequences of signed categories, and tc(C) will be used for the sequence of so-called terminal (signed) categories of a proof net C.

pn, the set of proof nets, is the smallest set satisfying the clauses (a) through (g) below, which also specify the sequence tc(C) for each C ∈ pn:^{18} (a) \overline{at^{−} at^{+}} ∈ pn and \overline{at^{+} at^{−}} ∈ pn;

18This definition is based on the definition in Roorda (1991, p. 30), but there are two differences: (i) the condition ‘X or Y is non-empty’ has been added to clause (b) and (c), to the effect that every proof net has at least one terminal category signed ‘−’.

This mirrors the ‘non-empty antecedent property’ of L, i.e., the fact that the left-hand side of L-derivable sequents is non-empty, a property which was effectuated in (4) above by requiring that T denote a non-empty sequence of categories (Roorda (1991, p. 37)

captures this aspect by a ‘proof net condition’ on the assignment of lambda terms); and (ii) anticipating the semantic interpretation of proof nets, the various cases collapsed by Roorda have been disentangled. (Note, for that matter, that Roorda collapses too much: his clauses 2a and 2b – which comprise the clauses (d) and (g), and (e) and (f), respectively – have the same condition: ‘if β and γ are proof nets with terminal formulas tA resp. uBv’ (t, u, v and A, B range over sequences of signed categories and signed categories,

tc(\overline{at^{−} at^{+}}) = at^{−},at^{+} and tc(\overline{at^{+} at^{−}}) = at^{+},at^{−};

(b) if A ∈ pn and tc(A) = X, a^{+}, b^{−}, Y and X or Y is non-empty, then C ∈ pn, where C results from applying \1 to a^{+} and b^{−};

tc(C) = X, b\a^{+}, Y;

(c) if A ∈ pn and tc(A) = X, b^{−}, a^{+}, Y and X or Y is non-empty, then C ∈ pn, where C results from applying /1 to b^{−} and a^{+};

tc(C) = X, a/b^{+}, Y;

(d) if A ∈ pn and tc(A) = X, a^{−}, Y and B ∈ pn and tc(B) = Z, b^{+}, then C ∈ pn, where C results from applying \2 to b^{+} and a^{−};

tc(C) = X, Z, b\a^{−}, Y;

(e) if A ∈ pn and tc(A) = X, b^{+}, Y and B ∈ pn and tc(B) = a^{−}, Z, then C ∈ pn, where C results from applying \2 to b^{+} and a^{−};

tc(C) = X, b\a^{−}, Z, Y;

(f) if A ∈ pn and tc(A) = X, a^{−}, Y and B ∈ pn and tc(B) = b^{+}, Z, then C ∈ pn, where C results from applying /2 to a^{−} and b^{+};

tc(C) = X, a/b^{−}, Z, Y;

(g) if A ∈ pn and tc(A) = X, b^{+}, Y and B ∈ pn and tc(B) = Z, a^{−}, then C ∈ pn, where C results from applying /2 to a^{−} and b^{+};

tc(C) = X, Z, a/b^{−}, Y.

The proof nets defined in clause (a) correspond to the axioms of L (where observation A of section 3 above – entailing the possibility of having only axiom sequents with atomic categories – has been incorporated), while the clauses (b), (c), (d) + (e), and (f) + (g) are the proof net counterparts of the L rules \R, /R, \L and /L, respectively.

On account of the clauses (d), (e), (f) and (g), two separate proof nets can be combined into one: application of \2 and /2 has the effect of inserting proof net B into proof net A.

respectively). Since one has to be ‘strict on order and adjacency of premises in proof nets’ (1991, p. 30), however, this will not work for clause 2b, which needs a separate condition, viz., ‘if β and γ are proof nets with terminal formulas At resp. uBv’.)

Note that for every proof net C, the sequence tc(C) consists of exactly one category signed ‘+’ and at least one category signed ‘−’. We will call the unique positively signed category in tc(C) the goal of C, which will be denoted by go(C). A proof net C corresponds to a sequent T ⊢ c iff

T = c_{1}, …, c_{i}, c_{i+1}, …, c_{n} and tc(C) = c_{i+1}^{−}, …, c_{n}^{−}, c^{+}, c_{1}^{−}, …, c_{i}^{−}.

By way of illustration of the definition, consider proof net (40), which corresponds to the L-derivable sequent a/b, b/c ⊢ a/c; tc(40) is the sequence listed in (40′).

(40′) b/c^{−}, a/c^{+}, a/b^{−}
b^{−} c^{+} b/c^{−}  c^{−} a^{+} a/c^{+}  a^{−} b^{+} a/b^{−}

(40)

Proof net (40) can be built up in two ways from the basic proof nets in (41), which have the sequences of terminal categories listed in (42):

(i)  ax b^{−}  b^{+}  (ii)  ax c^{+}  c^{−}  (iii)  ax a^{+}  a^{−}

(41)

{tc(i) =b^{−}, b^{+} ; tc(ii) =c^{+}, c^{−} ; tc(iii) =a^{+}, a^{−} . \atop (42)}

A first possibility is that we add a /2 link to a^{−} in (iii) and b^{+} in (i), due to clause (g) (where (i) and (iii) instantiate A and B, respectively). Note that (iii) is inserted into (i). The resulting proof net (43) has the terminal categories indicated in (43′):

(43′) b^{−}, a^{+}, a/b^{−}
a^{+}  a^{−} b^{+} b^{−}  /2 a/b^{−}

(43)

Next, we can add a /2 link to b^{−} in (43) and c^{+} in (ii), due to clause (f) (where (43) and (ii) instantiate A and B, respectively): (ii) is inserted into (43). The resulting proof net (44) has the terminal categories indicated in (44′):

(44′) b/c^{−}, c^{−}, a^{+}, a/b^{−}
b^{−} c^{+}  c^{−} a^{+} /2 b/c^{−}  a^{−} b^{+} a/b^{−}

(44)

Secondly, we may add a /2 link to b^{−} in (i) and c^{+} in (ii), due to clause (f) (where (i) and (ii) instantiate A and B, respectively): (ii) is inserted into (i). The resulting proof net (45) has the terminal categories indicated in (45′):

(45′) b/c^{−}, c^{−}, b^{+}
b^{−} c^{+}  c^{−} /2 b/c^{−}  b^{+}

(45)

Next, we can add a /2 link to a^{−} in (iii) and b^{+} in (45), due to clause (g) (where (45) and (iii) instantiate A and B, respectively): (iii) is inserted into (45). The resulting proof net (46) is identical to (44):

(46′) b/c^{−}, c^{−}, a^{+}, a/b^{−}
b^{−} c^{+}  c^{−} a^{+} b/c^{−}  a^{−} b^{+}/2 a/b^{−}

(46)

Finally, the addition of a /1 link (by clause (c)) to the categories c^{−} and a^{+} in proof net (44) (= (46)) yields proof net (40).

The above definition of the set pn is equivalent to the following one (in the sense that pn = pn_{2}), in which two sets, pn_{1} and pn_{2}, are defined as the smallest sets such that:

(a′) at^{−} at^{+} ∈pn_{1} and at^{+} at^{−} ∈pn_{1};

tc(at^{−} at^{+}) = at^{−},at^{+} and tc(at^{+} at^{−}) = at^{+},at^{−};

(b′) if A ∈ pn_{2} and tc(A) = X, a^{+}, b^{−}, Y and X or Y is non-empty,

then C ∈ pn_{2}, where C results from applying \1 to a^{+} and b^{−};

tc(C) = X, b\a^{+}, Y;

(c′) if A ∈ pn_{2} and tc(A) = X, b^{−}, a^{+}, Y and X or Y is non-empty, then C ∈ pn_{2}, where C results from applying /1 to b^{−} and a^{+};

tc(C) = X, a/b^{+}, Y;

(d′) if A ∈ pn_{1} and tc(A) = X, a^{−}, Y and B ∈ pn_{2} and tc(B) = Z, b^{+},

then C ∈ pn_{1}, where C results from applying \2 to b^{+} and a^{−};

tc(C) = X, Z, b\a^{−}, Y;

(e′) if A ∈ pn_{2} and tc(A) = X, b^{+}, Y and B ∈ pn_{1} and tc(B) = a^{−}, Z,

then C ∈ pn_{1}, where C results from applying \2 to b^{+} and a^{−};

tc(C) = X, b\a^{−}, Z, Y;

(f′) if A ∈ pn_{1} and tc(A) = X, a^{−}, Y and B ∈ pn_{2} and tc(B) = b^{+}, Z,

then C ∈ pn_{1}, where C results from applying /2 to a^{−} and b^{+};

tc(C) = X, a/b^{−}, Z, Y;

(g′) if A ∈ pn_{2} and tc(A) = X, b^{+}, Y and B ∈ pn_{1} and tc(B) = Z, a^{−},

then C ∈ pn_{1}, where C results from applying /2 to a^{−} and b^{+};

tc(C) = X, Z, a/b^{−}, Y;

(h′) if A ∈ pn_{1} and tc(A) = X, at^{+}, Y, then C ∈ pn_{2}, where C results from

applying ax to at^{+} and the non-connected occurrence of at^{−} in A;

tc(C) = X, at^{+}, Y.

Note (i) that for all A ∈ pn_{1}: go(A) is an atomic category; (ii) that every A ∈ pn_{1} contains exactly two occurrences of an atomic category at which are not connected by ax, viz., go(A) and one negatively signed occurrence of at; and (iii) that if C ∈ pn_{2}, then all occurrences of atomic categories in C are connected by ax. Hence clause (h′) yields a C ∈ pn_{2} for every A ∈ pn_{1}.

Let C ∈ pn_{2} be such that go(C) = at. The ax link which connects go(C) with some negatively signed occurrence of at will be called the goal link of C, and C^{−} will denote the structure from which C is obtained by adding a goal link. Obviously, if C ∈ pn_{2} is obtained from A ∈ pn_{1} by clause (h′), then A = C^{−}.

Now, the set pn_{1} is equal to { C^{−} | C ∈ pn & go(C) ∈ atom }, while pn_{2} is the same set as pn. This is shown by induction on the degree of tc(C):

• Observe that (b) through (g) and (b′) through (g′) yield structures C with d(tc(C)) > 0. Consequently, if d(tc(C)) = 0, then: (i) C ∈ pn must be due to (a), therefore C = \overline{at^{−} at^{+}} or C = \overline{at^{+} at^{−}}; and (ii) C ∈ pn_{2} must be due to (h′), i.e., C is obtained from C^{−} ∈ pn_{1}, where d(tc(C^{−})) = d(tc(C)) = 0. So, C^{−} ∈ pn_{1} must be due to (a′): C^{−} = at^{−} at^{+} (and C = \overline{at^{−} at^{+}}) or C^{−} = at^{+} at^{−} (and C = \overline{at^{+} at^{−}}).

• If d(tc(C)) > 0, then either (i) go(C) = b\a (or, analogously, a/b); or (ii) go(C) ∈ atom. ∘ (i) If go(C) = b\a and C ∈ pn, then tc(C) = X, b\a^{+}, Y, and – by an ‘easily verifiable’ fact^{19} – for some A ∈ pn with tc(A) = X, a^{+}, b^{−}, Y: C can be obtained by applying (b) to A. Conversely, C ∈ pn_{2} must be obtained by applying (b′) to A ∈ pn_{2}. Since A ∈ pn iff A ∈ pn_{2} by induction hypothesis, we have that C ∈ pn iff C ∈ pn_{2}. ∘ (ii) If go(C) ∈ atom, then C ∈ pn is due to (d), (e), (f) or (g). Suppose (d) is involved. Then tc(C) = X, Z, b\a^{−}, Y, and C is the result of applying \2 to b^{+} in B ∈ pn and a^{−} in A ∈ pn , where tc(B) = Z, b^{+} and tc(A) = X, a^{−}, Y. By induction hypothesis: B ∈ pn_{2} and A ∈ pn_{2}. Since go(B) = b, we have that at = go(A). Therefore, A ∈ pn_{2} must have been obtained by (h′) from A^{−} ∈ pn_{1}, i.e., A with missing goal link. By (d′), we can apply \2 to a^{−} in A^{−} ∈ pn_{1} and b^{+} in B ∈ pn_{2}, yielding C^{−} ∈ pn_{1}, i.e., C with missing goal link, which, by (h′), can be added so as to obtain C as a member of pn_{2}. (The cases (e), (f) and (g) are analogous.) Conversely, C ∈ pn_{2} must have been obtained by (h′) from C^{−} ∈ pn_{1}. Note that tc(C^{−}) = tc(C) and d(tc(C)) > 0, so C^{−} ∈ pn_{1} must be due to (d′), (e′), (f′) or (g′). If (d′) is responsible, then tc(C^{−}) = X, Z, b\a^{−}, Y, and C^{−} results from applying \2 to b^{+} in B ∈ pn_{2} and a^{−} in A′ ∈ pn_{1}, where tc(A′) = X, a^{−}, Y and tc(B) = Z, b^{+}. By induction hypothesis: A′ = A^{−} for A ∈ pn, while B ∈ pn. Therefore, by (d), we can apply \2 to b^{+} in B ∈ pn and a^{−} in A ∈ pn, yielding C^{−} with additional goal link – i.e., C – as a member of pn. (The cases (e′), (f′) and (g′) are analogous.) □

19Viz., the proof net version of observation B made in section 3 above: If C ∈ pn and tc(C) = X, b\a^{+}, Y (or X, a/b^{+}, Y), then there is an A ∈ pn with tc(A) = X, a^{+}, b^{−}, Y (or X, b^{−}, a^{+}, Y) such that C results from applying (b) (or (c)) to A. (Roorda (1991), p. 33)

It was said above that the definition of the set of proof nets in terms of (a′) through (h′) has two pleasant properties: (i) it allows a direct, inductive definition of the semantic interpretation of proof nets, and (ii) it brings out the correspondence between the application of rules in L* and the addition of links to proof nets.

As for (i): let u and v be different variables; let the sets of variables occurring in A and B be disjoint; let w be a variable which does not occur in A and B; and let A[v:=γ] denote the structure which results from A ∈ pn_{1} by replacing all occurrences of the variable v in A by the term γ. Then the semantic interpretation of proof nets can be defined as follows:

(a′′) at^{−}:u at^{+}:v ∈pn_{1} and at^{+}:v at^{−}:u∈pn_{1};

tc(at^{−}:u at^{+}:v) = at^{−}:u, at^{+}:v and tc(at^{+}:v at^{−}:u) = at^{+}:v, at^{−}:u; (b′′) if A ∈ pn_{2} and tc(A) = X, a^{+}:α, b^{−}:v, Y and X or Y is non-empty,

then C ∈ pn_{2}, where C results from applying \1 to a^{+}:α and b^{−}:v in A;

tc(C) = X, b\a^{+}:λv.α, Y;

(c′′) if A ∈ pn_{2} and tc(A) = X, b^{−}:v, a^{+}:α, Y and X or Y is non-empty, then C ∈ pn_{2}, where C results from applying /1 to b^{−}:v and a^{+}:α in A;

tc(C) = X, a/b^{+}:λv.α, Y;

(d′′) if A ∈ pn_{1} and tc(A) = X, a^{−}:v, Y and B ∈ pn_{2} and tc(B) = Z, b^{+}:β, then C ∈ pn_{1}, where C results from applying \2 to b^{+}:β in B and a^{−}:w(β) in A[v:=w(β)];

tc(C) = X′, Z, b\a^{−}:w, Y′, where X′, a^{−}:w(β), Y′ = tc(A[v:=w(β)]);

(e′′) if A ∈ pn_{2} and tc(A) = X, b^{+}:β, Y and B ∈ pn_{1} and tc(B) = a^{−}:v, Z, then C ∈ pn_{1}, where C results from applying \2 to b^{+}:β in A and a^{−}:w(β) in B[v:=w(β)]; tc(C) = X, b\a^{−}:w, Z′, Y, where a^{−}:w(β), Z′ = tc(B[v:=w(β)]);

(f′′) if A ∈ pn_{1} and tc(A) = X, a^{−}:v, Y and B ∈ pn_{2} and tc(B) = b^{+}:β, Z, then C ∈ pn_{1}, where C results from applying /2 to a^{−}:w(β) in A[v:=w(β)] and b^{+}:β in B;

tc(C) = X′, a/b^{−}:w, Z, Y′, where X′, a^{−}:w(β), Y′ = tc(A[v:=w(β)]);

(g′′) if A ∈ pn_{2} and tc(A) = X, b^{+}:β, Y and B ∈ pn_{1} and tc(B) = Z, a^{−}:v, then C ∈ pn_{1}, where C results from applying /2 to a^{−}:w(β) in B[v:=w(β)] and b^{+}:β in A; tc(C) = X, Z′, a/b^{−}:w, Y, where Z′, a^{−}:w(β) = tc(B[v:=w(β)]);

(h′′) if A ∈ pn_{1}, tc(A) = X, at^{+}:v, Y and at^{−}:γ in A is not connected by ax, then C ∈ pn_{2}, where C results from applying ax to at^{+}:γ and at^{−}:γ in A[v:=γ]; tc(C) = tc(A[v:=γ]).

The proof nets C defined in (b′′), (c′′), (d′′), (e′′), (f′′), (g′′), and (h′′) will be called \1(A), /1(A), \2(A^{w/v}, B), \2(A, B^{w/v}), /2(A^{w/v}, B), /2(A, B^{w/v}) and ax(A), respectively.

Though it is not exactly simple, the above definition is straightforward in comparison with the indirect semantic interpretation procedure given in Roorda (1991, pp. 34–38):

First, the set of proof frames pf is defined as the smallest set such that:

(a) if X is a list of signed atomic categories, then X ∈ pf; tc(X) = X;

(b) if A ∈ pf and tc(A) = X, a^{+}, b^{−}, Y, then C ∈ pf, where C results from

applying \1 to a^{+} and b^{−} in A; tc(C) = X, b\a^{+}, Y;

(c) if A ∈ pf and tc(A) = X, b^{−}, a^{+}, Y, then C ∈ pf, where C results from

applying /1 to b^{−} and a^{+} in A; tc(C) = X, a/b^{+}, Y;

(d) if A ∈ pf and tc(A) = X, b^{+}, a^{−}, Y, then C ∈ pf, where C results from

applying \2 to b^{+} and a^{−} in A; tc(C) = X, b\a^{−}, Y;

(e) if A ∈ pf and tc(A) = X, a^{−}, b^{+}, Y, then C ∈ pf, where C results from

applying /2 to a^{−} and b^{+} in A; tc(C) = X, a/b^{−}, Y.

Moreover, a proof structure is defined as a proof frame together with a linking of all its atomic categories by ax links, and a planar proof structure is defined as a proof structure of which the ax links do not cross.^{20}

Second, for every category occurrence in a proof structure C a lambda term is constructed:

(i) every category occurrence in tc(C) is assigned a different variable;

(ii) the assignment of terms to the conclusions of \2, /2, \1 and /1 links

in C is extended to the premises of these links in the following way:

b^{+}:? a^{−}:¿ \2 b\a^{−}:γ  a^{−}:¿ b^{+}:? /2 a/b^{−}:γ

In \2 and /2 links, the category b^{+} is assigned a fresh variable u,

and the term assigned to a^{−} is γ(u).

a^{+}:¿ b^{−}:? \1 b\a^{+}:δ  b^{−}:? a^{+}:¿ /1 a/b^{+}:δ

20Though a proof net also consists of linked signed categories of which the atomic ones are all connected by non-crossing ax links, the set of planar proof structures is considerably larger than the set pn defined earlier. This is due to the fact that on account of the clauses (b) through (e) above, the links \1, /1, \2 and /2 are allowed to connect any pair of adjacent (and appropriately signed) categories in a proof structure. The clauses (b) through (g), on the other hand, have the effect that the links \1 and /1 only connect adjacent terminal categories of a single proof structure, whereas the links \2 and /2 only connect adjacent terminal categories of separate proof structures.

In \1 and /1 links, the respective terms assigned to b^{−} and a^{+} are

two different fresh variables u and v, and the conclusion term δ

is rewritten^{21} as λu.v.

(iii) every ax link in C which connects at^{+}:γ and at^{−}:δ induces a sub-

stitution^{22} of γ by δ. This substitution is global: it involves all

occurrences of γ in C.

Third, Roorda supplies a list of five^{23} ‘proof net conditions’ which a proof structure interpreted in the way indicated in (i) through (iii) must observe in order to be a proof net, and shows that the set of proof nets corresponding to L-derivable sequents is identical to the set of planar proof structures which satisfy these conditions. Except for the first one (which requires that there be exactly one terminal category signed ‘+’), these conditions constrain the

21Positively signed categories are always assigned variables, so this rewriting of δ is essentially a substitution. Moreover, though Roorda (1991) does not mention this, the substitution will have to be global: just as the substitution specified in (iii) below, it must affect all occurrences of δ in the proof structure. This can be seen as follows:

a^{−}:x_{1}(x_{3})(x_{4}) a/b^{−}:x_{1}(x_{3})  c^{+}:x_{3} (a/b)/c^{−}:x_{1} b^{+}:x_{4}  c^{−}:x_{5}  b^{−}:x_{7}  a^{+}:x_{8} a/b^{+}:x_{6} (a/b)/c^{+}:x_{2}

Stage (i) yields the initial assignment of x_{1} and x_{2}; the clause for /2 in stage (ii) takes care of the assignment of x_{1}(x_{3}), x_{3}, x_{1}(x_{3})(x_{4}) and x_{4}. Now, the clause for /1 assigns x_{5} and x_{6}, substitutes x_{2} by λx_{5}.x_{6}, assigns x_{7} and x_{8}, and substitutes x_{6} by λx_{7}.x_{8}. If the latter substitution is local and does not affect the occurrence of x_{6} in λx_{5}.x_{6}, then after (iii) (which – globally – replaces x_{8}, x_{3} and x_{4} by x_{1}(x_{3})(x_{4}), x_{5}, and x_{7}, respectively) the undesirable term λx_{5}.x_{6} is obtained for the goal of the proof net. Global substitution, on the other hand, will eventually yield the right result, viz., λx_{5}λx_{7}.x_{1}(x_{5})(x_{7}).

22Roorda says that γ and δ are unified but that γ is always a variable, so ‘the unification is nothing else than the substitution [of γ by δ]’ (1991, p. 35). The notion of unification is probably invoked for the reason that Roorda wants the process to fail, ‘typically’ when γ occurs in δ. ‘In that case we draw the conclusion that the proof structure is not a proof net, and we do not provide a lambda term.’ (1991, p. 35). (Note that a substitution under such circumstances would be impeccable.) However, the fact that this eventuality does not arise in pn_{1} ∪ pn_{2} kept us from taking over this subtlety.

23In fact, a sixth proof net condition enforces the ‘non-empty antecedent property’ alluded to in footnote 18 above.

assignment of lambda terms to proof structures.

Their precise contents need not concern us here, since the equivalence of the interpretation procedures specified in (a′′) through (h′′) and (i) through (iii) for members C of the set pn_{1} ∪ pn_{2} can be established directly:^{24} it is easy to see that both (i) through (iii) and (a′′) through (h′′) license an assignment of lambda terms to category occurrences in C ∈ pn_{1} ∪ pn_{2} iff:

• every c^{−} occurring in tc(C) is assigned a different variable;

• the assignment to every \1, /1, \1 and /2 link in C is as follows:

b^{+}:β a^{−}:α(β) \2 b\a^{−}:α  a^{−}:α(β) b^{+}:β /2 a/b^{−}:α

a^{+}:γ b^{−}:v \1 b\a^{+}:λv.γ  b^{−}:v a^{+}:γ /1; and a/b^{+}:λv.γ

• if an ax link connects at^{−}:γ and at^{+}:δ, then γ is identical to δ.

Do proof nets consitute a solution to the problem of spurious ambiguity? Observe that the proof net semantics defined above in (b′′) through (h′′) is closely related to L*, viz., via the function k from L* proofs to the power set of pn_{1} ∪ pn_{2} which is defined below.

As before, we let π[T:T′ ⊢ c:γ] represent that π is an L* proof with interpreted conclusion sequent T:T′ ⊢ c:γ.

• k(at*:v ⊢ at :v) = {at^{−}:v at^{+}:u | u ≠ v} ∪ {at^{+}:u at^{−}:v | u ≠ v};

• for π[b:v, T:T′ ⊢ a*:α]: k(  [\R] π T:T′ ⊢ b\a*:λv.α  ) = {\1(A) | A ∈ k(π)};
• for π[T:T′, b:v ⊢ a*:α]: k(  [/R] π T:T′ ⊢ a/b*:λv.α  ) = {/1(A) | A ∈ k(π)};

• for π_{1}[T:T′ ⊢ b*:β] and π_{2}[U:U′, a*:v, V :V′ ⊢ at :γ]:

24Strictly speaking, the set pn_{1} transcends the range of the clauses (i) through (iii), because its members fail to be proof structures. However, they can be incorporated easily, for instance by allowing (i) through (iii) to operate on members of the set po (of proof objects): the smallest set which includes the set pf defined above and is closed under the operation of adding ax links.

k(  [\L] π_{1}  π_{2} U:U′, T:T′, b\a*:w, V :V′ ⊢ at :γ[v:=w(β)] ) =

{\2(A^{w/v}, B) | A ∈ k(π_{2}) & B ∈ k(π_{1}) & tc(B) =T^{−}:T′, b^{+}:β} ∪

{\2(A, B^{w/v}) | A ∈ k(π_{1}) & B ∈ k(π_{2}) & tc(B) =a^{−}:v, V^{−}:V′, at^{+}:u, U^{−}:U′};

k(  [/L] π_{1}  π_{2} U:U′, a/b*:w, T:T′, V :V′ ⊢ at :γ[v:=w(β)] ) =

{/2(A^{w/v}, B) | A ∈ k(π_{2}) & B ∈ k(π_{1}) & tc(B) =b^{+}:β, T^{−}:T′} ∪

{/2(A, B^{w/v}) | A ∈ k(π_{1}) & B ∈ k(π_{2}) & tc(B) =V^{−}:V′, at^{+}:u, U^{−}:U′, a^{−}:v};

• for π[U:U′, a*:v, V :V′ ⊢ at :γ]: k( [ * ] π U:U′, a:v, V :V′ ⊢ at*:γ ) =

{ax(A) | A ∈ k(π)}.

Next, for (non-asterisked) interpreted sequents T : T′ ⊢ c: γ, we define the set cp(T:T′ ⊢ c:γ) of cyclic permutations of T:T′ ⊢ c:γ, as follows:

cp(T:T′ ⊢ c:γ) = {T_{2}^{−}:T′_{2}, c^{+}:γ, T_{1}^{−}:T′_{1} | T:T′ = T_{1} :T′_{1}, T_{2} :T′_{2}}.

Note that a proof net C corresponds to a sequent T : T′ ⊢ c : γ if and only if tc(C) ∈ cp(T : T′ ⊢ c : γ). By a straightforward induction on the length of π (which will be omitted here) it can be proven that for L* proofs π[T:T′ ⊢ c*:γ] and ρ[U:U, c*:v, V :V′ ⊢ at :γ]:

k(π) = {C ∈ pn_{2} | tc(C) ∈ cp(T:T′ ⊢ c:γ)}; and

k(ρ) = {A ∈ pn_{1} | for some u: tc(A) ∈ cp(U:U′, c:v, V :V′ ⊢ at :u)

and at^{−}:γ occurs not connected by ax in A}.

So, the function k assigns a subset of pn_{2} to every L* proof of a sequent with an asterisked goal and a subset of pn_{1} to every L* proof of a sequent with a non-asterisked goal.

Moreover, the set {k(π) | π is an L* proof } partitions pn_{1} ∪ pn_{2}, for (i) it is obvious that every C ∈ pn_{1} ∪ pn_{2} is a member of at least one k(π); and (ii) Theorem 2 (see section 4 above) entails that every C ∈ pn_{1} ∪ pn_{2} is a member of at most one k(π).

Now, since for every L-derivable sequent c_{1} :v_{1}, …, c_{n}:v_{n} ⊢ c:γ there is one L* derivation of c_{1} :v_{1}, …, c_{n}:v_{n} ⊢ c*:γ′ such that γ = γ′ and since for a sequent c_{1} :v_{1}, …, c_{n}:v_{n} ⊢ c:γ the set cp(c_{1} :v_{1}, …, c_{n}:v_{n} ⊢ c:γ) contains n+1 members, the above means that every reading of an L-derivable sequent c_{1}, …, c_{n} ⊢ c corresponds to n + 1 proof nets.

Accordingly, there are four proof nets for the sequent c/c, c/c, c ⊢ c, and eight proof nets for s/(n\s), (n\s)/n, (s/n)\s ⊢ s.^{25} Note that the proof nets in (47) make up k(31), and that the proof nets in (48) and (49) constitute k(32) and k(33), respectively.

(47) _{c^{+}:z(y(x)) c^{−}:z(y(x)) c^{+}:y(x) c/c^{−}:z  c^{−}:y(x) c^{+}:x c/c^{−}:y  c^{−}:x}

c^{−}:x c^{+}:z(y(x)) c^{−}:z(y(x)) c^{+}:y(x) c/c^{−}:z  c^{−}:y(x) c^{+}:x c/c^{−}:y

c^{−}:x c^{+}:z(y(x)) c^{−}:z(y(x)) c^{+}:y(x) c/c^{−}:z c^{−}:y(x) c^{+}:x c/c^{−}:y

c^{−}:x c^{+}:z(y(x)) c^{−}:z(y(x)) c^{+}:y(x) c/c^{−}:z  c^{−}:y(x) c^{+}:x c/c^{−}:y

(48) _{s^{+}  s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−}  n^{+} n\s^{−}(n\s)/n^{−} s^{−}  n^{+}  n^{−} s/n^{+}(s/n)\s^{−} s^{+}  s^{−}}

25As above (cf. footnote 10), we identify all proof nets which differ only with respect to the particular variables assigned.

s^{+}  s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−}  n^{+} n\s^{−}(n\s)/n^{−} s^{−}  n^{+} n^{−} s/n^{+}(s/n)\s^{−} s^{+}  s^{−}

s^{+}  s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−} n^{+} n\s^{−}(n\s)/n^{−} s^{−}  s^{−} n^{−} s/n^{+}(s/n)\s^{−} s^{+} n^{+}

s^{+} s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−}  n^{+} n\s^{−}(n\s)/n^{−} s^{−}  s^{−} n^{−} s/n^{+}(s/n)\s^{−} s^{+} n^{+}

(49) _{s^{+}  s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−}  n^{+} n\s^{−}(n\s)/n^{−} s^{−}  n^{+}  n^{−} s/n^{+}(s/n)\s^{−} s^{+}  s^{−}}

s^{+}  s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−}  n^{+} n\s^{−}(n\s)/n^{−} s^{−}  n^{+} n^{−} s/n^{+}(s/n)\s^{−} s^{+}  s^{−}

s^{+}  s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−} n^{+} n\s^{−}(n\s)/n^{−} s^{−}  s^{−} n^{−} s/n^{+}(s/n)\s^{−} s^{+} n^{+}

s^{+} s^{−}  s^{+} n\s^{+} s/(n\s)^{−}  n^{−}  n^{+} n\s^{−}(n\s)/n^{−} s^{−}  s^{−} n^{−} s/n^{+}(s/n)\s^{−} s^{+} n^{+}

If s/(n\s)^{−}, (n\s)/n^{−}, and (s/n)\s^{−} are assigned the variables u, v and w, then the term u(λu′.w(λw′.v(u′)(w′))) is assigned to the positively signed terminal category s in the proof nets listed in (48), and w(λw′.u(λu′.v(u′)(w′))) is assigned to the positively signed terminal category s in the proof nets listed in (49).

Roorda (1991, p. 27) claims that

a proof net can be considered as a parallellized sequent proof and as such it lacks the spurious ambiguity of (even Cut-free) sequent proofs. A proof net is a concrete structure, not merely an abstract equivalence class of derivations […].

However, we have just seen that the set of proof nets has to be partitioned into equivalence classes if it is to serve as a solution to the spurious ambiguity problem: for every reading of an L-derivable sequent c_{1}, …, c_{n} ⊢ c, there are n + 1 proof nets.

Of course, these n + 1 proof nets are equivalent in that they make up a set of cyclic permutations. But on the one hand, one cannot isolate one specific representant – e.g., the proof net with its positive terminal category in rightmost position – from this set, since one has to be strict on order and adjacency of premises in proof nets, so that all these permutations are required for the definition (cf. clause (b) and (c)). And on the other hand, it is not possible to consider this set of permutations as a monolithic object, since sometimes a specific representant (e.g., the proof net with its positive terminal category in rightmost position – cf. B in clause (d)) has to be isolated from this set.

So, ironically, it is the proof net approach which has to resort to ‘abstract’ equivalence classes, whereas sequent normalization (as well as partial deduction) associates one concrete object with each interpretation of a derivable sequent: its L* (PD) proof.

6 Encoding Atomic Categories

Ponse (1988) proved that LP derivability in an atomic goal category can be mimicked by LP derivability using one atomic category only. LP refers to the Lambek calculus with Permutation, which is also known as Lambek-Van Benthem calculus.^{26} In the present section we will show that (a generalization of) this result can be extended to L, the Lambek calculus proper: L derivability in any category can be mimicked by L derivability using one atomic category only. More formally:

Let the set at consist of the distinct atomic categories at_{1}, …, at_{k}, let at be an atomic category, and let cat_{at} and cat_{{at}} be the sets of categories based on at and {at}, respectively. Then there is a substitution σ replacing every at_{i} ∈ at by a c_{i} ∈ cat_{{at}} such that for all c_{1}, …, c_{n}, c in cat_{at}:

(50) c_{1}, …, c_{n} ⊢_{L} c if and only if σ(c_{1}, …, c_{n}) ⊢_{L} σ(c).

If σ is a substitution and α is a category or a sequence of categories, then the expression σ(α) denotes the result of performing σ to α. The atomic category at will be abbreviated as t in the sequel.

The proof of theorem (50) is organized as follows. First, the calculus L* will be used for establishing the facts (51) and (53), which express useful properties of L-derivable sequents that will be exploited throughout. Next, a Lemma will be proven which concerns the non-derivability of certain sequents that involve categories built up from the categories (t/t)/t, ((t/t)/(t/t))/(t/t) and atomic categories different from t. This Lemma is then shown to entail Claim 1, which states that the categories (t/t)/t and ((t/t)/(t/t))/(t/t) can be used to encode two atomic categories, viz., t and some other atomic category, also in the presence of yet other atomic categories. Finally, the substitution σ employed in Claim 1 is generalized in Claim 2: by means of a substitution σ_{⟨t,at_{1},...,at_{m}⟩}, any finite number of atomic categories t, at_{1}, …, at_{m} can be encoded in terms of t.^{27}

26See Van Benthem (1986; 1991).

27The above theorem follows from Claim 2, since the following substitutions will meet the requirement specified in (50):

• σ_{⟨t,at_{1},...,at_{k}⟩} if t ∉ at (note that any category based on at is based on at ∪ {t});

• σ_{⟨t,at_{1},...,at_{i−1},at_{i+1},...,at_{k}⟩} if t ∈ at and at = {at_{1}, …, at_{i−1}, t, at_{i+1}, …, at_{k}}.

We start by putting each category c in cat_{at} into an equivalence class ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋. Let c and c_{1}, …, c_{p+q} be members of cat_{at} (where p + q ≥ 0), and let at ∈ at. Then:

c ∈ ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋ iff

(a) c = at and p + q = 0;

(b) c = c_{p}\c′ and c′ ∈ ⌊c_{p−1}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋; or

(c) c = c′/c_{p+q} and c′ ∈ ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q−1}⌋.

The sets ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋ partition cat_{at}.^{28} Note that the following claims hold:

If c ∈ ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋, then
T ⊢_{L} c iff c_{1}, …, c_{p}, T, c_{p+q}, …, c_{p+1} ⊢_{L} at.

(51)

U, c*, V ⊢_{L*} at and c ∈ ⌊c_{p}\...\c_{1}\at′/c_{p+1}/.../c_{p+q}⌋ iff
at′ = at; U = T_{1}, …, T_{p}; V = T_{p+q}, …, T_{p+1};
and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L*} c_{i}*.

(52)

Both (51) and (52) are proven by induction on p + q.

As for (51):

• If p + q = 0, then the claim is trivial.

• If p + q > 0, then (i) c = c_{p}\c′ and c′ ∈ ⌊c_{p−1}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋; or (ii) c = c′/c_{p+q} and c′ ∈ ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q−1}⌋. We only treat (i), since (ii) is analogous. Note that the following claims are equivalent: (1) T ⊢_{L} c_{p}\c′; (2) T ⊢_{L*} c_{p}\c′*; (3) c_{p}, T ⊢_{L*} c′*; (4) c_{p}, T ⊢_{L} c′;

(5) c_{1}, …, c_{p}, T, c_{p+q}, …, c_{p+1} ⊢_{L} at. Theorem 1.1 (see section 3 above) yields the equivalence of (1) and (2) as well as (3) and (4); the equivalence of (2) and (3) is due to L*; and (4) and (5) are equivalent on account of the induction hypothesis. □

As for (52):

28Different categories c and c′ are members of the same set ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋ iff c and c′ have the same final atomic value (viz., at) and the same series of left-hand side (c_{p}, …, c_{1}) and right-hand side (c_{p+1}, …, c_{p+q}) arguments, but combine with these arguments in a different order. The set ⌊t\t/(t/t)/t⌋, for example, consists of three categories:

(a) ((t\t)/(t/t))/t, (b) (t\(t/(t/t)))/t and (c) t\((t/(t/t))/t).

• p + q = 0. Then U, c*, V ⊢_{L*} at must be an axiom at* ⊢_{L*} at; so at′ = at and U and V are empty.

• p + q > 0. Then (i) c = c_{p}\c′ and c′ ∈ ⌊c_{p−1}\...\c_{1}\at′/c_{p+1}/.../c_{p+q}⌋; or (ii) c = c′/c_{p+q} and c′ ∈ ⌊c_{p}\...\c_{1}\at′/c_{p+1}/.../c_{p+q−1}⌋. We only treat (ii), since (i) is analogous. The sequent U, c′/c_{p+q}*, V ⊢ at must be derived by /L in L*. Hence U, c′/c_{p+q}*, V ⊢_{L*} at iff U, c′*, V′ ⊢_{L*} at and T_{p+q} ⊢_{L*} c_{p+q}*, where V = T_{p+q}, V′. By induction hypothesis: U, c′*, V′ ⊢_{L*} at iff at′ = at; U = T_{1}, … T_{p}; V′ = T_{p+q−1}, … T_{p+1}; and for all i such that 1 ≤ i ≤ p+q−1: T_{i} ⊢_{L*} c_{i}*. □

Given (52), suppose that T ⊢_{L} at. This holds iff T ⊢_{L*} at* by Theorem 1.1 (see Section 3 above). The sequent T ⊢ at* must have been derived by the * rule in L*. Therefore, T = U, c, V and U, c*, V ⊢_{L*} at. Now, for some c_{1}, …, c_{p+q}, at′: c ∈ ⌊c_{p}\...\c_{1}\at′/c_{p+1}/.../c_{p+q}⌋. By (52), we have that at′ = at; U = T_{1}, …, T_{p}; V = T_{p+q}, …, T_{p+1}; and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L*} c_{i}*, which is equivalent to T_{i} ⊢_{L} c_{i} by Theorem 1.1. Summing up:

T ⊢_{L} at iff there is a c ∈ ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋ such that T =

T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1} and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}.

(53)

Let A be a set of categories. In the sequel we will say that c is an Acategory iff c is built up from categories in A.^{29} We will abbreviate sequences t/t, …, t/t consisting of n occurrences of the category t/t as (t/t)^{n}.

Lemma: let A be the set {at_{1}, …, at_{k}, (t/t)/t, ((t/t)/(t/t))/(t/t)}, where at_{1},…,at_{k} and t are distinct atomic categories; and let T be a non-empty sequence of A-categories. Then:

(a) T, t ⊬_{L} t;
(b) for all n ∈ IN: T, (t/t)^{n} ⊬_{L} t; and
(c) T, t/t, t ⊬_{L} t.

Proof of (a) and (b): by induction on m, the number of occurrences of at_{1}, …, at_{k}, (t/t)/t and ((t/t)/(t/t))/(t/t) in T.

• m = 1. Then T = at_{i} (1 ≤ i ≤ k); T = (t/t)/t; or T = ((t/t)/(t/t))/(t/t):

29That is, the set of A-categories is the smallest set A′ such that (i) A ⊆ A′; and (ii) if c ∈ A′ and c′ ∈ A′, then c/c′ ∈ A′ and c′\c ∈ A′.

(a) at_{i}, t ⊬_{L} t; (t/t)/t, t ⊬_{L} t; and ((t/t)/(t/t))/(t/t), t ⊬_{L} t.

(b) That T, (t/t)^{n} ⊬_{L} t can be shown by at-count, a notion introduced in Van Benthem (1986). Let at ∈ at. Then at-count[c] is defined as follows: for c ∈ at, at-count[c] = 1 if c = at, while at-count[c] = 0 if c ≠ at; at-count[a/b] = at-count[b\a] = at-count[a] − at-count[b]. Moreover, at-count[c_{1}, …, c_{n}] = at-count[c_{1}]+…+at-count[c_{n}]. A useful property of L-derivable sequents T ⊢ c is that for all at ∈ at: at-count[T] = at-count[c]. (The proof proceeds by an easy induction on the length of the derivation of T ⊢ c.)

Note that t-count[(t/t)/t] = −1; that t-count[((t/t)/(t/t))/(t/t)] = 0; and that for all i ∈ {1, …, k} and n ∈ IN: t-count[at_{i}] = t-count[(t/t)^{n}] = 0. Hence t-count[(t/t)/t, (t/t)^{n}] = −1 and t-count[((t/t)/(t/t))/(t/t), (t/t)^{n}] = t-count[at_{i}, (t/t)^{n}] = 0. On the other hand, t-count[t] = 1. So, for all n ∈ IN: at_{i}, (t/t)^{n} ⊬_{L} t; (t/t)/t, (t/t)^{n} ⊬_{L} t; and ((t/t)/(t/t))/(t/t), (t/t)^{n} ⊬_{L} t.

• m > 1. Note^{30} that if c is an A-category and c∈⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋, then (i) c_{p+1} = c_{p+2} = t, so c ∈ ⌊c_{p}\...\c_{1}\t/t/t/c_{p+3}/.../c_{p+q}⌋; or (ii) c_{p+1} = t and c_{p+2} = c_{p+3} = t/t, so c ∈ ⌊c_{p}\...\c_{1}\t/t/(t/t)/(t/t)/c_{p+4}/.../c_{p+q}⌋.

(a) Suppose T, t ⊢_{L} t. By (53), there is a c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋ such that T, t = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1} and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}. Since T is non-empty, this c cannot be the rightmost category t in T, t. Hence c is an A-category in T and either (i) c ∈ ⌊c_{p}\...\c_{1}\t/t/t/c_{p+3}/.../c_{p+q}⌋; or (ii) c ∈ ⌊c_{p}\...\c_{1}\t/t/(t/t)/(t/t)/c_{p+4}/.../c_{p+q}⌋. Focus on T_{p+2}. On the one hand: if (i), then c_{p+2} = t, so T_{p+2} ⊢_{L} t; and if (ii), then c_{p+2} = t/t, so T_{p+2} ⊢_{L} t/t. On the other hand: T_{p+2} is non-empty, since T_{p+2} ⊢_{L} c_{p+2}; T_{p+2} is a sequence of A-categories, since t in T, t is part of T_{p+1} (which must be non-empty since T_{p+1} ⊢_{L} c_{p+1}); and T_{p+2} contains less occurrences of at_{1}, …, at_{k}, ((t/t)/(t/t))/(t/t) and (t/t)/t than T, since c occurs in T but not in T_{p+2}. Therefore, the induction hypothesis for (b) (n = 0) yields that T_{p+2} ⊬_{L} t, while the induction hypothesis for (a) yields that T_{p+2}, t ⊬_{L} t. Because t/t ∈ ⌊t/t⌋, the latter entails – by (51) – that T_{p+2} ⊬_{L} t/t. So, both (i) and (ii) lead to contradiction, which means that T, t ⊬_{L} t.

(b) Suppose T, (t/t)^{n} ⊢_{L} t. By (53), there is a c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋ such that T, (t/t)^{n} = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1} and for all i, 1 ≤ i ≤ p + q:

30This is easily seen by induction on the number of occurrences of at_{1}, …, at_{k}, (t/t)/t and ((t/t)/(t/t))/(t/t) in c.

T_{i} ⊢_{L} c_{i}. Since T is non-empty, this c cannot be a category in (t/t)^{n}. Hence c is an A-category in T and either (i) c ∈ ⌊c_{p}\...\c_{1}\t/t/t/c_{p+3}/.../c_{p+q}⌋; or (ii) c ∈ ⌊c_{p}\...\c_{1}\t/t/(t/t)/(t/t)/c_{p+4}/.../c_{p+q}⌋. Focus on T_{p+1}. On the one hand: both (i) and (ii) entail that c_{p+1} = t, so T_{p+1} ⊢_{L} t. On the other hand: T_{p+1} cannot be of the form (t/t)^{m} for m ≤ n, since (t/t)^{m} and t have different t-counts; hence T_{p+1} consists of a non-empty subsequence T′ of T followed by (t/t)^{n}, where T′ contains less occurrences of at_{1}, …, at_{k}, ((t/t)/(t/t))/(t/t) and (t/t)/t than T, since c occurs in T but not in T_{p+1}. Therefore, the induction hypothesis of (b) yields that T′, (t/t)^{n} ⊬_{L} t in both cases. Since T′, (t/t)^{n} = T_{p+1}, we have a contradiction. Consequently, T, (t/t)^{n} ⊬_{L} t.

Proof of (c): Suppose T, t/t, t ⊢_{L} t. By (53), there is a c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋ such that T, t/t, t = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1} and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}. Since T is non-empty, this c cannot be t/t or t in T, t/t, t. Hence c is an A-category in T and either (i) c ∈ ⌊c_{p}\...\c_{1}\t/t/t/c_{p+3}/.../c_{p+q}⌋; or (ii) c ∈ ⌊c_{p}\...\c_{1}\t/t/(t/t)/(t/t)/c_{p+4}/.../c_{p+q}⌋.

Suppose (i). Then on the one hand: c_{p+2} = t, so T_{p+2} ⊢_{L} t. But on the other hand: T_{p+1} ⊢_{L} t entails that T_{p+1} is non-empty and includes at least t. Hence t/t must be part of (a) T_{p+1} or (b) T_{p+2}. Suppose (a). Then T_{p+2} is a sequence of A-categories which is, moreover, non-empty since T_{p+2} ⊢_{L} c_{p+2}, so that T_{p+2} ⊢_{L} t contradicts Lemma (b) (n = 0). Suppose (b). Then T_{p+2} consists of a sequence T′ of A-categories followed by t/t and T′ must be non-empty since t/t ⊬_{L} t, so that T_{p+2} ⊢_{L} t contradicts Lemma (b) (n = 1).

Suppose (ii). Then on the one hand: c_{p+3} = t/t, so T_{p+3} ⊢_{L} t/t and T_{p+3}, t ⊢_{L} t by (51). But on the other hand: T_{p+1} ⊢_{L} t entails that T_{p+1} is non-empty and includes at least t. Hence t/t must be part of T_{p+1} or T_{p+2}. Anyway, T_{p+3} is a sequence of A-categories which is, moreover, non-empty since T_{p+3} ⊢_{L} c_{p+3}, so that T_{p+3}, t ⊢_{L} t contradicts Lemma (a).

All cases lead to contradiction, so T, t/t, t ⊬_{L} t. □

Corollary:

(1) There is no sequence S of A-categories such that S, t, t = T′′′, T′′, T′, where T′′′ ⊢_{L} t/t, T′′ ⊢_{L} t/t and T′ ⊢_{L} t.

Suppose the contrary. Then T′′′, T′′ and T′ are non-empty, so the second t in S, t, t is part of T′, and the first t is part of T′′ or T′. Either way T′′′ is a non-empty sequence of A-categories. But T′′′ ⊢_{L} t/t entails T′′′, t ⊢_{L} t by (51), and the latter contradicts Lemma (a).

(2) There is no sequence S of A-categories such that S, t/t, t/t, t = T′′, T′, where T′′ ⊢_{L} t and T′ ⊢_{L} t.

Suppose the contrary. Then T′′ and T′ are non-empty, so the category t in S, t/t, t/t, t is part of T′, so that T′′ = S′, (t/t)^{m}, where m ∈ {0, 1, 2} and S′ is (a subsequence of) S. But then T′′ ⊬_{L} t, since (t/t)^{m} ⊬_{L} t by t-count, and for non-empty S′: S′, (t/t)^{m} ⊬_{L} t by Lemma (b).

(3) There is no non-empty sequence S of A-categories such that S, t, t = T′′, T′, where T′′ ⊢_{L} t and T′ ⊢_{L} t.

Suppose the contrary. Then T′′ and T′ are non-empty, so the second t in S, t, t is part of T′, and (i) T′′ = S, t; or (ii) T′′ = S′ and non-empty S′ is (a subsequence of) S. Now, (ii) contradicts Lemma (b) (n = 0), and (i) contradicts Lemma (a) for non-empty S. Hence S is empty (and T′′ = T′ = t).

(4) There is no non-empty sequence S of A-categories such that S, t/t, t/t, t = T′′′, T′′, T′, where T′′′ ⊢_{L} t/t, T′′ ⊢_{L} t/t and T′ ⊢_{L} t.

Suppose the contrary. Then T′′′, T′′ and T′ are non-empty, and T′′′ is not a subsequence of S, since T′′′ ⊢_{L} t/t entails that T′′′, t ⊢_{L} t by (51), contradicting Lemma (a). So T′′′ includes the first t/t in S, t/t, t/t, t – but not the second one, for then T′′ or T′ would have to be empty. Hence T′′′ = S, t/t (so that T′′ = t/t and T′ = t) and S is empty, since S, t/t ⊢_{L} t/t entails S, t/t, t ⊢_{L} t by (53), and the latter is impossible for non-empty S on account of Lemma (c).

Let t and at_{0} be two distict atomic categories. The following claim shows that the compound categories (t/t)/t and ((t/t)/(t/t))/(t/t) can be used for encoding t and at_{0}, respectively.

Claim 1: Let the set at = {t, at_{0}, at_{1}, …, at_{k}} consist of distinct atomic categories; and let σ be the substitution [t:=(t/t)/t; at_{0} :=((t/t)/(t/t))/(t/t)]. Then for all T, c in cat_{at}: T ⊢_{L} c iff σ(T) ⊢_{L} σ(c).

Proof: by induction on d(T ⊢ c), the degree of T ⊢ c.

• d(T ⊢ c) = 0. Then the categories T, c are members of the set at = {t, at_{0}, at_{1}, …, at_{k}}, while the categories σ(T), σ(c) are members of the set at′ = {(t/t)/t, ((t/t)/(t/t))/(t/t), at_{1}, …, at_{k}}, and the claim holds in view of the fact that both for T, c ∈ at and for T, c ∈ at′ we have that T ⊢_{L} c entails that T = c. This is straightforward for T, c ∈ at (by at_{i}-count for at_{i} ∈ at). For T, c ∈ at′:

∘ If T ⊢_{L} at_{j} and 1 ≤ j ≤ k, then for c′ ∈ ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋: T = T_{1}, …, T_{p}, c′, T_{p+q}, …, T_{p+1} (and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}) by (53). The only member of at′ in ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋ is at_{j}, and at_{j} ∈ ⌊at_{j}⌋. Therefore, p + q = 0 and T = at_{j}.

∘ If T ⊢_{L} (t/t)/t, then T, t, t ⊢_{L} t by (51), since (t/t)/t ∈ ⌊t/t/t⌋. By (53), for c′ ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋: T, t, t = T_{1}, …, T_{p}, c′, T_{p+q}, …, T_{p+1} and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}. For c′ ∈ at′, this entails (i) c′ = (t/t)/t and c′ ∈ ⌊t/t/t⌋; or (ii) c′ = ((t/t)/(t/t))/(t/t) and c′ ∈ ⌊t/t/(t/t)/(t/t)⌋. If (ii), then T, t, t = ((t/t)/(t/t))/(t/t), S, t, t and S, t, t = T′′′, T′′, T′, where T′′′ ⊢_{L} t/t, T′′ ⊢_{L} t/t and T′ ⊢_{L} t – which is impossible by Corollary (1). So, assume (i). Then T, t, t = (t/t)/t, S, t, t and S, t, t = T′′, T′, where T′′ ⊢_{L} t and T′ ⊢_{L} t – which, by Corollary (3), entails that S is empty and, consequently, that T = (t/t)/t.

∘ If T ⊢_{L} ((t/t)/(t/t))/(t/t), then T, t/t, t/t, t ⊢_{L} t by (51), due to the fact that c ∈ ⌊t/t/(t/t)/(t/t)⌋. By (53), for c′ ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋: T, t/t, t/t, t = T_{1}, …, T_{p}, c′, T_{p+q}, …, T_{p+1} and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}, so that again (i) c′ = (t/t)/t; or (ii) c′ = ((t/t)/(t/t))/(t/t). If (i), then T, t/t, t/t, t = (t/t)/t, S, t/t, t/t, t and S, t/t, t/t, t = T′′, T′, where T′′ ⊢_{L} t and T′ ⊢_{L} t – which is impossible by Corollary (2). So, assume (ii). Then T, t/t, t/t, t = ((t/t)/(t/t))/(t/t), S, t/t, t/t, t and S, t/t, t/t, t = T′′′, T′′, T′, where T′′′ ⊢_{L} t/t, T′′ ⊢_{L} t/t and T′ ⊢_{L} t – which, by Corollary (4), entails that S is empty and, consequently, that T = ((t/t)/(t/t))/(t/t).

• d(T ⊢ c) > 0. If c ∈ cat_{at} and c ∈ ⌊c_{p}\...\c_{1}\at/c_{p+1}/.../c_{p+q}⌋, then:

(a) at ∈{at_{1}, …, at_{k}} and σ(c)∈⌊σ(c_{p})\...\σ(c_{1})\at/σ(c_{p+1})/.../σ(c_{p+q})⌋;

(b) at = t and σ(c)∈⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q})⌋; or

(c) at = at_{0} and σ(c)∈⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q})⌋. Since p + q > 0 or p + q = 0, six cases can be distinguished:

∘ c ∈ ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋, 1 ≤ j ≤ k, and p + q > 0: T ⊢_{L} c iff_{1} c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1} ⊢_{L} at_{j}

iff_{2} σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}) ⊢_{L} σ(at_{j}) =

σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}) ⊢_{L} at_{j} =

σ(c_{1}), …, σ(c_{p}), σ(T), σ(c_{p+q}) …, σ(c_{p+1}) ⊢_{L} at_{j}
iff_{3} σ(T) ⊢_{L} σ(c).

‘iff_{1}’ and ‘iff_{3}’ hold by (51) (since c ∈ ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋, while σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\at_{j}/σ(c_{p+1})/.../σ(c_{p+q)}⌋ due to (a); and ‘iff_{2}’ holds by induction hypothesis (d(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1} ⊢ at_{j}) < d(T ⊢ c), because p + q > 0).

∘ c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋ and p + q > 0: T ⊢_{L} c iff_{1} c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1} ⊢_{L} t

iff_{2} σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}) ⊢_{L} σ(t) =

σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}) ⊢_{L} (t/t)/t
iff_{3} σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}), t, t ⊢_{L} t =
σ(c_{1}), …, σ(c_{p}), σ(T), σ(c_{p+q}) …, σ(c_{p+1}), t, t ⊢_{L} t
iff_{4} σ(T) ⊢_{L} σ(c).

‘iff_{1}’, iff_{3}’ and iff_{4}’ hold by (51) (c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋, (t/t)/t ∈ ⌊t/t/t⌋, and σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q)}⌋ due to (b)); and ‘iff_{2}’ holds by induction hypothesis (since p + q > 0).

∘ c ∈ ⌊c_{p}\...\c_{1}\at_{0}/c_{p+1}/.../c_{p+q}⌋ and p + q > 0: T ⊢_{L} c iff_{1} c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1} ⊢_{L} at_{0}

iff_{2} σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}) ⊢_{L} σ(at_{0}) =

σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}) ⊢_{L} ((t/t)/(t/t))/(t/t)
iff_{3} σ(c_{1}, …, c_{p}, T, c_{p+q} …, c_{p+1}), t/t, t/t, t ⊢_{L} t =
σ(c_{1}), …, σ(c_{p}), σ(T), σ(c_{p+q}) …, σ(c_{p+1}), t/t, t/t, t ⊢_{L} t
iff_{4} σ(T) ⊢_{L} σ(c).

‘iff_{1}’, iff_{3}’ and iff_{4}’ hold by (51) (since c ∈ ⌊c_{p}\...\c_{1}\at_{0}/c_{p+1}/.../c_{p+q}⌋, ((t/t)/(t/t))/(t/t) ∈ ⌊t/t/(t/t)/(t/t)⌋ and – on account of (c) – σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q)}⌋); and ‘iff_{2}’ holds by induction hypothesis (since p + q > 0).

∘ c ∈ ⌊at_{j}⌋ and 1 ≤ j ≤ k: T ⊢_{L} at_{j} iff_{1} for c ∈ ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋:

T = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1}

and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}
iff_{2} for c ∈ ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋:
T = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1}
and for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i})
iff_{3} for σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\at_{j}/σ(c_{p+1})/.../σ(c_{p+q})⌋:
σ(T) = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1})

and for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i})
iff_{4} σ(T) ⊢_{L} at_{j}.

Note that at_{j} = σ(at_{j}), and that ‘iff_{1}’ holds by (53); ‘iff_{2}’ holds by induction hypothesis (d(T ⊢_{L} at_{j}) > 0 entails that p + q > 0, hence d(T_{i} ⊢_{L} c_{i}) < d(T ⊢_{L} at_{j}) for all i); ‘iff_{3}’ holds by (a); and ‘iff_{4}’ holds by (53).

∘ c ∈ ⌊t⌋: T ⊢_{L} t iff_{1} for c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋:

T = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1}

and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}
iff_{2} for c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋:
T = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1}
and for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i})
iff_{3} for σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q})⌋:
σ(T) = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1})
and for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i})
iff_{4} σ(T), t, t ⊢_{L} t
iff_{5} σ(T) ⊢_{L} (t/t)/t.

Note that (t/t)/t = σ(t), and that ‘iff_{1}’ holds by (53); ‘iff_{2}’ holds by induction hypothesis; ‘iff_{3}’ holds by (b); ‘iff_{5}’ holds by (51) (since (t/t)/t ∈ ⌊t/t/t⌋); and the ‘only if’ part of ‘iff_{4}’ is an application of (53) (since t ⊢_{L} t). As for the ‘if’ part of ‘iff_{4}’: if the final value of σ(c) is t, then either

σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q})⌋ or
σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q})⌋.

Hence if σ(T), t, t ⊢_{L} t, then, by (53), either

(i) for some σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q})⌋:

– σ(T), t, t = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1}), T′′′, T′′, T′,

– for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i}), and

– T′′′ ⊢_{L} t/t, T′′ ⊢_{L} t/t, and T′ ⊢_{L} t; or (ii) for some σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q})⌋:

– σ(T), t, t = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1}), T′′, T′,

– for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i}), and

– T′′ ⊢_{L} t and T′ ⊢_{L} t. However, (i) is impossible by Corollary (1), and Corollary (3) entails that (ii) is only possible if T′′ = T′ = t.

∘ c ∈ ⌊at_{0}⌋: T ⊢_{L} at_{0} iff_{1} for c ∈ ⌊c_{p}\...\c_{1}\t/c_{p+1}/.../c_{p+q}⌋:

T = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1}

and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L} c_{i}
iff_{2} for c ∈ ⌊c_{p}\...\c_{1}\at_{0}/c_{p+1}/.../c_{p+q}⌋:
T = T_{1}, …, T_{p}, c, T_{p+q}, …, T_{p+1}
and for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i})

iff_{3} for σ(c)∈⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q})⌋:

σ(T) = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1})
and for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i})
iff_{4} σ(T), t/t, t/t, t ⊢_{L} t
iff_{5} σ(T) ⊢_{L} ((t/t)/(t/t))/(t/t).

Note that ((t/t)/(t/t))/(t/t) = σ(at_{0}), and that ‘iff_{1}’ holds by (53); ‘iff_{2}’ holds by induction hypothesis; ‘iff_{3}’ holds by (c); ‘iff_{5}’ holds by (51) (since ((t/t)/(t/t))/(t/t) ∈ ⌊t/t/(t/t)/(t/t)⌋); and the ‘only if’ part of ‘iff_{4}’ is an application of (53) (since t/t ⊢_{L} t/t and t ⊢_{L} t). As for the ‘if’ part of ‘iff_{4}’: again, if the final value of σ(c) is t, then either

σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q})⌋ or
σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q})⌋.

Hence if σ(T), t/t, t/t, t ⊢_{L} t, then, by (53), either

(i) for some σ(c) ∈ ⌊σ(c_{p})\...\σ(c_{1})\t/t/t/σ(c_{p+1})/.../σ(c_{p+q})⌋:

– σ(T), t/t, t/t, t = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1}), T′′, T′,

– for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i}), and

– T′′ ⊢_{L} t and T′ ⊢_{L} t; or (ii) for some σ(c)∈⌊σ(c_{p})\...\σ(c_{1})\t/t/(t/t)/(t/t)/σ(c_{p+1})/.../σ(c_{p+q})⌋:

– σ(T), t/t, t/t, t = σ(T_{1}), …, σ(T_{p}), σ(c), σ(T_{p+q}), …, σ(T_{p+1}), T′′′, T′′, T′,

– for all i, 1 ≤ i ≤ p + q: σ(T_{i}) ⊢_{L} σ(c_{i}), and

– T′′′ ⊢_{L} t/t, T′′ ⊢_{L} t/t, and T′ ⊢_{L} t. This time, (i) is impossible by Corollary (2), and Corollary (4) entails that (ii) is only possible if T′′′ = T′′ = t/t and T′ = t. □

Finally, the following claim shows that one can generalize the substitution used in Claim 1 to encode any finite number of atomic categories. Let, for c ∈ cat and n ∈ IN:

β(c) = ((c/c)/(c/c))/(c/c);
α(c) = (c/c)/c;

α^{0}(c) = c; and
α^{n+1}(c) = α^{n}(α(c)).

Claim 2: Let A = ⟨t, at_{1}, …, at_{m}⟩ be a sequence of distinct atomic categories such that m ≥ 1, and let σ_{A} be the substitution

[t:=α^{m}(t); at_{1} :=β(α^{m−1}(t)); …; at_{m}:=β(α^{m−m}(t))].

Then for all T, c in cat_{{t,at_{1},...,at_{m}}}: T ⊢_{L} c iff σ_{A}(T) ⊢_{L} σ_{A}(C).

Proof: by induction on m.

• m = 1. Then Claim 2 comes down to Claim 1 (with at_{0} and k instantiated as at_{1} and 0, respectively).

• m > 1. Observe (i) that σ_{A}(c) = σ′_{A}(σ′′_{A}(c)) for the substitutions σ′_{A} = [t := α^{m−1}(t); at_{1} := β(α^{(m−1)−1}(t)); …; at_{m−1} := β(α^{(m−1)−(m−1)}(t))] and σ′′_{A} = [t:=α(t); at_{m}:=β(t)]; and (ii) that σ′_{A}(c) = σ_{A′}(c) for the sequence A′ = ⟨t, at_{1}, …, at_{m−1}⟩. Consequently, we have the following equivalences: σ_{A}(T) ⊢_{L} σ_{A}(c) iff_{1} σ′_{A}(σ′′_{A}(T)) ⊢_{L} σ′_{A}(σ′′_{A}(c))

iff_{2} σ′′_{A}(T) ⊢_{L} σ′′_{A}(c)

iff_{3} T ⊢_{L} c.

‘iff_{1}’ holds by observation (i); ‘iff_{2}’ holds by induction hypothesis and observation (ii) (note that m − 1 < m, and that σ′′_{A}(c) ∈ cat_{{t,at_{1},...,at_{m−1}}} if c ∈ cat_{{t,at_{1},...,at_{m}}}); and ‘iff_{3}’ is another application of Claim 1 (with at_{0} and k instantiated as at_{m} and m − 1, respectively). □

References

Benthem, J. van (1986). Essays in Logical Semantics. Reidel, Dordrecht. Benthem, J. van (1991). Language in Action. Categories, Lambdas and Logic. North Holland, Amsterdam. Bouma, G. (1989). ‘Structural Completeness’. Manuscript Research Institute for Knowledge Systems, Maastricht. Buszkowski, W., W. Marciszewski and J. van Benthem (eds.) (1988). Categorial Grammar. John Benjamins, Amsterdam. Girard, J.-Y. (1987). ‘Linear Logic’. Theoretical Computer Science 50, 1–102. Hepple, M. (1990). The Grammar and Processing of Order and Dependency: a Categorial Approach. Dissertation University of Edinburgh. Klein, E. and J. van Benthem (eds.) (1988). Categories, Polymorphism and Unification, Centre for Cognitive Science, University of Edinburgh, and Institute for Language, Logic and Information, University of Amsterdam. König, E. (1989). ‘Parsing as Natural Deduction’. In Proceedings of the 27th Annual Meeting of the Association for Computational Linguistics. Vancouver. Lambek, J. (1958). ‘The Mathematics of Sentence Structure’. American Mathematical Monthly 65, 154–169. Reprinted in Buszkowski, Marciszewski and Van Benthem (eds.). Moortgat, M. (1988). Categorial Investigations. Logical and Linguistic Aspects of the Lambek Calculus. Foris, Dordrecht. Moortgat, M. (1990). ‘Unambiguous Proof Representations for the Lambek Calculus’. In: Stokhof and Torenvliet (eds.). Ponse, A. (1988). ‘Encoding Types in the Lambek Calculus’. In Klein and Van Benthem (eds.). Roorda, D (1991). Resource Logics: Proof-theoretical Investigations. Dissertation University of Amsterdam. Stokhof, M., and L. Torenvliet (eds.) (1990). Proceedings of the Seventh Amsterdam Colloquium. Institute for Language, Logic and Information, University of Amsterdam.