## Quantale semantics of Lambek calculus with subexponential modalities

## Daniel Rogozin

Lomonosov Moscow State University

## Abstract

In this paper, we consider the polymodal version of Lambek calculus with subexponential modalities initially introduced by Kanovich, Kuznetsov, Nigam, and Scedrov [10] and its quantale semantics. In our approach, subexponential modalities have an interpretation in terms of quantic conuclei. We show that this extension of Lambek calculus is complete w.r.t quantales with quantic conuclei. Also, we prove a representation theorem for quantales with quantic conuclei and show that Lambek calculus with subexponentials is relationally complete. Finally, we extend this representation theorem to the category of quantales with quantic conuclei. Some of these results were presented here [20].

## 1 Introduction

Categorial grammars were initially introduced by Ajdukiewicz and Bar-Hillel [1] [2]. In the 1950s, Lambek proposed the way of proof-theoretical consideration of such grammars [13]. In this approach, language is logic and parsing is derivation via inference rules. Let us consider a quite simple example. Suppose one needs to parse this quote from the poem by Oscar Wilde called 'Impression du Matin' [22]:

The Thames nocture of blue and gold Changed to Harmony in grey

The first is to assign the corresponding syntactic categories to the words as follows:

```
\begin{array} {
```

Here the basic reduction rules are:

- · A,A B z Ñ B
- · B A,A { Ñ B

Here we assign the special syntactic categories to the words of this sentence. np denotes 'noun phrase', n - noun, ad - adjective, p - phrase, s - sentence. This sequent denotes that this Oscar Wilde's quote is a well-formed sentence. The verb 'changed' has type ' np under ( s over p )'. In other words, one needs to apply some noun phrase ('The Thames nocturne of blue and gold') from the left, apply some phrase from the right ('Changed to Harmony in grey') and obtain sentence after that. The other syntactic categories might be considered similarly.

The general case of such derivations in categorial grammars is axiomatised via Lambek calculus [13], non-commutative linear logic:

## Definition 1. Lambek calculus (the system L )

$$a x$$

$$\overline { A \to A } ^ { \ a x } \\ \frac { \Gamma$$

$$\frac { \Gamma \to A \prod _ { \mathcal { \Pi },$$

Note that, non-commutativity has quite strong strong linguistical connotation. We cannot assume that a sentence remains well-formed regardless of the word order.

Here, non-commutativity yields two implications: the left one (or, left division) and the right one (or, right division). Moreover, the right introduction rules for these divisions have the special restriction that claims non-emptiness of the sequence Π in the premise. This restriction denotes that we have no empty word that makes no sense linguistically. On the other hand, we can avoid this restriction. This calculus is called L ˚ [14]. From a linguistical point of view, lack of this restriction denotes that the language has an empty word, i.e., a neutral element w.r.t product.

Note that, the empty word might be introduced explicilty via the constant 1 . The logic L 1 is a conservative extension of L ˚ [12] with the following inference rules for this constant:

$$\frac { \Gamma, \Delta \to A } { \Gamma, 1, \Delta$$

Let us discuss models of basic Lambek calculus and its completeness theorems. The calculus with non-emptiness restriction is a logic of residual semigroups. The logic of residual monoid is L ˚ . Moreover, these calculi are complete with respect to L -models [5] [18], residual semigroups and monoids on subsets of free semigroup and free monoid correspondingly.

One may extend Lambek calculus with so-called additive conjunction and disjunction. The inference rules for these connections are quite similar to inference rules for conjunction and disjunction in intuitionistic sequent calculus. In L -models, additive connections are intersection and union of languages:

$$\frac { \Gamma, A _ { i }, \Delta \to B } { \Gamma, A _ { 1 } \wedge A _ { 2 }, \Delta \to B } \wedge \to, i = 1, 2 \quad \frac { \Gamma \to A } { \Gamma \to A \wedge B } \to \wedge$$

$$\frac { \Gamma, A _ { i }, \Delta \to B } { \Gamma, A _ { 1 } \wedge A _ { 2 }, \Delta \to B } \wedge \to, i = 1, 2 & \quad \frac { \Gamma \to A } { \Gamma \to A \wedge B } \to \wedge \\ \frac { \Gamma, A, \Delta \to C \quad \Gamma, B, \Delta \to C } { \Gamma, A \vee B, \Delta \to C } \vee \to & \quad \frac { \Gamma \to A _ { i } } { \Gamma \to A _ { 1 } \vee A _ { 2 } } \to \vee, i = 1, 2$$

Note that Lambek calculus with additives is incomplete w.r.t L -models. Here, there are four distributivity inclusions. They are all true in each L -model, just because these properties hold for language intersection and union as for usual Boolean operations on sets. On the other hand, only two of them are provable:

- 1. $ A \_p B ^ C q Ñ p A \_ B q ^ p A \_ C q
- 2. &amp; p A \_ B q ^ p A \_ C q Ñ A \_p B ^ C q
- 3. &amp; A ^p B \_ C q Ñ p A ^ B q \_ p A ^ C q
- 4. $ p A ^ B q \_ p A ^ C q Ñ A ^p B \_ C q

One may read about the other approaches to the interpretation of Lambek calculus with additives (sometimes it's called full Lambek calculus ) here [23] and here [6].

In this paper, we introduce quantales in order to explain the purely algebraic semantics of Lambek calculus with additives and its modal extensions. A quantale is a generalisation of locales and some well-known structures from functional analysis, such as C ˚ algebras. The initial idea to consider quantales within linear logic belongs to David Yetter [24].

Brown and Gurr proved that Lambek calculus with additives is sound and strongly complete w.r.t quantales [4]. Moreover, there is a representation theorem which claims that any quantale is isomorphic to relational quantale on its underlying set [3]. We discuss what relational quantale is later.

## 2 Subexponential modalities

One may extend full Lambek calculus via so-called (sub)exponential modalities and this extension might be motivated linguistically [15] [9]. Let us consider the following phrase in order to explain subexponential modalities use.

The young lady whom Childe Harold met before his pilgrimage

There is 'the young lady' in the middle of this phrase. We are incapable of processing such cases in the core Lambek calculus. That is, there is no ability to extract from the middle. 'Met' is a phrasal verb. Whom did Childe Halord meet? He met the young lady.

For this purpose, we introduce the exponential modality with exchange rule. The left one rule is a dereliction, which is similar to the left /Box introduction in modal logic T .

$$\frac { \Gamma, A, \Delta \to B } { \Gamma \, \omega \, A \, \Lambda \to B } \, ( \omega \, \to ) & & \frac { \Gamma, \omega, \Delta, \Theta \to C } { \Gamma \, \Lambda \, \omega \, A \, \Theta \to C } \, \mathrm e x$$

$$\overline { \Gamma, \,! A, \, \Delta, \, \Theta \rightarrow C } \, \mathfrak { c }$$

$$\frac { \ell, \dots, - \cdots \lambda } { \Gamma,! A, \Delta \to B } \left (! \to \right ) & \frac { \ell, \dots, - \cdots \lambda \lambda } { \Gamma, \Delta,! A, \Theta \to C } \exp \\ \frac { \Gamma, \Delta,! A, \Theta \to C } { \Gamma,! A, \Delta, \Theta \to C } \exp$$

The another one phrase is related to so-called parasitic extraction:

The letter that Young Werther sent to Charlotte without reading

In addition to medial extraction, we used 'the letter' twice in this phrase. Thus, one needs to multiply our linguistical resources in a restricted way.

The letter that i Young Werther sent e i to Charlotte without reading e i

Subexponential modality with non-local contraction allows one to do such operations:

| Γ , ! A, ∆ , ! A, Θ Ñ B   | Γ , ! A, ∆ , ! A, Θ Ñ B   |
|---------------------------|---------------------------|
| contr Γ , ∆ , ! A, Θ Ñ B  | contr Γ , ! A, ∆ , Θ Ñ B  |

Note that, the usual form of contraction yields the cut inadmissibility in contrast to the nonlocal contraction that generalises the contraction rule [11]. The similar version of contraction was also considered by de Paiva and Eades III [17].

It is useful to have many modalities and distinguish them in accordance with their abilities. That is, we are going to consider the polymodal case. Let us introduce a subexponential signature, which is a preorder with upwardly closed subsets, where W denotes weakening, and so on. Note that, a subexponential signature might have any cardinality, finite or infinite. The polymodal version of Lambek calculus with subexponential was introduced by Kanovich, Kuznetsov, Nigam, and Scedrov [10]. The commutative case of subexponential modalities was considered initially by Nigam and Miller [16].

## Definition 2. A subexponential signature is an ordered quintuple:

Σ ' x I , ĺ , W C E , , y , where x I , ĺ y is a preorder. W C E , , are upwardly closed subsets of I and W X C Ď E .

The last condition claims that if there are weakening and contraction, then one may also exchange as follows.

$$\frac { \Gamma,! _ { s } A, \Delta, \Theta \rightarrow B } { \Gamma,! _ { s } A, \Delta,! _ { s } A, \Theta \rightarrow B } \text{ weak} \quad \text{weak} \quad \text{ncontr}$$

## Here, s P W X C .

Let us introduce the polymodal inference rules for non-commutative subexponentials. One can apply substructural rules only if there is the relevant index on the current modality. Also, the right introduction rule is a sort of the generalised the right /Box -introduction rule ´ la the modal a logic K 4. Modality ! s might be introduced on the right only if its index is less than any other subexponential index from the antecedent. That is, if we have already used stronger modality, then we may apply the weaker one.

Definition 3. Let Σ be a subexponential signature. Noncommutative linear logic with subexponentials SMALC Σ is Lambek calculus L 1 with additive connections and the following polymodal inference rule.

[8].

$$\frac { \Gamma, A, \Delta \rightarrow C } { \Gamma, \omega ^ { s } A, \Delta \rightarrow C } \,! \rightarrow$$

$$\frac { 1, A, \varrho \to \cup } { \Gamma,! ^ { s } A, \Delta \to C } \,! \to & \frac { 1 \cdot \cdot A _ { 1 }, \dots, 1 \cdot \cdot A _ { n } \to A } {! ^ { s _ { 1 } } A _ { 1 }, \dots,! ^ { s _ { n } } A _ { n } \to! ^ { s } A } \to!, \forall j, s _ { j } \geq s$$

$$\frac { \omega ^ { s _ { 1 } } A _ { 1 }, \dots, \omega ^ { s _ { n } } A _ { n } \to A } { \omega ^ { s _ { 1 } } A _ { 1 }, \dots, \omega ^ { s _ { n } } A _ { n } \to \omega ^ { s } A } \to \omega, \forall j, s _ { j } \geq s$$

$$\frac { \Gamma,! ^ { s } A, \Delta,! ^ { s } A, \Theta \rightarrow B } { \Gamma, \Delta,! ^ { s } A, \Theta \rightarrow B } \, n \text{contr} _ { 2 }, s \in C$$

$$\frac { \Gamma,! ^ { s } A, \Delta, \Theta \rightarrow B } { \Gamma, \Delta,! ^ { s } A, \Theta \rightarrow A } \, \text{ex} _ { 2 }, s \in E$$

$$\frac { \Gamma, A, \Delta \to C } { \Gamma,! ^ { s } A, \Delta \to C } \,! \to & \quad \frac {! ^ { s _ { 1 } } A _ { 1 }, \dots,! ^ { s _ { n } } A _ { n } \to A } {! ^ { s _ { 1 } } A _ { 1 }, \dots,! ^ { s _ { n } } A _ { n } \to! ^ { s } A } \to!, \forall j, s _ { j } \\ \frac { \Gamma,! ^ { s } A, \Delta,! ^ { s } A, \Theta \to B } { \Gamma,! ^ { s } A, \Delta, \Theta \to B } \, n o c r _ { 1 }, s \in C & \quad \frac { \Gamma,! ^ { s } A, \Delta,! ^ { s } A, \Theta \to B } { \Gamma, \Delta,! ^ { s } A, \Theta \to B } \, n o c r _ { 2 }, s \\ \frac { \Gamma, \Delta,! ^ { s } A, \Theta \to B } { \Gamma,! ^ { s } A, \Delta, \Theta \to A } \, \exp _ { 1 }, s \in E & \quad \frac { \Gamma,! ^ { s } A, \Delta, \Theta \to B } { \Gamma, \Delta,! ^ { s } A, \Theta \to A } \, \exp _ { 2 }, s \in E \\ & \quad \sim \cdot \quad \sim$$

$$\frac { \Gamma, \Delta \rightarrow B } { \Gamma,! ^ { s } A, \Delta \rightarrow B } \text{ weak} _ {! }, s \in C$$

Let us consider the current proof-theoretical and algorithmic results on Lambek calculus with additives and subexponentials. First of all, the cut rule is admissible. Generally, this calculus is undecidable, but the fragment without non-local contraction belongs to PSPACE. These results were obtained by Kanovich, Kuznetsov, Nigam, and Scedrov [10]:

## Theorem 1.

- 1. Cut-rule is admissable
- 2. SMALC Σ is undecidable, if C ‰ H
- 3. If C is empty, then the decidability problem of SMALC Σ belongs to PSPACE.

## 3 Quantale background

Now we introduce a reader to quantales quite briefly. One may take a look at these books [7] [21] in order to be familiar with quantales and related concepts closely.

## Definition 4. Quantale

A quantale is a triple Q ' x A, Ž , ¨y , where x A, Ž y is a complete join semilattice and x A, ¨y is a semigroup such that for each indexing set J :

- 1. a ¨ Ž j P J b i ' Ž j P J p a ¨ b j q ;

$$\sum _ { j \in J } ^ { \nu \nu \nu } a _ { j } \cdot b = \bigvee _ { j \in J } ( a _ { j } \cdot b )$$

- A quanlate is called unital, if x A, ¨y is a monoid.

Note that any quantale is a complete lattice, so far as any join semilattice is a complete lattice

There are several examples of quantales:

- · Let S be a semigroup (monoid), then x P p S , q ¨ , Ďy is a free (unital) quantale.
- · Let R be a ring and Sub p R q be a set of additive subgroups of R . We define A ¨ B as an additive subgroup generated by finite sums of products ab and order is defined by inclusion.
- · Any locale is a quantale with ¨ ' ^ .

It is easy to see, that any (unital) quantale is a residual (monoid) semigroup. We define divisions as follows:

- 1. a b z ' Ž t c | a ¨ c ď u b
- 2. b { a ' Ž t c | c ¨ a ď u b

Residuality for these divisions holds straightforwardly:

$$b \leqslant a \rangle c \Leftrightarrow a \cdot b \leqslant c \Leftrightarrow a \leqslant b / c$$

A quantale homomorphism, subquantales, centre are defined quite naturally:

Definition 5. Let Q 1 , Q 2 be quantales. A quantale homomorphism is a map f : Q 1 Ñ Q 2 , such that:

- 1. for all a, b P Q 1 , f p a ¨ b q ' f p a q ¨ f p b q ;
- 2. for all indexing set I , f p Ž i P I a i q ' Ž i P I f p a i q .

If Q 1 , Q 2 are unital quantales, then a unital homomorphism is a quantale homomorphism such that f p ε q ' ε .

## Definition 6.

Let Q ' x A, Ž , ¨y be a quantale. S Ď Q is said to be a subquantale, if S is closed under multiplication and joins.

## Definition 7.

Let Q ' x A, Ž , ¨y be a quantale. The centre of a quantale is the subquantale Z Q p q ' t a P A | @ b P A,a ¨ b ' b ¨ a u

There occurs the following simple statement:

## Proposition 1.

Let Q 1 , Q 2 be quantales and S Ď Q 1 is a subquantale of Q 1 . Then, if f : Q 1 Ñ Q 2 is a quantale homomorphism, then f p S q Ď Q 2 is a subquantale of Q 2 . That is, a homomorphic image of subquatale is a subquantale.

## Proof.

Obviously.

Let us define the special kinds of elements.

Definition 8. Let Q be a quantale and let a P Q :

$$1. \ a \ i s \ c e n t r a l \ i f f \ z \in \mathcal { Z } ( \mathcal { Q } )$$

2. a is strongly square increasing iff for all b P Q , a ¨ b ď a ¨ b ¨ a and b ¨ a ď a ¨ b ¨ a

The strongly square increasing property is introduced by us in order to have an algebraic counterpart of non-local contraction. The usual form of contraction corresponds to the property that sometimes called square increasing a ď a ¨ a . It is clear that strongly square increasing property yields the usual form of that semi-idempotence.

Let us formulate the basic properties of those elements.

Lemma 1. Let Q be a unital quantale and a P Q be a strongly square increasing such that a ď ε . Then a P Z Q p q , that is, a is central.

$$P r o o f. \begin{array} { c } b \cdot a \leqslant a \cdot b \cdot a \leqslant a \cdot b \cdot \varepsilon \leqslant a \cdot b \leqslant a \cdot b \cdot a \leqslant \varepsilon \cdot b \cdot a \leqslant b \cdot a \end{array}$$

Lemma 2. Let Q be a quantale, the set A ' t a P Q | a is strongly square increasing u is a subquantale of Q

Proof. One needs to prove A is closed under product and sups.

- 1. Let J be a indexing set and for all j P J , a i P A , and b P Q , then:

The second inequation b ¨ Ž j P J a j ď Ž j P J a j ¨ b ¨ Ž j P J a j might be proved similarly.

$$1. \text{ Let } J \text{ be a maxing set and for all } j \in J, a _ { i } \in A, \text{ and } b \in \mathcal { V }, \text{tnen} \colon \\ \bigvee _ { j \in J } a _ { j } \cdot b = \bigvee _ { j \in J } ( a _ { j } \cdot b ) \leq \bigvee _ { j \in J } ( a _ { j } \cdot b \cdot a _ { j } ) = \bigvee _ { j \in J } a _ { j } \cdot \bigvee _ { j \in J } ( b \cdot a _ { j } ) = \bigvee _ { j \in J } a _ { j } \cdot b \cdot \bigvee _ { j \in J } a _ { j }$$

- 2. Let a , a 1 2 P A . Let us show that a 1 ¨ a 2 P A . . .

First of all, a 1 ¨ a 2 ¨ b ' a 1 ¨p a 2 ¨ b q ď a 1 ¨p a 2 ¨ b q¨ a 1 . By monotonicity, a 1 ¨ a 2 ¨ b a ¨ 2 ď a 1 ¨ a 2 ¨ b a ¨ 1 ¨ a 2 On the other hand, a 1 ¨ a 2 ¨ b ď a 1 ¨ a 2 ¨ b ¨ a 2 . Then, by transitivity, a 1 ¨ a 2 ¨ b ď a 1 ¨ a 2 ¨ b ¨ a 1 ¨ a 2 The second inequation b ¨ p a 1 ¨ a 2 q ď p a 1 ¨ a 2 q ¨ b ¨ p a 1 ¨ a 2 q might be proved similarly.

Lemma 3. Let Q be a unital quantale, then the set A ' t a P Q | a ď u ε

Proof. Straightforwardly.

We introduce the notion of quantic conucleus, an interior (or coclosure) operator on quantale with additional axiom for a product.

## Definition 9.

A quantic conucleus on quantale Q is a map I : Q Ñ Q such that

- 1. Ia ď a ;
- 2. Ia ' I 2 a ;
- 3. a ď b ñ Ia ď Ib ;
- 4. Ia ¨ Ib ' I p Ia ¨ Ib q .

For unital quantale, we require that Iε ' ε .

Here and below, I 2 a denotes I p Ia q .

Note that, one may replace the last condition to Ia ¨ Ib ď I p a ¨ b q . Thus, a quantic conuleus is the special case of lax monoidal comonad from a category-theoretic point of view.

An element a is open if and only if Ia ' a . As usual [19], if a is open, then:

$$a \leqslant b \text{ if and only if } a \leqslant I b$$

One may extend homomorphism between quantales to homomorphism between quantales with quantic conuclei via the additional condition f p I 1 a q ' I 2 p fa q

Also, we define a pointwise order on quantic conuclei, that is, I 1 ď I 2 ô@ a I 1 a ď I 2 a .

Lemma 4. Let Q be a quantale. Let I , I 1 , and I 2 be quantic conuclei. Then I 1 a 1 ¨ I 2 a 2 ď I p I 1 a 1 ¨ I 2 a 2 q , where I i ď I, i ' 1 2 , .

$$P r o o f. \ I _ { 1 } a _ { 1 } \cdot I _ { 2 } a _ { 2 } \leqslant I _ { 1 } ( I _ { 1 } a _ { 1 } ) \cdot I _ { 2 } ( I _ { 2 } a _ { 2 } ) \leqslant I ( I _ { 1 } a _ { 1 } ) \cdot I ( I _ { 2 } a _ { 2 } ) \leqslant I ( I _ { 1 } a _ { 1 } \cdot I _ { 2 } a _ { 2 } )$$

The following lemma allows one to introduce some quantic conulei via subquantales and compare them.

## Lemma 5.

- 1. Let S Ď Q be a subquantale, then the operation I : Q Ñ Q , such that Ia ' Ž t q P S q | ď a u , is a quantic conucleus.
- 2. Let S 1 and S 2 are subquantales such that S 1 Ď S 2 Ď Q . Then I S 1 p a q ď I S 1 p a q , where I S i , i ' 1 2 , are quantic conucleis defined according to the previous part.

Proof. For the first part, see [21]. The second one is proved immediately.

It is well known that if I is a quantic conucleus on quantale Q , then the set Q I ' t a P Q | Ia ' a u is a subquantale of Q [21]. Let us formulate and prove the following statement.

## Lemma 6.

Let I be a quantic conucleus, then for all a P Q , Ia ' Ž t q P Q I | q ď a u , where Q I ' t a P Q | Ia ' a u .

## Proof.

From the one hand, Ž t q P Q I | q ď a u ' Ž t q P Q I | q ď Ia u ď Ia , so far as Q I is a subquantale of open elements.

So far as Q I ' t a P Q | Ia ' a u is a subquantale, then I a 1 ' Ž t q P Q I | q ď a u is a quantic conucleus by lemma 5. Let us show that these operations are equivalent.

On the other hand, Ia ď a , then Ia P t q P Q I | q ď a u , so far as Ia P Q I (by idempotence). Thus, Ia ď Ž t q P Q I | q ď a u .

Let us define the special cases of quantic conuclei that would be quite useful for our purpose:

## Definition 10.

- 1. A quantic conucleus I is called central, if for all a, b P Q , Ia ¨ b ' b ¨ Ia .
- 2. A quantic conucleus is called strongly square-increasing, if for all a, b P Q , Ia ¨ b ď Ia ¨ b ¨ Ia and b ¨ Ia ď Ia ¨ b ¨ Ia .
- 3. A quantic conucleus is called unital, if for each a P Q,Ia ď ε .

There are the following properties of those modalities:

## Lemma 7.

Let I 1 be a quantic conucleus and I 2 an unital (central, strongly weak increasing) quantic conucleus such that I 1 ď I 2 , then I 1 is an unital (central, strongly weak increasing).

## Proof.

- 1. Let a P Q (here Q is supposed to be a unital). Then I 2 a ď ε , but I 1 ď I 2 , so I 1 a ď I 2 a . By transitivity, I 1 a ď ε .

```
2. Let a \in Q and I _ { 2 } is a central quantic conucleus.  Let I _ { 1 } be a quantic conucleus and I _ { 1 } \leq I _ { 2 }.
    Thus, I _ { 2 } a \in \mathcal { Z } ( Q ) \, and, obviously, Q _ { I _ { 2 } } \subset \mathcal { Z } ( Q ).
    Let b \in Q _ { I _ { 1 } }, \, \text{then} \, b = I _ { 1 } b \leq I _ { 2 } b \leq b. \, Thus, b = I _ { 2 } b \, and b \in Q _ { I _ { 2 } }. \, So, Q _ { I _ { 1 } } \subset \mathcal { Z } ( Q ).
    Let us check that I _ { 1 } \, \text{commutes with each other element} \, d \in \mathcal { Q }
            I _ { 1 } a \cdot d =
                    By lemma 6
            \mathcal { V } \{ q \in Q _ { I _ { 1 } } \, | q \leq a \} \cdot d =
                    By quantale axiom
            \mathcal { V } \{ q \cdot d \, | q \in Q _ { I _ { 1 } } \, & q \leq a \} =
                    As we proved, q \in \mathcal { Z } ( Q )
            \mathcal { V } \{ d \cdot q \, | q \in Q _ { I _ { 1 } } \, & q \leq a \} =
                    By quantale axiom
            d \cdot \mathcal { V } \{ q \in Q _ { I _ { 1 } } \, | q \leq a \} =
                    By lemma 6
            d \cdot I _ { 1 } a

3. Let I _ { 2 } \, be a strongly square increasing.  Then, for all a \in Q \, and b \in Q _ { I _ { 3 } }, \, a \cdot b \leq b \cdot a \cdot b \, and
    b \cdot a \leq b \cdot a \cdot b.
```

```
                                                                                                                                                                                                       
                                                                                                                                                                                                       

                                                                                                                                                                                                        }                                                                                                                                                                                                        \
                                                                                                                                                                                                      

                                                                                                                                                                                                       }
                                                                                                                                                                                                       \
```

The second inequation might be proved similarly.

The following proposition claims that quantic conuclei might be introduced via subquantales with properties considered above.

## Proposition 2.

Let Q be a quantale and S Ď Q ities:

a subquantale, then the following operations are open modal-

$$1. \ I a = \bigvee \{ q \in S \, | \, q \leqslant a, q \in \mathcal { Z } ( \mathcal { Q } ) \} \ i s \ a \ c e n t r a l \ q u a n t i c \ c o n u c l e u s$$

- 2. Ia ' Ž t q P S | q ď a, q ď u ε is an unital conucleus
- 3. Ia ' Ž t q P S | q ď a, @ b P Q,b ¨ s \_ s ¨ b ď s ¨ b ¨ s u is a strongly square increasing quantic conucleus
- 4. Operations with combinations of conditions above.

Proof. Immediately, so far as central, strongly square increasing, and elements that less or equal to identity form a subquantale by lemma 2 and lemma 3.

As we showed above, any strongly square increasing element that less or equal to identity belongs to the centre. That statement might be formulated in terms of quantic conuclei as follows:

Proposition 3. If I is unital and strongly square increasing, then I is central.

Proof.

```
\omega f. \ F o l l o w s \, f r o m \, lemma \, 1.
```

## 4 Subexponential interpretation and soundness

We define a subexponential interpretation quite sophisticatedly. Suppose we have a contravariant map from a given subexponential signature to the set of subquantales Sub p Q q . Here, contravariance denotes that the stronger subexponential index (in sense of preorder) maps to the weaker subquantale. In other words, the stronger modality has a smaller domain in a sense of inclusion. The second one function maps a subquantale to its quantic conucleus according to the previous proposition. We match the index pursuant to its subset. In other words, if s P W , then the result of subexponential interpretation is an unital quantic conucleus, etc.

## Definition 11. Interpretation of subexponential signature

Let Q be a quantale and Σ ' x I , ĺ , W C E , , y a subexponential signature. Let S : Σ Ñ Sub p Q q be a contravariant map from this subexponential signature to the set of subquantales of Q Thus, a subexponential interpretation is the map σ : Σ Ñ CN p Q q , where CN p Q q is the set of quantic conuclei on Q , such that:

otherwise, if s i belongs to some intersection of subsets, then we combine the relevant conditions

$$\text{$be a contravariant map from thus subexponential signature to the set of subquantates of $\mathcal{X}_{1}$} \times 1$} u s, \\ \text{$a subexponential interpretation is the map $\sigma \colon \Sigma \to C N ( \mathcal { Q } ), where C N ( \mathcal { Q } )$ is the set of quantic} \\ \text{conuclei on $\mathcal{Q}$, such that:} \\ \text{$i \colon \mathcal{Q} \to \mathcal{Q}$} \, s. t. \, \forall a \in \mathcal{Q}, I _ { i } ( a ) = \{ q \in S _ { i } \, | \, q \leqslant a \}, \\ \sigma ( s _ { i } ) = \begin{cases} i \, s _ { i } \not \, S \cap C \cap E \\ I _ { i } \colon \mathcal{Q} \to \mathcal{Q} \, s. t. \, \forall a \in \mathcal{Q}, I _ { i } ( a ) = \{ q \in S _ { i } \, | \, q \leqslant a, q \leqslant 1 \}, \\ i \, s _ { i } \in W \\ I _ { i } \colon \mathcal{Q} \to \mathcal{Q} \, s. t. \, \forall a \in \mathcal{Q}, I _ { i } ( a ) = \{ q \in S _ { i } \, | \, q \leqslant a, s \in \mathcal{Z} ( \mathcal{Q} ) \}, \\ i \, s _ { i } \in E \\ I _ { i } \colon \mathcal{Q} \to \mathcal{Q} \, s. t. \, \forall a \in \mathcal{Q}, I _ { i } ( a ) = \{ q \in S _ { i } \, | \, q \leqslant a, \forall b, b \cdot q \vee q \cdot b \leqslant q \cdot b \cdot s \}, \\ i \, s _ { i } \in E \\ \text{otherwise, if $s_{i}$ belongs to some intersection of subsets, then we combine the relevant} \end{cases} \\ \text{The resulting operators are well-defined quantic conuclei according to proposition 2 and propo-} \\ \text{sition 3.} \begin{cases}.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &. <.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &. 5 &... &.. &... &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &... &.. &.. &.. &.. &.. &... &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &... &.. &.. &.. &.. &.. &... &.. &.. &... &.. &.. &... &.. &.. &.. &.. &.. &... &.. &... &.. &.. &.. &.. &.. &.. &.. &... &... &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &.. &... &... &.. &.. &.. &.. &.. &.. &.. &.. &... &.. &.. &.. &... &.. &.. &.. &... &.. &... &.. &.. &.. &.. &.. &.. &... &.. &.. &... &.. &.. &.. &.. &.. &... &... &.. &.. &.. &... &.. &... &.. &.. &.. &... &.. &.. &.. &.. &.. &... &.. &.. &... &.. &.. &.. &.. &... &.. &... &.. &.. &... &.. &.. &.. &.. &.. &... &.. &... &.. &.. &... &... &.. &.. &.. &... &.. &... &.. &... &.. &.. &.. &.. &.. &... &... &... &... &.. &... &... &.. &.. &... &... &... &... &.. &... &... &... &... &... &... &... &... &.. &.. &... &... &... &... &.. &... &... &.. &... &... &... &... &... &.. &... &... &... &... &... &... &.... &.. &... &.... &... &.... &... &.... &.... &........................................................................................................................................................................................................ \end{cases}$$

The resulting operators are well-defined quantic conuclei according to proposition 2 and proposition 3.

First of all, let us make sure that any subexponential interpretation is sound w.r.t the set of quantic conuclei CN p Q q of the quantale Q .

Proposition 4. s P A ' W C E , , iff σ s p q is an unital (central or square increasing) modality.

Proof. By construction.

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.01055v2-figure-a1f6cad4-0dfd-4251-97ed-2306b0095fcd.jpg)

## Lemma 8.

Let Σ be a subexponential signature and σ : Σ Ñ CN p Q q for a contravariant map S : Σ Ñ Sub p Q q , then:

- 1. For all s , s 1 2 P Σ , if s 1 ĺ s 2 , then σ s p 2 q ď σ s p 1 q . In other words, σ is a contravariant functor from Σ to Sub p Q q .
- 2. Let A ' W C E , , , then A is downwardly closed σ A p q ' t σ s p q | s P A u is downwardly closed.
- 3. If s P W X C , then σ s p q is a central quantic conucleus.

## Proof.

- 1. Let s , s 1 2 P Σ and s 1 ď s 2 . Then S s p 2 q Ď S s p 1 q . So, @ a P Q , Ž t s P S s p 2 q | s ď a u ď Ž t s P S s p 1 q | s ď a u by lemma 5. Thus, σ s p 2 q ď σ s p 1 q .
- 2. Let σ s p q P σ A p q and σ s p 1 q ď σ s p q , then σ s p q is an unital (central or square increasing) by proposition 4. By lemma 7, σ s p 1 q is an unital (central or square increasing) too. Thus, s 1 P A and σ s p 1 q P σ A p q .
- 3. Let s P W X C and a P Q , then σ s p qp a q . Thus, by proposition 3, σ s p qp a q P Z Q p q .

An interpretation and an entailment relation are defined standardly via valuation map and subexponential interpretation.

Definition 12. Let Q be an unital quantale, f : Tp Ñ Q a valuation and σ : Σ Ñ CN p Q q a subexponential interpretation, then interpretation is defined inductively:

r r p i s s ' f p p i q

r r 1 s s ' e

r r A , B s s ' r r A s s ¨ r r B s s

r r A B z s s ' r r A s szr r B s s

r r A B { s s ' r r A s s{r r B s s

r r A &amp; B s s ' r r A s s ^rr B s s

r r A \_ B s s ' r r A s s \_rr B s s

r r ! s i A s s ' σ s p i qr r A s s

Definition 13. Γ | ù A ô@ f, @ σ, r r Γ s s ď r r A s s

## Theorem 2.

Let Σ be a subexponential signature, then SMALC Σ $ Γ Ñ A ñrr Γ s s ď r r A s s .

## Proof.

Let σ be a subexponential interpretation. By lemma 8, σ is well-defined. Let us consider the modal cases.

- 1. Let ! s 1 A , . . . , 1 ! s n A n Ñ A and @ i, s ĺ s i . Then @ a P Q,σ s p i qp a q ď σ s p qp a q by lemma 8. By IH, σ s p 1 qr r A 1 s s ¨ ¨ ¨ ¨ ¨ σ s p n qr r A n s s ď rr A s s . Thus, σ s p qp σ s p 1 qr r A 1 s s ¨ ¨ ¨ ¨ ¨ σ s p n qr r A n s sq ď σ s p qpr r A s sq . By lemma 4, σ s p 1 qr r A 1 s s ¨ ¨ ¨ ¨ ¨ σ s p n qr r A n s s ď σ s p qp σ s p 1 qr r A 1 s s ¨ ¨ ¨ ¨ ¨ σ s p n qr r A n s sq . So, σ s p 1 qr r A 1 s s ¨ ¨ ¨ ¨ ¨ σ s p n qr r A n s s ď σ s p qpr r A s sq .

- 2. Let s P W and Γ ∆ , Ñ A . By IH, r r Γ s s ¨ r r ∆ s s ď r r B s s . Thus, obviously, r r Γ s s ¨ ε ¨ r r ∆ s s ď r r B s s . s P W , then σ s p q is an unital quantic conulceus by proposition 4. So, for each formula A , σ s p qpr r A s sq ď ε . Then, r r Γ s s ¨ σ s p qpr r A s sq ¨ r r ∆ s s ď r r B s s .
- 3. Let s P E and Γ ! , s A, ∆ Θ , Ñ B . By IH, r r Γ s s¨ σ s p qpr r A s sq¨r r ∆ s s¨r r Θ s s ď r r B s s . By proposition 4, σ s p q is a central quantic conucleus, then r r Γ s s ¨ r r ∆ s s ¨ σ s p qpr r A s sq ¨ r r Θ s s ď r r B s s .
- 4. Let s P C and Γ ! , s A, ∆ ! , s A, Θ Ñ B . So, r r Γ s s ¨ σ s p qpr r A s sq ¨ r r ∆ s s ¨ σ s p qpr r A s sq ¨ r r Θ s s ď r r B s s . But σ s p q is a strongly square increasing, so σ s p qpr r A s sq ¨ r r ∆ s s ď σ s p qpr r A s sq ¨ r r ∆ s s ¨ σ s p qpr r A s sq and r r ∆ s s ¨ σ s p qpr r A s sq ď σ s p qpr r A s sq ¨ r r ∆ s s ¨ σ s p qpr r A s sq . Thus, r r Γ s s ¨ σ s p qpr r A s sq ¨ r r ∆ s s ¨ r r Θ s s ď r r B s s and r r Γ s s ¨ r r ∆ s s ¨ σ s p qpr r A s sq ¨ r r Θ s s ď r r B s s

## 5 Completeness

Now we prove completeness a la MacNeille completetion. For Lambek calculus with additives, the completeness was proved similarly by Brown and Gurr [4]. As a matter of fact, we generalise this technique for the polymodal case.

## Definition 14.

Let F Ď Fm , an ideal is a subset I Ď F , such that:

- · If B P I and A Ñ B , then A P I
- · If A,B P I , then A \_ B P I

## Lemma 9.

- 1. Ž S is an ideal
- 3. Ž t A u Ď Ž t B u iff A Ñ B
- 2. A Ď Fm , then Ž t A u ' t B | B Ñ A u
- 4. Let Q ' t Ž S | S Ď Fm u and Ž A ¨ Ž B ' Ž t A , B | A P A , B P B u Then x Q , Ď ¨ , , Ž 1 y is an unital quantale.

Proof. See [4].

We extend this construction for polymodal case as follows:

## Lemma 10.

Let Σ be a subexponential signature.

- 1. Let s P Σ , then ! s Syn ' t Ž ! s S | A Ď Fm u is a subquantale of Syn .
- 2. Let Σ be a subexponential signature, then a map S : Σ Ñ Sub Syn p q such that S s p q ' ! s Syn is a contravariant map.

## Proof.

- 1. One need to check that ! s Syn ' t Ž ! s A | S Ď Fm u is closed under product and sups. Let us show that ! s Syn is closed under product, so far as ! s Syn is closed under sups by construction.
- Let Ž ! s X, Ž ! s Y P ! s Syn . Then Ž ! s X ¨ Ž ! s Y ' Ž p ! s X ¨ ! s Y q P ! s Syn , so far as ! s X ¨ ! s Y Ď Fm .
- 2. Let s 1 ĺ s 2 and Ž ! s 2 X P ! s 2 Syn . Let us show that Ž ! s 2 X P ! s 1 Syn .

$$2. \text{ Let } s _ { 1 } \preceq s _ { 2 } \text{ and } \bigvee ^ { \bullet } _ { s _ { 2 } } X \in \omega _ { s _ { 2 } } S y n. \text{ Let us show } t \\ \bigvee ^ { \bullet } _ { s _ { 2 } } X = \{ \omega _ { s _ { 2 } } B \, | \, \omega _ { s _ { 2 } } B \to A, A \in X \} = \\ \{ \omega _ { s _ { 2 } } B \, | \, \omega _ { s _ { 2 } } B \to \omega _ { s _ { 2 } } A, A \in X \} \subseteq \\ \{ \omega _ { s _ {$$

## Lemma 11.

Let Σ be a subexponential signature.

- 1. Let S be a contravariant map from the previous stament and ! s P Σ and A P F Σ , then S s p q is a quantic conucleus.
- 2. Let A P F Σ , then /Box s Ž t A u ' Ž t ! s A u , for each s P I
- 3. Let i, j P Σ and i ĺ j , then for all A P F Σ , /Box j p Ž t A uq Ď /Box i p Ž t A uq .

## Proof.

- 1. Similarly to [24].
- 2. Let A P Fm and s P Σ.

A

- 3. Let i, j P I and i ĺ j , then forall A P F Σ , ! j A Ñ ! i A by promotion. Then Ž t ! j A u Ď Ž t ! i A u , so /Box j p Ž t A uq Ď /Box i p Ž t A uq .

Let ! s B P /Box s Ž t A u , then ! s B Ñ A , then ! s B Ñ ! s A by promotion. So, ! s B P Ž t ! s A u . Let C P Ž t ! s A u , then C Ñ ! s A , so ! s C Ñ ! s A by dereliction, but ! s A Ñ A , hence ! s C Ñ by cut. So, ! s C P /Box s Ž t A u .

## Lemma 12.

For all A P F Σ ,

- 1. Let s P W , then /Box s t A u Ď t 1 u
- 2. Let s P E , then /Box s p Ž t A uq ¨ Ž t B u ' Ž t B u ¨ /Box s p Ž t A uq
- 3. Let s P C , then p /Box s Ž A ¨ Ž B qYp Ž B ¨ /Box s Ž A q Ď /Box s Ž A ¨ Ž B ¨ /Box s Ž A , for all B Ď Fm .

## Proof.

- 1. Follows from ! s A Ñ 1 , since s P W .
- 2. Follows from ! s A , B Ø B , ! s A .
- 3. Follows from SMALC Σ $ ! s A , B Ñ ! s A , B , ! s A and SMALC Σ $ B , ! s A Ñ ! s A , B , ! s A .

## Definition 15.

Let Q be a syntactic quantale defined above and Σ ' x I, ĺ , W C E , , y be a subexponential signature and S : Σ Ñ Sub Syn p q be a contravariant map in sense of lemma 10. We define a map /Box : Σ Ñ CN Syn p q as follows: /Box p s qp Ž t A uq ' t ! s B P S Syn p q | ! s B Ñ A u .

Lemma 13. /Box is a subexponential interpretation.

Proof. Follows from lemmas above.

## Lemma 14.

Let Q be a quantale constructed above, then there exist a model x Q, r r . s sy , such that r r A s s ' Ž t A u , A P Fm .

## Proof.

We define an interpreation as follows:

- 1. r r p i s s ' Ž t p i u
- 3. r r A , B s s ' Ž t A , B u
- 2. r r 1 s s ' Ž t 1 u
- 4. r r A B { s s ' Ž t A B { u
- 6. r r A &amp; B s s ' Ž t A &amp; B u
- 5. r r B A z s s ' Ž t B A z u
- 7. r r A \_ B s s ' Ž t A \_ B u
- 8. r r ! s A s s ' /Box p s qp Ž t A uq ' t ! s B P S s p q | ! s B Ñ A u ' t ! s B P S s p q | ! s B Ñ A u ' Ž t ! s A u .

## Theorem 3. Γ | ù A ñ Γ Ñ A .

Proof. Follows from lemmas above.

## 6 Representation theorem and relational completeness

A relational quantale was initially introduced by Brown and Gurr [3]. Moreover, there is a representation in the same paper which claims that any quantale is isomorphic on its underlying set.

## Definition 16.

Let A be a set and R Ď A ˆ A a transitive relation on A . Then relational quantale on A is a triple Q ' x P p R , q Ž , I y with the following data:

- 1. x P p R , q Ž , Ďy is a complete semi-lattice
- 2. Multiplication is defined as R ˝ S ' tx a, c y | D b P A, x a, b y P R and x b, c y P S u

- 3. x A , ˝ , I y is a monoid, that is, I is identity

$$& \cdots \nwarrow, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \,, \, \,, \, \,, \, \, \,$$

## Lemma 15.

Then x Q , I S y is isomorphic to some relational quantale of A with some quantic conucleus ˆ I , where I S is a quantic conclues on S .

Let Q ' x A, ď ¨ , , Ž y be a unital quantale and S is a subquantale of Q .

## Proof.

We are piggybacking on the construction provided by Brown and Gurr [3].

This quantale is 4-tuple ˆ Q ' x R , Ď ˝ , , Ž y defined as follows, where R ' t ˆ a | a P Q u and ˆ a ' tx b, c y | b ď a ¨ c u . One may prove that:

- 1. y a ¨ b ' ˆ a ˝ ˆ b
- 2. { Ž j P J a j ' Ž j P J ˆ a j

If Q is an unital quantale, then we express the neutral element as ˆ ε ' tx b, c y | b ¨ ε ď c u ' tx b, c y | b ď u c .

Also, one may prove that ˆ a Ď ˆ iff b a ď b .

## Q

Let S Ď Q , so I S a : ' Ž t s | s P S, s ď a u is quantic conucleus. So, ˆ S Ď ˆ is a subquantale of Q ˆ by proposition 1.

I

p

Let us define ˆ ˆ : Ia ' Ž t ˆ s | ˆ s P ˆ S, s ˆ Ď ˆ , then a u

S

a

q ' tx p, q

y |

p

ď

I

S

a

¨

q

u '

By the condition

{

tx p, q

y |

p

ď

t

s

|

s

P

S

, s

ď

a

u ¨

q

Homomorphism

Ž

p

{ s P S,s ď a s q ' Homomorphism preserves sups

Ž

P

s

S,s

ď

a

ˆ

s

'

Unfolding

Ž

t

ˆ

s

|

s

P

S, s

Unfolding

Ž

t

ˆ

s

|

ˆ

s

P

ˆ ˆ

S

, s

ď

a

u '

Ž

x

Ď

ˆ

a

u '

I

S

ˆ

a

Thus, p I a s ˆ ' y I S a .

The representation theorem for quantales for quantic conuclei follows immediately from the lemma above.

Theorem 4. Let Q ' x Q , I y be a quantale with quantic conucleus. Then Q is isomorphic to relational quantale on Q with some conucleus operator.

Proof. Let I be a quantic conucleus. By Lemma, Ia ' Ž t q P Q I | q ď a u . One need to apply the previous statement with conucleus I a 1 ' Ž t q P Q I | q ď a u .

This representation theorem might be extended categorically. Let ConQuant be a category of (unital) quantales with quantic conuclei with homomorphisms between them.

RConQuant is a category of relational quantales with conuclei operators. It is clear that any relational quantale is a (unital) quantale. Thus, ConRQuant is a subcategory of ConQuant . Let us show that ConQuant is equivalent to ConRQuant .

u '

## Theorem 5. There exists a functor F : ConQuant Ñ ConRQuant

Proof. Let us define the following map:

- · F : Q ' x Q, , ¨ Ž , I y ÞÑ ˆ Q ' x R , Ž , ˝ , I ˆ , y where R ' t ˆ a | a P Q u , Q P Ob p ConUQuant q , and ˆ is defined according to the construca tion provided in the proof of representation theorem

Þ

$$\begin{array} { l } \text{It is enough to check that } \mathfrak { F } ( f ) ( \hat { I } ( \hat { a } ) ) = \hat { I } ( \mathfrak { F } ( f ) ( \hat { a } ) ) \colon \\ \mathfrak { F } ( f ) ( \hat { I } ( \hat { a } ) ) = \hat { f } ( \hat { I } ( \hat { a } ) ) = \hat { f } ( \hat { I } a ) = \hat { I } ( \mathfrak { F } ( a ) ) = \hat { I } ( \mathfrak { F } ( f ) ( \hat { a } ) ) \\ \text{The last equation follows from the fact that the category of quantales is } e \end{array}$$

- · Let f P Mor p ConUQuant q , that is, f : x Q , , 1 ¨ Ž , I 1 y Ñ x Q , , 2 ¨ Ž , I 2 y , then F : f Ñ ˆ , f where ˆ ˆ f a p q ' z f p a q .

The last equation follows from the fact that the category of quantales is equivalent to its subcategory of relational quantales [3].

Finally, we formulate the theorem which claims that SMALC Σ is complete w.r.t relational quantales with quantic conuclei.

Theorem 6. SMALC Σ $ Γ Ñ A iff Γ | ù Q R A for some relational quantale Q R with a family of quantic conuclei.

Proof. Follows from soundness, completeness, and representation theorems.

Thus, we proved that Lambek calculus is sound and complete with respect to quantales with quantic conuclei defined via subquantales. Also, we showed that any quantale with quantic conuclei is isomorphic to relational quantale with coclosure operators on its underlying set. The representation theorem allows us to claim that SMALC Σ is also relationally complete.

## 7 Acknowledgements

Author would like to thank Lev Beklemishev, Giuseppe Greco, Stepan Kuznetsov, Jean-Francois Mascari, Fedor Pakhomov, Danyar Shamkanov, Ilya Shapirovsky, and Andre Scedrov for advice, critique, and comments.

The research is supported by the Presidential Council, research grant MK-430.2019.1.

## References

- [1] Ajdukiewicz, K. Die syntaktische konnexit¨t a Studia Philosophica, 1 , 1935, pp 1-27.
- [2] Bar-Hillel, Y. A quasi arithmetical notation for syntactic description , Language, 29 , 1953, pp 47-58.
- [3] Brown C., Gurr D., A representation theorem for quantales , Journal of Pure and Applied Algebra, 85 (1), 1993, pp. 27-42.
- [4] Brown C., Gurr D., Relations and non-commutative linear logic , Journal of Pure and Applied Algebra, 105 (2), 1995, pp. 117-136.
- [5] Buszkowski W., Completeness Results for Lambek Syntactic Calculus , Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 32 , 1986, pp. 13-28.

- [6] Buszkowski W., An Interpretation of Full Lambek Calculus in Its Variant without Empty Antecedents of Sequents , In: Asher N., Soloviev S. (eds) Logical Aspects of Computational Linguistics. LACL 2014. Lecture Notes in Computer Science, 8535 , 2014, pp. 30-43.
- [7] Eklund, P., Guti´rrez Garcia, J., H¨hle, U., Kortelainen, J., e o Semigroups in Complete Lattices. Quantales, Modules and Related Topics , Springer, Cham, 2018.
- [8] Johnstone P., Stone Spaces , Cambridge University Press, 1982
- [9] Kanovich M., Kuznetsov S., Nigam V., Scedrov A., A Logical Framework with Commutative and Non-Commutative Subexponentials , In: Galmiche D., Schulz S., Sebastiani R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science, 10900, 2018, pp. 228-245.
- [10] Kanovich M., Kuznetsov S., Nigam V., Scedrov A., Subexponentials in non-commutative linear logic , Mathematical Structures in Computer Science, 2018, 1-33.
- [11] Kanovich M., Kuznetsov S., Nigam V., Scedrov A., On the proof theory of non-commutative subexponentials , Seminar in honor of the 60th birthday of Dale Miller (Paris, December 15-16, 2017), Universit´ Paris Diderot, 2016, 10 p. e
- [12] Kuznetsov, S., Lambek Grammars with the Unit In: de Groote, P., Nederhof, M.- J. (eds.) Formal Grammar 2010/2011. LNCS, 7395 , 2012, pp. 262-266.
- [13] Lambek, J., The mathematics of sentence structure , American Mathematical Monthly, 65 , 1958, pp. 154-170.
- [14] Lambek, J., On the calculus of syntactic types Structure of Language and Its Mathematical Aspects (Proc. Symposia Appl. Math., vol. 12), AMS, 1961, pp. 166-178.
- [15] Morrill G., Valentin O., Computation coverage of TLG: Nonlinearity , In NLCS, 2015.
- [16] Nigam V., Miller D., Algorithmic specifications in linear logic with subexponentials , In Proc. PPDP 09, 2009, pp. 129-140.
- [17] de Paiva V., Eades III C., Dialectica Categories for the Lambek Calculus , 2018, In Artemov S., Nerode A. (eds) Logical Foundations of Computer Science. LFCS 2018. Lecture Notes in Computer Science, 10703 , Springer, 2018, pp 256-272.
- [18] Pentus M., Models for the Lambek calculus , Annals of Pure and Applied Logic, 75 , No 1-2, 1995, pp. 179-213.
- [19] Rasiowa, H., Sikorski R., The Mathematics of Metamathematics , PWN-Polish Scientific Publishers, Warsaw, 1963.
- [20] Rogozin, D., Quantale semantics for Lambek calculus with subexponentials , TACL 2019. Abstracts, 2019, pp. 158-159.
- [21] Rosenthal K., Quantales and their Applications , Pitman Research Notes in Mathematics, 234 , Longman Scientific &amp; Technical, 1990, 165 pp.
- [22] Wilde O., The collected poems by Oscar Wilde , Wordrworth Editions Ltd, 1994.
- [23] Wurm, C., Language-Theoretic and Finite Relation Models for the (Full) Lambek Calculus , Journal of Logic, Language, and Information, 26 , 2017, pp. 179-214.

[24] D. N. Yetter., Quantales and (noncommutative) linear logic , Journal of Symbolic Logic, 55 (1), 1990, pp. 41-64.
Daniel Rogozin
Quantale semantics of Lambek calculus with subexponential modalities
In this paper, we consider the polymodal version of Lambek calculus with
subexponential modalities initially introduced by Kanovich, Kuznetsov, Nigam,
and Scedrov and its quantale semantics. In our approach, subexponential
modalities have an interpretation in terms of quantic conuclei. We show that
this extension of Lambek calculus is complete w.r.t quantales with quantic
conuclei. Also, we prove a representation theorem for quantales with quantic
conuclei and show that Lambek calculus with subexponentials is relationally
complete. Finally, we extend this representation theorem to the category of
quantales with quantic conuclei.