Structural Control ^{∗}

Natasha Kurtonina and Michael Moortgat Research Institute for Language and Speech (OTS) Trans 10, 3512 JK Utrecht {kurtonina,moortgat}@let.ruu.nl

September 8, 1995

Abstract

In this paper we study Lambek systems as grammar logics: logics for reasoning about structured linguistic resources. The structural parameters of precedence, dominance and dependency generate a cube of resource-sensitive categorial type logics. From the pure logic of residuation NL, one obtains L, NLP and LP in terms of Associativity, Commutativity, and their combination. Each of these systems has a dependency variant, where the product is split up into a left-headed and a right-headed version.

We develop a theory of systematic communication between these systems. The communication is two-way: we show how one can fully recover the structural discrimination of a weaker logic from within a system with a more liberal resource management regime, and how one can reintroduce the structural flexibility of a stronger logic within a system with a more articulate notion of structure-sensitivity.

In executing this programme we follow the standard logical agenda: the categorial formula language is enriched with extra control operators, so-called structural modalities, and on the basis of these control operators, we prove embedding theorems for the two directions of substructural communication. But our results differ from the Linear Logic style of embedding with S4-like modalities in that we realize the communication in both directions in terms of a minimal pair of structural modalities. The control devices ◇, □^{↓} used here represent the pure logic of residuation for a family of unary multiplicatives: they do not impose any restrictions on the binary accessibility relation interpreting the unary modalities, unlike the S4 operators which require a transitive and reflexive interpretation. With the more delicate control devices we can avoid the model-theoretic and prooftheoretic problems one encounters when importing the Linear Logic modalities in a linguistic setting.

1 Logics of structured resources

This paper is concerned with the issue of communication between categorial type logics of the Lambek family. Lambek calculi occupy a lively corner in the broader landscape of resource-sensitive systems of inference. We study these systems here as grammar logics. In line with the ‘Parsing as Deduction’ slogan, we present the key concept in grammatical analysis — well-formedness — in logical terms, i.e. grammatical well-formedness amounts to derivability in our grammar logic. In the grammatical application, the resources we are talking about are linguistic expressions — multidimensional form-meaning complexes, or signs as they have come to be called in current grammar formalisms. These resources are structured in a number of grammatically relevant dimensions. For the sake of concreteness, we concentrate on three types of linguistic structure of central importance: linear order, hierarchical grouping (constituency) and dependency. The structure of the linguistic resources in these dimensions plays a crucial role in determining well-formedness: one cannot generally assume that changes in the structural configuration of the resources will preserve well-formedness. In logical terms, we are interested in structure-sensitive notions of linguistic inference.

∗An earlier version of this paper appeared under the title ‘Controlling resource management’ in Deliverable R1.1.B of the Esprit BRA 6852 Dyana-2 (Dynamic Interpretation of Natural Language). The present version is to appear, with slight modifications, in Blackburn & de Rijke (eds)

Logic, Structures and Syntax. We thank Johan van Benthem and Dick Oehrle for comments. All errors are our own.

Fig 1 charts the eight logics that result from the interplay of the structural parameters of precedence, dominance and dependency. The systems lower in the cube exhibit a more fine-grained sense of structure-sensitivity; their neighbours higher up loose discrimination for one of the structural parameters we distinguish here.

[figure: NLP; LP; L; NL; DNLP; DLP; DL; DNL]

Figure 1: Resource-sensitive logics: precedence, dominance, dependency

Let us present the essentials (syntactically and semantically) of the framework we are assuming before addressing the communication problem. For a fuller treatment of multimodal categorial architecture, the reader can turn to [Moortgat 95, M & O 94, M & M 91, M & O 93, Morrill 94]. Consider the standard language of categorial type formulae F freely generated from a set of atomic formulae A: F ::= A | F/F | F • F | F\F. The most general interpretation for such a language can be given in terms of Kripke style relational structures — ternary relational structures ⟨W, R^{3}⟩ in the case of the binary connectives (cf. [Došen 92]). W here is to be understood as the set of linguistic resources (signs) and the accessibility relation R as representing linguistic composition. From a ternary frame 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}

With no restrictions on R, we obtain the pure logic of residuation known as NL.

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

And with restrictions on the interpretation of R, and corresponding structural postulates, we obtain the systems NLP, L and LP. Below we give the structural postulates of Associativity (A) and Permutation (P) and the corresponding frame conditions F (A) and F (P). Notice that the structural discrimination gets coarser as we impose more constraints on the interpretation of R. In the presence of Permutation, well-formedness is unaffected by changes in the linear order of the linguistic resources. In the presence of Associativity, different groupings of the linguistic resources into hierarchical constituent structures has no influence on derivability.

\begin{matrix}(A) & A • (B • C) ⟷ (A • B) • C \\ F (A) & (∀xyz ∈ W) ∃t.Rxyt & Rtzu ⇔ ∃v.Rvyz & Rxvu \\ (P) & A • B → B • A \\ F (P) & (∀xyz ∈ W) Rxyz ⇔ Rxzy \end{matrix}

What we have said so far concerns the upper face of the cube of Fig 1. To obtain the systems at the lower face, we split the connective • in left-headed •_{l} and right-headed •_{r}, taking into account the asymmetry between heads and dependents. It is argued in [M & M 91] that the dependency dimension should be treated as orthogonal in principle to the functor/argument asymmetry. The distinction between left-headed •_{l} and right-headed •_{r} (and their residual implications) makes the type language articulate enough to discriminate between head/complement configurations, and modifier/head or specifier/head configurations. A determiner, for example, could be typed as np/_{r}n. Such a declaration naturally accounts for the fact that determiners act semantically as functions from n-type meanings to np-type meanings, whereas in the form dimension they should be treated as dependent on the common noun they are in construction with, so that they can derive their agreement properties from the head noun.

In the Kripke models, the lower plane of Fig 1 is obtained by moving from unimodal to multimodal (in this case: bimodal) frames ⟨W, R_{l}^{3}, R_{r}^{3}⟩, with a distinct accessibility relation for each product. Again, we have the pure (bimodal) logic of residuation DNL, with an arbitrary interpretation for R_{l}^{3}, R_{r}^{3}, and its relatives DNLP, DL, DLP, obtained by imposing associativity or (dependency-preserving!) commutativity constraints on the frames. The relevant structural postulates are given below. The distinction between the left-headed and right-headed connectives is destroyed by the postulate (D).

\begin{matrix}(A_{l}) & A •_{l} (B •_{l} C) ⟷ (A •_{l} B) •_{l} C \\ (A_{r}) & A •_{r} (B •_{r} C) ⟷ (A •_{r} B) •_{r} C \\ (P_{l,r}) & A •_{l} B ⟷ B •_{r} A \\ (D) & A •_{l} B ⟷ A •_{r} B \end{matrix}

It will be clear already from the foregoing that in presenting the grammar for a given language, we will in general not be in a position to restrict ourselves to one particular type logic — we want to have access to the combined inferential capacities of the different logics, without destroying their individual characteristics. For this to be possible we need a theory of systematic communication between type systems.

The structural postulates presented above do not have the required granularity for such a theory of communication: they globally destroy structure sensitivity in one of the relevant dimensions, whereas we would like to have lexical control over resource management. Depending on the direction of communication, one can develop two perspectives on controlled resource management. On the one hand, one would like to have control devices to license limited access to a more liberal resource management regime from within a system with a higher sense of structural discrimination. On the other hand, one would like to impose constraints on resource management in systems where such constraints are lacking by default. For discussion of linguistic phenomena motivating these two types of communication, the reader can turn to the papers in [Barry & Morrill 90] where the licensing perspective was originally introduced, and to [Morrill 94] where apart from licensing of structural relaxation one can also find discussion of constraints with respect to the associativity dimension. We give an illustration for each type of control, drawing on the references just mentioned.

Licensing structural relaxation. For the licensing type of communication, consider type assignment to relative pronouns like that in the sentences below.

the book that John read

the book that John read yesterday

L ⊢ r/(s/np), np, (np\s)/np ⇒ r
L ⊬ r/(s/np), np, (np\s)/np, s\s ⇒ r
NL ⊬ (r/(s/np), (np, (np\s)/np)) ⇒ r

Suppose first we are dealing with the associative regime of L, and assign the relative pronoun the type r/(s/np), abbreviating n\n as r, i.e. the pronoun looks to its right for a relative clause body missing a noun phrase. The first example is derivable^{1} (because ‘John read np’ indeed yields s), the second is not (because the hypothetical np assumption in the subderivation ‘John read yesterday np’ is not in the required position adjacent to the verb ‘read’). We would like to refine the assignment to the relative pronoun to a type r/(s/np^{♯}), where np^{♯} is a noun phrase resource which has access to Permutation in virtue of its ·^{♯} decoration. Similarly, if we change the default regime to NL, already the first example fails on the assignment r/(s/np) with the indicated constituent bracketing: although the hypothetical np in the subcomputation ‘((John read) np)’ finds itself in the right position with respect to linear order requirements, it cannot satisfy the direct object role for ‘read’ being outside the clausal boundaries. A refined assignment r/(s/np^{♯}) here could license the marked np^{♯} a controlled access to the structural rule of Associativity which is absent in the NL default regime.

Imposing structural constraints. For the other direction of communication, we take an example from [Morrill 94] which again concerns relative clause formation, but this time in its interaction with coordination. Assume we are dealing with an associative default regime, and let the conjunction particle ‘and’ be polymorphically typed as (X\X)/X. With the instantiation X = s/np we can derive the first example. But, given Associativity and an instantiation X = s, nothing blocks the ungrammatical second example: ‘Melville wrote Moby Dick and John read np’ derives s, so that withdrawing the np hypothesis indeed gives s/np, the type required for the relative clause body.

the book that Melville wrote and John read

L ⊢ r/(s/np), np, (np\s)/np, (X\X)/X, np, (np\s)/np ⇒ r (X = s/np)

*the book that Melville wrote Moby Dick and John read

L ⊢ r/(s/np), np, (np\s)/np, np, (X\X)/X, np, (np\s)/np ⇒ r (X = s)

1The Appendix gives axiomatic and Gentzen style presentation of the logics under discussion.

To block this violation of the so-called Coordinate Structure Constraint, while allowing Across-the-Board Extraction as exemplified by our first example, we would like to refine the type assignment for the particle ‘and’ to (X\X^{♭})/X, where the intended interpretation for the marked X^{♭} now would be the following: after combining with the right and the left conjuncts, the ·^{♭} decoration makes the complete coordination freeze into an island configuration which is inaccessible to extraction under the default associative resource management regime.

Minimal structural modalities. Our task in the following pages is to give a logical implementation of the informal idea of decorating formulas with a label (·)^{♯} or (·)^{♭}, licensing extra flexibility or imposing a tighter regime for the marked formulae. The original introduction of the licensing type of communication in [Barry & Morrill 90] was inspired by the modalities ‘!,?’ of Linear Logic — unary operators which give marked formulae access to the structural rules of Contraction and Weakening, thus making it possible to recover the full power of Intuitionistic or Classical Logic from within the resource sensitive linear variants. On the proof-theoretic level, the ‘!,?’ operators have the properties of S4 modalities. It is not self-evident that S4 behaviour is appropriate for substructural systems weaker than Linear Logic — indeed [Venema 93] has criticised an S4 ‘!’ in such settings for the fact that the proof rule for ‘!’ has undesired side-effects on the meaning of other operators. On the semantic level it has been shown in [Versmissen 93] that the S4 regime is incomplete with respect to the linguistic interpretation which was originally intended for the structural modalities — a subalgebra interpretation in a general groupoid setting, cf. [Morrill 94] for discussion.

Given these model-theoretic and proof-theoretic problems with the use of Linear Logic modalities in linguistic analysis, we will explore a different route and develop an approach attuned to the specific domain of application of our grammar logics — a domain of structured linguistic resources.

[Moortgat 95] proposes an enrichment of the type language of categorial logics with unary residuated operators, interpreted in terms of a binary relation of accessibility. These operators will be the key devices in our strategy for controlled resource management. If we were talking about temporal organization, ◇ and □^{↓} could be interpreted as future possibility and past necessity, respectively. But in our grammatical application, R^{2} just like R^{3} is to be interpreted in terms of structural composition. Where a ternary configuration (xyz) ∈ R^{3} interpreting the product connective abstractly represents putting together the components y and z into a structured configuration x in the manner indicated by R^{3}, a binary configuration (xy) ∈ R^{2} interpreting the unary ◇ can be seen as the construction of the sign x out of a structural component y in terms of the building instructions referred to by R^{2}.

res(1) ◇A → B ⟺ A → □^{↓}B
V (◇A) = {x | ∃y(R^{2}xy ∧ y ∈ V (A)}
V (□^{↓}A) = {x | ∀y(R^{2}yx ⇒ y ∈ V (A)}

From the residuation laws res(1) one directly derives the monotonicity laws below and the properties of the compositions of ◇ and □^{↓}:

A → B implies ◇A → ◇B and □^{↓}A → □^{↓}B
◇□^{↓}A → A  A → □^{↓}◇A

In the Appendix, we present the sequent logic for these unary operators. It is shown in [Moortgat 95] that the Gentzen presentation is equivalent to the axiomatic presentation, and that it enjoys Cut Elimination. For our examples later on we will use decidable sequent proof search.

Semantically, the pure logic of residuation for ◇, □^{↓} does not impose any restrictions on the interpretation of R^{2}. As in the case of the binary connectives, we can add structural postulates for ◇ and corresponding frame constraints on R^{2}. With a reflexive and transitive R^{2}, one obtains an S4 system. Our objective here is to show that one can develop a systematic theory of communication, both for the licensing and for the constraining perspective, in terms of the minimal structural modalities, i.e. the pure logic of residuation for ◇, □^{↓}.

Completeness. The communication theorems to be presented in the following sections rely heavily on semantic argumentation. The cornerstone of the approach is the completeness of the logics compared, which guarantees that syntactic derivability ⊢ A → B and semantic inclusion V (A) ⊆ V (B) coincide for the classes of models we are interested in. For the F(/, •, \) fragment, [Došen 92] shows that NL is complete with respect to the class of all ternary models, and L, NLP, LP with respects to the classes of models satisfying the frame constraints for the relevant packages of structural postulates. The completeness results are obtained on the basis of a simple canonical model construction which directly accomodates bimodal dependency systems with F(/_{i}, •_{i}, \_{i}) (i ∈ {l, r}). And it is shown in [Moortgat 95] that the construction also extends unproblematically to the language enriched with ◇, □^{↓} as soon as one realizes that ◇ can be seen as a ‘truncated’ product and □^{↓} its residual implication.

Definition 1.1 Define the canonical model for mixed (2,3) frames as M = ⟨W, R^{2}, R_{i}^{3}⟩, where

W is the set of formulae F(/_{i}, •_{i}, \_{i}, ◇, □^{↓})

R_{i}^{3}(A, B, C) iff ⊢ A → B •_{i} C, R^{2}(A, B) iff ⊢ A → ◇B

A ∈ V (p) iff ⊢ A → p.

The Truth Lemma then states that, for any formula ϕ, M, A ⊧ ϕ iff ⊢ 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.

We have to check the Truth Lemma 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.

Apart from global structural postulates we will introduce in the remainder of this paper ‘modal’ versions of such postulates — versions which are relativized to the presence of ◇ control operators. The completeness results extend to these new structural postulates. Syntactically, they consist of formulas built up entirely in terms of the • operator and its truncated one-place variant ◇. This means they have the required shape for a generalized Sahlqvist-van Benthem theorem and frame completeness result which is proved in [Kurtonina 95]:

If R_{⋄} : A → B is a modal version of a structural postulate, then there exists a first order frame condition effectively obtainable from R_{⋄}, and any logic L + R_{⋄} is complete if L is complete.

Embedding theorems: the method in general. In the sections that follow, we consider pairs of logics L_{0}, L_{1} where L_{0} is a ‘southern’ neighbour of L_{1}. Let us write L◇ for a system L extended with the unary operators ◇, □^{↓} with their minimal residuation logic. For the 12 edges of the cube of Fig 1, we define embedding translations (·)^{♭} : F(L_{0}) ↦ F(L_{1}◇) which impose the structural discrimination of L_{0} in L_{1} with its more liberal resource management, and (·)^{♯} : F(L_{1}) ↦ F(L_{0}◇) which license relaxation of structure sensitivity in L_{0} in such a way that one fully recovers the flexibility of the the coarser L_{1}.

Our strategy for obtaining the embedding results is quite uniform. It will be helpful to present the recipe first in abstract terms, so that in the following sections we can supply the particular ingredients with reference to the general scheme. The embedding theorems have the format shown below. We call L the source logic, L′ the target.

L ⊢ A → B iff L′◇(+R_{⋄}) ⊢ A^{♮} → B^{♮}

For the constraining perspective, (·)^{♮} is (·)^{♭} with L = L_{0} and L′ = L_{1}. For the licensing type of embedding, (·)^{♮} is (·)^{♯} with L = L_{1} and L′ = L_{0}. The embedding translation (·)^{♮} decorates critical subformulae in the target logic with the operators ◇, □^{↓}. The translations are defined on the product • of the source logic: their action on the implicational formulas is fully determined by the residuation laws. A • configuration of the source logic is mapped to the composition of ◇ and the product of the target logic. The elementary compositions are given below (writing ∘ for the target product). They mark the product as a whole, or one of the subtypes with the ◇ control operator.

◇(− ∘ −)  ((◇−) ∘ −)  (− ∘ (◇−))

Sometimes the modal decoration in itself is enough to obtain the required structural control. We call these cases pure embeddings. In other cases realizing the embedding requires the addition of R_{⋄} — the modalized version of a structural rule package discriminating L from L′. Typically, this will be the case for communication in the licensing direction: the target logics lack an option for structural manipulation that is present in the source.

The proof of the embedding theorems comes in two parts.

(⇒) Soundness of the embedding. The (⇒) half is the easy part. Using the Lambek-style axiomatization of A.1 we obtain this direction of the embedding by a straightforward induction on the length of derivations in L.

(⇐) Completeness of the embedding. For the proofs of the (⇐) part, we reason semantically and rely on the completeness of the logics compared. To show that ⊢ A^{♮} → B^{♮} in L′◇ implies ⊢ A → B in L we proceed by contraposition. Suppose L ⊬ A → B. By completeness, there is an L model M = ⟨F, V ⟩ falsifying A → B, i.e. there is a point a such that M, a ⊧ A but M, a |̸= B. We obtain the proof for the (⇐) direction in two steps.

Model construction. From M, we construct an L′◇ model M′ = ⟨F′, V′⟩. For the valuation, we set V′(p) = V (p). For the frames, we define a mapping between the R^{3} configurations in F and corresponding mixed R^{2′}, R^{3′} configurations in F′. We make sure that the mapping reflects the properties of the translation schema, and that it takes into account the different frame conditions for F and F′.

Truth preservation lemma. We prove that for any a ∈ W ∩ W′, M, a ⊧ A iff M′, a ⊧ A^{♮}, i.e. that the construction of M′ is truth preserving.

Now, if M is a countermodel for A → B, so is M′ for A^{♮} → B^{♮}. Soundness then leads us to the conclusion that L′◇ ⊬ A^{♮} → B^{♮}.

With this proof recipe in hand, the reader is prepared to tackle the sections that follow. Recovery of structural discrimination is the subject of §2. In §3 we turn to licensing of structural relaxation. In §4 we reflect on general logical and linguistic features of the proposed architecture, signaling some open questions and directions for future research.

2 Imposing structural constraints

Let us first look at the embedding of more discriminating logics within systems with a less fine-grained sense of structure sensitivity. Modal decoration, in this case, serves to block structural manipulation that would be available by default. The section is organised as follows. In §2.1, we give a detailed treatment of a representative case for each of the structural dimensions of precedence, dominance and dependency. This covers the edges connected to the pure logic of residuation, NL. With minor adaptions the embedding translations of §2.1 can be extended to the remaining edges, with the exception of the four associative logics at the right back face of the cube. We present these generalisations in §2.2. This time we refrain from fully explicit treatment where extrapolation from §2.1 is straightforward. The remaining systems are treated in §2.3. They share associative resource management but differ in their sensitivity for linear order or dependency structure. We obtain the desired embeddings in these cases via a tactical manoeuvre which combines the composition of simple translation schemata and the reinstallment of Associativity via modally controlled structural postulates.

2.1 Simple embeddings

Prop 2.6: Commutativity NLP

L

[figure] [figure]

Prop 2.2: Associativity

NL

Prop 2.4: Dependency

DNL

Figure 2: Imposing constraints: precedence, dominance, dependency

Associativity

Consider first the pair NL versus L◇. Let us subscript the symbols for the connectives in NL with 0 and those of L with 1. The L family /_{1}, •_{1}, \_{1} has an associative resource management. We extend L with the operators ◇, □^{↓} and recover control over associativity by means of the following translation.

Definition 2.1 Translation ·^{♭} : F(NL) ↦ F(L◇) as below.

p^{♭} = p
(A •_{0} B)^{♭} = ◇(A^{♭} •_{1} B^{♭})
(A/_{0}B)^{♭} = □^{↓}A^{♭}/_{1}B^{♭}
(B\_{0}A)^{♭} = B^{♭}\_{1}□^{↓}A^{♭}

Proposition 2.2

NL ⊢ A → B iff L◇ ⊢ A^{♭} → B^{♭}

Proof. (⇒) Soundness of the embedding. For the left-to-right direction we use induction on the length of derivations in NL on the basis of the Lambekstyle axiomatization given in the Appendix, where apart from the identity axiom and Transitivity, the Residuation rules are the only rules of inference. Assume A •_{0} B → C is derived from A → C/_{0}B in NL. By inductive hypothesis, L ⊢ A^{♭} → (C/_{1}B)^{♭}, i.e. (†) A^{♭} → □^{↓}C^{♭}/_{1}B^{♭}. We have to show (‡) L ⊢ (A •_{1} B)^{♭} → C^{♭}, i.e. ◇(A^{♭} •_{1} B^{♭}) → C^{♭}. By res(2) we have from (†) A^{♭} •_{1} B^{♭} → □^{↓}C^{♭} which derives (‡) by res(1). For the other side of the residuation inferences, assume A → C/_{0}B is derived from A •_{0} B → C. By inductive hypothesis, L ⊢ (A •_{1} B^{♭}) → C^{♭}, i.e. (‡) ◇(A^{♭} •_{1} B^{♭}) → C^{♭}. We have to show L ⊢ A^{♭} → C/_{1}B^{♭}, i.e. (†) A^{♭} → □^{↓}C^{♭}/_{1}B^{♭}. By res(1) we have from (‡) A^{♭} •_{1} B^{♭} → □^{↓}C^{♭} which derives (†) by res(2). The residual pair (•_{0}, \_{0}) is treated in a fully symmetrical way. □

(⇐) Completeness of the embedding. We apply the method outlined in §1. From a falsifying model M = ⟨W, R_{0}^{3}, V ⟩ for A → B in NL we construct M′ = ⟨W′, R_{1}^{3}, R_{⋄}^{2}, V′⟩. We prove that the construction is truth preserving, so that we can conclude from Soundness that M′ falsifies A^{♭} → B^{♭} in L◇.

Model construction. Let W_{1} be a set such that W ∩ W_{1} = Ø and f : R_{0}^{3} ↦ W_{1} a bijection associating each triple (abc) ∈ R_{0}^{3} with a fresh point f((abc)) ∈ W_{1}. M′ is defined as follows:

\begin{aligned}W′ & = & W ∪ W_{1} \\ R_{1} & = & \{(a′bc) | ∃a.R_{0}abc ∧ f((abc)) = a′\} \\ R_{⋄} & = & \{(aa′) | ∃bc.R_{0}abc ∧ f((abc)) = a′\} \\ V′(p) & = & V (p) \end{aligned}

The following picture will help the reader to visualize how the model construction relates to the translation schema.

\begin{aligned}M & [figure: a; b; c] & ⇝^{f} & a [figure: a′; b; c] & M′ \\ & A •_{0} B & ⇝^{♭} & ◇(A^{♭} •_{1} B^{♭}) \end{aligned}

We have to show that M′ is an appropriate model for L, i.e. that the construction of M′ realizes the frame condition for associativity:

F (A) ∀xyzw ∈ W′(∃t(R_{1}wxt ∧ R_{1}tyz) ⟺ ∃t′(R_{1}wt′z ∧ R_{1}t′xy))

F (A) is satisfied automatically because, by the construction of M′, there are no x, y, z, w ∈ W′ that fulfill the requirements: for every triple (xyz) ∈ R_{1}^{3}, the point x is chosen fresh, which implies that no point of W′ can be both the root of one triangle and a leaf in another one.

Lemma: Truth Preservation. By induction on the complexity of A we show that for any a ∈ W

M, a ⊧ A iff M′, a ⊧ A^{♭}

We prove the biconditional for the product and for one of the residual implications.

(⇒). Suppose M, a ⊧ A•_{0}B. By the truth conditions for •_{0}, there exist b, c such that (i) R_{0}abc and (ii) M, b ⊧ A, (iii) M, c ⊧ B. By inductive hypothesis, from (ii) and (iii) we have (ii’) M′, b ⊧ A^{♭} and (iii’) M′, c ⊧ B^{♭}. By the construction of M′, we conclude from (i) that there is a fresh a′ ∈ W_{1} such that (iv) R_{⋄}aa′ and (v) R_{1}a′bc. Then, from (v) and (ii’,iii’) we have M′, a′ ⊧ A^{♭} •_{1} B^{♭} and from (iv) M′, a ⊧ ◇(A^{♭} •_{1} B^{♭}) .

(⇐). Suppose M′, a ⊧ ◇(A^{♭} •_{1} B^{♭}). From the truth conditions for •_{1}, ◇, we know there are x, y, z ∈ W′ such that (i) R_{⋄}ax, (ii) R_{1}xyz and (iii) M′, y ⊧ A^{♭} and M′, z ⊧ B^{♭}. In he construction of M′ the function f is a bijection, so that we can conclude that the configuration (i,ii) has a unique preimage, namely (iv) R_{0}ayz. By inductive hypothesis, we have from (iii) M, y ⊧ A, and M, z ⊧ B, which then with (iv) gives M, a ⊧ A •_{0} B.

(⇒). Suppose (i) M, a ⊧ A\_{0}B. We have to show M′, a ⊧ A^{♭}\_{1}□^{↓}B^{♭}. Suppose we have (ii) R_{1}yxa such that M′, x ⊧ A^{♭}. It remains to be shown that M′, y ⊧ □^{↓}B^{♭}. Suppose we have (iii) R_{⋄}zy. It remains to be shown that M′, z ⊧ B^{♭}. The configuration (ii,iii) has a unique preimage by the construction of M′, namely R_{0}zxa. By inductive hypothesis from (ii) we have M, x ⊧ A which together with (i) leads to M, z ⊧ B and, again by inductive hypothesis M′, z ⊧ B^{♭}, as required.

(⇐). Suppose (i) M′, a ⊧ A^{♭}\_{1}□^{↓}B^{♭}. We have to show M, a ⊧ A\_{0}B. Suppose we have (ii) R_{0}cba such that M, b ⊧ A. To be shown is whether M, c ⊧ B. By the model construction and inductive hypothesis we have R_{⋄}cc′, R_{1}c′ba and M′, b ⊧ A^{♭}. Hence by (i) M′, c ⊧ □^{↓}B^{♭} and therefore M′, c ⊧ B^{♭}. By inductive hypothesis this leads to M, c ⊧ B as required. □

Illustration: islands. For a concrete linguistic illustration, we return to the Coordinate Structure Constraint violations of §1. The translation schema of Def 2.1 was originally proposed by [Morrill 92], who conjectured on the basis of this schema an embedding of NL into L extended with a pair of unary ‘bracket’ operators closely related to ◇, □^{↓}. Whether the conjecture holds for the bracket operators remains open. But it is easy to recast Morrill’s analysis of island constraints in terms of ◇, □^{↓}. We saw above that on an assignment (X\X)/X to the particle ‘and’, both the grammatical and the illformed examples are L derivable. Within L◇, we can refine the assignment to (X\□^{↓}X)/X. The relevant sequent goals now assume the following form (omitting the associative binary structural punctuation, but keeping the crucial (·)^{⋄}):

(†) the book that Melville wrote and John read
L ⊢ r/(s/np), (np, (np\s)/np, (X\□^{↓}X)/X, np, (np\s)/np)^{⋄} ⇒ r (X = s/np)
(‡) *the book that Melville wrote Moby Dick and John read
L◇ ⊬ r/(s/np), (np, (np\s)/np, np, (X\□^{↓}X)/X, np, (np\s)/np)^{⋄} ⇒ r (X = s)

The (X\□^{↓}X)/X assignment allows the particle ‘and’ to combine with the left and right conjuncts in the associative mode. The resulting coordinate structure is of type □^{↓}X. To eliminate the □^{↓} connective, we have to close off the coordinate structure with ◇ (or the corresponding structural operator (·)^{⋄} in the Gentzen presentation)

— recall that ◇□^{↓}X → X. The Accross-the-Board case of extraction (†) works out fine, the island violation (‡) fails because the hypothetical gap np assumption finds itself outside the scope of the (·)^{⋄} operator.

Dependency

For a second straightforward application of the method, we consider the dependecy calculus DNL of [M & M 91] and show how it can be emdedded in NL. Recall that DNL is the pure logic of residuation for a bimodal system with asymmetric products •_{l}, •_{r} for left-headed and right-headed composition respectively. The distinction between left- and right-headed products can be recovered within NL◇, where we have the unary residuated pair ◇, □^{↓} next to a symmetric product • and its implications. For the embedding translation (·)^{♭}, we label the head subtype of a product with ◇. The residuation laws then determine the modal decoration of the implications.

Definition 2.3 The embedding translation (·)^{♭} : F(DNL) ↦ F(NL◇) is defined as follows.

p^{♭} = p
(A •_{l} B)^{♭} = ◇A^{♭} • B^{♭} (A •_{r} B)^{♭} = A^{♭} • ◇B^{♭}
(A/_{l}B)^{♭} = □^{↓}(A^{♭}/B^{♭}) (A/_{r}B)^{♭} = A^{♭}/◇B^{♭}
(B\_{l}A)^{♭} = ◇B^{♭}\A^{♭}  (B\_{r}A)^{♭} = □^{↓}(B^{♭}\A^{♭})

Proposition 2.4

DNL ⊢ A → B iff NL◇ ⊢ A^{♭} → B^{♭}

Proof. (⇒) Soundness of the embedding. The soundness half is proved by induction on the length of the derivation of A → B in DNL. We trace the residuation inferences under the translation mapping for the pair (•_{l}, /_{l}). The remaining cases are completely parallel.

DNL \begin{matrix}A •_{l} B → C \\ A → C/_{l}B \end{matrix} ⇝ \begin{matrix}(A •_{l} B)^{♭} → C^{♭} \\ A^{♭} → (C/_{l}B)^{♭} \end{matrix} ⇝ \begin{matrix}◇A^{♭} • B^{♭} → C^{♭} \\ ◇A^{♭} → C^{♭}/B^{♭} \\ A^{♭} → □^{↓}(C^{♭}/B^{♭}) \end{matrix} NL

(⇐) Completeness of the embedding. Suppose DNL ⊬ A → B. By completeness, there is a model M = ⟨W, R_{l}^{3}, R_{r}^{3}, V ⟩ falsifying A → B. From M, we want to construct a model M′ = ⟨W′, R_{•}^{3}, R_{⋄}^{2}, V′⟩ which falsifies A^{♭} → B^{♭}. Then from soundness we will be able to conclude NL◇ ⊬ A^{♭} → B^{♭}.

Model construction. Let W, W_{l}, W_{r} be disjoint sets and f : R_{l}^{3} ↦ W_{l} and g : R_{r}^{3} ↦ W_{r} bijective functions. M′ is defined as follows:

W′ = W ∪ W_{l} ∪ W_{r}
R_{•} = {(ab′c) | ∃b.R_{l}abc ∧ f((abc)) = b′} ∪
{(abc′) | ∃c.R_{r}abc ∧ g((abc)) = c′}
R_{⋄} = {(c′c) | ∃ab.R_{r}abc ∧ g((abc)) = c′} ∪
{(b′b) | ∃ac.R_{l}abc ∧ f((abc)) = b′}
V′(p) = V (p)

We comment on the frames. For every triple (abc) ∈ R_{l}^{3}, we introduce a fresh b′ and put the worlds a, b, b′, c ∈ W′, (b′b) ∈ R_{⋄}^{2} and (ab′c) ∈ R_{•}^{3}. Similarly, for every triple (abc) ∈ R_{r}^{3}, we introduce a fresh c′ and put the worlds a, b, c, c′ ∈ W′, (c′c) ∈ R_{⋄}^{2} and (abc′) ∈ R_{•}^{3}. In a picture (with dotted lines for the dependent daughter for R_{l}, R_{r}):

\begin{matrix}M  [figure: a; b; c] & ⇝ & [figure: a; b′ b; c]  M′ \\ M  [figure: a; b; c] & ⇝ & [figure: a; b; c′ c]  M′ \end{matrix}

Lemma: truth preservation. By induction on the complexity of A, we show that for any a ∈ W, M, a ⊧ A iff M′, a ⊧ A^{♭}. We prove the biconditional for the left-headed product. The other connectives are handled in a similar way.

(⇒). Suppose M, a ⊧ A•_{l}B. By the truth conditions for •_{l}, there exist b, c such that (i) R_{l}abc and (ii) M, b ⊧ A, (iii) M, c ⊧ B. By the construction of M′, we conclude from (i) that there is a fresh b′ ∈ W′ such that (iv) R_{⋄}^{2}b′b and (v) R_{•}^{3}ab′c. By inductive hypothesis, from (ii) and (iii) we have M′, b ⊧ A^{♭} and M′, c ⊧ B^{♭}. Then, from (iv) we have M′, b′ ⊧ ◇A^{♭} and from (v), M′, a ⊧ ◇A^{♭} • B^{♭}.

(⇐). Suppose M′, a ⊧ ◇A^{♭} • B^{♭}. From the truth conditions for •, ◇, we know there are d′, d, e ∈ W′ such that (i) R_{⋄}^{2}d′d, (ii) R_{•}^{3}ad′e and (iii) M′, d ⊧ A^{♭} and M′, e ⊧ B^{♭}. From the construction of M′, we may conclude that d′ = b′, d = b, e = c, since every triple (abc) ∈ R_{l}^{3} is keyed to a fresh world b′ ∈ W′. So we actually have (i’) R_{⋄}^{2}b′b, (ii’) R_{•}^{3}ab′c and (iii’) M′, b ⊧ A^{♭} and M′, c ⊧ B^{♭}. (i’) and (ii’) imply R_{l}^{3}abc. By inductive hypothesis, we have from (iii’) M, b ⊧ A, and M, c ⊧ B. But then M, a ⊧ A •_{l} B. □

Illustration. Below two instances of lifting in DNL. The left one is derivable, the right one is not.

\begin{matrix}\begin{matrix}\begin{matrix}A^{♭} ⇒ A^{♭} \\ (A^{♭})^{⋄} ⇒ ◇A^{♭} \end{matrix} ◇R & B^{♭} ⇒ B^{♭} \\ ((A^{♭})^{⋄}, ◇A^{♭}\B^{♭})^{•} ⇒ B^{♭} \end{matrix} & \L \\ (A^{♭})^{⋄} ⇒ B^{♭}/(◇A^{♭}\B^{♭}) \end{matrix} ; /R ; A^{♭} ⇒ □^{↓}(B^{♭}/(◇A^{♭}\B^{♭})) ; □^{↓}R ; A ⇒ B/_{l}(A\_{l}B) ; ·^{♭}  \begin{matrix}\begin{matrix}? \\ ((A^{♭})^{⋄}, □^{↓}(A^{♭}\B^{♭}))^{•} ⇒ B^{♭} \end{matrix} ; (A^{♭})^{⋄} ⇒ B^{♭}/□^{↓}(A^{♭}\B^{♭}) & /R \\ A^{♭} ⇒ □^{↓}(B^{♭}/□^{↓}(A^{♭}\B^{♭})) \end{matrix} ; □^{↓}R ; A ⇒ B/_{l}(A\_{r}B) ; ·^{♭}

Commutativity

We can exploit the strategy for modal embedding of the dependency calculus to recover control over Permutation. Here we look at the pure case: the embedding of NL into NLP◇. In §2.2 we will generalize the result to the other cases where Permutation is involved. For the embedding, choose one of the (asymmetric) dependency product translations for • in NL. Permutation in NLP spoils the asymmetry of the product. Whereas one could read the ◇ label in the cases of Def2.3 as a head marker, in the present case ◇ functions as a marker of the first daughter.

Definition 2.5 The embedding translation ·^{♭} : F(NL) ↦ F(NLP◇) is defined as follows.

p^{♭} = p
(A • B)^{♭} = ◇A^{♭} ⊗ B^{♭}
(A/B)^{♭} = □^{↓}(A^{♭}∘−B^{♭})
(B\A)^{♭} = ◇B^{♭}−∘A^{♭}

Proposition 2.6

NL ⊢ A → B iff NLP◇ ⊢ A^{♭} → B^{♭}

Proof sketch. The (⇒) part again is proved straightforwardly by induction on the length of the derivation of A → B in NL. We leave this to the reader. For the (⇐) direction, suppose NL ⊬ A → B. By completeness, there is a model M = ⟨W, R_{•}^{3}, V ⟩ falsifying A → B. From M, we now have to construct a commutative model M′ = ⟨W′, R_{⊗}^{3}, R_{⋄}^{2}, V′⟩ which falsifies A^{♭} → B^{♭}. From soundness we will conclude that NLP◇ ⊬ A^{♭} → B^{♭}.

The construction of the frame for M′ in this case proceeds as follows. For every triple (abc) ∈ R_{•}^{3}, we introduce a fresh b′ and put the worlds a, b, b′, c ∈ W′, (b′b) ∈ R_{⋄}^{2} and both (ab′c), (acb′) ∈ R_{⊗}^{3}. The construction makes the frame for M′ commutative. But because every commutative triple (ab′c) depends on a fresh b′ ∈ W′ − W, the commutativity of M′ has no influence on M. For the valuation, we set V′(p) = V (p). Now for any a ∈ W ∩ W′, we can show by induction on the complexity of A that M, a ⊧ A iff M′, a ⊧ A^{♭} which then leads to the proof of the main proposition in the usual way.

Illustration. Below first a theorem of NL, followed by a non-theorem. We compare their image under ·^{♭} in NLP◇. And we notice that the second example is derivable in NLP.

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}B^{♭} ⇒ B^{♭} & A^{♭} ⇒ A^{♭} \\ (A^{♭}∘−B^{♭}, B^{♭})^{⊗} ⇒ A^{♭} \end{matrix} & ∘−L \\ ((□^{↓}(A^{♭}∘−B^{♭}))^{⋄}, B^{♭})^{⊗} ⇒ A^{♭} \end{matrix} ; □^{↓}L ; (□^{↓}(A^{♭}∘−B^{♭}))^{⋄} ⇒ A^{♭}∘−B^{♭} ; ∘−R ; □^{↓}(A^{♭}∘−B^{♭}) ⇒ □^{↓}(A^{♭}∘−B^{♭}) ; □^{↓}R ; (□^{↓}(A^{♭}∘−B^{♭}))^{⋄} ⇒ ◇□^{↓}(A^{♭}∘−B^{♭}) ; ◇R & A^{♭} ⇒ A^{♭} \\ ((□^{↓}(A^{♭}∘−B^{♭}))^{⋄}, ◇□^{↓}(A^{♭}∘−B^{♭})−∘A^{♭})^{⊗} ⇒ A^{♭} \end{matrix} & −∘L \\ (□^{↓}(A^{♭}∘−B^{♭}))^{⋄} ⇒ A^{♭}∘−(◇□^{↓}(A^{♭}∘−B^{♭})−∘A^{♭}) \end{matrix} ; ∘−R ; □^{↓}(A^{♭}∘−B^{♭}) ⇒ □^{↓}(A^{♭}∘−(◇□^{↓}(A^{♭}∘−B^{♭})−∘A^{♭})) ; □^{↓}R ; NL ⊢ A/B ⇒ A/((A/B)\A) ; ·^{♭}

\begin{matrix}\begin{matrix}? \\ ((□^{↓}(A^{♭}∘−B^{♭}))^{⋄}, □^{↓}(A^{♭}∘−(◇B^{♭}−∘A^{♭})))^{⊗} ⇒ A^{♭} \end{matrix} ; (□^{↓}(A^{♭}∘−B^{♭}))^{⋄} ⇒ A^{♭}∘−(□^{↓}(A^{♭}∘−(◇B^{♭}−∘A^{♭})) & ∘−R \\ □^{↓}(A^{♭}∘−B^{♭}) ⇒ □^{↓}(A^{♭}∘−(□^{↓}(A^{♭}∘−(◇B^{♭}−∘A^{♭}))) \end{matrix} ; □^{↓}R ; NL ⊬ A/B ⇒ A/(A/(B\A)) ; ·^{♭}

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}B ⇒ B & A ⇒ A \\ (A∘−B, B)^{⊗} ⇒ A \end{matrix} & ∘−L \\ (B, A∘−B)^{⊗} ⇒ A \end{matrix} ; P ; A∘−B ⇒ B−∘A ; −∘R & A ⇒ A \\ (A∘−(B−∘A), A∘−B)^{⊗} ⇒ A \end{matrix} & ∘−L \\ (A∘−B, A∘−(B−∘A))^{⊗} ⇒ A \end{matrix} ; P ; NLP ⊢ A∘−B ⇒ A∘−(A∘−(B−∘A)) ; ∘−R

2.2 Generalisations

The results of the previous section can be extended with minor modifications to the five edges that remain when we keep the Associativity face for §2.3.

What we have done in Prop 2.4 for the pair DNL versus NL◇ can be adapted straightforwardly to the commutative pair DNLP versus NLP◇. Recall that in DNLP, the dependency products satisfy head-preserving commutativity (P_{l,r}), whereas in NLP we have simple commutativity (P).

\begin{matrix}P_{l,r} : A ⊗_{l} B ⟷ B ⊗_{r} A \\ P : A ⊗ B → B ⊗ A \end{matrix}

Accomodating the commutative products, the embedding translation is that of Prop 2.4: ◇ marks the head subtype.

Definition 2.7 Translation (·)^{♭} : F(DNLP) ↦ F(NLP◇):

p^{♭} = p
(A ⊗_{l} B)^{♭} = ◇A^{♭} ⊗ B^{♭}  (A ⊗_{r} B)^{♭} = A^{♭} ⊗ ◇B^{♭}
(A∘−_{l}B)^{♭} = □^{↓}(A^{♭}∘−B^{♭}) (A∘−_{r}B)^{♭} = A^{♭}∘−◇B^{♭}
(B−∘_{l}A)^{♭} = ◇B^{♭}−∘A^{♭}  (B−∘_{r}A)^{♭} = □^{↓}(B^{♭}−∘A^{♭})

Proposition 2.8

DNLP ⊢ A → B iff NLP◇ ⊢ A^{♭} → B^{♭}

For the proof of the (⇐) direction, we combine the method of construction of Prop 2.4 with that of Prop 2.6. For a configuration R_{l}^{⊗}abc in M, we take fresh b′ and put the configurations R_{⋄}b′b, R_{⊗}ab′c, R_{⊗}acb′ in M′. Similarly, for a configuration R_{r}^{⊗}abc in M, we take fresh c′ and put the configurations R_{⋄}c′c, R_{⊗}abc′, R_{⊗}ac′b in M′. The commutativity property of ⊗ is thus realized by the construction.

\begin{matrix}M [figure: a; b; c] ⇝ [figure: a; b′ b; c] + [figure: a; c; b′ b] M′ \\ M [figure: a; b; c] ⇝ [figure: a; b; c′ c] + [figure: a; c′ c; b] M′ \end{matrix}

Let us check the truth preservation lemma. This time a configuration (⋆) in M′ does not have a unique pre-image: it can come from R_{l}^{⊗}xyz or R_{r}^{⊗}xzy. But because of head-preserving commutativity (DP), these are both in M.

(⋆) [figure: x; z; y′ y]

Similarly, the embedding construction presented in Prop 2.6 for the pair NL versus NLP◇ can be generalized directly to the related pair DNL versus DNLP◇. This time, we want the embedding translation to block the structural postulate of head-preserving commutativity in DNLP. The translation below invalidates the postulate by uniformly decorating with ◇, say, the left subtype of a product.

Definition 2.9 Define (·)^{♭} : F(DNL) ↦ F(DNLP◇) as follows.

p^{♭} = p
(A •_{l} B)^{♭} = ◇A^{♭} ⊗_{l} B^{♭} (A •_{r} B)^{♭} = ◇A^{♭} ⊗_{r} B^{♭}
(A/_{l}B)^{♭} = □^{↓}(A^{♭}∘−_{l}B^{♭}) (A/_{r}B)^{♭} = □^{↓}(A^{♭}∘−_{r}B^{♭})
(B\_{l}A)^{♭} = ◇B^{♭}−∘_{l}A^{♭} (B\_{r}A)^{♭} = ◇B^{♭}−∘_{r}A^{♭}

We then have the following proposition. The proof is entirely parallel to that of Prop 2.6 before. Proposition 2.10

DNL ⊢ A → B iff DNLP◇ ⊢ A^{♭} → B^{♭}

The method of Prop 2.2 generalizes to the following cases with some simple changes.

Definition 2.11 Translation (·)^{♭} : F(NLP) ↦ F(LP◇) as below.

p^{♭} = p
(A ⊗ B)^{♭} = ◇(A^{♭} ⊗ B^{♭})
(A∘−B)^{♭} = □^{↓}A^{♭}∘−B^{♭}
(B−∘A)^{♭} = B^{♭}−∘□^{↓}A^{♭}

Proposition 2.12

NLP ⊢ A → B iff LP◇ ⊢ A^{♭} → B^{♭}

The only difference with Prop 2.2 is that the product in input and target logic are commutative. Commutativity is realized automatically by the construction of M′. Proposition 2.13

DNL ⊢ A → B iff DL◇ ⊢ A^{♭} → B^{♭}

Proposition 2.14

DNLP ⊢ A → B iff DLP◇ ⊢ A^{♭} → B^{♭}

2.3 Composed translations

The remaining cases concern the right back face of the cube, where we find the systems DL, L, LP, and DLP. These logics share associative resource management, but they differ with respect to one of the remaining structural parameters — sensitivity for linear order (L versus LP, DL versus DLP) or for dependency structure (DL versus L, and DLP versus LP). We already know how to handle each of the structural dimensions individually. We use this knowledge to obtain the embeddings for systems with shared Associativity. Our strategy has two components. First we neutralize direct appeal to Associativity by taking the composition of the translation schema blocking Associativity with the schema responsible for control in the structural dimension which discriminates between the source and target logics. This first move does not embed the source logic, but its non-associative neighbour. The second move then is to reinstall associativity in terms of ◇ modally controlled versions of the Associativity postulates.

Associative dependency calculus. We work out the ‘rear attack’ manoeuvre first for the pair DL versus L. In DNL we have no restrictions on the interpretation of •_{l}, •_{r}. In DL we assume •_{l}, •_{r} are interpreted on (bimodal) associative frames, and we have structural associativity postulates A(l), A(r) on top of the pure logic of residuation for •_{l}, •_{r}. In L we cannot discriminate between •_{l} and •_{r} — there is just one • operator, which shares the associative resource management with its dependency variants. The objective of the embedding is to recover the distinction between left- and right-headed structures in a system which has only one product connective.

\begin{matrix}A(l) : (A •_{l} B) •_{l} C ⟷ A •_{l} (B •_{l} C) \\ A(r) : A •_{r} (B •_{r} C) ⟷ (A •_{r} B) •_{r} C \end{matrix}

For the embedding translation, we compose the mappings of Def 2.3 embedding DNL into NL and Def 2.1 embedding NL into L.

Definition 2.15

p^{♭} = p
(A •_{l} B)^{♭} = ◇(◇A^{♭} • B^{♭}) (A •_{r} B)^{♭} = ◇(A^{♭} • ◇B^{♭})
(A/_{l}B)^{♭} = □^{↓}(□^{↓}A^{♭}/B^{♭}) (A/_{r}B)^{♭} = □^{↓}A^{♭}/◇B^{♭}
(B\_{l}A)^{♭} = ◇B^{♭}\□^{↓}A^{♭} (B\_{r}A)^{♭} = □^{↓}(B^{♭}\□^{↓}A^{♭})

From the proof of the embedding of NL into L we know that ◇ neutralizes the effects of the associativity of • in the target logic L: the frame condition for Associativity is satisfied vacuously. To realize the desired embedding of DL into L, we reinstall modal versions of the associativity postulates.

\begin{matrix}A(l)^{⋄} : ◇(◇◇(◇A • B) • C ⟷ ◇(◇A • ◇(◇B • C)) \\ A(r)^{⋄} : ◇(A • ◇◇(B • ◇C)) ⟷ ◇(◇(A • ◇B) • ◇C) \end{matrix}

Figure 3 is a graphical illustration of the interplay between the composed translation schema and the modal structural postulate. f is the translation schema (·)^{♭} of Def 2.1, g that of Def 2.3.

Modalized structural postulates: frame completeness. The modalized structural postulates A(l, r)^{⋄} introduce a new element in the discussion. Semantically, these postulates require frame constraints correlating the binary and ternary relations of structural composition. Fortunately we know, from the generalized Sahlqvistvan Benthem Theorem and frame completeness result discussed in §1, that from A(l, r)^{⋄} we can effectively obtain the relevant first order frame conditions, and that completeness of L◇ extends to the system augmented with A(l, r)^{⋄}. We check

[figure: NL; L; h = f ∘ g, A(l, r)^{⋄}; DNL; g; f; A(l, r)^{⋄}; DL]

Figure 3: Rear Attack Embedding DL into L.

completeness for A(l)^{⋄} here as an illustration — the situation for A(r)^{⋄} is entirely similar. Fig 4 gives the frame condition for A(l)^{⋄}.

The models for L◇ are structures ⟨W, R_{⋄}^{2}, R_{•}^{3}, V ⟩. Now consider (⇒) in Figure 4 below. Given the canonical model construction of Def 1.1 the following are derivable by the definition of R_{⋄}^{2}, R_{•}^{3}:

\begin{matrix}a → ◇b, & e → ◇f, \\ b → c • d, & f → g • h, \\ c → ◇e, & g → ◇i. \end{matrix}

From these we can conclude ⊢ a → ◇(◇◇(◇i • h) • d)), i.e. a ∈ V (◇(◇◇(◇i • h) • d))), given the definition of the canonical valuation (⋆). For (‡) we have to find b′, c′, d′, e′, f′ such that

\begin{matrix}a → ◇b′, & d′ → ◇e′, \\ b′ → c′ • d′, & e′ → f′ • d, \\ c′ → ◇i, & f′ → ◇h. \end{matrix}

Let us put

f′ = ◇h,
e′ = f′ • d = ◇h • d,
d′ = ◇e′ = ◇(◇h • d),
c′ = ◇i,
b′ = c′ • d′ = ◇i • ◇(◇h • d).

Together they imply ⊢ a → ◇(◇i • ◇(◇h • d)), i.e. a ∈ V (◇(◇i • ◇(◇h • d))) can be shown to follow from (⋆). Similarly for the other direction.

Now for the embedding theorem.

Proposition 2.16

DL ⊢ A → B iff L◇ + A(l, r)^{⋄} ⊢ A^{♭} → B^{♭}

Model construction. Suppose DL ⊬ A → B. Then there is a model M = ⟨W, R_{l}, R_{r}, V ⟩ where A → B fails. From M we construct M′ as follows. For every triple (abc) ∈ R_{l} we take fresh a′, b′ and put (aa′) ∈ R_{⋄}, (a′b′c) ∈ R_{•}, (b′b) ∈ R_{⋄}.

(†)  a [figure: b; c; e; f; gi; h; d] ⟺  a [figure: b′; c′i; d′; e′; f′ h; d]  (‡)

F (A(l)^{⋄}) : ∃bcefg(R_{⋄}ab ∧ R_{•}bcd ∧ R_{⋄}ce ∧ R_{⋄}ef ∧ R_{•}fgh ∧ R_{⋄}gi) ⟺ ∃b′c′d′e′f′(R_{⋄}ab′ ∧ R_{•}b′c′d′ ∧ R_{⋄}c′i ∧ R_{⋄}d′e′ ∧ R_{•}e′f′d ∧ R_{⋄}f′h)

Figure 4: Frame condition for A(l)^{⋄}

Similarly, for every triple (abc) ∈ R_{r} we take fresh a′, c′ and put (aa′) ∈ R_{⋄}, (a′bc′) ∈ R_{•}, (c′c) ∈ R_{⋄}.

We have to check whether M′ is an appropriate model for L◇ + A(l, r)_{⋄}, specifically, whether the frame condition of Fig 4 is satisfied. Suppose (‡) holds, and let us check whether (†). Note that a configuration R_{⋄}ab′, R_{•}b′c′d′, R_{⋄}c′i can only hold in M′ if in M we had R_{l}aid′ (⋆). And a configuration R_{⋄}d′e′, R_{•}e′f′d, R_{⋄}f′h can be in M′ only if in M we had R_{l}d′hd (⋆⋆). The frame for M is associative. Therefore, from (⋆, ⋆⋆) we can conclude M also contains a configuration R_{l}aed, R_{l}eih for some e ∈ W. Applying the M′ construction to that configuration we obtain (†). Similarly for the other direction.

From here on, the proof of Prop 2.16 follows the established path.

Generalisation. The rear attack strategy can be generalized to the remaining edges. Below we simply state the embedding theorems with the relevant composed translations and modal structural postulates. We give the salient ingredients for the construction of M′, leaving the elaboration as an exercise to the reader.

Consider first embedding of L into LP. The discriminating structural parameter is Commutativity. For the translation schema, we compose the translations of Def 2.11 and Def 2.5. Associativity is reinstalled in terms of the structural postulate A_{⊗}^{⋄}.

A_{⊗}^{⋄} : ◇(◇◇(◇A ⊗ B) ⊗ C ⟷ ◇(◇A ⊗ ◇(◇B ⊗ C))

Definition 2.17 Embedding translation (·)^{♭} : F(L) ↦ F(LP◇).

p^{♭} = p
(A • B)^{♭} = ◇(◇A^{♭} ⊗ B^{♭})
(A/B)^{♭} = □^{↓}(□^{↓}A^{♭}∘−B^{♭})
(B\A)^{♭} = ◇B^{♭}−∘□^{↓}A^{♭}

Proposition 2.18

L ⊢ A → B iff LP◇ + A_{⊗}^{⋄} ⊢ A^{♭} → B^{♭}

Semantically, the commutativity of R_{⊗} is realized via the construction of M′, as in the case of Prop 2.6:

M [figure: a; b; c] ⇝  a [figure: a′; b′ b; c] +  a [figure: a′; c; b′ b] M′

For the pair DL versus DLP, again Commutativity is the discriminating structural parameter, but now in a bimodal setting. We compose the translations for the embedding of DNLP into DLP and DNL into DNLP The structural postulates A_{⊗_{l}}^{⋄} and A_{⊗_{r}}^{⋄} are the dependency variants of A_{⊗}^{⋄} above.

\begin{matrix}A_{⊗_{l}}^{⋄} : ◇(◇◇(◇A ⊗_{l} B) ⊗_{l} C ⟷ ◇(◇A ⊗_{l} ◇(◇B ⊗_{l} C)) \\ A_{⊗_{r}}^{⋄} : ◇(◇◇(◇A ⊗_{r} B) ⊗_{r} C ⟷ ◇(◇A ⊗_{r} ◇(◇B ⊗_{r} C)) \end{matrix}

Definition 2.19 Embedding translation (·)^{♭} : F(DL) ↦ F(DLP◇).

p^{♭} = p
(A •_{l} B)^{♭} = ◇(◇A^{♭} ⊗_{l} B^{♭}) (A •_{r} B)^{♭} = ◇(◇A^{♭} ⊗_{r} B^{♭})
(A/_{l}B)^{♭} = □^{↓}(□^{↓}A^{♭}∘−_{l}B^{♭}) (A/_{r}B)^{♭} = □^{↓}(□^{↓}A^{♭}∘−_{r}B^{♭})
(B\_{l}A)^{♭} = ◇B^{♭}−∘_{l}□^{↓}A^{♭} (B\_{r}A)^{♭} = ◇B^{♭}−∘_{r}□^{↓}A^{♭}

Proposition 2.20

DL ⊢ A → B iff DLP◇ + (A_{⊗_{l}}^{⋄}, A_{⊗_{r}}^{⋄}) ⊢ A^{♭} → B^{♭}

Finally, for the pair DLP versus LP, the objective of the embedding is to recapture the dependency distinctions. We compose the translations of Def 2.11 and Def 2.7. The modal structural postulates A(l, r)_{⊗}^{⋄} are obtained from A(l, r)^{⋄} by replacing • by ⊗.

Definition 2.21 Embedding translation ·^{♭} : F(DLP) ↦ F(LP◇).

p^{♭} = p
(A ⊗_{l} B)^{♭} = ◇(◇A^{♭} ⊗ B^{♭}) (A ⊗_{r} B)^{♭} = ◇(A^{♭} ⊗ ◇B^{♭})
(A∘−_{l}B)^{♭} = □^{↓}(□^{↓}A^{♭}∘−B^{♭}) (A∘−_{r}B)^{♭} = □^{↓}A^{♭}∘−◇B^{♭}
(B−∘_{l}A)^{♭} = ◇B^{♭}−∘□^{↓}A^{♭}  (B−∘_{r}A)^{♭} = □^{↓}(B^{♭}−∘□^{↓}A^{♭})

Proposition 2.22

DLP ⊢ A → B iff LP◇ + A(l, r)_{⊗}^{⋄} ⊢ A^{♭} → B^{♭}

2.4 Constraining embeddings: summary

We have completed the tour of the landscape and shown that the connectives ◇, □^{↓} can systematically reintroduce structural discrimination in logics where on the level of the binary multiplicatives such discrimination is destroyed by global structural postulates. In Fig 5 we label the edges of the cube with the numbers of the embedding theorems.

[figure: 2.8; NLP; 2.12; LP; 2.18; L; 2.4; 2.2; 2.20; 2.6; 2.14; NL; 2.10; DNLP; 2.22; DLP; 2.16; 2.13; DL; DNL]

Figure 5: Embedding translations: recovering resource control

3 Licensing structural relaxation

In the present section we shift the perspective: instead of using modal decorations to block structural options for resource management, we now take the more discriminating logic as the starting point and use the modal operators to recover the flexibility of a neighbouring logic with a more liberal resource management regime from within a system with a more rigid notion of structure-sensitivity.

Licensing of structural relaxation has traditionally been addressed (both in logic [Došen 92] and in linguistics [Morrill 94]) in terms of a single universal □ modality with S4 type resource management. Here we stick to the minimalistic principles set out at the beginning of this paper, and realize also the licensing embeddings in terms of the pure logic of residuation for the pair ◇, □^{↓} plus modally controlled structural postulates. In §3.1 we present an external strategy for modal decoration: in the scope of the ◇ operator, products of the more discriminating logics gain access to structural rules that are inaccessible in the non-modal part of the logic. In §3.2 we develop a complementary strategy for internal modal decoration, where modal versions of the structural rules are accessible provided one or all of the immediate substructures are labelled with ◇. We present linguistic considerations that will affect the choice for the external or internal approach.

3.1 Modal labelling: external perspective

Licensing structural relaxation is simpler than recovering structural control: the target logics for the embeddings in this section lack an option for structural manipulation which can be reinstalled straightforwardly in terms of a modal version of the relevant structural postulate. We do not have to design specific translation strategies for the individual pairs of logics, but can do with one general translation schema.

Definition 3.1 General translation schema (·)^{♯} : F(L_{1}) ↦ F(L_{0}◇) embedding a stronger logic L_{1} into a weaker logic L_{0} extended with ◇, □^{↓}.

p^{♯} = p
(A •_{1} B)^{♯} = ◇(A^{♯} •_{0} B^{♯})
(A/_{1}B)^{♯} = □^{↓}A^{♯}/_{0}B^{♯}
(B\_{1}A)^{♯} = B^{♯}\_{0}□^{↓}A^{♯}

The embedding theorems we are interested in now have the general format shown below, where R_{⋄} is (a package of) the modal translation(s) A^{♯} → B^{♯} of the structural rule(s) A → B which differentiate(s) L_{1} from L_{0}.

L_{1} ⊢ A → B iff L_{0}◇ + R_{⋄} ⊢ A^{♯} → B^{♯}

We look at the dimensions of dependency, precedence and dominance in general terms first, discussing the relevant aspects of the model construction. Then we comment on individual embedding theorems.

Relaxation of dependency sensitivity. For a start let us look at a pair of logics L_{0},L_{1}, where L_{0} makes a dependency distinction between a left-dominant and a right-dominant product, whereas L_{1} cannot discriminate these two. There is two ways of setting up the coarser logic L_{1}. Either we present L_{1} as a bimodal system where the distinction between right-dominant •_{r} and left-dominant •_{l} collapses as a result of the structural postulate (D).

L_{1} : A •_{r} B ⟷ A •_{l} B (D)

Or we have a unimodal presentation for L_{1} and pick an arbitrary choice of the dependency operators for the embedding translation. We take the second option here, and realize the embedding translation as indicated below.

p^{♯} = p
(A • B)^{♯} = ◇(A^{♯} •_{r} B^{♯})
(A/B)^{♯} = □^{↓}A^{♯}/_{r}B^{♯}
(B\A)^{♯} = B^{♯}\_{r}□^{↓}A^{♯}

Relaxation of dependency sensitivity is obtained by means of a modally controlled version of (D). Corresponding to the structural postulate (D_{⋄}) we have the frame condition F (D_{⋄}) as a restriction on models for the more discriminating logic.

L_{0} : ◇(A •_{r} B) ⟷ ◇(A •_{l} B) (D_{⋄})

x [figure: t; y; z] ⟺ x [figure: t′; y; z]

F (D_{⋄}) : (∀xyz ∈ W_{0}) ∃t(R_{⋄}xt ∧ R_{r}tyz) ⇔ ∃t′(R_{⋄}xt′ ∧ R_{r}t′yz)

Model construction. To construct an L_{0} model ⟨W_{0}, R_{⋄}^{2}, R_{l}^{3}, R_{r}^{3}, V_{0}⟩ from a model

⟨W_{1}, R_{1}^{3}, V_{1}⟩ for L_{1} we proceed as follows. For every triple (xyz) ∈ R_{1} we take fresh points x_{1}, x_{2}, put x, x_{1}, x_{2}, y, z in W_{0} with (xx_{1}) ∈ R_{⋄}, (x_{1}yz) ∈ R_{l} and (xx_{2}) ∈ R_{⋄}, (x_{2}yz) ∈ R_{r}.

M_{1} : [figure: x; y; z] ⇝ x [figure: x_{1}; y; z] + x [figure: x_{2}; y; z] : M_{0}

To show that the generated model M_{0} satisfies the required frame condition F (D_{⋄}), assume there exists b ∈ W_{0} such that R_{⋄}ab and R_{r}bcd. Such a configuration has a unique preimage in M_{1} namely R_{1}acd. By virtue of the construction of M_{0} this means there exists b′ ∈ W_{0} such that R_{⋄}ab′ and R_{l}b′cd, as required for F (D_{⋄}).

Truth preservation of the model construction is unproblematic. The proof of the following proposition then is routine.

Proposition 3.2

NL ⊢ A → B iff DNL◇ + D_{⋄} ⊢ A^{♯} → B^{♯}

Relaxation of order sensitivity. Here we compare logics L_{1} and L_{0} where the structural rule of Permutation is included in the resource management package for L_{1}, but not in that of L_{0}. Controlled Permutation is reintroduced in L_{0} in the form of the modal postulate (P_{⋄}). The corresponding frame condition on L_{0} models M_{0} is given as F (P_{⋄}).

L_{1} : A •_{1} B ⟷ B •_{1} A (P)
L_{0} : ◇(A •_{0} B) ⟷ ◇(B •_{0} A) (P_{⋄})

x [figure: t; y; z] ⟺ x [figure: t′; z; y]

F (P_{⋄}) : (∀xyz ∈ W_{0}) ∃t(R_{⋄}xt ∧ R_{0}tyz) ⇒ ∃t′(R_{⋄}xt′ ∧ R_{0}t′zy)

To generate the required model M_{0} from M_{1} we proceed as follows. If (xyz) ∈ R_{1} we take fresh x_{1}, x_{2} and put both (xx_{1}) ∈ R_{⋄} and (x_{1}yz) ∈ R_{0} and (xx_{2}) ∈ R_{⋄} and (x_{2}zy) ∈ R_{0}.

We have to show that the generated model M_{0} satisfies F (P_{⋄}). Assume there exists b ∈ W_{0} such that R_{⋄}ab and R_{0}bcd. Because of the presence of Permutation in L_{1} this configuration has two preimages, R_{1}acd and R_{1}adc. By virtue of the construction algorithm for M_{0} each of these guarantees there exists b′ ∈ W_{0} such that R_{⋄}ab′ and R_{0}xdc.

Proposition 3.3

NLP ⊢ A → B iff NL◇ + P_{⋄} ⊢ A^{♯} → B^{♯}

Relaxation of constituent sensitivity. Next compare a logic L_{1} where Associativity obtains with a more discriminating logic without global Associativity.

We realize the embedding by introducing a modally controlled form of Associativity (A_{⋄}) with its corresponding frame condition F (A_{⋄}).

L_{1} : A •_{1} (B •_{1} C) ⟷ (A •_{1} B) •_{1} C (A)
L_{0} : ◇(A •_{0} ◇(B •_{0} C)) ⟷ ◇(◇(A •_{0} B) •_{0} C) (A_{⋄})

x [figure: v; u; t; y; z; w] ⟺ x [figure: v′; y; u′; t′; x; w]

\begin{matrix}F (A_{⋄}) : (∀xyzw ∈ W_{0}) \\ ∃tuv(R_{⋄}xv ∧ R_{0}vuw ∧ R_{⋄}ut ∧ R_{0}tyz) ⇔ ∃t′u′v′(R_{⋄}xv′ ∧ R_{0}v′yu′ ∧ R_{⋄}u′t′ ∧ R_{0}t′zw) \end{matrix}

The M_{0} model is generated from M_{1} in the familiar way. For every triple (xyz) ∈ R_{1}, we take a fresh point x′, and put x, x′, y, z ∈ W_{0}, with (xx′) ∈ R_{⋄} and (x′yz) ∈ R_{0}.

We have to show that the frame condition F (A_{⋄}) holds in the generated model. Suppose (†) R_{⋄}ab and R_{0}bcd and (‡) R_{⋄}ce and R_{0}efg. We have to show that there are x, y, z ∈ W_{0} such that R_{⋄}ax and R_{0}xfy and R_{⋄}yz and R_{0}zgd. Observe that the configurations (†) and (‡) both have unique preimages in M_{1}, R_{1}acd and R_{1}cfg respectively. Because R_{1} is associative, there exists y ∈ W_{1} such that R_{1}afy and R_{1}ygd. But then, by the construction of M_{0}, also y ∈ W_{0} and there exist x, z ∈ W_{0} such that R_{⋄}ax, R_{0}xfy, R_{⋄}yz and R_{0}zgd, as required.

Proposition 3.4

L ⊢ A → B iff NL◇ + A_{⋄} ⊢ A^{♯} → B^{♯}

Generalisations. The preceding discussion covers the individual dimensions of structural organisation. Generalizing the approach to the remaining edges of Fig 1 does not present significant new problems. Here are some suggestions to assist the tenacious reader who wants to work out the full details.

The embeddings for the lower plane of Fig 1 are obtained from the parallel embeddings in the upper plane by doubling the construction from a unimodal product setting to the bimodal situation with two dependency products.

Embeddings between logics sharing associative management, but differing with respect to order or dependency sensitivity require modal associativity A_{⋄} in addition to P_{⋄} or D_{⋄} for the more discriminating logic: as we have seen in §2, the external ◇ decoration on product configurations pre-empts the conditions of application for the non-modal associativity postulate. We have already come across this interplay between the translation schema and modal structural postulates in §2.3. For the licensing type of embedding, concrete instances are the embedding of LP into L◇+ A_{⋄} + P_{⋄}, and the embedding of L into DL◇ + A_{⋄} + D_{⋄}.

External decoration: applications. Linguistic application for the external strategy of modal licensing will be found in areas where one wants to induce

Prop 3.3: Commutativity NLP

L

[figure]

Prop 3.4: Associativity

NL

Prop 3.2: Dependency

DNL

Figure 6: Licensing structural relaxation: precedence, dominance, dependency

structural relaxation in a configuration from the outside. The complementary view, where a subconfiguration induces structural relaxation in its context, is explored in §3.2 below. For the outside perspective, consider a non-commutative default regime with P_{⋄} for the modal extension. Collapse of the directional implications is underivable, ⊬ A/B ⟷ B\A, but the modal variant below is. In general terms: a lexical assignment A/□^{↓}◇B will induce commutativity for the argument subtype.

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

Similarly, in the context of a non-associative default regime with A_{⋄} for the modal extension, one finds the following modal variant of the Geach rule, which remains underivable without the modal decoration.

\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)^{•})^{⋄}, C)^{•})^{⋄} ⇒ ◇A \end{matrix} ; A_{⋄} ; (((A/B, □^{↓}B/C)^{•})^{⋄}, C)^{•} ⇒ □^{↓}◇A ; □^{↓}R ; ((A/B, □^{↓}B/C)^{•})^{⋄} ⇒ □^{↓}◇A/C ; /R ; (A/B, □^{↓}B/C)^{•} ⇒ □^{↓}(□^{↓}◇A/C) ; □^{↓}R ; A/B ⇒ □^{↓}(□^{↓}◇A/C)/(□^{↓}B/C) ; /R

3.2 Modal labelling: the internal perspective

The embeddings discussed in the previous section license special structural behaviour by external decoration of product configurations: in the scope of the ◇ operator the product gains access to a structural rule which is unavailable in the default resource management of the logic in question. In view of the intended linguistic applications of structural modalities we would like to complement the external modalization strategy by an internal one where a structural rule is applicable to a product configuration provided one of its subtypes is modally decorated. In fact, the examples of modally controlled constraints we gave at the beginning of this paper were of this form. For the internal perspective, the modalized versions of Permutation and Associativity take the form shown below.

(P′_{⋄})  ◇A • B ⟷ B • ◇A
(A′_{⋄}) A_{1} • (A_{2} • A_{3}) ⟷ (A_{1} • A_{2}) • A_{3} (provided A_{i} = ◇A, 1 ≤ i ≤ 3)

We prove embedding theorems for internal modal decoration in terms of the following translation mapping, which labels positive (proper) subformulae with the modal prefix ◇□^{↓} and leaves negative subformulae undecorated.

Definition 3.5 Embedding translations (·)^{+}, (·)^{−} : F(L_{1}) ↦ F(L_{0}◇) for positive and negative formula occurrences.

\begin{aligned}(p)^{+} & = & p \\ (A •_{1} B)^{+} & = & ◇□^{↓}(A)^{+} •_{0} ◇□^{↓}(B)^{+} \\ (A/_{1}B)^{+} & = & ◇□^{↓}(A)^{+}/_{0}(B)^{−} \\ (B\_{1}A)^{+} & = & (B)^{−}\_{0}◇□^{↓}(A)^{+} \end{aligned}  \begin{aligned}(p)^{−} & = & p \\ (A •_{1} B)^{−} & = & (A)^{−} •_{0} (B)^{−} \\ (A/_{1}B)^{−} & = & (A)^{−}/_{0}◇□^{↓}(B)^{+} \\ (B\_{1}A)^{−} & = & ◇□^{↓}(B)^{+}\_{0}(A)^{−} \end{aligned}

The theorems embedding a stronger logic L_{1} into a more discriminating system L_{0} now assume the following general form, where R′_{⋄} is the modal version of the structural rule package discriminating between L_{1} and L_{0}.

Proposition 3.6

L_{1} ⊢ A → B iff L_{0}◇ + R′_{⋄} ⊢ A^{+} → B^{−}

As an illustration we consider the embedding of L into NL◇ which involves licensing of Associativity in terms of the postulate (A′_{⋄}). The frame construction method we employ is completely general: it can be used unchanged for the other cases of licensing embedding one may want to consider.

The proof of the (⇒) direction of Prop 3.6 is by easy induction. We present a Gentzen derivation of the Geach rule as an example. The type responsible for licensing A′_{⋄} in this case is ◇□^{↓}(B/C)^{+}.

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}C^{+} ⇒ C^{−} \\ (□^{↓}C^{+})^{⋄} ⇒ C^{−} \end{matrix} & L□^{↓} \\ ◇□^{↓}C^{+} ⇒ C^{−} \end{matrix} ; L◇ & \begin{matrix}… \\ ◇□^{↓}B^{+} ⇒ B^{−} \end{matrix} \\ ◇□^{↓}B^{+}/C^{−}, ◇□^{↓}C^{+} ⇒ B^{−} \end{matrix} & L/ \\ ((□^{↓}(◇□^{↓}B^{+}/C^{−}))^{⋄}, ◇□^{↓}C^{+}) ⇒ B^{−} \end{matrix} ; L□^{↓} & \begin{matrix}… \\ ◇□^{↓}A^{+} ⇒ A^{−} \end{matrix} \\ (◇□^{↓}A^{+}/B^{−}, ((□^{↓}(◇□^{↓}B^{+}/C^{−}))^{⋄}, ◇□^{↓}C^{+})) ⇒ A^{−} \end{matrix} & L/ \\ ((◇□^{↓}A^{+}/B^{−}, (□^{↓}(◇□^{↓}B^{+}/C^{−}))^{⋄}), ◇□^{↓}C^{+}) ⇒ A^{−} \end{matrix} ; A′_{⋄} ; ((◇□^{↓}A^{+}/B^{−}, ◇□^{↓}(◇□^{↓}B^{+}/C^{−})), ◇□^{↓}C^{+}) ⇒ A^{−} ; L◇ ; ◇□^{↓}A^{+}/B^{−} ⇒ (A^{−}/◇□^{↓}C^{+})/◇□^{↓}(◇□^{↓}B^{+}/C^{−}) ; R/, R/ ; (A/B)^{+} ⇒ ((A/C)/(B/C))^{−} ; (·)^{+}, (·)^{−}

For the (⇐) direction, we proceed by contraposition. Suppose L ⊬ A → B. Completeness tells us there exists an L model M_{1} = ⟨W_{1}, R_{1}, V_{1}⟩ with a point a ∈ W such that M_{1}, a ⊧ A but M_{1}, a |̸= B. From M_{1} we want to construct an NL◇+A′_{⋄} model M_{0} = ⟨W_{0}, R_{⋄}, R_{0}, V_{0}⟩ such that A^{+} → B^{−} fails. Recall that R_{0} has to satisfy the frame conditions for the modal versions A′_{⋄} of the Associativity postulate. We give one instantiation below.

(A′_{⋄}) ◇A •_{0} (B •_{0} C) ⟷ (◇A •_{0} B) •_{0} C

[figure: x; ty; u; z; w] ⇔ [figure: x; u′; t′ y; z; w]

(†) (∀xyzw ∈ W_{0})
∃tu(R_{0}xtu ∧ R_{⋄}ty ∧ R_{0}uzw) ⇔ ∃t′u′(R_{0}xu′w ∧ R_{0}u′t′z ∧ R_{⋄}t′y)

The model construction proceeds as follows. We put the falsifying point a ∈ W_{0}, and for every triple (xyz) ∈ R_{1} we put x, y, z ∈ W_{0} and (xyz) ∈ R_{0}, (yy) ∈ R_{⋄}, (zz) ∈ R_{⋄}.

M_{1} [figure: x; y; z] ⇝ [figure: x; yy; zz] M_{0}

We have to show that the model construction realizes the frame condition (†) (and its relatives) in M_{0}. Suppose ∃xy(R_{0}axy ∧ R_{⋄}xb ∧ R_{0}ycd). By the model construction, x = b, so R_{0}aby which has the pre-image R_{1}aby. The pre-image of R_{0}ycd is R_{1}ycd. The combination of these two R_{1} triangles satisfies the Associativity frame condition of L, so that we have a point t such that R_{1}atd ∧ R_{1}tbc. Again by the model construction, this means in M_{0} we have ∃z, t(R_{0}tzc ∧ R_{⋄}zb ∧ R_{0}atd), as required.

M_{1} [figure: a; b; y; c; d] ⇔ [figure: a; t; b; c; d] ⇝ [figure: a; t; bb; c; d] M_{0}

The central Truth Preservation Lemma now is that for any a ∈ W_{1} ∩ W_{0},

M_{1}, a ⊧ A iff M_{0}, a ⊧ A^{+} iff M_{0}, a ⊧ A^{−}

We concentrate on the (·)^{+} case — the (·)^{−} case is straightforward.

(⇒) Suppose M_{1}, a ⊧ A •_{1} B. We have to show that M_{0}, a ⊧ ◇□^{↓}A^{+} •_{0} ◇□^{↓}B^{+}. By assumption, there exist b, c such that R_{1}abc, and M_{1}, b ⊧ A, M_{1}, c ⊧ B. By inductive hypothesis and the model construction algorithm, we have in M_{0}

[figure: a; bb; cc]  M_{0}, b ⊧ A^{+} M_{0}, c ⊧ B^{+}

Observe that if x is the only point accessible from x via R_{⋄} (as is the case in M_{0}), then for any formula ϕ, x ⊧ ϕ iff x ⊧ ◇ϕ iff x ⊧ □^{↓}ϕ iff x ⊧ ◇□^{↓}ϕ. Therefore, from the above we can conclude M_{0}, b ⊧ ◇□^{↓}A^{+} and M_{0}, c ⊧ ◇□^{↓}B^{+}, hence M_{0}, a ⊧ ◇□^{↓}A^{+} •_{0} ◇□^{↓}B^{+}.

(⇐) Suppose M_{0}, a ⊧ ◇□^{↓}A^{+} •_{0} ◇□^{↓}B^{+}. We show that M_{1}, a ⊧ A •_{1} B. By assumption, there exist b, c such that R_{0}abc, and M_{0}, b ⊧ ◇□^{↓}A^{+}, M_{0}, c ⊧ ◇□^{↓}B^{+}. In M_{0} all triangles are such that the daughters have themselves and only themselves accessible via R_{⋄}. Using our observation again, we conclude that M_{0}, b ⊧ A^{+}, M_{0}, c ⊧ B^{+}, and by inductive assumption M_{1}, a ⊧ A • B.

We leave the implicational formulas to the reader.

Comment: full internal labeling. Licensing of structural relaxation is implemented in the above proposal via modal versions of the structural postulates requiring at least one of the internal subtypes to be ◇ decorated. It makes good sense to consider a variant of internal licensing, where one requires all relevant subtypes of a structural configuration to be modally decorated — depending on the application one has in mind, one could choose one or the other. Embeddings with this property have been studied for algebraic models by [Venema 93, Versmissen 93]. In the terms of our minimalistic setting, modal structural postulates with full internal labeling would assume the following form.

\begin{matrix}(P′′_{⋄}) & ◇A • ◇B ⟷ ◇B • ◇A \\ (A′′_{⋄}) & ◇A • (◇B • ◇C) ⟷ (◇A • ◇B) • ◇C \end{matrix}

One obtains the variant of the embedding theorems for full internal labeling on the basis of the modified translation (·)^{++} which marks all positive subformulae with the modal prefix ◇□^{↓}. (Below we abbreviate ◇□^{↓} to μ.) In the model construction, one puts (xx) ∈ R_{⋄} (and nothing more) for every point x that has to be put in W_{0}.

\begin{aligned}(p)^{++} & = & μp \\ (A •_{1} B)^{++} & = & μ(μ(A)^{++} •_{0} μ(B)^{++}) \\ (A/_{1}B)^{++} & = & μ(μ(A)^{++}/_{0}(B)^{−}) \\ (B\_{1}A)^{++} & = & μ((B)^{−}\_{0}μ(A)^{++}) \end{aligned}  \begin{aligned}(p)^{−} & = & p \\ (A •_{1} B)^{−} & = & (A)^{−} •_{0} (B)^{−} \\ (A/_{1}B)^{−} & = & (A)^{−}/_{0}μ(B)^{++} \\ (B\_{1}A)^{−} & = & μ(B)^{++}\_{0}(A)^{−} \end{aligned}

Proposition 3.7

L_{1} ⊢ A → B iff L_{0}◇ + R′′_{⋄} ⊢ A^{++} → B^{−}

Illustration: extraction. For a concrete linguistic illustration of ◇□^{↓} labeling licensing structural relaxation, we return to the example of extraction from non-peripheral positions in relative clauses. The example below becomes derivable in NL◇ + (A′_{⋄}, P′_{⋄}) given a modally decorated type assignment r/(s/◇□^{↓}np) to the relative pronoun, which allows the hypothetical ◇□^{↓}np assumption to find its appropriate location in the relative clause body via controlled Associativity and Permutation. We give the relevant part of the Gentzen derivation, abbreviating (np\s)/np as tv.

… that ((John read) yesterday)

NL◇ + (A′_{⋄}, P′_{⋄}) ⊢ (r/(s/◇□^{↓}np), ((np, (np\s)/np), s\s)) ⇒ r

\begin{matrix}\begin{matrix}⋯ \\ ((np, (tv, np)), s\s) ⇒ s \end{matrix} ; ((np, (tv, (□^{↓}np)^{⋄})), s\s) ⇒ s & L□^{↓} \\ (((np, tv), (□^{↓}np)^{⋄}), s\s) ⇒ s \end{matrix} ; A′_{⋄} ; ((np, tv), ((□^{↓}np)^{⋄}, s\s)) ⇒ s ; A′_{⋄} ; ((np, tv), (s\s, (□^{↓}np)^{⋄})) ⇒ s ; P′_{⋄} ; (((np, tv), s\s), (□^{↓}np)^{⋄}) ⇒ s ; A′_{⋄} ; (((np, tv), s\s), ◇□^{↓}np) ⇒ s ; L◇ ; ((np, tv), s\s) ⇒ s/◇□^{↓}np ; R/

Comparing this form of licensing modal decoration with the treatment in terms of a universal □ operator with S4 structural postulates, one observes that on the proof-theoretic level, the ◇□^{↓} prefix is able to mimick the behaviour of the S4 □ modality, whereas on the semantic level, we are not forced to impose transitivity and reflexivity constraints on the interpretation of R_{⋄}. With a translation (□A)^{∼} = ◇□^{↓}(A)^{∼}, the characteristic T and 4 postulates for □ become valid type transitions in the pure residuation system for ◇, □^{↓}, as the reader can check.

\begin{matrix}T : & □A → A & ⇝ & ◇□^{↓}A → A \\ 4 : & □A → □□A & ⇝ & ◇□^{↓}A → ◇□^{↓}◇□^{↓}A \end{matrix}

4 Discussion

In this final section, we reflect on some general logical and linguistic aspects of the proposed architecture, and raise a number of questions for future research.

Linear Logic and the sublinear landscape. In order to obtain controlled access to Contraction and Weakening, Linear Logic extends the formula language with operators which on the proof-theoretic level are governed by an S4-like regime. The ‘sublinear’ grammar logics we have studied show a higher degree of structural organization: not only the multiplicity of the resources matters, but also the way they are put together into structured configurations. These more discriminating logics suggest more delicate instruments for obtaining structural control. We have presented embedding theorems for the licensing and for the constraining perspective on substructural communication in terms of the pure logic of residuation for a set of unary multiplicatives ◇, □^{↓}. In the frame semantics setting, these operators make more fine-grained structural distinctions than their S4 relatives which are interpreted with respect to a transitive and reflexive accessibility relation. But they are expressive enough to obtain full control over grammatical resource management. Our minimalistic stance is motivated by linguistic considerations. For reasons quite different from ours, and for different types of models, a number of recent proposals in the field of Linear Logic proper have argued for a decomposition of the ‘!,?’ modalities into more elementary operators. For comparison we refer the reader to [Bucalo 94, Girard 95].

The price of diamonds. We have compared logics with a ‘standard’ language of binary multiplicatives with systems where the formula language is extended with the unary logical constants ◇, □^{↓}. The unary operators, one could say, are the price one has to pay to gain structural control. Do we really have to pay this price, or could one faithfully embed the systems of Fig 1 as they stand? For answers in a number of specific cases, one can turn to [van Benthem 91].

A question related to the above point is the following. Our embeddings compare the logics of Fig 1 pairwise, adding a modal control operator for each translation. This means that self-embeddings, from L to L′ and back, end up two modal levels higher, a process which reaches equilibrium only in languages with infinitely many ◇, □^{↓} control operators. Can one stay within some finite modal repertoire? We conjecture the answer is positive, but a definitive result would require a deeper study of the residuation properties of the ◇, □^{↓} family.

Pure embeddings versus modal structural rules. The embedding results presented here are globally of two types. One type — what we have called the pure embeddings — obtains structural control solely in terms of the modal decoration added in the translation mapping. The other type adds a relativized structural postulate which can be accessed in virtue of the modal decoration of the translation. For the licensing type of communication, the second type of embedding is fully natural. The target logic, in these cases, does not allow a form of structural manipulation which is available in the source logic: in a controlled form, we want to regain this flexibility. But the distinction between the two types of embedding does not coincide with the shift from licensing to constraining communication. We have seen in §2.3 that imposing structural constraints for logics sharing associative resource management requires modalized structural postulates, in addition to the modal decoration of the translation mapping. In these cases, the ◇ decoration has accidentally damaged the potential for associative rebracketing: the modalized associativity postulates repair this damage. We leave it as an open question whether one could realize pure embeddings for some of the logics of §2.3. A related question can be raised for the same family of logics under the licensing perspective: in these cases, we find not just the modal structural postulate for the parameter which discriminates between the logics, but in addition modal associativity, again because the translation schema has impaired the normal rebracketing.

Uniform versus customized translations. Another asymmetry that may be noted here is our implementation of the licensing type of communication in terms of a uniform translation schema, versus the constraining type of embeddings where the translations are specifically tailored towards the particular structural dimension one wants to control. Could one treat the constraining embeddings of §2 also in terms of a uniform translation scheme? And if so, would such a scheme be cheaper or more costly than the individual schemes in the text?

Complexity. A final set of questions relates to issues of computational complexity. For many of the individual logics in the sublinear cube complexity results (pleasant or unpleasant) are known. Do the embeddings allow transfer of such results to systems where we still face embarrassing open questions (such as: the issue of polynomial complexity for L)? In other words: what is the computational cost of the translations and modal structural postulates proposed? We conjecture that modalized versions of structural rules have the same computational cost as corresponding structural rules themselves.

Embeddings: linguistic relevance. We close with a remark for the reader with a linguistics background. The embedding results presented in this paper may seem somewhat removed from the daily concerns of the working grammarian. Let us try to point out how our results can contribute to the foundations of grammar development work. In the literature of the past five years, a great variety of ‘structural modalities’ has been introduced, with different proof-theoretic behaviour and different intended semantics. It has been argued that the defects of particular type systems (either in the sense of overgeneration, or of undergeneration) can be overcome by refining type assignment in terms of these structural modalities. The accounts proposed for individual linguistic phenomena are often ingenious, but one may legitimately ask what the level of generality of the proposals is. The embedding results of this paper show that the operators ◇, □^{↓} provide a general logic of constraints in the dimensions of order, dominance and dependency.

A Appendix

A.1 Axiomatic and Gentzen presentation

In this section we juxtapose the axiomatic presentations and the Gentzen formulation of the logics under discussion. The Lambek and Došen style axiomatic presentations are two equivalent ways of characterizing ◇, □^{↓}, •, / and •, \ as residuated pairs of operators. For the equivalence between the axiomatic and the Gentzen presentations, we refer to [Moortgat 95]. This paper also establishes a Cut Elimination result for the language extended with ◇, □^{↓}.

Definition A.1 Lambek-style axiomatic presentation.

A → A  \frac{A → B B → C}{A → C}

◇A → B ⟺ A → □^{↓}B
A → C/B ⟺ A • B → C ⟺ B → A\C

Definition A.2 Došen style axiomatization.

A → A  \frac{A → B B → C}{A → C}

◇□^{↓}A → A  A → □^{↓}◇A
A/B • B → A  A → (A • B)/B
B • B\A → A  A → B\(B • A)

\frac{A → B}{◇A → ◇B}  \frac{A → B}{□^{↓}A → □^{↓}B}

\frac{A → B C → D}{A • C → B • D}

\frac{A → B C → D}{A/D → B/C}  \frac{A → B C → D}{D\A → C\B}

The formulations of Def A.1 and Def A.2 give the pure residuation logic for the unary and binary families. The logics of Fig 1 are then obtained by adding different packages of structural postulates, as discussed in §1.

Definition A.3 Gentzen presentation. Sequents Γ ⇒ A with Γ a structured database of linguistic resources, A a formula. Structured databases are inductively defined as terms T ::= F | (T , T )^{m} | (T )^{⋄}, with binary (·, ·)^{m} or unary (·)^{⋄} structural connectives corresponding to the (binary, unary) logical connectives. We add resource management mode indexing for logical and structural connectives to keep families with different resource management properties apart. This strategy goes back to [Belnap 82] and has been applied to modal display logics in [Kracht 93, Wansing 92], two papers which are related in a number of respects to our own efforts.

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

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

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

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

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

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

Structural postulates, in the axiomatic presentation, have been presented as transitions A → B where A and B are constructed out of formula variables p_{1}, …, p_{n} and logical connectives •_{m}, ◇. For structure variables Δ_{1}, …, Δ_{n} and structural connectives (·, ·)^{m}, (·)^{⋄}, define the structural equivalent σ(A) of a formula A as indicated below (cf [Kracht 93]):

σ(p_{i}) = Δ_{i} σ(A •_{m} B) = (σ(A), σ(B))^{m} σ(◇A) = (σ(A))^{⋄}

The transformation of structural postulates into Gentzen rules allowing Cut Elimination then is straightforward: a postulate A → B translates as the Gentzen rule

\begin{matrix}Γ[σ(B)] ⇒ C \\ Γ[σ(A)] ⇒ C \end{matrix}

In the cut elimination algorithm, one shows that if a structural rule precedes a Cut inference, the order of application of the inferences can be permuted, pushing the Cut upwards. See [Došen 89] for the case of global structural rules, [Moortgat 95] for the ◇ cases.

In the multimodal setting, structural rules are relativized to the appropriate resource management modes, as indicated by the mode index. An example is given below (for k a commutative and l an associative regime). Where no confusion is likely to arise, in the text we use the conventional symbols for different families of operators, rather than the official mode indexing on one generic set of symbols.

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

cf A •_{k} B → B •_{k} A  cf A •_{l} (B •_{l} C) → (A •_{l} B) •_{l} C

A.2 Trading ternary relations for binary ones

The embedding results developed above suggest the question whether Lambek systems can be embedded into standard modal logic with unary modalities. Moreover, it is at least of purely modal interest to see if the work of a ternary accessibility relation can be done by binary ones. So far, we have analyzed the Lambek Calculus NL and its neighbours as a modal logic with binary modalities. Can we also analyze it as a modal logic with only unary modalities? The answer is positive: we prove that NL can be faithfully embedded into minimal temporal logic K^{t}. The job will be done in two steps: first, we show how NL can be embedded into bimodal temporal logic K_{1,2}^{t}, and then we use Thomason’s result on embedding bimodal systems into unary ones.

Definition A.4 Minimal Bi-Tense Logic. Let K_{1,2}^{t} be a minimal tense logic having two ‘forward looking operators’ □_{1}, □_{2} (with existential duals ◇_{1}, ◇_{2}) and two corresponding ‘backward looking’ operators □_{1}^{↓}, □_{2}^{↓} (with existential duals ◇_{1}^{↓}, ◇_{2}^{↓}). The modal language of K_{1,2}^{t} has its formulas built up from propositional letters according to the rule:

ϕ ::= p|¬ϕ|ϕ&ψ|◇_{1}ϕ|◇_{2}ϕ|◇_{1}^{↓}ϕ|◇_{2}^{↓}ϕ|□_{1}ϕ|□_{2}ϕ|□_{1}^{↓}ϕ|□_{2}^{↓}ϕ

By standard methods, K_{1,2}^{t} can be axiomatized using

Axioms

– all tautologies of classical propositional logic

– all modal distribution axioms □_{i}(A ⊃ B) ⊃ (□_{i}A ⊃ □_{i}B) and □_{i}^{↓}(A ⊃ B) ⊃ (□_{i}^{↓}A ⊃ □_{i}^{↓}B)

– all tense-logical conversion axioms ◇_{i}□_{i}^{↓}A ⊃ A and A ⊃ □_{i}^{↓}◇_{i}A

Rules

– modus ponens

– necessitation A/□_{i}A and A/□_{i}^{↓}A , where i=1,2.

A K_{1,2}^{t} model is an ordinary bimodal model M = ⟨W, R_{1}^{2}, R_{2}^{2}, V ⟩ with truth definition (i=1,2)

\begin{aligned}M, a ⊧ □_{i}A & ⟺ & ∀b(R_{i}ab ⇒ M, b ⊧ A) \\ M, a ⊧ □_{i}^{↓}A & ⟺ & ∀b(R_{i}ab ⇒ M, b ⊧ A) \end{aligned}

A faithful embedding of the non-associative Lambek Calculus into K_{1,2}^{t} runs as follows:

\begin{aligned}p^{♯} & = & p \\ (A • B)^{♯} & = & ◇_{1}(◇_{1}A^{♯}&◇_{2}B^{♯}) \\ (A\B)^{♯} & = & □_{2}^{↓}(◇_{1}A^{♯} ⊃ □_{1}^{↓}B^{♯}) \\ (B/A)^{♯} & = & □_{1}^{↓}(◇_{2}A^{♯} ⊃ □_{1}^{↓}B^{♯}) \end{aligned}

Theorem A.5 First Embedding Theorem. The following assertions are equivalent:

(i) A ⊢ B is derivable in NL
(ii) A^{♯} ⊢ B^{♯} is derivable in K_{1,2}^{t}

Proof. The direction (i) ⇒ (ii) can be proved by an easy induction on the length of the NL-derivation for A ⊢ B. For example, consider the axiom

A ⊢ B\(B • A)

Its translation

A^{♯} ⊢ □_{2}^{↓}(◇_{1}B^{♯} ⊃ □_{1}^{↓}◇_{1}(◇_{1}B^{♯}&◇_{2}A^{♯}))

is derivable in the minimal bi-tense logic K_{1,2}^{t}. For the converse direction (ii) ⇒ (i), we use a semantical representation argument. Let A ⊢ B be underivable in NL. By the above completeness of NL with respect to ternary semantics, there exists a ternary model M where A ⊢ B fails. So, there exists a world k ∈ W which verifies A, but falsifies B. We construct a K_{1,2}^{t} model M = ⟨W^{∗}, R_{1}, R_{2}, V^{∗}⟩ where A^{♯} ⊢ B^{♯} fails, as follows:

• put k in W^{∗}

• if ⟨a, bc⟩ ∈ R, then take a fresh object x, and put ⟨ax⟩ and ⟨xb⟩ in R_{1} , ⟨xc⟩ in R_{2}, a, b, c, x in W^{∗}

• set for all a ∈ W ∩ W^{∗}, a ∈ V^{∗}(p) iff a ∈ V (p)

□

Claim A.6 For all categorial formulas A, and all a ∈ W ∩ W^{∗},

M^{∗}, a ⊧ A^{♯} ⟺ M, a ⊧ A

Proof. Induction on the length of A. The basic case is a direct consequence of the definition of M^{∗}. We demonstrate only one typical clause of the inductive step, to illustrate this kind of elementary semantic argument over ternary models.

(1) Suppose M^{∗}, a ⊧ □_{2}^{↓}(◇_{1}A^{♯} ⊃ □_{1}^{↓}B^{♯})

We need to show that M, a ⊧ A → B.

(2) Suppose (a) R^{3}c, ba and (b) M, b ⊧ A We need to show that M, c ⊧ B

(3) By the inductive hypothesis : M^{∗}, b ⊧ A^{♯}. By the above construction of M^{∗}, (2(a)) yields

(4) (a) R_{1}cx (b) R_{1}xb (c) R_{2}xa

(5) By the truth definition:

M^{∗}, x ⊧ ◇_{1}A^{♯} From (1) and (4(c)) M^{∗}, x ⊧ ◇_{1}A♯ ⊃ □_{1}^{↓}B^{♯} Thus M^{∗}, x ⊧ □_{1}^{↓}B^{♯}

(6) From (4(a)) we get M^{∗}, c ⊧ B^{♯} and by inductive hypothesis M, c ⊧ B.

Here is the converse argument. Again, we start by successively unpacking what needs to be shown.

(1) Suppose M, a ⊧ A → B.

We need to shaw that M^{∗}, a ⊧ □_{2}^{↓}(◇_{1}A^{♯} ⊃ □_{1}^{↓}B^{♯})

(2) Suppose (a) R_{2}xa (b) M^{∗}, x ⊧ ◇_{1}A^{♯} (c) R_{1}bx We need to show that M^{∗}, b ⊧ B^{♯}

(3) By (2(b)) there exists c such that (a) R_{1}xc and (b) M^{∗}, c ⊧ A^{♯} By inductive assumption :

(c) M, c ⊧ A

(4) Note, that by the construction of M^{∗}, R_{1}bx, R_{1}xc, R_{2}xa must ‘come from’ a unique triangle, namely Rb, ca. Then, from (1) and (3(c)), M ⊧ B, and therefore M^{∗}, b ⊧ B^{♯}. □

The preceding Claim implies that any ternary NL-counter-model M for a sequent A ⊢ B can be transformed into K_{1,2}^{t} model M^{∗} where A^{♯} ⊢ B^{♯} fails. Hence A^{♯} ⊢ B^{♯} is not derivable in K_{1,2}^{t}. This proves the faithful embedding. □

Theorem A.7 Second Embedding Theorem. The following assertions are equivalent:

(i) A ⊢ B is derivable in NL
(ii) A^{♯} ⊢ B^{♯} is derivable in Kt

Proof. This is a direct consequence of S.K. Thomason’s results on embeddings of bimodal systems into unary modal ones, see [Thomason 72]. □

References

[Barry & Morrill 90] Barry, G. and G. Morrill (eds) (1990) Studies in Categorial Grammar. Edinburgh Working Papers in Cognitive Science, Vol 5. CCS, Edinburgh.

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

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

[Bucalo 94] Bucalo, A. (1994) ‘Modalities in Linear Logic weaker than the exponential “of course”: algebraic and relational semantics’. JoLLI 3, 3, 211–232.

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

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

[Došen 92] Došen, K. (1992) ‘Modal translations in substructural logics’. Journal of Philosophical Logic 21, 283–336.

[Dunn 91] 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.

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

[Girard 95] Girard, J.-Y., (1995) ‘Light Linear Logic: extended abstract’. Ms LMD, Marseille.

[Kracht 93] Kracht, M. (1993) ‘Power and weakness of the modal Display Calculus’. Ms Freie Universität Berlin.

[Kurtonina 95] Kurtonina, N. (1995) Frames and Labels. A Modal Analysis of Categorial Inference. PhD Dissertation, OTS Utrecht, ILLC Amsterdam.

[K & M 94] Kurtonina, N. and M. Moortgat (1994) ‘Controlling resource management’. Esprit BRA Dyana-2 Deliverable R1.1.B, pp 45– 62.

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

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

[Moortgat 95] Moortgat, M. (1995), ‘Multimodal linguistic inference’, IGPL Bulletin, Vol 3 (2,3), p 371–421. Special issue Deduction and Language (guest editor: Ruth Kempson). (Revised version to appear in JoLLI).

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

[M & O 93] 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.

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

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

[Morrill 94] Morrill, G. (1994) Type Logical Grammar. Kluwer, Dordrecht.

[Thomason 72] Thomason S.K. (1972) ‘Semantic analysis of Tense Logic’. Journal of Symbolic Logic, 1972, vol. 37, 1.

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

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

[Wansing 92] Wansing, H. (1992) ‘Sequent calculi for normal modal propositional logics’. ILLC Report LP–92–12.