Residuation in mixed Lambek systems^{∗}

Michael Moortgat Research Institute for Language and Speech (OTS) Trans 10, Utrecht moortgat@let.ruu.nl

Abstract

In this paper we compare grammatical inference in the context of simple and of mixed Lambek systems. Simple Lambek systems are obtained by taking the logic of residuation for a family of multiplicative connectives /, •, \, together with a package of structural postulates characterizing the resource management properties of the • connective. Different choices for Associativity and Commutativity yield the familiar Lambek systems NL, L, NLP, LP. Semantically, a simple Lambek system is a unimodal logic: the connectives get a Kripke style interpretation in terms of a single ternary accessibility relation modeling the notion of linguistic composition for each individual system.

The simple systems each have their virtues in linguistic analysis. But none of them in isolation provides a basis for a full theory of grammar. In the second part of the paper, we consider two types of mixed Lambek systems. The first type is obtained by generalizing residuation to families of n-ary connectives, and by putting together the different arities in one logic. We focus on residuation for unary connectives, hence on mixed (2,3) frames, as these already represent the complexities in full. We prove a number of elementary logical results for unary families of residuated connectives and their combination with binary families.

The second type of mixed system is obtained by combining a number of unimodal systems into one multimodal logic. The combined multimodal logic is set up in such a way that the individual resource management properties of the constituting logics are preserved. But the inferential capacity of the mixed logic is greater than the sum of its component parts through the addition of frame conditions with the corresponding interaction postulates regulating the communication between the component logics.

The Appendix presents a number of new proof-theoretic invariants for the logics discussed.

∗The materials in this paper prepare the ground for the sections on multiplicative connectives in a chapter on categorial grammar for the Handbook of Logic and Language (Van Benthem and ter Meulen (eds), Elsevier, to appear). Earlier versions of the paper were presented at the ‘Deduction and Language’ workshop, London, March 1994, and the Rome workshop on Lambek Calculus, May 1994. I thank the editors of the Handbook and the audiences at these workshops for comments.

I have greatly benefited from discussion, and joint work, with Natasha Kurtonina, Glyn Morrill and Dick Oehrle. All errors are my own.

1 Residuation: simple Lambek systems

This paper traces the ramifications of Residuation in a variety of categorial type logics. To set the scene, we briefly present the concept of residuation in general algebraic terms as it arises in the study of order-preserving mappings. In Moortgat and Oehrle ([24]) the reader can find a more thorough treatment with reference to the source material (such as [12, 6]).

Residuated pairs

Let A = (A, ⊑_{A}) and B = (B, ⊑_{B}) be partially ordered sets. Consider a pair of functions f : A ↦ B and g : B ↦ A. The pair (f, g) is called residuated if the inequalities of (⋆) hold. Alternatively, a pair of functions (f, g) is characterized as residuated by requiring f and g to be isotone (†), and by having the composition of the functions satisfy the inequalities of (‡).

(⋆)  fx ⊑_{B} y iff x ⊑_{A} gy
(†) if x ⊑_{A} y (x ⊑_{B} y) then fx ⊑_{B} fy (gx ⊑_{A} gy)
(‡)  fgx ⊑_{B} x, x ⊑_{A} gfx

Dunn’s papers on ‘gaggle theory’ ([10, 11]) provide an excellent survey of the many guises under which Residuation presents itself in (intuitionistic, modal, relevance, dynamic, temporal, linear,…) logic, and in Lambek style type logics — the object of our investigation which we now turn to.

Binary multiplicatives

We start with a quick review of the landscape of binary multiplicative operators. This is extremely well-trodden ground, and the present section contains nothing new. But it sets the agenda for our exploration of more adventurous territory in §2.1 and §2.2

Consider the language F of category formulae (or: types) of a simple Lambek system. F is obtained by closing a set of prime formulae (or: basic types, e.g. s, np, n, …) under binary connectives (or: type forming operators) /, •, \.

A ::= p_{0} | p_{1} | p_{2} | …
F ::= A | F/F | F • F | F\F

Type formulae have a quite general interpretation in the power set algebra of Kripke style relational structures — ternary relational structures in the case of the binary connectives ([8]). A ternary frame is a structure ⟨W, R^{3}⟩. W in the application we envisage here is to be thought of as a set of linguistic resources (or: signs, pieces of multidimensional linguistic information). The accessibility relation R can be understood as representing linguistic composition: Rzxy holds in case one can fuse together the information of signs x and y into a sign z. We obtain a model by adding a valuation v sending prime formulae to subsets of W and satisfying the clauses below for compound formulae.

\begin{aligned}v(A • B) & = & \{z |∃x∃y[Rzxy & x ∈ v(A) & y ∈ v(B)]\} \\ v(C/B) & = & \{x |∀y∀z[(Rzxy & y ∈ v(B)) ⇒ z ∈ v(C)]\} \\ v(A\C) & = & \{y |∀x∀z[(Rzxy & x ∈ v(A)) ⇒ z ∈ v(C)]\} \end{aligned}

Turning now to the logic of these type systems, we are interested in characterizing a relation of derivability between formulae such that A → B is provable iff v(A) ⊆ v(B). It is not difficult to check that given the above interpretation of compound formulae, the following laws determine the properties of • vis à vis /, \ with respect to derivability.

(res) A → C/B ⟺ A • B → C ⟺ B → A\C

The pairs of connectives (•, /) and (•, \) are easily recognized as the binary incarnations of the notion of residuation just defined for the case of unary operations f, g. Interpret the partially ordered set A (= B) as the set of type formulae F, ordered by derivability → (i.e. set-theoretic inclusion, semantically). For the right residual pair (•, /) we can read f as − • B and g as −/B, i.e. the product and division operations indexed by the fixed type B. The defining biconditional fx ≤ y iff x ≤ gy then becomes (†) below. Similarly for the left residual pair (•, \), where we read f as A • − and g as A\−, and obtain (‡).

\begin{matrix}(†) & A • B → C ⟺ A → C/B \\ (‡) & A • B → C ⟺ B → A\C \end{matrix}

Putting things together, we see that the anatomy of the most elementary Lambek type logic is given by the basic properties of the derivability relation (Reflexivity, Transitivity) plus the Residuation Laws establishing the relation between • and the two implications /, \. Below the axiomatic presentation of the system known as NL. Following [22], we add combinator proof terms: they will provide a compact way of referring to complete deductions later on. Via a canonical model construction Došen [8] obtains the elementary soundness and completeness result: in NL provability coincides with semantic inclusion for all ternary frames and all interpretations v.

NL: the pure logic of residuation

Combinator proof terms. We write f : A → B for a proof of the inclusion v(A) ⊆ v(B).

\begin{matrix}id_{A} : A → A & \frac{f : A → B g : B → C}{g ∘ f : A → C} \\ \frac{f : A • B → C}{β(f) : A → C/B} & \frac{f : A • B → C}{γ(f) : B → A\C} \\ \frac{g : A → C/B}{β^{−1}(g) : A • B → C} & \frac{g : B → A\C}{γ^{−1}(g) : A • B → C} \end{matrix}

Structural postulates, constraints on frames

Starting from the pure logic of residuation NL one can unfold a landscape of categorial type logics by gradually relaxing structure sensitivity in a number linguistically relevant dimensions. Below we consider the dimensions of linear precedence (order sensitivity) and immediate dominance (constituent sensitivity). Adding the structural postulates for Associativity or Commutativity (or both) to the pure logic of residuation, one obtains the systems L, NLP, LP.

\begin{matrix}ass & A • (B • C) ⟷ (A • B) • C \\ comm & A • B → B • A \end{matrix}

Using Correspondence Theory [4] one computes frame conditions restricting the interpretation of R^{3} for the different structural postulates. Došen’s completeness result for NL is then extended to the stronger logics by restricting the attention to ass (L), comm (NLP) or ass+comm frames (LP).

\begin{matrix}ass & A • (B • C) ⟷ (A • B) • C & ∃t.Rtxy & Rutz ⟺ ∃v.Rvyz & Ruxv \\ comm & A • B → B • A & Rzxy ⟺ Rzyx \end{matrix}

Gentzen calculus

The axiomatic presentation is the proper vehicle for model-theoretic investigation of the logics we have considered: it closely follows the semantics, thus providing a suitable basis for ‘easy’ completeness results. Proof-theoretically the axiomatic presentation has a serious drawback: because it is essentially based on Transitivity, it does not offer an appropriate basis for proof search. For proof-theoretic investigation of the categorial type logics one introduces a Gentzen presentation, and proves a Cut Elimination result, with its corollaries of decidability and the subformula property. Of course, one has to establish the equivalence between the axiomatic and the Gentzen presentations of the logic for all this to make sense. For L Lambek [21] has established the essential results. They have been extended to the full landscape of type logics in [19, 9].

In the axiomatic presentation, we consider arrows A → B with A, B ∈ F. In Gentzen presentation, the derivability relation is stated to hold between a term T (the antecedent) and a type formula (the succedent). A Gentzen term is a structured configuration of formulae — a structured database, in the terminology of Gabbay [13]. The term language is defined inductively as T ::= F | (T , T ). The structural connective (·, ·) in the term language tells you how to put together structured databases Δ_{1} and Δ_{2} into a structured database (Δ_{1}, Δ_{2}). The structural connective mimics the logical connective • in the type language. A sequent is a pair (Γ, A) with Γ ∈ T and A ∈ F, written as Γ ⇒ A.

To compare the two presentations, we define the formula equivalent Δ^{♭} of a structured database Δ. Let (Δ_{1}, Δ_{2})^{♭} = Δ_{1}^{♭} • Δ_{2}^{♭}, and A^{♭} = A for A ∈ F. The Gentzen presentation can be show to be equivalent to the combinator axiomatisation in the sense of the following proposition from [21].

Every combinator f : A → B gives a proof of A ⇒ B, and every proof of a sequent Γ ⇒ B gives a combinator f : Γ^{♭} → B.

As was the case for the combinator presentation, the sequent architecture consists of three components: (i) [Ax] and [Cut] capture the basic properties of the derivability relation ‘⇒’: reflexivity and contextualized transitivity for the ‘surgical’ Cut, (ii) each connective comes with two logical rules: a rule of use introducing the connective to the left of ‘⇒’ and a rule of proof introducing it on the right of ‘⇒’, finally (iii) there is a block of structural rules, possibly empty, with different packages of structural rules resulting in systems with different resource management properties.

Gentzen presentation: structured databases Sequents T ⇒ F where T ::= F | (T , T ). Notation: Γ[Δ] for an antecedent term Γ containing a distinguished occurrence of the subterm Δ.

[Ax] \overline{A ⇒ A}  \frac{Δ ⇒ A Γ[A] ⇒ C}{Γ[Δ] ⇒ C} [Cut]
[/R] \frac{(Γ, B) ⇒ A}{Γ ⇒ A/B}  \frac{Δ ⇒ B  Γ[A] ⇒ C}{Γ[(A/B, Δ)] ⇒ C} [/L]
[\R] \frac{(B, Γ) ⇒ A}{Γ ⇒ B\A}  \frac{Δ ⇒ B  Γ[A] ⇒ C}{Γ[(Δ, B\A)] ⇒ C} [\L]
[•L] \frac{Γ[(A, B)] ⇒ C}{Γ[A • B] ⇒ C}  \frac{Γ ⇒ A  Δ ⇒ B}{(Γ, Δ) ⇒ A • B} [•R]

Resource sensitive structural rules Permutation and Associativity.

\frac{Γ[(Δ_{2}, Δ_{1})] ⇒ A}{Γ[(Δ_{1}, Δ_{2})] ⇒ A} [P]  Γ[((Δ_{1}, Δ_{2}), Δ_{3})] ⇒ A Γ[(Δ_{1}, (Δ_{2}, Δ_{3}))] ⇒ A [A]

For the logics L and LP where • is associative, resp. associative and commutative, explicit application of the structural rules is generally compiled away by means of syntactic sugaring of the sequent language. Antecendent terms then take the form of sequences of formulae T ::= F, …, F where the comma is now of variable arity, rather than a binary structural connective. Reading these antecedents as sequences, one avoids explicit reference to the structural rule of Associativity; reading them as multisets, one also makes Permutation implicit.

Characteristic theorems, derived rules of inference We close this overview with an inventory of theorems and derived inference rules for the various logics.

1. Application: A/B • B → A, B • B\A → A

2. Co-application: A → (A • B)/B, A → B\(B • A)

3. Monotonicity •: if A → B and C → D, then A • C → B • D

4. Isotonicity ·/C, C\·: if A → B, then A/C → B/C and C\A → C\B

5. Antitonicity C/·, ·\C: if A → B, then C/B → C/A and B\C → A\C

6. Lifting: A → B/(A\B), A → (B/A)\B

7. Geach (main functor): A/B → (A/C)/(B/C), B\A → (C\B)\(C\A)

8. Geach (secondary functor): B/C → (A/B)\(A/C), C\B → (C\A)/(B\A)

9. Composition: A/B • B/C → A/C, C\B • B\A → C\A

10. Restructuring: (A\B)/C ⟷ A\(B/C)

11. (De)Currying: A/(B • C) ⟷ (A/C)/B, (A • B)\C ⟷ B\(A\C)

12. Permutation: if A → B\C then B → A\C 13. Exchange: A/B ⟷ B\A

14. Preposing/Postposing: A → B/(B/A), A → (A\B)\B

15. Mixed Composition: A/B • C\B → C\A, B/C • B\A → A/C

Items (1) to (5) are valid in the weakest logic NL. They provide an alternative to res to express the fact that (•,/) and (•,\) are residuated pairs, cf. (†,‡) of Def 1.1. Lifting is the closest one can get to (2) in ‘product-free’ type languages, i.e. type languages where the role of the product operator (generally left implicit) is restricted to glue together types on the left-hand side of the arrow. Items (7) to (11) mark the transition to L: their derivation involves the structural postulate of associativity for •. Rule (12) is characteristic for systems with a commutative •, NLP and LP. From (12) one immediately derives the collapse of the implications / and \, (13). As a result of this collapse, one gets variants of the earlier theorems obtained by substituting subtypes of the form A/B by B\A or vice versa. Examples are (14), an NLP variant of Lifting, or (15), an LP variant of Composition.

The simple Lambek systems each have their merits and their limitations when it comes to grammatical analysis. In Combinatory Categorial Grammar ([32]) instances of the full scala of type transitions above live together. In the presence of Residuation, such promiscuity has unpleasant consequences. The point here is that when one moves from a logic with a higher degree of structure sensitivity to a system with more relaxed resource management, one immediately looses sensitivity for the relevant structural parameter of the weaker logic. For example: the system NL has a hierarchically structured database which fully respects constituent structure. For cases of so-called non-constituent coordination, one would like to relax constituent structure. One could try to achieve this by adding Composition (or the Geach laws) to NL. But the addition of such postulates makes NL collapse into L: from Geach one easily obtains the unconditional Associativity postulate for • via Residuation. We leave this as an exercise for the reader.

In the following sections we try to develop a more articulate view on mixed styles of inference where such collapse is avoided.

2 Residuation in mixed logics

2.1 Mixed inference: combining 1-ary and 2-ary families

In the recent literature one finds a panoply of unary operators in addition to the multiplicatives we have discussed in the previous section:

• The ‘domain modality’ □ of Hepple [16]. Used to enforce locality constraints in terms of syntactic domains. Generalized to multimodal □_{i} to distinguish domain barriers of different strength. A syntactiv version of the semantically interpreted intensionality operator of Morrill [26].

• The ‘bracket operators’ [], []^{−1} of Morrill [27, 28]. Serving the same purpose, but implementing the idea in a quite different way.

• The ◇ operator of Morrill [27], declaring argument positions as licensing extraction.

• The Edinburgh ‘structural modalities’. Modelled after Linear Logic’s ‘!’ (bang) operator. Providing controlled access to more linguistically relevant structural options such as Permutation, Associativity.

Although the various operators are introduced with intended semantics and (Gentzen, natural deduction) proof theory, discussion of the relation between the model theory and the proof theory is lacking. This can easily lead to confusion. For example, the domain modalities and the Edinburgh structural modalities have been introduced with an S4 proof theory, borrowed from LL, and a subalgebra semantics in a general groupoid setting. But for the subalgebra semantics, the S4 proof theory is inadequate ([34]): it imposes semantic constraints which the subalgebra interpretation cannot support. There is a choice here: if it is the proof theory one likes, one should provide an adequate semantics with a soundness and completeness result ([20]). Or if the structure of the semantics is the linguistically important factor, one should provide appropriate proof theory ([33]).

Our aim in this section is to provide a general framework within which the different proposals for unary operators can be compared. The key concept, again, is residuation. We extend the language of binary multiplicatives with a unary pair of residual operators ◇, □^{↓} and establish some elementary logical results for the extended language. Parallel to our treatment of the binary multiplicatives /, •, \ in the previous section, we start from the pure logic of residuation for ◇, □^{↓}, and gradually add structural postulates in view of the linguistic applications.

Items (1) and (3), (4) closely follow Lambek’s [21] treatment of the binary multiplicative operators. We refer to Kurtonina [20] for a thorough investigation of the further logical ramifications of the matters dealt with here.

1. Axiomatic (‘combinator’) presentations of the pure logic of residuation for ◇, □^{↓}.

2. Soundness and completeness via the Došen canonical model construction.

3. Gentzen presentation, equivalence between the axiomatic and the Gentzen presentation.

4. Cut elimination for the Gentzen presentation. Decidability, subformula property.

5. Structural postulates T, 4, K. Items (1)–(3) for the systems with a choice from P({T, 4, K}).

Residuation: n-ary generalisation

The concept of residuation can be readily generalized to the case of n-ary connectives, as is shown in [10] in the general logical setting. Discussion of such generalizations for categorial type logics can be found in [7] and [24]. In the context of Kripke style frame semantics, we have n-ary products interpreted via n+1-ary accessibility relations. These products have a residual implication for each of their n factors. Let us write f_{•}(A_{1}, …, A_{n}) for the product and f\underrightarrow{i}(A_{1}, …, A_{n}) for the i-th place residual. And let us define R^{−i}y_{i}, y_{1}, …, x, …, y_{n} iff Rx, y_{1}, …, y_{i}, …, y_{n} to facilitate the statement of the interpretation clauses. Valuation for the n-ary families exhibits the familiar pattern: existential closure of a conjunctive statement for the product, universal closure of disjunctions for the residual implications.

\begin{matrix}v(f_{•}(A_{1}, …, A_{n})) = \{x | ∃y_{1} … y_{n}(Rx, y_{1} … y_{n} & y_{1} ∈ v(A_{1}) & … & y_{n} ∈ v(A_{n})\} \\ v(f\underrightarrow{i}(A_{1}, …, A_{n})) = \{x | ∀y_{1} … y_{n}((R^{−i}x, y_{1} … y_{n} & y_{j(j≠i)} ∈ v(A_{j})) ⇒ y_{i} ∈ v(A_{i})\} \end{matrix}

Unary residuated pairs

Let us focus now on the case of unary connectives. The connectives ◇, □^{↓} form (dual) residuated pairs (analogous to future possibility, past necessity), interpreted with respect to a binary accessibility relation R^{2}. One can think of ◇ (□^{↓}) as a truncated multiplicative product (implication). The defining residuation inference (⋆) here takes the form (⋆⋆).

\begin{aligned}(⋆) & fx ≤ y & ⟺ & x ≤ gy \\ (⋆⋆) & ◇A → B & ⟺ & A → □^{↓}B \end{aligned}

Again the extended valuation for ◇, □^{↓} formulae has the required properties for residuation to arise: existential closure of a conjunctive statement for ◇, universal closure of a disjunction for the residual □^{↓}. Note carefully that the □^{↓} interpretation moves you back along the R^{2} accessibility relation.

\begin{matrix}v(◇A) = \{x | ∃y(Rxy ∧ y ∈ v(A)\} \\ v(□^{↓}A) = \{x | ∀y(Ryx ⇒ y ∈ v(A)\} \end{matrix}

Kripke graphs: unary vs binary connectives

A picture may clarify the relation between the unary and the binary residuated pairs of connectives. In the case of • we make an existential move along the branching accessibility relation R^{3}. In the case of ◇ we make an existential move in the same direction, this time for a non-branching accessibility relation. In both cases, universal moves in the opposite direction bring you back to the point of origin.

[figure: \begin{matrix}C/B \\ A \\ x \end{matrix}; R^{3}z, xy; \begin{matrix}A\C \\ B \\ y \end{matrix}; \begin{matrix}z \\ A • B \\ C \end{matrix}; A x □^{↓}B; R^{2}y, x; ◇A y B]
A → C/B ⇔ A • B → C  ◇A → B ⇔ A → □^{↓}B
A • B → C ⇔ B → A\C

Axiomatisation: Lambek style

Let us put together the binary and the unary families of connectives and consider the mixed language

F ::= A | F/F | F • F | F\F | ◇F | □^{↓}F

Axiomatic presentation of the pure logic of residuation for the extended language is given below. We decorate the arrows A → B with combinator proof terms. This makes it easy later on to refer to deductions by means of their combinator.

\begin{matrix}id_{A} : A → A & \frac{f : A → B g : B → C}{g ∘ f : A → C} \\ \frac{f : ◇A → B}{μ(f) : A → □^{↓}B} & \frac{g : A → □^{↓}B}{μ^{−1}(g) : ◇A → B} \\ \frac{f : A • B → C}{β(f) : A → C/B} & \frac{g : A → C/B}{β^{−1}(g) : A • B → C} \\ \frac{f : A • B → C}{γ(f) : B → A\C} & \frac{g : B → A\C}{γ^{−1}(g) : A • B → C} \end{matrix}

Axiomatisation: Došen style

Below a deductive presentation based on the alternative way of characterizing a pair of residual operations f, g in terms of Isotonicity (⋆) and the inequalities (⋆⋆) for the compositions fg, gf.

(⋆) x ≤ y ⇒ fx ≤ fy, gx ≤ gy
(⋆⋆) fgx ≤ x, x ≤ gfx

In this presentation, the unit, co-unit combinators are primitive type transitions, recursively generalized via the Isotonicity rules of inference (Antitonicity for the negative subtype of implications /, \).

id_{A} : A → A  \frac{f : A → B g : B → C}{g ∘ f : A → C}

unit_{□^{↓}} : ◇□^{↓}A → A  co-unit_{□^{↓}} : A → □^{↓}◇A
unit_{/} : A/B • B → A co-unit_{/} : A → (A • B)/B
unit_{\} : B • B\A → A co-unit_{\} : A → B\(B • A)

\frac{f : A → B}{(f)^{⋄} : ◇A → ◇B}  \frac{f : A → B}{(f)^{□^{↓}} : □^{↓}A → □^{↓}B}

\frac{f : A → B g : C → D}{f · g : A • C → B • D}

\frac{f : A → B g : C → D}{f/g : A/D → B/C}  \frac{f : A → B g : C → D}{g\f : D\A → C\B}

Equivalence of the deductive presentations

For the /, •, \ fragment, we know the two deductive presentations are equivalent, cf. Lambek [21] for one direction, Došen [9] for the other. We take the Lambek presentation as our starting point here, and show for the extended system how from μ, μ^{−1} we obtain the alternative axiomatisation in terms of Isotonicity and the inequalities for the compositions ◇□^{↓} and □^{↓}◇ (Term decoration for the right column left to the reader.)

{id_{□^{↓}A} : □^{↓}A → □^{↓}A \atop μ^{−1}(id_{□^{↓}A} ) : ◇□^{↓}A → A}  \begin{matrix}◇A → ◇A \\ A → □^{↓}◇A \end{matrix}

\begin{matrix}f : A → B & {id_{◇B} : ◇B → ◇B \atop μ(id_{◇B} ) : B → □^{↓}◇B} \\ μ(id_{◇B} ) ∘ f : A → □^{↓}◇B \end{matrix}

μ^{−1}(μ(id_{◇B} ) ∘ f) : ◇A → ◇B

\begin{matrix}\begin{matrix}□^{↓}A → □^{↓}A \\ ◇□^{↓}A → A \end{matrix} & A → B \\ ◇□^{↓}A → B \end{matrix} ; □^{↓}A → □^{↓}B

Soundness, Completeness

For ternary frame semantics for the F(/, •, \) fragment, Došen [8] proves soundness and completeness on the basis of a canonical model construction. Došen’s results extend unproblematically to the ◇, □^{↓} extended language. We now consider mixed frames ⟨W, R^{2}, R^{3}⟩ with W the set of linguistic resources as before, and R^{2}, R^{3} arbitrary binary and ternary relations on W.

⊢ A → B iff, for every valuation v on every frame, v(A) ⊆ v(B).

(⇒) Induction on the length of proofs of A → B. (⇐) Extend Došen’s canonical model construction for the R^{2} relation as follows. For the canonical frame, let W be the formulae of F(/, •, \, ◇, □^{↓}). In the canonical frame, we define the accessibility relations R^{2} and R^{3} as follows:

R^{3}(C, A, B) ⟺ ⊢ C → A • B R^{2}(A, B) ⟺ ⊢ A → ◇B

Define the canonical valuation as v(A) = {B | ⊢ B → A}. Now suppose v(A) ⊆ v(B) but ⊬ A → B. If ⊬ A → B with the canonical valuation on the canonical frame, A ∈ v(A) but A ∉ v(B) so v(A) ⊈ v(B). Contradiction.

Canonical model: compound formulae

We have to check the canonical model construction for the new compound formulae ◇A, □^{↓}A. Below the direction that requires a little thinking.

(◇) Assume A ∈ v(◇B). We have to show ⊢ A → ◇B. A ∈ v(◇B) implies ∃A′ such that R^{2}AA′ and A′ ∈ v(B). By inductive hypothesis, ⊢ A′ → B. By Isotonicity for ◇ this implies ⊢ ◇A′ → ◇B. We have ⊢ A → ◇A′ by (Def R^{2}) in the canonical frame. By Transitivity, ⊢ A → ◇B.

(□^{↓}) Assume A ∈ v(□^{↓}B). We have to show ⊢ A → □^{↓}B. A ∈ v(□^{↓}B) implies that ∀A′ such that R^{2}A′A we have A′ ∈ v(B). Let A′ be ◇A. R^{2}A′A holds in the canonical frame since ⊢ ◇A → ◇A. By inductive hypothesis we have ⊢ A′ → B, i.e. ⊢ ◇A → B. By Residuation this gives ⊢ A → □^{↓}B.

Logical versus structural connectives

Following the agenda set out in §1 for the binary connectives, we now introduce a Gentzen presentation, and show that it is equivalent to the deductive presentation. For the Gentzen presentation we prove Cut Elimination, with its pleasant corollaries of Decidability and the Subformula property.

In order to present Gentzen calculus for the extended type language, we need an n-ary structural operator for every family of n-ary logical operators: binary (·, ·) for the family /, •, \, and unary (·) for the family ◇, □^{↓}. Corresponding to the formula language F we have a language of terms T (structured configurations of formulae).

F ::= A | F/F | F • F | F\F | ◇F | □^{↓}F
T ::= F | (T , T ) | (T )

Gentzen presentation

As before, sequents are pairs (Γ, A), Γ ∈ T , A ∈ F, written Γ ⇒ A. We have Belnap-style antecedent punctuation, with for ◇, □^{↓} the unary structural connective (·) matching the unary logical connectives. Below the rules of use [◇L], [□^{↓}L] and the rules of proof [◇R], [□^{↓}R] for the new connectives. It may be helpful to compare the ◇ rules with the rules for •, and the □^{↓} rules with the rules for an implication, say /.

Compare the ◇ rules with the rules for binary product •:

\begin{matrix}Γ ⇒ A \\ (Γ) ⇒ ◇A \end{matrix} ◇R \begin{matrix}Γ[(A)] ⇒ B \\ Γ[◇A] ⇒ B \end{matrix} ◇L

\begin{matrix}Γ ⇒ A & Δ ⇒ B \\ (Γ, Δ) ⇒ A • B \end{matrix} •R \begin{matrix}Γ[(A, B)] ⇒ C \\ Γ[A • B] ⇒ C \end{matrix} •L

Compare again the □^{↓} rules with the rules for binary implication /:

\begin{matrix}(Γ) ⇒ A \\ Γ ⇒ □^{↓}A \end{matrix} □^{↓}R \begin{matrix}Γ[A] ⇒ B \\ Γ[(□^{↓}A)] ⇒ B \end{matrix} □^{↓}L

\begin{matrix}(Γ, B) ⇒ A \\ Γ ⇒ A/B \end{matrix} /R \begin{matrix}Δ ⇒ B & Γ[A] ⇒ C \\ Γ[(A/B, Δ)] ⇒ C \end{matrix} /L

The astute reader will observe that, with some adaptation of the notation, the [◇L], [◇R] and [□^{↓}R] rules above are the ones Morrill ([27]) proposes in (one of the versions) of his ‘bracket’ operators. (The [□^{↓}L] rule of [27] is flawed: it derives the non-theorem □^{↓}◇A ⇒ A.) But the same observant reader will notice that the intended semantics for the bracket operators in [27] and [28] is less general, in assuming (quasi)functionality for the bracket/anti-bracket operators. Because our objective here is to start from the pure logic of residuation for ◇, □^{↓}, we stick to the unconstrained relational semantics for R^{2} for which completeness holds.

Extending the valuation to structured terms

To obtain direct semantic interpretation for sequents Γ ⇒ A we can extend the valuation to antecedent terms. Compare again the valuation for logical operators •, ◇ with that of their structural counterparts (·, ·), (·)

\begin{aligned}v(A • B) & = & \{z |∃x∃y[Rz, xy & x ∈ v(A) & y ∈ v(B)]\} \\ v((Δ_{1}, Δ_{2})) & = & \{z |∃x∃y[Rz, xy & x ∈ v(Δ_{1}) & y ∈ v(Δ_{2})]\} \end{aligned}

\begin{aligned}v(◇A) & = & \{x | ∃y(Rxy ∧ y ∈ v(A)\} \\ v((Δ)) & = & \{x | ∃y(Rxy ∧ y ∈ v(Δ)\} \end{aligned}

Truth and validity for sequents are then defined the usual way. We have completeness in case ⊢ Γ ⇒ A iff for every valuation v on every frame we have v(Γ) ⊆ v(A).

Equivalence of Gentzen and combinator presentations

To compare the two presentations, define for the language F(/, •, \, ◇, □^{↓}) the formula representation Δ^{♭} of a structural configuration Δ as follows:

(Δ_{1}, Δ_{2})^{♭} = Δ_{1}^{♭} • Δ_{2}^{♭}, (Δ)^{♭} = ◇Δ^{♭}, A^{♭} = A

The sequent presentation for the language F(/, •, \, ◇, □^{↓}) can be shown to be equivalent to the combinator axiomatisation in the sense of the following proposition.

Every combinator f : A → B gives a proof of A ⇒ B, and every proof of a sequent Γ ⇒ B gives a combinator f : Γ^{♭} → B.

From combinators to sequents

To obtain the Gentzen rules [◇L], [◇R], [□^{↓}L], [□^{↓}R] from combinator deductions, we use Isotonicity of ◇, □^{↓} in addition to the residuation inferences μ, μ^{−1}. Given the formula equivalent Γ^{♭} for sequent terms Γ, μ gives [□^{↓}R]^{♭}, [◇L]^{♭} makes premise and conclusion identical, and Isotonicity for ◇ gives [◇R]^{♭}. The only non-trivial case is [□^{↓}L]. Consider first the case where the context Γ is empty. The combinator derivation of [□^{↓}L]^{♭} is given below.

{f : A → B \atop (f)^{□^{↓}} : □^{↓}A → □^{↓}B} ; μ((f)^{□^{↓}} ) : ◇□^{↓}A → B  \begin{matrix}A ⇒ B \\ (□^{↓}A) ⇒ B \end{matrix} □^{↓}L

Next the case where the context Γ in the [□^{↓}L] premise Γ[A] ⇒ B is non-empty. Let g be Γ[A]^{♭} → B. Let π(g) be a sequence of μ, β, γ residuation inferences isolating A on the left of the arrow. Then we obtain the formula equivalent of the conclusion of [□^{↓}L] via the deduction π^{−1}(μ(□^{↓}(π(g)))).

From sequents to combinators

To obtain the combinators id, f ∘ g (Transitivity), μ(f), μ^{−1}(g) (Residuation) from sequent derivations, we use the Cut rule. Once we have established the equivalence of the combinator and the sequent presentation, we prove Cut Elimination for the latter. [Ax] gives id, f ∘ g is a special case of Cut. The crucial new cases μ(f), μ^{−1}(g) follow.

\begin{matrix}\begin{matrix}\begin{matrix}A ⇒ A \\ (A) ⇒ ◇A \end{matrix} & ◇R \\ A ⇒ □^{↓}◇A \end{matrix} ; □^{↓}R & \begin{matrix}f : ◇A ⇒ B \\ (□^{↓}◇A) ⇒ B \end{matrix} □^{↓}L \\ (A) ⇒ B \end{matrix} ; (cut) ; μ(f) : A ⇒ □^{↓}B ; □^{↓}R  \begin{matrix}g : A ⇒ □^{↓}B & \begin{matrix}B ⇒ B \\ (□^{↓}B) ⇒ B \end{matrix} □^{↓}L \\ (A) ⇒ B \end{matrix} ; (cut) ; μ^{−1}(g) : ◇A ⇒ B ; ◇L

Cut elimination: principal cuts

We now extend the Cut Elimination result to the new connectives ◇, □^{↓}. We proceed by induction on the complexity of the cut formula, and distinguish principal cuts, where the cut formula is active in both cut premises, from permutation conversions, where this is not the case.

Below the new cases of principal cuts, with cut formula ◇A and □^{↓}A. Replacement of a cut on ◇A (□^{↓}A) by a cut on A of smaller degree.

\begin{matrix}\begin{matrix}Δ ⇒ A \\ (Δ) ⇒ ◇A \end{matrix} ◇R & \begin{matrix}Γ[(A)] ⇒ B \\ Γ[◇A] ⇒ B \end{matrix} ◇L \\ Γ[(Δ)] ⇒ B \end{matrix} ; (cut) ⇝ \begin{matrix}Δ ⇒ A & Γ[(A)] ⇒ B \\ Γ[(Δ)] ⇒ B \end{matrix} (cut)

\begin{matrix}\begin{matrix}(Δ) ⇒ A \\ Δ ⇒ □^{↓}A \end{matrix} □^{↓}R & \begin{matrix}Γ[A] ⇒ B \\ Γ[(□^{↓}A)] ⇒ B \end{matrix} □^{↓}L \\ Γ[(Δ)] ⇒ B \end{matrix} ; (cut) ⇝ \begin{matrix}(Δ) ⇒ A & Γ[A] ⇒ B \\ Γ[(Δ)] ⇒ B \end{matrix} (cut)

Cut elimination: permutation conversions

The new cases where the active formula in the left or right premise is different from the Cut formula allow for the usual elimination strategy: permutation of the Cut rule and the logical rule. The Cut is moved upwards , and becomes of lower degree. Below the left premise antecedent cases for ◇A and □^{↓}A.

\begin{matrix}\begin{matrix}Γ[(A)] ⇒ B \\ Γ[◇A] ⇒ B \end{matrix} ◇L & Δ[B] ⇒ C \\ Δ[Γ[◇A]] ⇒ C \end{matrix} (cut) ⇝ \begin{matrix}\begin{matrix}Γ[(A)] ⇒ B & Δ[B] ⇒ C \\ Δ[Γ[(A)]] ⇒ C \end{matrix} & (cut) \\ Δ[Γ[◇A]] ⇒ C \end{matrix} ; ◇L

\begin{matrix}\begin{matrix}Δ[A] ⇒ B \\ Δ[(□^{↓}A)] ⇒ B \end{matrix} □^{↓}L & Γ[B] ⇒ C \\ Γ[Δ[(□^{↓}A)]] ⇒ C \end{matrix} (cut) ⇝ \begin{matrix}\begin{matrix}Δ[A] ⇒ B & Γ[B] ⇒ C \\ Γ[Δ[A]] ⇒ C \end{matrix} & (cut) \\ Γ[Δ[(□^{↓}A)]] ⇒ C \end{matrix} ; □^{↓}L

Permutation conversion: right premise antecedent

Active type ◇A or □^{↓}A in the antecedent of the right Cut premise. Notation: Γ[Δ_{1}, Δ_{2}] for a structure Γ with substructures Δ_{1}, Δ_{2}, not necessarily sisters.

\begin{matrix}Δ ⇒ A & \begin{matrix}Γ[A, (B)] ⇒ C \\ Γ[A, ◇B] ⇒ C \end{matrix} ◇L \\ Γ[Δ, ◇B] ⇒ C \end{matrix} ; (cut) ⇝ \begin{matrix}\begin{matrix}Δ ⇒ A & Γ[A, (B)] ⇒ C \\ Γ[Δ, (B)] ⇒ C \end{matrix} & (cut) \\ Γ[Δ, ◇B] ⇒ C \end{matrix} ; ◇L

\begin{matrix}Δ ⇒ A & \begin{matrix}Γ[A, B] ⇒ C \\ Γ[A, (□^{↓}B)] ⇒ C \end{matrix} □^{↓}L \\ Γ[Δ, (□^{↓}B)] ⇒ C \end{matrix} ; (cut) ⇝ \begin{matrix}\begin{matrix}Δ ⇒ A & Γ[A, B] ⇒ C \\ Γ[Δ, B] ⇒ C \end{matrix} & (cut) \\ Γ[Δ, (□^{↓}B)] ⇒ C \end{matrix} ; □^{↓}L

Permutation conversion: right premise succedent

Active type ◇A or □^{↓}A in the succedent of the right Cut premise.

\begin{matrix}Γ ⇒ A & \begin{matrix}(Δ[A]) ⇒ B \\ Δ[A] ⇒ □^{↓}B \end{matrix} □^{↓}R \\ Δ[Γ] ⇒ □^{↓}B \end{matrix} ; (cut) ⇝ \begin{matrix}\begin{matrix}Γ ⇒ A & (Δ[A]) ⇒ B \\ (Δ[Γ]) ⇒ B \end{matrix} & (cut) \\ Δ[Γ] ⇒ □^{↓}B \end{matrix} ; □^{↓}R

\begin{matrix}Δ ⇒ A & \begin{matrix}Γ[A] ⇒ B \\ (Γ[A]) ⇒ ◇B \end{matrix} ◇R \\ (Γ[Δ]) ⇒ ◇B \end{matrix} ; (cut) ⇝ \begin{matrix}\begin{matrix}Δ ⇒ A & Γ[A] ⇒ B \\ Γ[Δ] ⇒ B \end{matrix} & (cut) \\ (Γ[Δ]) ⇒ ◇B \end{matrix} ; ◇R

Illustration: Residuation laws

As an example, we check the compositions ◇□^{↓} and □^{↓}◇ (cf Application, Co-Application). Below their cut-free Gentzen derivations.

\begin{matrix}\begin{matrix}\begin{matrix}A ⇒ A \\ (□^{↓}A) ⇒ A \end{matrix} & □^{↓}L \\ ◇□^{↓}A ⇒ A \end{matrix} ; ◇L & \begin{matrix}\begin{matrix}A ⇒ A \\ (A) ⇒ ◇A \end{matrix} & ◇R \\ A ⇒ □^{↓}◇A \end{matrix} ; □^{↓}R \\ fgx ≤ x & x ≤ gfx \end{matrix}

Structural postulates

What we have discussed so far is the pure logic of residuation for the unary family ◇, □^{↓}. By imposing conditions ass, comm or their combination on ternary frames, we generate the landscape NL, L, NLP, LP with completeness results for the relevant classes of frames (Došen). Along the same lines, we can develop the substructural landscape for the unary family ◇, □^{↓} and its binary accessibility relation R^{2}, and for the mixed R^{2}, R^{3} system.

The following structural postulates constrain R^{2} to be transitive (4), or reflexive (T). Communication between R^{2} and R^{3} can be established via the strong distributivity postulate K, which distributes unary ◇ over both components of a binary •, or, in a more constrained way, via the weak distributivity postulates K1, K2, where ◇ selects the left or right subtype of a product.

\begin{matrix}4 : & ◇◇A → ◇A \\ T : & A → ◇A \\ K1 : & ◇(A • B) → ◇A • B \\ K2 : & ◇(A • B) → A • ◇B \\ K : & ◇(A • B) → ◇A • ◇B \end{matrix}

Below the correponding frame conditions (∀x, y, z, w ∈ W).

\begin{matrix}4 : & (Rxy & Ryz) ⇒ Rxz \\ T : & Rxx \\ K(1, 2) : & (Rwx & Rxyz) ⇒ ∃y′(Ry′y & Rwy′z) ∨ ∃z′(Rz′z & Rwyz′) \\ K : & (Rwx & Rxyz) ⇒ ∃y′∃z′(Ry′y & Rz′z & Rwy′z′) \end{matrix}

The K condition is the correlation postulate for Relevance logic from Routley and Meyer [31]. See Kurtonina [20] for discussion in the context of logics of linguistic resources. The weak distributivity principles K1, K2 play an important role in the applications discussed later in this paper.

Structural rules

The structural rules below translate the postulates T, 4, K1, K2, K from the formula level to the term level. As before, we prove equivalence between the rule and the postulate versions, and show that the Gentzen formulation allows cut-free proof search.

\begin{matrix}Γ[(Δ)] ⇒ A \\ Γ[((Δ))] ⇒ A \end{matrix} 4 \begin{matrix}Γ[(Δ)] ⇒ A \\ Γ[Δ] ⇒ A \end{matrix} T

\begin{matrix}Γ[((Δ_{1}), Δ_{2})] ⇒ A \\ Γ[((Δ_{1}, Δ_{2}))] ⇒ A \end{matrix} K1 \begin{matrix}Γ[((Δ_{1}), (Δ_{2}))] ⇒ A \\ Γ[((Δ_{1}, Δ_{2}))] ⇒ A \end{matrix} K \begin{matrix}Γ[(Δ_{1}, (Δ_{2}))] ⇒ A \\ Γ[((Δ_{1}, Δ_{2}))] ⇒ A \end{matrix} K2

Structural rules from structural postulates

We have to extend the equivalence between axiomatic and Gentzen style presentation to the structural postulates and rules. To obtain the sequent rules T, 4, K from combinator deductions, it is enough to consider the case where the context Γ is empty, as we have seen above. The following deductions give the formula equivalent of the structural rules T, 4, K. We leave K1, K2 to the reader.

\begin{matrix}4 : ◇◇Δ^{♭} → ◇Δ^{♭} & f : ◇Δ^{♭} → A \\ f ∘ 4 : ◇◇Δ^{♭} → A \end{matrix}  ⇝  \begin{matrix}(Δ)^{♭} ⇒ A \\ ((Δ))^{♭} ⇒ A \end{matrix} 4

\begin{matrix}T : Δ^{♭} → ◇Δ^{♭} & f : ◇Δ^{♭} → A \\ f ∘ T : Δ^{♭} → A \end{matrix}  ⇝  \begin{matrix}(Δ)^{♭} ⇒ A \\ Δ^{♭} ⇒ A \end{matrix} T
K : ◇(Δ_{1}^{♭} • Δ_{2}^{♭}) → ◇Δ_{1}^{♭} • ◇Δ_{2}^{♭} f : ◇Δ_{1}^{♭} • ◇Δ_{2}^{♭} → A

f ∘ K : ◇(Δ_{1}^{♭} • Δ_{2}^{♭}) → A ⇝ \begin{matrix}((Δ_{1}), (Δ_{2}))^{♭} ⇒ A \\ ((Δ_{1}, Δ_{2}))^{♭} ⇒ A \end{matrix} K

Structural postulates from structural rules

Derivation of the structural postulates via Gentzen proofs is straightforward.

\begin{matrix}\begin{matrix}A ⇒ A \\ (A) ⇒ ◇A \end{matrix} & ◇R \\ A ⇒ ◇A \end{matrix} ; T \begin{matrix}\begin{matrix}A ⇒ A \\ (A) ⇒ ◇A \end{matrix} & ◇R \\ ((A)) ⇒ ◇A \end{matrix} ; 4 ; (◇A) ⇒ ◇A ; ◇L ; ◇◇A ⇒ ◇A ; ◇L \begin{matrix}\begin{matrix}A ⇒ A \\ (A) ⇒ ◇A \end{matrix} ◇R & \begin{matrix}B ⇒ B \\ (B) ⇒ ◇B \end{matrix} ◇R \\ ((A), (B)) ⇒ ◇A • ◇B \end{matrix} ; •R ; ((A, B)) ⇒ ◇A • ◇B ; K ; ((A • B)) ⇒ ◇A • ◇B ; •L ; ◇(A • B) ⇒ ◇A • ◇B ; ◇L

Cut elimination: structural rules

We extend the cut elimination algorithm to logics with a structural rule package from P({T, 4, K}). Recall that in the case of connectives the proof of the Cut Elimination theorem is by induction on the complexity of Cut inferences, measured in terms of the number of connectives in the cut formula. The structural rules do not involve decomposition of formulae, so we need an additional complexity measure here.

Following [9, 3], let the trace of a cut formula A be the sum of the lengths of the paths in the derivations of the cut premises connecting the two occurrences of A with the point of their first introduction in the proof. The cut elimination steps involving structural rules now assimilate to the permutation cases: if a structural rule feeds the cut inference, we can interchange the order of application of the cut and the structural rule, leading to a situation with decreased trace, as the inductive hypothesis requires. Two examples are given below.

\begin{matrix}Δ[(Δ′)] ⇒ A \\ Δ[Δ′] ⇒ A \end{matrix} T Γ[A] ⇒ B Γ[Δ[Δ′]] ⇒ B (cut) ⇝

\begin{matrix}Δ[(Δ′)] ⇒ A & Γ[A] ⇒ B \\ Γ[Δ[(Δ′)]] ⇒ B \end{matrix} (cut)

Γ[Δ[Δ′]] ⇒ B T

Δ ⇒ A \begin{matrix}Γ[(Γ′[A])] ⇒ B \\ Γ[((Γ′[A]))] ⇒ B \end{matrix} 4

Γ[((Γ′[Δ]))] ⇒ B (cut) ⇝

\begin{matrix}Δ ⇒ A & Γ[(Γ′[A])] ⇒ B \\ Γ[(Γ′[Δ])] ⇒ B \end{matrix} (cut)

Γ[((Γ′[Δ]))] ⇒ B 4

Structural postulates: universal variant

In our discussion of structural postulates for •, we have seen that we can express Associativity, Commutativity either via a • postulate, or via implicational postulates, if we prefer to keep the language product-free. In a similar vein we could have presented T, 4, K in their □^{↓} forms:

\begin{matrix}4□^{↓} : & □^{↓}A → □^{↓}□^{↓}A \\ T □^{↓} : & □^{↓}A → A \\ K□^{↓}/ : & □^{↓}(A/B) → □^{↓}A/□^{↓}B \\ K□^{↓}\ : & □^{↓}(B\A) → □^{↓}B\□^{↓}A \end{matrix}

Below an illustration for the derivation of the universal variant K□^{↓}/.

\begin{matrix}\begin{matrix}\begin{matrix}B ⇒ B & A ⇒ A \\ (A/B, B) ⇒ A \end{matrix} & /L \\ ((□^{↓}(A/B)), (□^{↓}B)) ⇒ A \end{matrix} & □^{↓}L, □^{↓}L \\ ((□^{↓}(A/B), □^{↓}B)) ⇒ A \end{matrix} ; K ; (□^{↓}(A/B), □^{↓}B) ⇒ □^{↓}A ; □^{↓}R ; □^{↓}(A/B) ⇒ □^{↓}A/□^{↓}B ; /R

S4: Compilation of structural rules

We saw above that in the presence of Associativity for •, we have a sugared Gentzen presentation where the structural rule is compiled away, and the binary sequent punctuation (·, ·) omitted. Analogously, for □^{↓} with the combination KT 4 (S4), we have a sugared version of the Gentzen calculus, where the KT 4 structural rules are compiled away, so that the unary (·) punctuation can be omitted. Compare the following. (Notation †Γ for a term Γ of which the (pre)terminal subterms are of the form †A. The 4(cut) step is a series of replacements of terminal □^{↓}A by □^{↓}□^{↓}A via cuts depending on 4.)

\begin{matrix}\begin{matrix}Γ[A] ⇒ B \\ Γ[(□^{↓}A)] ⇒ B \end{matrix} & □^{↓}L \\ Γ[□^{↓}A] ⇒ B \end{matrix} ; T ⇝ \begin{matrix}Γ[A] ⇒ B \\ Γ[□^{↓}A] ⇒ B \end{matrix} □^{↓}L(S4)

\begin{matrix}\begin{matrix}□^{↓}Γ ⇒ A \\ (□^{↓}□^{↓})Γ ⇒ A \end{matrix} & □^{↓}L \\ (□^{↓})Γ ⇒ A \end{matrix} ; 4(cut) ; (□^{↓}Γ) ⇒ A ; K ; □^{↓}Γ ⇒ □^{↓}A ; □^{↓}R ⇝ \begin{matrix}□^{↓}Γ ⇒ A \\ □^{↓}Γ ⇒ □^{↓}A \end{matrix} □^{↓}R(S4)

Embedding NL in modal L: locality constraints

Morrill ([28]) conjectures the following. Define an embedding translation (·)^{♯} : F(NL) ↦ F(L + {◇, □^{↓}}):

(p)^{♯} = p
(A • B)^{♯} = ◇((A)^{♯} • (B)^{♯})
(A/B)^{♯} = □^{↓}(A)^{♯}/(B)^{♯}
(B\A)^{♯} = (B)^{♯}\□^{↓}(A)^{♯}
NL ⊢ A → B iff L+{◇, □^{↓}} ⊢ (A)^{♯} → (B)^{♯}

A (non-trivial) proof of the conjecture, based on a semantic completeness argument, is given in Kurtonina [20]. The linguistic relevance is the following: Hepple in [16] proposes a treatment of locality constraints in terms of an S4 universal modality. A legitimate question, from our ‘minimalistic’ perspective is: What resource management properties are needed to enforce a general theory of locality constraints? Proof of the Morrill conjecture above shows that in fact the pure logic of residuation for the pair ◇, □^{↓} is enough.

Application: modalities as procedural control features

There is a wide range of linguistic applications for the modal operators ◇, □^{↓}. For a start, we can now ‘situate’ with a high degree of precision the various unary operators that have been proposed in the literature. At one end of the spectrum, one finds a trimmed-down version of Morrill’s bracket operators realizing the pure logic of residuation for ◇, □^{↓}. At the other end, we find Hepple’s KT 4 syntactic domain modality. And — more excitingly — one can look for occupants of corners of the landscape that have not been explored. Here we give one surprising application, from the field of algorithmic proof theory. Below we show how one can enforce a uniform head-driven search regime for L on the basis of a modal decoration of L sequents.

Uniform head-driven search: L*

In the literature on automated deduction, it is well known that cut-free Gentzen proof search is still suboptimal from the efficiency perspective: there may be different (cut-free!) derivations leading to one and the same proof term. Restricting ourselves to the implicational fragment, the spurious non-determinism in the search space has two causes ([35]): (i) permutability of [L] and [R] inferences, and (ii) permutability of [L] inferences among themselves, i.e. non-determinism in the choice of the active formula in the antecedent. A so-called goal directed (or: uniform) search regime performs the non-branching [R] inferences before the [L] inferences (re (i)), whereas head driven search commits the choice of the antecedent active formula in terms of the goal formula (re (ii)).

In the context of categorial theorem proving, a goal-directed head-driven regime for L has been proposed in Hepple [16] with a proof of the safeness (no proof terms are lost) and non-redundancy (each proof term has a unique derivation). We present the Hepple regime in the format of Hendriks [15] where the reader can find a detailed discussion of the spurious ambiguity problem in the context of Gentzen proof search.

[Ax/⋆L] \overline{x : p^{⋆} ⇒ x : p}  \frac{Γ, u : B^{⋆}, Γ′ ⇒ t : p}{Γ, u : B, Γ′ ⇒ t : p^{⋆}} [⋆R]

[/R] \frac{Δ, x : B ⇒ t : A^{⋆}}{Δ ⇒ λx.t : A/B^{⋆}}  \frac{Δ ⇒ u : B^{⋆} Γ, x : A^{⋆}, Γ′ ⇒ t : C}{Γ, s : A/B^{⋆}, Δ, Γ′ ⇒ t[x/su] : C} [/L]

[\R] \frac{x : B, Δ ⇒ t : A^{⋆}}{Δ ⇒ λx.t : B\A^{⋆}}  \frac{Δ ⇒ u : B^{⋆} Γ, x : A^{⋆}, Γ′ ⇒ t : C}{Γ, Δ, s : B\A^{⋆}, Γ′ ⇒ t[x/su] : C} [\L]

Comments

The L* calculus eliminates the spurious non-determinism of the original presentation L by annotating sequents with a procedural control operator ‘*’. Goal sequents Γ ⇒ t : A in L are replaced by L* goal sequents Γ ⇒ t : A^{⋆}. With respect to the first cause of spurious ambiguity (permutability of [L] and [R] inferences), the control part of the [R] inferences forces one to remove all connectives from the succedent until one reaches an atomic succedent.

At that point, the ‘*’ control is transmitted from succedent to antecedent: the [*R] selects an active antecedent formula the head of which ultimately, by force of the control version of the Axiom sequent [*L], will have to match the (now atomic) goal type. The [L] implication inferences initiate a ‘*’ control derivation on the minor premise, and transmit the ‘*’ active declaration from conclusion to major (right) premise. The effect of the flow of control information is to commit the search to the target type selected in the [*R] step. This removes the second source of spurious ambiguity: permutability of [L] inferences.

Our labeling for the ‘*’ version of the Axiom sequent, [*L], is suggestive for the type of modal control we are about to propose.

Proofs and readings

The following theorem from [15] sums up the situation with respect to proofs and readings in L and L*.

1. L^{⋆} ⊢ Γ ⇒ A^{⋆} iff L ⊢ Γ ⇒ A

2. L^{⋆} ⊢ Γ ⇒ t : A^{⋆} implies L ⊢ Γ ⇒ t : A

3. L ⊢ Γ ⇒ t : A implies ∃t′, t′ = t and L^{⋆} ⊢ Γ ⇒ t′ : A^{⋆}

4. if π_{1} is an L* proof of Γ ⇒ t : A and π_{2} is an L* proof of Γ ⇒ t′ : A with t = t′, then π_{1} = π_{2}

Of the above, (1) asserts that, syntactically, derivability in L and L* coincide. Semantically, the set of L* proof terms forms a subset of the L terms (2). But, modulo logical equivalence, no readings are lost moving from L to L* (3). Moreover, the L* system has the desired one-to-one correspondence between readings and proofs (4).

Uniform proof search: modal control

In this section we show how to enforce the Hepple-Hendriks uniform head-driven search regime via a modal translation. The basic idea is to use the logical properties of the connectives ◇, □^{↓} to capture the effects of the ‘*’ procedural control marking in L*. We use the base residuation logic for ◇, □^{↓}, plus weak distributivity principles K1, K2 for the interaction between the unary and the binary families. For convenience we repeat the frame conditions and the Gentzen transformation of the K1, K2 structural postulates from our discussion above.

structural postulate  frame condition
K1 :  ◇(A • B) → ◇A • B  (Rwx & Rxyz) ⇒ ∃y′(Ry′y & Rwy′z)
K2 :  ◇(A • B) → A • ◇B  (Rwx & Rxyz) ⇒ ∃z′(Rz′z & Rwyz′)

In structural rule format these take the following form.

\begin{matrix}Γ[((Δ_{1})^{⋄}, Δ_{2})] ⇒ A \\ Γ[((Δ_{1}, Δ_{2}))^{⋄}] ⇒ A \end{matrix} K1 \begin{matrix}Γ[(Δ_{1}, (Δ_{2})^{⋄})] ⇒ A \\ Γ[((Δ_{1}, Δ_{2}))^{⋄}] ⇒ A \end{matrix} K2

To establish the equivalence with L* search, we can use the sugared presentation of L where Associativity is compiled away so that binary punctuation (·, ·) can be omitted (but not the unary (·)^{⋄}!). This gives the following compiled format for K1, K2:

\begin{matrix}Γ, (Δ)^{⋄}, Γ′ ⇒ B \\ (Γ, Δ, Γ′)^{⋄} ⇒ B \end{matrix} K′

Translation: formulae, sequents

We define the translation mapping first on the formula level, and then extend it to the level of L* sequents, where we have to distinguish marked and unmarked formulae. On the formula level, define mappings (·)^{1}, (·)^{0} : F(/, \) ↦ F(/, \, ◇, □^{↓}), for antecedent and succedent formula occurrences respectively.

(p)^{1} = p (p)^{0} = □^{↓}p
(A/B)^{1} = (A)^{1}/(B)^{0} (A/B)^{0} = (A)^{0}/□^{↓}(B)^{1}
(B\A)^{1} = (B)^{0}\(A)^{1} (B\A)^{0} = □^{↓}(B)^{1}\(A)^{0}

The formulae of a sequent Γ ⇒ A in L* are partitioned by the ‘*’ annotation in a set of marked formulae — a singleton, since there is only one ‘*’ per sequent — and a set of unmarked formulae. We extend the translation mapping taking this difference into account. The antecedent and succedent translation functions (·)_{1}, (·)_{0} below are defined in terms of (·)^{1}, (·)^{0}, but they act in a different way on marked and on unmarked formulae.

(A_{1}, …, A_{n})_{1} = \overline{A_{1}}, …, \overline{A_{n}} where \overline{A} = \{ \begin{matrix}(A)^{1} & if A is ‘*’ marked \\ □^{↓}(A)^{1} & otherwise \end{matrix}

(A)_{0} = \{ \begin{matrix}(A)^{0} & if A is ‘*’ marked \\ A & otherwise \end{matrix}

We now have the following proposition.

L^{⋆} ⊢ Γ ⇒ A^{⋆}  iff  L◇K′ ⊢ (Γ)_{1} ⇒ (A)_{0}

Equivalence of L* and L◇K′

The (⇒) direction of the equivalence can be proved by straightforward induction on the length of derivations in L*. For the more delicate (⇐) direction, we have to show that L◇K′ does not derive more than L*. We give a case analysis of the choice points in the top-down (backward-chaining) unfolding of the search space, and show that L◇K′ can make no moves that would lead the search out of the space defined by the translation mapping.

Below we juxtapose the L* rules and axiom and their counterpart in L◇K′. We treat only one implication. For the L◇K′ version, we interleave the proof unfolding with the evaluation of the translation mapping. As an auxiliary notion, we have functions active and locked which for a sequent return the set of formulae matching the input condition for a logical rule (active), and those which no logical rule is applicable to (locked).

Proof search starts with an L* goal sequent Γ ⇒ (A)^{⋆}. The goal type A is either atomic or complex, the antecedent is of length 1 or greater than 1. Consider first the case of a complex goal type and 1 ≤ |Γ|. On the left the L* [/R] rule, on the right the corresponding derivation in L◇K′. Both (†) and (‡) stand in a feeding relation with themselves. For the roots of the derivations, we have active(†)= {A/B}, active(‡)= {(A/B)^{0}}; for the leaves, active(†)= {A}, active(‡)= {(A)^{0}}. Note that all antecedent formulae in (‡) have main connective □^{↓} as a result of the translation mapping. The □^{↓} connective acts as a lock: embedded connectives in these formulae will only be accessible after the removal of □^{↓}.

(†) \begin{matrix}Γ, B ⇒ (A)^{⋆} \\ Γ ⇒ (A/B)^{⋆} \end{matrix} /R  \begin{matrix}\begin{matrix}□^{↓}(Γ)^{1}, □^{↓}(B)^{1} ⇒ (A)^{0} \\ □^{↓}(Γ)^{1} ⇒ (A)^{0}/□^{↓}(B)^{1} \end{matrix} & /R \\ □^{↓}(Γ)^{1} ⇒ (A/B)^{0} \end{matrix} ; (·)^{0} (‡)

Consider now the case where the recursion on succedent implications bottoms out, i.e. where we reach the ‘*’ marked atomic head of the goal formula. In L* the only applicable rule in this situation is [⋆R] which transmits the ‘*’ marking from succedent to antecedent. [⋆R] is non-deterministic: any antecedent formula B can receive the ‘*’ marking. In L◇K′ the active atom is realized as (p)^{0} = □^{↓}p. The only applicable rule here is [□^{↓}R] which, by residuation, realizes □^{↓} as (·)^{⋄} on the antecedent. [□^{↓}R] can only be followed by [K′], which non-deterministically pushes (·)^{⋄} to an arbitrary antecedent formula □^{↓}(B)^{1}. At that point [□^{↓}L] becomes applicable, which through the elimination of □^{↓} shifts (B)^{1} from locked to active. Again, roots and leaves of the (†) (‡) derivations agree on active and locked.

(†) \begin{matrix}Γ, (B)^{⋆}, Γ′ ⇒ p \\ Γ, B, Γ′ ⇒ (p)^{⋆} \end{matrix} ⋆R  \begin{matrix}\begin{matrix}□^{↓}(Γ)^{1}, (B)^{1}, □^{↓}(Γ′)^{1} ⇒ p \\ □^{↓}(Γ)^{1}, (□^{↓}(B)^{1})^{⋄}, □^{↓}(Γ′)^{1} ⇒ p \end{matrix} & □^{↓}L \\ (□^{↓}(Γ)^{1}, □^{↓}(B)^{1}, □^{↓}(Γ′)^{1})^{⋄} ⇒ p \end{matrix} ; K′ □^{↓}(Γ)^{1}, □^{↓}(B)^{1}, □^{↓}(Γ′)^{1} ⇒ □^{↓}p □^{↓}R □^{↓}(Γ)^{1}, □^{↓}(B)^{1}, □^{↓}(Γ′)^{1} ⇒ (p)^{0} (·)^{0} (‡)

Next we analyse the possible antecedent configurations for the different choices of active formula. The active formula is either atomic or complex, and the context is either empty or non-empty. Let us consider these in turn, starting with the nonempty context case. If the active formula is atomic, the derivation fails, in L* and in L◇K′. If the active formula is complex (i.e. of the form B/C or C\B), the only applicable rule, in L* and in L◇K′, is [/L] ([\L]). The derivation branches, initiating uniform head-driven search for the negative subtype of the goal formula in the left premise, and declaring the positive subtype active in the right premise. Roots and leaves of the derivations in L* and in L◇K′ agree on the active, locked partitioning.

\begin{matrix}Δ ⇒ (B)^{⋆} & Γ, (A)^{⋆}, Γ′ ⇒ p \\ Γ, (A/B)^{⋆}, Δ, Γ′ ⇒ p \end{matrix} /L

\begin{matrix}□^{↓}(Δ)^{1} ⇒ (B)^{0} & □^{↓}(Γ)^{1}, (A)^{1}, □^{↓}(Γ′)^{1} ⇒ p \\ □^{↓}(Γ)^{1}, (A)^{1}/(B)^{0}, □^{↓}(Δ)^{1}, □^{↓}(Γ′)^{1} ⇒ p \end{matrix} /L

□^{↓}(Γ)^{1}, (A/B)^{1}, □^{↓}(Δ)^{1}, □^{↓}(Γ′)^{1} ⇒ p (·)^{1}

Finally, consider the base cases of the recursion. Below the correspondence when the L* Axiom sequent, i.e. [⋆L] is reached.

(p)^{⋆} ⇒ p ⋆L  \begin{matrix}p ⇒ p \\ (p)^{1} ⇒ p \end{matrix} (·)^{1}

For the sake of completeness, one should add the case of the trivial initial sequent p ⇒ (p)^{⋆}, though the issue of spurious ambiguity hardly arises here. Below the L* form and its L◇K′ counterpart.

\begin{matrix}(p)^{⋆} ⇒ p & ⋆L \\ p ⇒ (p)^{⋆} \end{matrix} ; ⋆R  \begin{matrix}\begin{matrix}p ⇒ p \\ (□^{↓}p)^{⋄} ⇒ p \end{matrix} & □^{↓}L \\ □^{↓}p ⇒ □^{↓}p \end{matrix} ; □^{↓}R ; □^{↓}(p)^{1} ⇒ (p)^{0} ; (·)^{1}, (·)^{0}

Illustration: Geach

Without the constraint on uniform head-driven search, there are two L sequent derivations for the Geach transition. They produce the same proof term.

\begin{matrix}\begin{matrix}\begin{matrix}c ⇒ c & b ⇒ b \\ b/c, c ⇒ b \end{matrix} /L & a ⇒ a \\ a/b, b/c, c ⇒ a \end{matrix} & /L \\ a/b, b/c ⇒ a/c \end{matrix} ; /R ; a/b ⇒ (a/c)/(b/c) ; /R  \begin{matrix}c ⇒ c & \begin{matrix}b ⇒ b & a ⇒ a \\ a/b, b ⇒ a \end{matrix} /L \\ a/b, b/c, c ⇒ a \end{matrix} ; /L ; a/b, b/c ⇒ a/c ; /R ; a/b ⇒ (a/c)/(b/c) ; /R

Geach: uniform head-driven search

Of these two, only the first survives in the L* regime.

\begin{matrix}\begin{matrix}\begin{matrix}(c)^{⋆} ⇒ c & ⋆L \\ c ⇒ (c)^{⋆} \end{matrix} ; ⋆R & (b)^{⋆} ⇒ b ⋆L \\ (b/c)^{⋆}, c ⇒ b \end{matrix} ; /L ; b/c, c ⇒ (b)^{⋆} ; ⋆R & (a)^{⋆} ⇒ a ⋆L \\ (a/b)^{⋆}, b/c, c ⇒ a \end{matrix} ; /L ; a/b, b/c, c ⇒ (a)^{⋆} ; ⋆R ; a/b, b/c ⇒ (a/c)^{⋆} ; /R ; a/b ⇒ ((a/c)/(b/c))^{⋆} ; /R  \begin{matrix}\begin{matrix}\begin{matrix}(c)^{⋆} ⇒ c & ⋆L \\ c ⇒ (c)^{⋆} \end{matrix} ; ⋆R & \begin{matrix}fail \\ a/b, (b)^{⋆} ⇒ a \end{matrix} \\ a/b, (b/c)^{⋆}, c ⇒ a \end{matrix} & /L \\ a/b, b/c, c ⇒ (a)^{⋆} \end{matrix} ; ⋆R ; a/b, b/c ⇒ (a/c)^{⋆} ; /R ; a/b ⇒ ((a/c)/(b/c))^{⋆} ; /R

Uniform head-driven search: modal control

We interleave the proof unfolding and the unpacking of the (·)^{1}, (·)^{0} translations.

to be cont’d (a)^{1}/(b)^{0}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ a

(a/b)^{1}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ a (·)^{1}

(□^{↓}(a/b)^{1})^{⋄}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ a □^{↓}L

(□^{↓}(a/b)^{1}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1})^{⋄} ⇒ a K′

□^{↓}(a/b)^{1}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ □^{↓}a □^{↓}R

□^{↓}(a/b)^{1}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ (a)^{0} (·)^{0}

□^{↓}(a/b)^{1}, □^{↓}(b/c)^{1} ⇒ (a)^{0}/□^{↓}(c)^{1} /R

□^{↓}(a/b)^{1}, □^{↓}(b/c)^{1} ⇒ (a/c)^{0} (·)^{0}

□^{↓}(a/b)^{1} ⇒ (a/c)^{0}/□^{↓}(b/c)^{1} /R

□^{↓}(a/b)^{1} ⇒ ((a/c)/(b/c))^{0} (·)^{0}

Consider first the interaction of [/R] rules and selection of the active antecedent type. Antecedent types all have □^{↓} as main connective. The □^{↓} acts as a lock: a □^{↓}A formula can only become active when it is unlocked by the key ◇ (or (·)^{⋄} in structural terms). The key becomes available only when the head of the goal formula is reached: through residuation, [□^{↓}R] transmits ◇ to the antecedent, where it selects a formula via [K′].

Transmission of the active formula

There is only one key ◇ by residuation on the □^{↓} of the goal formula. As soon as it is used to unlock an antecedent formula, that formula has to remain active and connect to the Axiom sequent.

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}c ⇒ c \\ (c)^{1} ⇒ c \end{matrix} & (·)^{1} \\ (□^{↓}(c)^{1})^{⋄} ⇒ c \end{matrix} ; □^{↓}L ; □^{↓}(c)^{1} ⇒ □^{↓}c ; □^{↓}R ; □^{↓}(c)^{1} ⇒ (c)^{0} ; (·)^{0} & \begin{matrix}b ⇒ b \\ (b)^{1} ⇒ b \end{matrix} (·)^{1} \\ (b)^{1}/(c)^{0}, □^{↓}(c)^{1} ⇒ b \end{matrix} ; /L ; (b/c)^{1}, □^{↓}(c)^{1} ⇒ b ; (·)^{1} ; (□^{↓}(b/c)^{1})^{⋄}, □^{↓}(c)^{1} ⇒ b ; □^{↓}L ; (□^{↓}(b/c)^{1}, □^{↓}(c)^{1})^{⋄} ⇒ b ; K′ ; □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ □^{↓}b ; □^{↓}R ; □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ (b)^{0} ; (·)^{0} & \begin{matrix}a ⇒ a \\ (a)^{1} ⇒ a \end{matrix} (·)^{1} \\ (a)^{1}/(b)^{0}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ a \end{matrix} ; /L

Below, we show how the wrong identification of the antecedent head leads to failure. The key to unlock □^{↓}(a/b)^{1} has been spent on the wrong formula. As a result, the implication in (a/b)^{1} cannot become active. Compare with the failure of the corresponding L* derivation above.

\begin{matrix}\begin{matrix}\begin{matrix}c ⇒ c \\ (c)^{1} ⇒ c \end{matrix} & (·)^{1} \\ (□^{↓}(c)^{1})^{⋄} ⇒ c \end{matrix} ; □^{↓}L ; □^{↓}(c)^{1} ⇒ □^{↓}c ; □^{↓}R ; □^{↓}(c)^{1} ⇒ (c)^{0} ; (·)^{0} & \begin{matrix}fails \\ □^{↓}(a/b)^{1}, (b)^{1} ⇒ a \end{matrix} † \\ □^{↓}(a/b)^{1}, (b)^{1}/(c)^{0}, □^{↓}(c)^{1} ⇒ a \end{matrix} ; /L ; □^{↓}(a/b)^{1}, (b/c)^{1}, □^{↓}(c)^{1} ⇒ a ; (·)^{1} ; □^{↓}(a/b)^{1}, (□^{↓}(b/c)^{1})^{⋄}, □^{↓}(c)^{1} ⇒ a ; □^{↓}L ; (□^{↓}(a/b)^{1}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1})^{⋄} ⇒ a ; K′ ; □^{↓}(a/b)^{1}, □^{↓}(b/c)^{1}, □^{↓}(c)^{1} ⇒ □^{↓}a ; □^{↓}R

2.2 Mixed inference: multimodal systems

Our second generalizing move is from mixed (2,3) frames (unimodal for each arity) to multimodal frames. The objective here is to combine the virtues of the distinct logics we have discussed before in one multimodal system, and at the same time to overcome the limitations of the individual systems in isolation. Each of the component logics has its own specific resource management properties: when combining the different logics, we have to take care that these individual characteristics are left intact. We do this by relativizing linguistic composition to specific resource management modes. But also, we want the inferential capacity of the combined logic to be more than the sum of the parts. The extra expressivity comes from interaction postulates that hold when different modes are in construction with one another.

We have treated the multimodal style of inference and its linguistic applications in greater detail elsewhere (cf [24, 25, 23]). In the present section we draw special attention to the interaction postulates, highlighting the correspondence between the type (1,2) K distributivity principles discussed in §2.1 and the type (2,2) principles regulating communication among binary modes.

On the syntactic level, the category formulae for the multimodal system are defined inductively on the basis of a set of category atoms A and a set of indices I as shown below. We refer to the i ∈ I as resource management modes, or modes for short.

F ::= A | F/_{i}F | F •_{i} F | F\_{i}F | ◇_{i}F | □_{i}^{↓}F

The semantics for the mixed language is a straightforward generalisation of frame semantics for the simple systems. Rather than interpret multiplicative connectives in terms of one (binary, ternary) privileged notion of linguistic composition, we throw different forms of linguistic composition together and interpret in multimodal frames ⟨W, {R_{i}^{2}}_{i∈I}, {R_{i}^{3}}_{i∈I}⟩. A valuation on a frame respects the structure of the complex types in the familiar way, interpreting each of the modes i ∈ I with its own (binary or ternary) accesibility relation.

\begin{aligned}v(◇_{i}A) & = & \{x | ∃y(R_{i}xy ∧ y ∈ v(A)\} \\ v(□_{i}^{↓}A) & = & \{x | ∀y(R_{i}yx ⇒ y ∈ v(A)\} \\ v(A ∘_{i} B) & = & \{z |∃x∃y[R_{i}zxy & x ∈ v(A) & y ∈ v(B)]\} \\ v(C/_{i}B) & = & \{x |∀y∀z[(R_{i}zxy & y ∈ v(B)) ⇒ z ∈ v(C)]\} \\ v(A\_{i}C) & = & \{y |∀x∀z[(R_{i}zxy & x ∈ v(A)) ⇒ z ∈ v(C)]\} \end{aligned}

We can present the multimodal logic axiomatically or in Gentzen style. In the axiomatic presentation, we have the familiar residuation pattern now relativized to resource management modes:

\begin{matrix}◇_{i}A → B & iff & A → □_{i}^{↓}B \\ A → C/_{i}B & iff & A ∘_{i} B → C & iff & B → A\_{i}C \end{matrix}

In sequent presentation, each residuated family of multiplicatives {◇_{i}, □_{i}^{↓}}, {/_{i}, ∘_{i}, \_{i}} has a matching structural connective, again relativized to resource management modes. Antecedent terms are inductively defined as

T ::= F | (T , T )^{i} | (T )^{i}

Logical rules insist that use and proof of connectives respect the resource management modes.

Multimodal sequent calculus

[Ax] \overline{A ⇒ A}  \frac{Γ ⇒ A Δ[A] ⇒ C}{Δ[Γ] ⇒ C} [Cut]

[R◇_{i}] \frac{Γ ⇒ A}{(Γ)^{i} ⇒ ◇_{i}A}  \frac{Γ[(A)^{i}] ⇒ B}{Γ[◇_{i}A] ⇒ B} [L◇_{i}]

[R□_{i}^{↓}] \frac{(Γ)^{i} ⇒ A}{Γ ⇒ □_{i}^{↓}A}  \frac{Γ[A] ⇒ B}{Γ[(□_{i}^{↓}A)^{i}] ⇒ B} [L□_{i}^{↓}]

[R/_{i}] \frac{(Γ, B)^{i} ⇒ A}{Γ ⇒ A/_{i}B}  \frac{Γ ⇒ B  Δ[A] ⇒ C}{Δ[(A/_{i}B, Γ)^{i}] ⇒ C} [L/_{i}]

[R\_{i}] \frac{(B, Γ)^{i} ⇒ A}{Γ ⇒ B\_{i}A}  \frac{Γ ⇒ B  Δ[A] ⇒ C}{Δ[(Γ, B\_{i}A)^{i}] ⇒ C} [L\_{i}]

[L∘_{i}] \frac{Γ[(A, B)^{i}] ⇒ C}{Γ[A ∘_{i} B] ⇒ C}  \frac{Γ ⇒ A  Δ ⇒ B}{(Γ, Δ)^{i} ⇒ A ∘_{i} B} [R∘_{i}]

In addition to the residuation inferences which are shared by all resource management modes, there are mode-specific structural options. In axiomatic style, they take the form of structural axioms; in sequent presentation, we have the corresponding structural rules. As an illustration, see the structural axioms/rules for a commutative mode c. In the semantics the R_{c} interpreting this connective will be constrained to satisfy (∀x, y, z ∈ W)R_{c}zxy ⇒ R_{c}zyx.

A ∘_{c} B ⟷ B ∘_{c} A \frac{Γ[(Δ_{2}, Δ_{1})^{c}] ⇒ A}{Γ[(Δ_{1}, Δ_{2})^{c}] ⇒ A} [Comm]

Multimodal communication principles

What we have done so far is simply put together the individual systems discussed before in isolation. This is enough to gain combined access to the inferential capacities of the component logics, and one avoids the unpleasant collapse into the least discriminating logic that results from combining logics without taking into account the mode specifications, cf our discussion of CCG in §1. But as things are, the borders between the constituting logics in our multimodal setting are still hermetically closed. Let us turn then to the question of multimodal communication.

Communication between different modes is obtained semantically by frame conditions linking R_{i} and R_{j}. Two types of constraints can be distinguished:

• ordering of the accesibility relations R_{i} in terms of the information they provide about the structure of the linguistic resources. In terms of frame conditions, say for R_{i}^{3} more informative than R_{j}^{3}, this means (∀x, y, z ∈ W)R_{i}xyz ⇒ R_{j}xyz. For example, since the non-commutative product • is more informative than the commutative product ⊗, we’d have the constraint: (∀x, y, z)R_{•}xyz ⇒ R_{⊗}xyz. Corresponding to this form of frame condition, there will be Inclusion Postulates in the logic.

• frame conditions ‘mixing’ distinct R_{i} implementing, for example, mixed associativity or commutativity laws. This form of constraint is expressed in the logic in terms of Interaction Postulates.

We discuss them in turn.

Inclusion: products

As a simple example of an inclusion constraint, consider the following cut-free Gentzen derivation showing that commutative ⊗ is derivable from non-commutative • product. The derivation uses Left and Right logical rules (which depend on the proper sequent punctuation), the inclusion structural rule connecting •-type and ⊗- type configurations, and the Permutation structural rule for ⊗-type configurations.

\begin{matrix}\begin{matrix}B ⇒ B & A ⇒ A \\ (B, A)^{⊗} ⇒ B ⊗ A \end{matrix} & ⊗R \\ (A, B)^{⊗} ⇒ B ⊗ A \end{matrix} ; P ⊗ ; (A, B)^{•} ⇒ B ⊗ A ; • ⊑ ⊗ ; A • B ⇒ B ⊗ A ; •L

Compare the combinatory derivation, which depends on non-logical axiom schemata (π_{⊗} and the inclusion postulate λ_{•,⊗}) and transitivity.

\begin{matrix}λ_{•,⊗} : A • B → A ⊗ B & π_{⊗} : A ⊗ B → B ⊗ A \\ π_{⊗} ∘ λ_{•,⊗} : A • B → B ⊗ A \end{matrix}

Inclusion: order reversal through residuation

Where the inclusion for products gives A•_{i} B → A•_{j} B, derivability for the residual implications is the other way around. Below the combinator derivation and its cut-free Gentzen variant.

\begin{matrix}λ_{i,j} : A/_{j}B •_{i} B → A/_{j}B •_{j} B & {id : A/_{j}B → A/_{j}B \atop β_{j}^{−1}(id) : A/_{j}B •_{j} B → A} \\ β_{j}^{−1}(id) ∘ λ_{i,j} : A/_{j}B •_{i} B → A \end{matrix}

β_{i}(β_{j}^{−1}(id) ∘ λ_{i,j}) : A/_{j}B → A/_{i}B

\begin{matrix}\begin{matrix}B ⇒ B & A ⇒ A \\ (A/_{j}B, B)^{j} ⇒ A \end{matrix} & /_{j}L \\ (A/_{j}B, B)^{i} ⇒ A \end{matrix} ; •_{i} ⊑ •_{j} ; A/_{j}B ⇒ A/_{i}B ; /_{i}R

To convince oneself that the intuitions are satisfied here, let mode i be non-commutative, and mode j commutative, as in our previous example. Now consider a conjunction of commutative A/_{j}B and non-commutative A/_{i}B. Given the direction of the derivability arrow established above, the conjunction as a whole is A/_{i}B — which is as it should be: the commutativity of the j mode should not spoil the more discriminating resource management of the i mode.

The reader may be interested in comparing the treatment of inclusion constraints given here with that of Hepple [17] where the derivability arrows are systematically reversed.

Interaction principles: type (1,2)

In the discussion of (2,3) frames in §2.1 we have already seen the K principles of (strong, weak) distributivity for the communication between unary ◇, □^{↓} and binary /, •, \. In the multimodal setting, these principles can be relativized to specific mode interactions, resulting in a vastly increased control over resource management.

\begin{matrix}K1_{i,j} : & ◇_{i}(A •_{j} B) → ◇_{i}A •_{j} B \\ K2_{i,j} : & ◇_{i}(A •_{j} B) → A •_{j} ◇_{i}B \\ K_{i,j} : & ◇_{i}(A •_{j} B) → ◇_{i}A •_{j} ◇_{i}B \end{matrix}

Below the correponding frame conditions (∀x, y, z, w ∈ W).

\begin{matrix}K(1, 2)_{i,j} : & (R_{i}wx & R_{j}xyz) ⇒ ∃y′(R_{i}y′y & R_{j}wy′z) ∨ ∃z′(R_{i}z′z & R_{j}wyz′) \\ K_{i,j} : & (R_{i}wx & R_{j}xyz) ⇒ ∃y′∃z′(R_{i}y′y & R_{i}z′z & R_{j}wy′z′) \end{matrix}

A linguistic application of relativized K principles can be found in [23], where a head-selection ◇ interacts via K1 with left-headed dependency product •_{l}, and via K2 with right-headed dependency product •_{r}.

Interaction principles: type (2,2)

Consider finally interaction principles for inter-mode communication among binary families. Above, we distinguished weak and strong distributivity principles for (1,2) type interactions. Let us do exactly the same for interaction of the (2,2) type.

Consider first interaction of the weak distributivity type. Below one finds principles of mixed associativity and commutativity. Instead of the global associativity and commutativity options characterizing L, NLP, LP, we find mixed versions constrained to the situation where modes i and j are in construction. (Symmetric duals can be added, with the j mode adjunction distributing from the left.)

\begin{matrix}MC : (A •_{i} B) •_{j} C ⟷ (A •_{j} C) •_{i} B : MC′ \\ MA : (A •_{i} B) •_{j} C ⟷ A •_{i} (B •_{j} C) : MA′ \end{matrix}

The postulates correspond to frame conditions (∀xyzuv ∈ W):

MC : (R_{i}xyz & R_{j}zuv) ⇒ ∃t(R_{j}xut & R_{i}tyv)
MA : (R_{i}xyz & R_{j}zuv) ⇒ ∃t(R_{j}yut & R_{i}xtv)
MC′ : (R_{j}xyz & R_{i}zuv) ⇒ ∃t(R_{i}xut & R_{j}tyv)
MA′ : (R_{j}xyz & R_{i}uzv) ⇒ ∃t(R_{i}uxt & R_{j}tyv)

And they manifest themselves in structural rules in Gentzen presentation.

Γ[((Δ_{1}, Δ_{3})^{j}, Δ_{2})^{i}] ⇒ A Γ[((Δ_{1}, Δ_{2})^{i}, Δ_{3})^{j}] ⇒ A MC Γ[(Δ_{1}, (Δ_{2}, Δ_{3})^{j})^{i}] ⇒ A Γ[((Δ_{1}, Δ_{2})^{i}, Δ_{3})^{j}] ⇒ A MA

Γ[((Δ_{1}, Δ_{2})^{i}, Δ_{3})^{j}] ⇒ A Γ[((Δ_{1}, Δ_{3})^{j}, Δ_{2})^{i}] ⇒ A MC’ Γ[((Δ_{1}, Δ_{2})^{i}, Δ_{3})^{j}] ⇒ A Γ[(Δ_{1}, (Δ_{2}, Δ_{3})^{j})^{i}] ⇒ A MA’

Application: mixed composition

For linguistic application of these general postulates, we refer to [25, 23], where it is shown that a multimodal variant of CCG ‘mixed composition’ laws — which in the absence of mode constraints cause collapse of L into LP, as we saw above — are theorems in combined logics with the MC/MA principles. Schematically, in ‘Geach’ version, we have the following valid type transition (and the symmetric case), where the w mode stands for head adjunction and the r mode for righ-headed dependency adjunction.

A/_{w}B ⇒ (C\_{r}A)/_{w}(C\_{r}B)

\begin{matrix}\begin{matrix}\begin{matrix}C ⇒ C & B ⇒ B \\ (C, C\_{r}B)^{r} ⇒ B \end{matrix} \_{r}L & A ⇒ A \\ (A/_{w}B, (C, C\_{r}B)^{r})^{w} ⇒ A \end{matrix} & /_{w}L \\ (C, (A/_{w}B, C\_{r}B)^{w})^{r} ⇒ A \end{matrix} ; MC ; (A/_{w}B, C\_{r}B)^{w} ⇒ C\_{r}A ; \_{r}R ; A/_{w}B ⇒ (C\_{r}A)/_{w}(C\_{r}B) ; /_{w}R

Type (2,2) interaction: strong distributivity

The weak distributivity principles MC, MA keep us within the family of resource neutral logics: they do not affect the multiplicity of the resources in a configuration. Strong distributivity principles of the (2,2) type are not resource neutral: they duplicate resources. But in the multimodal setting, this gives access to modecontrolled forms of Contraction.

We give one illustration. Consider the distributivity principle S below, which strongly distributes mode j over mode i thus copying a C datum.

S : (A •_{i} B) •_{j} C → (A •_{j} C) •_{i} (B •_{j} C)

We leave it to the reader to compute frame conditions and structural rules. But we close this section pointing out that the S combinator of CCG (used in the derivation of parasitic gaps) is an immediate consequence of the S postulate. Again, in a unimodal setting the S combinator in combination with Residuation causes disaster. (Abbreviation: D = ((A/_{i}B)/_{j}C •_{j} C) •_{i} ((B/_{j}C) •_{j} C).)

\begin{matrix}S : ((A/_{i}B)/_{j}C •_{i} B/_{j}C) •_{j} C → D & f : D → A \\ f ∘ S : ((A/_{i}B)/_{j}C •_{i} B/_{j}C) •_{j} C → A \end{matrix} ; β_{j}(f ∘ S) : (A/_{i}B)/_{j}C •_{i} B/_{j}C → A/_{j}C

3 Conclusion

This paper is a technical investigation of the architecture of mixed categorial type logics. The raison d’être for such an exercise, we hope to have made clear, is the linguistic application of these logics to problems of grammatical analysis — without the linguistic motivation many of the logical issues addressed above would simply not arise. At the same time, we would like to stress that progress on the descriptive level of linguistic analysis is really dependent on a clear understanding of the logical structure of the type systems employed.

A Appendix: Invariants

Type transformations A → B in the Lambek systems NL, L, NLP, LP preserve the resource sensitivity properties of the individual logics. As a result one can characterize necessary conditions for derivability A → B in the different Lambek logics in terms of a number of useful invariants. In this Appendix, we present the known invariants for L and LP and add new ones for the systems NL and NLP, and for the extension with unary ◇, □^{↓} connectives.

A.1 Preservation properties: NL, L, NLP, LP

On the most general level, all members of the family of occurrence logics share the property of resource preservation: in a derivation A → B there is an equilibrium between available and consumed resources, i.e. between positive and negative occurrences of atomic type formulae. The atom count of Van Benthem [2] measures this property. We present the stronger invariants in a format due to Pentus [29] which translates type formulae into elements of the free group generated by the type atoms. First, resource preservation can be sharpened to order preservation for the systems L and NL where derivability is dependent on the linear order of the resources (Roorda, [30]). Order preservation, in its turn, can be sharpened to structure preservation for NL, where apart from linear order also the hierarchical grouping of resources determines derivability. In the setting of Abelian groups, finally, we obtain the NLP version of structure preservation, and an alternative way of expressing resource preservation.

Notice carefully that the invariants to be discussed here provide necessary but not sufficient conditions for derivability: they do not take into account the difference between A → B and B → A. They will be typically used then in arguments about non-derivability, and in a more practical context, in pruning the search space for categorial theorem proving, where the invariants allow early detection of nontheorems.

Proposition A.1 Resource preservation. (Atom count, Van Benthem.) Let #_{p}(A) be a function counting positive and negative occurrences of atomic formulae p in arbitrary formulae A defined as below.

#_{p}(p) = 1, #_{p}(q) = 0 for atoms p, q, p ≠ q
#_{p}(A/B) = #_{p}(B\A) = #_{p}(A) − #_{p}(B), #_{p}(A • B) = #_{p}(A) + #_{p}(B)

NL, L, NLP, LP ⊢ A → B implies #_{p}(A) = #_{p}(B) for any p ∈ A.

The proof of Prop A.1, and of the invariants to be discussed below, is obtained by straightforward induction on derivations using the axiomatic presentation of the logics. The axioms can be shown by inspection to have the relevant property (the logical axiom A → A plus structural postulates, if any), and the rules of inference (transitivity, residuation) preserve it.

For the order preservation invariant, we interpret type formulae as elements of G(A), the free group generated by the type atoms A. The group is equiped with an associative operation ‘·’ and with a two-sided identity element e satisfying e·p = p = p·e. As an element of the free group each prime formula p has an inverse p^{−1} such that p^{−1} · p = e = p · p^{−1}. The translations (·)^{1}, (·)^{0} are each other’s opposite in the sense that (A)^{1}(A)^{0} = e = (A)^{0}(A)^{1} for arbitrary types A.

Proposition A.2 Order preservation (‘Balance’, Roorda, Pentus.) Let G(A) be the free group generated by the atomic type formulae A. Define translations (·)^{1}, (·)^{0} : F ↦ G(A):

(p)^{1} = p, (p)^{0} = p^{−1}
(A • B)^{1} = (A)^{1} · (B)^{1}, (A • B)^{0} = (B)^{0} · (A)^{0}
(A/B)^{1} = (A)^{1} · (B)^{0}, (A/B)^{0} = (B)^{1} · (A)^{0}
(B\A)^{1} = (B)^{0} · (A)^{1}, (B\A)^{0} = (A)^{0} · (B)^{1}
NL, L ⊢ A → B implies (A)^{1} · (B)^{0} = e.

Observe that an alternative version of resource preservation in the sense of Proposition A.1 can be obtained via the free group interpretation of Proposition A.2 by turning G(A) into an Abelian group, where the group operation ‘·’ is commutative as well as associative.

For the system NL we need an invariant capturing the fact that derivability is dependent not only on the linear order of the resources but also on their hierarchical structuring. Structure preservation is obtained by doubling up the recursion of the order preservation invariant: instead of mappings (·)^{1}, (·)^{0}, with (A)^{1}(A)^{0} = e, we have four translation mappings (·)^{1}, (·)^{0},^{1}(·),^{0}(·) set up in such a way that 1(A)(A)^{0} = (A)^{0}^{1}(A) = ^{0}(A)(A)^{1} = (A)^{1}^{0}(A) = e for arbitrary A. The recursion keeps track of whether a subformula is within an even or odd number of brackets. For the basis of the recursion, i.e. the translation of prime formulae, we have a choice. Either (†) we augment the free group interpretation with a pair of elements 1, 0, to be thought of as structure markers. They are each other’s inverses, i.e. 1 · 0 = e = 0 · 1. Or (‡) we have for each prime formula p an even (^{⊤}p) and an odd (p^{⊤}) representative in the group, together with their inverses (p^{⊥} and ^{⊥}p respectively).

Proposition A.3 Structure preservation. Let G(A ∪ {1, 0}) be the free group generated by the union of atomic type formulae A and structure markers 1, 0 satisfying 1 · 0 = e = 0 · 1 (†). Let G(A^{⊥,⊤}) be the free group generated by the union of even/odd atomic type formula tokens A satisfying ^{⊤}p · p^{⊥} = e = p^{⊤} ·^{⊥}p (‡). Define translations (·)^{1}, (·)^{0},^{1}(·),^{0}(·) : F ↦ G(A ∪ {1, 0})(†) or F ↦ G(A^{⊥,⊤})(‡) as follows:

(†) (p)^{1} = p · 1, (p)^{0} = p^{−1} · 0, ^{1}(p) = 1 · p, ^{0}(p) = 0 · p^{−1},
(‡) ^{1}(p) = ^{⊤}p, (p)^{0} = p^{⊥}, (p)^{1} = p^{⊤}, ^{0}(p) = ^{⊥}p,
1(A • B) = (A)^{1} · (B)^{1}, (A • B)^{0} = ^{0}(B) ·^{0}(A)
(A • B)^{1} = ^{1}(A) ·^{1}(B), ^{0}(A • B) = (B)^{0} · (A)^{0}
1(A/B) = (A)^{1} · (B)^{0}, (A/B)^{0} = ^{1}(B) ·^{0}(A)
(A/B)^{1} = ^{1}(A) ·^{0}(B), ^{0}(A/B) = (B)^{1} · (A)^{0}
1(B\A) = (B)^{0} · (A)^{1}, (B\A)^{0} = ^{0}(A) ·^{1}(B)
(B\A)^{1} = ^{0}(B) ·^{1}(A), ^{0}(B\A) = (A)^{0} · (B)^{1}
NL ⊢ A → B implies ^{1}(A) · (B)^{0} = e.

Example A.4 We check an NL theorem, Lifting p → q/(p\q) and a non-theorem of NL, the Geach transformation p/q → (p/r)/(q/r). Both are order-preserving (⋆). Structure preservation (⋆⋆) holds for Lifting, not for Geach.

NL ⊢ p → q/(p\q)
(⋆) (p)^{1}(q/(p\q))^{0} = p(p\q)^{1}(q)^{0} = p(p)^{0}(q)^{1}q^{−1} = pp^{−1}qq−1 = e

(⋆⋆ †) ^{1}(p)(q/(p\q))^{0} = 1p^{1}(p\q)^{0}(q) = 1p(p)^{0}(q)^{1}0q^{−1} = 1pp^{−1}0q10q^{−1} = e

NL ⊬ p/q → (p/r)/(q/r)
(⋆) (p/q)^{1}((p/r)/(q/r))^{0} =
(p)^{1}(q)^{0}(q/r)^{1}(p/r)^{0} = pq^{−1}(q)^{1}(r)^{0}(r)^{1}(p)^{0} = pq^{−1}qr^{−1}rp^{−1} = e
(⋆⋆ ‡) ^{1}(p/q)((p/r)/(q/r))^{0} =
(p)^{1}(q)^{0}^{1}(q/r)^{0}(p/r) = p^{⊤}q^{⊥}(q)^{1}(r)^{0}(r)^{1}(p)^{0} = p^{⊤}q^{⊥}q^{⊤}r^{⊥}r^{⊤}p^{⊥} ≠ e

The two versions of the structure preservation invariant each have their merit. On the basis of (‡) one obtains the NLP variant of structure preservation by interpreting G(A^{⊥,⊤}) as an Abelian group (Kurtonina p.c.). For the (†) version, Abelianization does not have the desired effect because the positional information of the structure markers is destroyed by the commutativity of the group operation. But on the basis of the (†) version, we can obtain a more economical translation, where structure markers 0, 1 are cashed out not at the level of prime formulae, but at the points where the recursion breaks up compound formulae. The version of A.5 subsumes a sharpened form of Janssen’s ([18]) slash balance, which checks the balance of positive/negative occurrences of implications, ignoring directionality. Prop A.5 generalizes the operator count to the full set of connectives and keeps track of the difference between right and left implications.

Proposition A.5 Structure preservation with operator balance. Let G(A ∪ {1, 0}) be as in Prop A.3 Define translations (·)^{1}, (·)^{0},^{1}(·),^{0}(·) : F ↦ G(A ∪ {1, 0}):

(p)^{1} = p = ^{1}(p), ^{0}(p) = p^{−1} = (p)^{0}
1(A • B) = ^{1}(A) ·^{1}(B) · 1, (A • B)^{0} = 0 · (B)^{0} · (A)^{0}
(A • B)^{1} = 1 · (A)^{1} · (B)^{1}, ^{0}(A • B) = ^{0}(B) ·^{0}(A) · 0
1(A/B) = ^{1}(A) · 0 · (B)^{0}, (A/B)^{0} = ^{1}(B) · 1 · (A)^{0}
(A/B)^{1} = 0 · (A)^{1} ·^{0}(B), ^{0}(A/B) = (B)^{1} ·^{0}(A) · 1
1(B\A) = (B)^{0} ·^{1}(A) · 0, (B\A)^{0} = 1 · (A)^{0} ·^{1}(B)
(B\A)^{1} = ^{0}(B) · 0 · (A)^{1}, ^{0}(B\A) = ^{0}(A) · 1 · (B)^{1}
NL ⊢ A → B implies ^{1}(A) · (B)^{0} = e.

Example A.6 We compare the first (†) and second (‡) versions of structure preservation for an NL theorem, Lifting p → q/(p\q) and a non-theorem of NL, the Geach transformation p/q → (p/r)/(q/r).

NL ⊢ p → q/(p\q)

(†) ^{1}(p)(q/(p\q))^{0} = 1p^{1}(p\q)^{0}(q) = 1p(p)^{0}(q)^{1}0q^{−1} = 1pp^{−1}0q10q^{−1} = e (‡) ^{1}(p)(q/(p\q))^{0} = p^{1}(p\q)1(q)^{0} = p(p)^{0}^{1}(q)01q^{−1} = pp^{−1}q01q^{−1} = e

NL ⊬ p/q → (p/r)/(q/r)
(†) ^{1}(p/q)((p/r)/(q/r))^{0} =

(p)^{1}(q)^{0}^{1}(q/r)^{0}(p/r) = p1q^{−1}0(q)^{1}(r)^{0}(r)^{1}(p)^{0} = p1q^{−1}0q1r^{−1}0r1p^{−1}0 ≠ e

(‡) ^{1}(p/q)((p/r)/(q/r))^{0} =

1(p)0(q)^{0}^{1}(q/r)1(p/r)^{0} = p0q^{−1}^{1}(q)0(r)^{0}1^{1}(r)1(p)^{0} = p0q^{−1}q0r^{−1}1r1p^{−1} ≠ e

The table below summarizes the situation of invariants for the Lambek logics in terms of the free group interpretation.

logic  preservation  proposition  group operation
LP, L, NLP, NL  Resources  Prop A.2  abelian
L, NL  Order  Prop A.2  non-abelian
NL, NLP  Structure  Prop A.3 (†)  abelian
NL  Structure, Order Prop A.3 (‡), A.5  non-abelian

Table 1: Invariants

Illustrations

The reader may find it helpful to perform the calculations of the free group interpretation in terms of formula decomposition trees. Below we give some examples, starting with failure of structure preservation for Associativity (product variant and Geach variant).

\begin{aligned}{a \atop ^{1}(a)} & \begin{matrix}{b \atop ^{1}(b)} & {c \atop ^{1}(c)} & 1 \\ ^{1}(b • c) \end{matrix} & 1 \\ & ^{1}(a • (b • c)) \end{aligned} \begin{aligned}0 & {c^{−1} \atop (c)^{0}} & \begin{aligned}0 & {b^{−1} \atop (b)^{0}} & {a^{−1} \atop (a)^{0}} \\ & (a • b)^{0} \end{aligned} \\ & ((a • b) • c)^{0} \end{aligned}
NL ⊬ a • (b • c) → (a • b) • c
a · b · c · 1 · 1 · 0 · c^{−1} · 0 · b^{−1} · a^{−1} ≠ e

\begin{matrix}{a \atop ^{1}(a)} & 0 & {b^{−1} \atop (b)^{0}} \\ ^{1}(a/b) \end{matrix} \begin{matrix}\begin{matrix}{b \atop ^{1}(b)} & 0 & {c^{−1} \atop (c)^{0}} \\ ^{1}(b/c) \end{matrix} & 1 & \begin{matrix}{c \atop ^{1}(c)} & 1 & {a^{−1} \atop (a)^{0}} \\ (a/c)^{0} \end{matrix} \\ ((a/c)/(b/c))^{0} \end{matrix}

NL ⊬ a/b → (a/c)/(b/c)
a · 0 · b^{−1} · b · 0 · c^{−1} · 1 · c · 1 · a^{−1} ≠ e

Structure preserving commutativity in NLP.

\begin{matrix}{a^{⊤} \atop (a)^{1}} & \begin{matrix}{^{⊤}b \atop ^{1}(b)} & {^{⊤}c \atop ^{1}(c)} \\ (b • c)^{1} \end{matrix} \\ ^{1}(a • (b • c)) \end{matrix} \begin{matrix}{^{⊥}a \atop ^{0}(a)} & \begin{matrix}{b^{⊥} \atop (b)^{0}} & {c^{⊥} \atop (c)^{0}} \\ ^{0}(c • b) \end{matrix} \\ ((c • b) • a)^{0} \end{matrix}

NLP ⊢ a • (b • c) → (c • b) • a
a^{⊤} ·^{⊤}b ·^{⊤}c ·^{⊥}a · b^{⊥} · c^{⊥} = a^{⊤} ·^{⊥}a · b^{⊥} ·^{⊤}b · c^{⊥} ·^{⊤}c = e

Violation of structure preservation in NLP.

\begin{matrix}{a^{⊤} \atop (a)^{1}} & \begin{matrix}{^{⊤}b \atop ^{1}(b)} & {^{⊤}c \atop ^{1}(c)} \\ (b • c)^{1} \end{matrix} \\ ^{1}(a • (b • c)) \end{matrix} \begin{matrix}\begin{matrix}{b^{⊥} \atop (b)^{0}} & {a^{⊥} \atop (a)^{0}} \\ ^{0}(a • b) \end{matrix} & {^{⊥}c \atop ^{0}(c)} \\ (c • (a • b))^{0} \end{matrix}

NLP ⊬ a • (b • c) → c • (a • b)
a^{⊤} ·^{⊤}b ·^{⊤}c · b^{⊥} · a^{⊥} ·^{⊥}c ≠ e

A.2 Invariants: unary connectives

How do the invariants discussed above extend to the language F(/, •, \, ◇, □^{↓}) ?. For the combination of the pure logic of residuation for ◇, □^{↓} (no frame conditions on R^{2}) with NL (no frame conditions on R^{3}), and with L (Associativity for R^{3}) we have the following result, which is significant in the light of the modal embedding of NL in L◇ discussed in the main text. Other combinations are left as a topic for further research.

Let G(A ∪ {1, 0}) (†) and G(A^{⊤,⊥} ∪ {1, 0}) (‡) have the group theoretic interpretation discussed in the previous section. Define translations (·)^{1}, (·)^{0},^{1}(·),^{0}(·) : F ↦ G(A∪{1, 0}) (†) or F ↦ G(A^{⊤,⊥}∪{1, 0}) (‡) for the extended modal language as follows:

(†) (p)^{1} = p = ^{1}(p), ^{0}(p) = p^{−1} = (p)^{0}
(‡) ^{1}(p) = ^{⊤}p, (p)^{0} = p^{⊥}, (p)^{1} = p^{⊤}, ^{0}(p) = ^{⊥}p
1(◇A) = (A)^{1} · 1, (◇A)^{0} = 0 ·^{0}(A)
(◇A)^{1} = 1 ·^{1}(A), ^{0}(◇A) = (A)^{0} · 0
1(□^{↓}A) = 0 · (A)^{1}, (□^{↓}A)^{0} = ^{0}(A) · 1
(□^{↓}A)^{1} = ^{1}(A) · 0, ^{0}(□^{↓}A) = 1 · (A)^{0}
1(A • B) = (A)^{1} · (B)^{1}, (A • B)^{0} = ^{0}(B) ·^{0}(A)
(A • B)^{1} = ^{1}(A) ·^{1}(B), ^{0}(A • B) = (B)^{0} · (A)^{0}
1(A/B) = (A)^{1} · (B)^{0}, (A/B)^{0} = ^{1}(B) ·^{0}(A)
(A/B)^{1} = ^{1}(A) ·^{0}(B), ^{0}(A/B) = (B)^{1} · (A)^{0}
1(B\A) = (B)^{0} · (A)^{1}, (B\A)^{0} = ^{0}(A) ·^{1}(B)
(B\A)^{1} = ^{0}(B) ·^{1}(A), ^{0}(B\A) = (A)^{0} · (B)^{1}
L◇ ⊢ A → B implies ^{1}(A) · (B)^{0} = e.

(We present the NL and L case here in uniform fashion. If one is just interested in the L case, one can take the simpler Roorda marking, augmented with the 1,0 clauses for the ◇, □^{↓} formulae.)

In the following illustrations we show how the structure-preservation translation of Prop A.5 for NL theorems A → B and the embedding translation presented above for (A)^{♯} → (B)^{♯} in L◇ have the same group-theoretic interpretation.

Failure of associativity: NL

\begin{aligned}{a \atop ^{1}(a)} & \begin{matrix}{b \atop ^{1}(b)} & {c \atop ^{1}(c)} & 1 \\ ^{1}(b • c) \end{matrix} & 1 \\ & ^{1}(a • (b • c)) \end{aligned} \begin{aligned}0 & {c^{−1} \atop (c)^{0}} & \begin{aligned}0 & {b^{−1} \atop (b)^{0}} & {a^{−1} \atop (a)^{0}} \\ & (a • b)^{0} \end{aligned} \\ & ((a • b) • c)^{0} \end{aligned}

a • (b • c) → (a • b) • c

a · b · c · 1 · 1 · 0 · c^{−1} · 0 · b^{−1} · a^{−1} ≠ e

Failure of associativity: modal L

\begin{matrix}\begin{matrix}{a \atop ^{1}(a)} & \begin{matrix}\begin{matrix}{b \atop ^{1}(b)} & {c \atop ^{1}(c)} \\ (b • c)^{1} \end{matrix} & 1 \\ ^{1}(◇(b • c)) \end{matrix} \\ (a • ◇(b • c))^{1} \end{matrix} & 1 \\ ^{1}(◇(a • ◇(b • c))) \end{matrix} \begin{matrix}0 & \begin{matrix}{c^{−1} \atop (c)^{0}} & \begin{matrix}0 & \begin{matrix}{b^{−1} \atop (b)^{0}} & {a^{−1} \atop (a)^{0}} \\ ^{0}(a • b) \end{matrix} \\ (◇(a • b))^{0} \end{matrix} \\ ^{0}(◇(a • b) • c) \end{matrix} \\ (◇(◇(a • b) • c))^{0} \end{matrix}

◇(a • ◇(b • c)) → ◇(◇(a • b) • c)

a · b · c · 1 · 1 · 0 · c^{−1} · 0 · b^{−1} · a^{−1} ≠ e

Failure of associativity: NL, Geach

\begin{matrix}{a \atop ^{1}(a)} & 0 & {b^{−1} \atop (b)^{0}} \\ ^{1}(a/b) \end{matrix} \begin{matrix}\begin{matrix}{b \atop ^{1}(b)} & 0 & {c^{−1} \atop (c)^{0}} \\ ^{1}(b/c) \end{matrix} & 1 & \begin{matrix}{c \atop ^{1}(c)} & 1 & {a^{−1} \atop (a)^{0}} \\ (a/c)^{0} \end{matrix} \\ ((a/c)/(b/c))^{0} \end{matrix}

a/b → (a/c)/(b/c)

a · 0 · b^{−1} · b · 0 · c^{−1} · 1 · c · 1 · a^{−1} ≠ e

Failure of associativity (Geach): modal L

\begin{matrix}\begin{matrix}{a \atop ^{1}(a)} & 0 \\ (□^{↓}a)^{1} \end{matrix} & {b^{−1} \atop (b)^{0}} \\ ^{1}(□^{↓}a/b) \end{matrix} \begin{matrix}\begin{matrix}\begin{matrix}{b \atop ^{1}(b)} & 0 \\ (□^{↓}b)^{1} \end{matrix} & {c^{−1} \atop (c)^{0}} \\ ^{1}(□^{↓}b/c) \end{matrix} & \begin{matrix}1 & \begin{matrix}{c \atop ^{1}(c)} & \begin{matrix}1 & {a^{−1} \atop (a)^{0}} \\ ^{0}(□^{↓}a) \end{matrix} \\ (□^{↓}a/c)^{0} \end{matrix} \\ ^{0}(□^{↓}(□^{↓}a/c)) \end{matrix} \\ (□^{↓}(□^{↓}a/c)/(□^{↓}b/c))^{0} \end{matrix}

□^{↓}a/b → □^{↓}(□^{↓}a/c)/(□^{↓}b/c)

a · 0 · b^{−1} · b · 0 · c^{−1} · 1 · c · 1 · a^{−1} ≠ e

References

[1] Abrusci, M., C. Casadio and M. Moortgat (eds) (1994) Linear Logic and Lambek Calculus. Proceedings 1st Rome Workshop, June 1993. OTS/DYANA, Utrecht, Amsterdam.

[2] Benthem, J. van (1983) ‘The semantics of variety in categorial grammar’. Report 83–29, Math Dept. Simon Fraser University, Burnaby, Canada.

[3] Benthem, J. van (1991) Language in Action. Categories, Lambdas, and Dynamic Logic. Studies in Logic, North-Holland, Amsterdam.

[4] Benthem, J. van (1984) ‘Correspondence theory’. In Gabbay and Guenthner (eds) Handbook of Philosophical Logic. Vol II. Dordrecht, pp 167–247.

[5] Belnap, N.D. (1982) ‘Display Logic’. Journal of Philosophical Logic, 11, 375– 417.

[6] Blyth, T.S. and M.F. Janowitz (1972) Residuation Theory. New York.

[7] Buszkowski, W. (1988) ‘Generative power of categorial grammars’. In Oehrle, Bach and Wheeler (eds) Categorial Grammars and Natural Language Structures. Dordrecht.

[8] Došen, K. (1992) ‘A brief survey of frames for the Lambek calculus’. Zeitschr. f. math. Logik und Grundlagen d. Mathematik 38, 179–187.

[9] Došen, K. (1988,1989) ‘Sequent systems and groupoid models’. Studia Logica 47, 353–385, 48, 41–65.

[10] Dunn, J.M. (1991) ‘Gaggle theory: an abstraction of Galois connections and residuation, with applications to negation, implication, and various logical operators’. In Van Eijck (ed.) Logics in AI. JELIA Proceedings. Springer, Berlin.

[11] Dunn, M. (1993) ‘Partial Gaggles Applied to Logics With Restricted Structural Rules’. In Došen and Schröder-Heister (eds) Substructural Logics. Oxford.

[12] Fuchs, L. (1963) Partially-ordered Algebraic Systems. New York.

[13] Gabbay, D. (1991) Labelled Deductive Systems. Draft. Oxford University Press (to appear).

[14] Gabbay, D. (1993) ‘A general theory of structured consequence relations’. In Došen and Schröder-Heister (eds) Substructural Logics. Oxford.

[15] Hendriks, H. (1993) Studied Flexibility. PhD Dissertation, ILLC, Amsterdam.

[16] Hepple, M. (1990) The Grammar and Processing of Order and Dependency: A Categorial Approach. Ph.D. Dissertation, Edinburgh.

[17] Hepple, M. (1994) ‘Labelled deduction and discontinuous constituency’. In [1].

[18] Janssen, Th. (1991) ‘On properties of the Zielonka-Lambek calculus’. In Dekker and Stokhof (eds) Proceedings 8th Amsterdam Colloquium. ILLC, Amsterdam, pp 303–308.

[19] Kandulski, W. (1988) ‘The non-associative Lambek calculus’. In Buszkowski, Marciszewski and van Benthem (eds) Categorial Grammar. Amsterdam.

[20] Kurtonina, N. (1994) ‘On some modal extensions of the Lambek Calculus’. In [1].

[21] Lambek, J. (1958) ‘The Mathematics of Sentence Structure’, American Mathematical Monthly 65, 154–170.

[22] Lambek, J. (1988) ‘Categorial and categorical grammar’. In Oehrle, Bach and Wheeler (eds) Categorial Grammars and Natural Language Structures. Dordrecht.

[23] Moortgat, M. and G. Morrill (1991) ‘Heads and phrases. Type calculus for dependency and constituent structure’. Ms OTS Utrecht.

[24] Moortgat, M. and R. Oehrle (1993) Logical parameters and linguistic variation. Lecture notes on categorial grammar. 5th European Summer School in Logic, Language and Information. Lisbon.

[25] Moortgat, M. and R.T. Oehrle (1994) ‘Adjacency, dependency and order’. Proceedings 9th Amsterdam Colloquium, pp 447–466.

[26] Morrill, G. (1990) ‘Intensionality and boundedness’. L& P 13, pp 699–726.

[27] Morrill, G. (1992) ‘Categorial formalisation of relativisation: pied-piping, islands and extraction sites’. Report LSI–92–23–R, Universitat Politècnica de Catalunya.

[28] Morrill, G. (1994) ‘Structural facilitation and structural inhibition’. In [1].

[29] Pentus, M. (1992) ‘Equivalent types in Lambek Calculus and Linear Logic’. MIAN Prepublication LCS–92–02. To appear in JoLLI.

[30] Roorda, D. (1991) Resource logics. Proof-theoretical investigations. Ph.D. Dissertation, ILLC, Amsterdam.

[31] Routley, R. and R.K. Meyer (1972–73) ‘The semantics of entailment I’. In H.Leblanc (ed) Truth, Syntax, Modality, North-Holland, Amsterdam, pp 199– 243.

[32] Steedman, M. (1993) ‘Categorial grammar. Tutorial overview’. Lingua 90, 221-258.

[33] Venema, Y. (1993) ‘Meeting strength in substructural logics’. UU Logic Preprint. To appear in Studia Logica.

[34] Versmissen, K. (1993) ‘Categorial grammar, modalities and algebraic semantics’. Proceedings EACL93, pp 377–383.

[35] Wallen, L.A. (1990) Automated Deduction in Nonclassical Logics. MIT Press, Cambridge, London.