Encoding Atomic Categories: Rendering It Strictly Directed

Herman Hendriks

Abstract

This paper solves the directed counterpart of a problem addressed in Language in Action (Van Benthem 1991: 108–9). There it is observed that LP derivability in an atomic goal category can be mimicked by LP derivability using one atomic category only. The abbreviation LP refers to the non-directed Lambek calculus with Permutation, a system which has also become known as the Lambek-Van Benthem calculus, and the result is due to Ponse (1988). In the present paper we will show that—a generalization of—this result can be extended to the directed system L, i.e., the associative calculus that was introduced in Lambek (1958): L derivability in any category can be mimicked by L derivability using one atomic category only.

You don’t want your paper rejected? Then render it strictly directed:

Each referee crashes On seeing your slashes,

And errors just won’t be detected!

Herman Hendriks

This paper solves the directed counterpart of a problem addressed in Language in Action (Van Benthem 1991: 108–9). There it is observed that LP derivability in an atomic goal category can be mimicked by LP derivability using one atomic category only. The abbreviation LP refers to the non-directed Lambek calculus with Permutation, a system which has also become known as the Lambek-Van Benthem calculus, and the result is due to Ponse (1988). In the present paper we will show that—a generalization of—this result can be extended to the directed system L, i.e., the associative calculus that was introduced in Lambek (1958): L derivability in any category can be mimicked by L derivability using one atomic category only. More formally (definitions of the relevant notions are given in (2) through (5) below):

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}:

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

If σ is a substitution and α is a category or a sequence of categories, then σ(α) denotes the result of performing σ to α. The category at is written as t below.

The proof of Theorem (1) is organized as follows. First, we will present L and introduce an equivalent (see Claim 1) normalized calculus L* that will be used for establishing the facts (9) and (11), which express useful properties of L-derivable sequents that will be exploited later. 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 2, 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 2 is generalized in Claim 3: 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. We note here that Theorem (1) actually follows from Claim 3, since the following substitutions will meet the requirement specified in (1):

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

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

When Lambek (1958) introduced his syntactic calculus, he showed that it is equivalent to a sequent axiomatization L, the Lambek-Gentzen sequent calculus. 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 notions of category and sequent are defined as follows:

Let at be a finite set of atomic categories. Then cat_{at}, the set of categories based on at, is the smallest set such that (i) at ⊆ cat_{at}, and (ii) if a, b ∈ cat_{at}, then (a/b) ∈ cat_{at} and (b\a) ∈ cat_{at}.

(2)

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

(3)

We assume that no atomic category is of the form (a/b) or (b\a) and omit outermost brackets of categories. The categories c_{1}, …, c_{n} constitute the lefthand side of c_{1}, …, c_{n} ⊢ c, and category c is the right-hand side or goal of the sequent. If the identity of at is not an issue, we will write cat instead of cat_{at}.

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

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

\begin{matrix}\begin{matrix}T ⊢ b & U, a, V ⊢ c \\ U, a/b, T, V ⊢ c \end{matrix} [/L] & {T, b ⊢ a \atop T ⊢ a/b} [/R] & \begin{matrix}T ⊢ a & U, a, V ⊢ c \\ U, T, V ⊢ c \end{matrix} [Cut] \\ \begin{matrix}T ⊢ b & U, a, V ⊢ c \\ U, T, b\a, V ⊢ c \end{matrix} [\L] & {b, T ⊢ a \atop T ⊢ b\a} [\R] \end{matrix} (5)

The calculus L contains, among other rules, the so-called Cut rule. Lambek (1958) established that the set of theorems of L is not increased by adding Cut. The proof of this fact is constructive: Lambek specifies an algorithm which enables one to transform every proof which makes use of Cut into a Cut-free proof. In any application of Cut, of which at least one premise has been proven without Cut, either the conclusion coincides with one of the premises so that the application of Cut can be eliminated immediately, or the application of Cut can be replaced by one or two applications of Cut of smaller degree. The latter notion 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 α = \begin{matrix}T ⊢ a & U, a, V ⊢ c \\ U, T, V ⊢ c \end{matrix}
equals d(T) + d(U) + d(V) + d(a) + d(c).

(6)

Thus, the degree of a category, a sequence of categories and a sequent is equal to the number of slashes and backslashes it contains. Since the minimal degree of a Cut inference is zero, the Cut elimination algorithm is doomed to terminate.

Lambek’s proof entails 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.^{1} 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’ in König (1989): the problem that different proofs of a given sequent may yield one and the same semantic interpretation. Hepple (1990) and Hendriks (1993) show how this problem can be solved by further restricting the Cut-free calculus. The resulting system, which is called L* in Hendriks (1993), is a solution to the spurious ambiguity problem in that it provides exactly one proof per interpretation. We will not go into semantic interpretation here, but note that the calculus L* is based on the following syntactic observations: (a) each non-atomic axiom instance a/b ⊢ a/b or b\a ⊢ b\a can be decomposed into a proof with two less complex axiom premises, a ⊢ a and b ⊢ b; (b) 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; and (c) whenever a \L or /L inference yields the right-hand side premise of another \L or /L inference, and the inferences have different active categories, we can reverse the order of the inferences and shift the latter inference to the left-hand side premise or to the right-hand side premise of the former one. Observation (a) entails that for every proof of a sequent, there is an alternative proof of that sequent in which (i) all axiom instances are atomic. Given such an alternative proof, moreover, we can use observations (b) and (c) for obtaining a proof of the sequent in which (ii) no right-hand side premise of a \L or /L inference is the conclusion of a \R or /R inference (this corresponds to (b));^{2} and (iii) the same left-hand side category remains active whenever one goes down from axioms via right-hand side premises of \L and /L inferences (this corresponds to (c)). These considerations can be summarized in the form of the calculus L* given in (7) below, which observes the same conventions as (5) above, with the addition that at represents an arbitrary atomic category while * denotes an operator which controls the activity of categories in derivations:

1Note that 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.

2Consequently, every right-hand side 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 right-hand side premise and conclusion, every \L and /L inference must derive a conclusion sequent with an atomic goal category: T ⊢ at.

{U, a*, V ⊢ at \atop U, a, V ⊢ at*} [ * ]  at* ⊢ at [Ax]
\begin{matrix}T ⊢ b* & U, a*, V ⊢ at \\ U, a/b*, T, V ⊢ at \end{matrix} [/L] {T, b ⊢ a* \atop T ⊢ a/b*} [/R]
\begin{matrix}T ⊢ b* & U, a*, V ⊢ at \\ U, T, b\a*, V ⊢ at \end{matrix} [\L] {b, T ⊢ a* \atop T ⊢ b\a*} [\R]

(7)

An important property of L* is expressed by the following:

Claim 1:

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

Proof: We have seen that if T ⊢_{L} c, then there is a Cut-free L proof π of T ⊢ c such that π has the following properties: (a) all axiom instances in π are atomic; (b) no right-hand side 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 right-hand side premises of \L and /L inferences in π. But this is sufficient, for there is a Cut-free L proof π of T ⊢ c with the properties (a) through (c) if and only if there is an L* proof π′ of T ⊢ c*. This can be seen as follows:

Note (a′) that L* axioms at* ⊢ at involve only atomic categories; (b′) that the right-hand side 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 right-hand side 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 Cut-free L proof π of a sequent T ⊢ c with the properties (a) through (c) can be turned into an L* proof π′ of T ⊢ c* by adding an asterisk to the left-hand side category of axiom instances; adding an asterisk to the active left-hand side category in every conclusion sequent of a \L, /L, \R and /R inference; and replacing every sequent U, a*, V ⊢ at which is not the right-hand side premise of a \L or /L inference by the following inference:

{U, a*, V ⊢ at \atop U, a, V ⊢ at*} [ * ]  (8)

And, conversely, every L* proof π′ of T ⊢ c* can be turned into a Cut-free L proof π of T ⊢ c with properties (a) through (c) by replacing every inference of the form (8) by the sequent U, a, V ⊢ at and deleting all remaining asterisks. □

Let us now proceed by putting every 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} (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}.^{3} We have:

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. (9)

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

(10)

Proof of (9) and (10) by induction on p + q:

As for (9): if p + q = 0, then the claim is trivial; and 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 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. Claim 1 yields the equivalence of (1) and (2) as well as (3) and (4); the equivalence of (2) and (3) is due to the design of L*; and (4) and (5) are equivalent on account of the induction hypothesis. □

As for (10): if p + q = 0, then U, c*, V ⊢_{L*} at must be an axiom sequent at* ⊢_{L*} at, that is, at′ = at and U and V are empty; 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 (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 U = T_{1}, … T_{p}; V′ = T_{p+q−1}, … T_{p+1}; at′ = at and for all i, 1 ≤ i ≤ p + q − 1: T_{i} ⊢_{L*} c_{i}*. □

Given (10), suppose that T ⊢_{L} at. This holds iff T ⊢_{L*} at* by Claim 1. The sequent T ⊢ at* must have been derived by the * rule in L*. Therefore, T = U, c, V and U, c*, V ⊢_{L*} at. For some c_{1}, …, c_{p+q}, at′ it holds that c ∈ ⌊c_{p}\...\c_{1}\at′/c_{p+1}/.../c_{p+q}⌋. By (10), we have that U = T_{1}, …, T_{p}; V = T_{p+q}, …, T_{p+1}; at′ = at; and for all i, 1 ≤ i ≤ p + q: T_{i} ⊢_{L*} c_{i}*, which is equivalent to T_{i} ⊢_{L} c_{i} by Claim 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}. (11)

3Different 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:

(1) ((t\t)/(t/t))/t, (2) (t\(t/(t/t)))/t and (3) t\((t/(t/t))/t).

Let C be a set of categories. A category c is a C-category iff c is built up from categories in C.^{4} Sequences t/t, …, t/t consisting of n occurrences of the category t/t will be abbreviated as (t/t)^{n}.

Lemma:

Let A = {at_{1}, …, at_{k}, (t/t)/t, ((t/t)/(t/t))/(t/t)}, for distinct atomic categories at_{1}, …, at_{k} and t; 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 the number m of occurrences of the categories 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):

(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). For at ∈ at and c ∈ cat_{at}, the definition of at-count[c] is as follows: 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[c] = at-count[c]. (This is proven by a simple induction on the length of the proof 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. Therefore, 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[c] = 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^{5} 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 (11), 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 (9)—that T_{p+2} ⊬_{L} t/t. So, both (i) and (ii) lead to contradiction, which means that T, t ⊬_{L} t.

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

5This 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.

(b) Suppose T, (t/t)^{n} ⊢_{L} t. By (11), 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: 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}. Hence 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. So T, (t/t)^{n} ⊬_{L} t. □

Proof of (c): suppose T, t/t, t ⊢_{L} t. 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} by (11). 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 (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). Therefore, 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 (9). 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). Apparently, both (i) and (ii) lead to contradiction, so that 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.
(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.
(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.
(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.

Proof: Suppose the contrary of (1). 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 (9), and the latter contradicts Lemma (a). Suppose the contrary of (2). 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). Suppose the contrary of (3). 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. Suppose the contrary of (4). 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 (9), 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′ has to be empty). Hence T′′′ = S, t/t and S is empty, since S, t/t ⊢_{L} t/t entails S, t/t, t ⊢_{L} t by (11), which is impossible for non-empty S on account of Lemma (c). □

Let t and at_{0} be two distict atomic categories. Claim 2 shows that (t/t)/t and ((t/t)/(t/t))/(t/t) can be used for encoding t and at_{0}, respectively.

Claim 2:

Let 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 for T, c ∈ at and for T, c ∈ at′ we have that if T ⊢_{L} c, then T = c. This is obvious for T, c ∈ at (by at_{i}-count). For T, c ∈ at′:

∘ If T ⊢_{L} at_{j} for 1 ≤ j ≤ k, then for c′ ∈ ⌊c_{p}\...\c_{1}\at_{j}/c_{p+1}/.../c_{p+q}⌋ by (11): 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}). 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 (9), since (t/t)/t ∈ ⌊t/t/t⌋. By (11), 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, hence, that T = (t/t)/t.

∘ If T ⊢_{L} ((t/t)/(t/t))/(t/t), then T, t/t, t/t, t ⊢_{L} t by (9), due to the fact that c ∈ ⌊t/t/(t/t)/(t/t)⌋. By (11), 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′ such that 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 (9) (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 (9) (because 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 ⊢ _{mboxL} t
iff_{4} σ(T) ⊢_{L} σ(c).

‘iff_{1}’, iff_{3}’ and iff_{4}’ hold by (9) (for observe that 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—as was observed in (c) above— σ(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 (11); ‘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 (11).

∘ 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 (11); ‘iff_{2}’ holds by induction hypothesis; ‘iff_{3}’ holds by (b); ‘iff_{5}’ holds by (9) (since (t/t)/t ∈ ⌊t/t/t⌋); and the ‘only if’ part of ‘iff_{4}’ is an application of (11) (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 (11), 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 (11); ‘iff_{2}’ holds by induction hypothesis; ‘iff_{3}’ holds by (c); ‘iff_{5}’ holds by (9) (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 (11) (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 (11), 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, Claim 3 generalizes the substitution of Claim 2 for the encoding of any finite number of atomic categories. Let, for c ∈ cat and n ∈ IN:

\begin{matrix}β(c) = ((c/c)/(c/c))/(c/c) & α(c) = (c/c)/c \\ α^{0}(c) = c & α^{n+1}(c) = α^{n}(α(c)) \end{matrix}

Claim 3:

Let, for a sequence A = ⟨t, at_{1}, …, at_{m}⟩ of distinct atomic categories such that m ≥ 1, the substitution σ_{A} be defined [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 3 comes down to Claim 2 (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 2 (with at_{0} and k instantiated as at_{m} and m − 1, respectively). □

References

Benthem, J. van, 1986, Essays in Logical Semantics. Dordrecht: Reidel. Benthem, J. van, 1991, Language in Action. Categories, Lambdas and Logic. Amsterdam: North Holland. Buszkowski, W., Marciszewski, W., and Benthem, J. van, eds., 1988, Categorial Grammar. Amsterdam: John Benjamins. Hendriks, H., 1993, Studied Flexibility. Categories and Types in Syntax and Semantics. Dissertation University of Amsterdam. Hepple, M., 1990, The Grammar and Processing of Order and Dependency: a Categorial Approach. Dissertation University of Edinburgh. Klein, E., and Benthem, J. van, eds., 1988, Categories, Polymorphism and Unification, University of Edinburgh: Centre for Cognitive Science; and University of Amsterdam: Institute for Language, Logic and Information. 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 W. Buszkowski, W. Marciszewski and J. van Benthem, eds. Ponse, A., 1988, ‘Encoding Types in the Lambek Calculus,’ in E. Klein and J. van Benthem, eds.