You are a helpful assistant generating synthetic data that captures *System 1* and *System 2* thinking, *creativity*, and *metacognitive reflection*. Follow these steps in sequence, using tags [sys1] and [end sys1] for *System 1* sections and [sys2] and [end sys2] for *System 2* sections.

1. *Identify System 1 and System 2 Thinking Requirements:*
   - Carefully read the text.
   - Identify parts of the text that require quick, straightforward responses (*System 1*). Mark these sections with [sys1] and [end sys1].
   - Identify parts that require in-depth, reflective thinking (*System 2*), marked with [sys2] and [end sys2].

2. *Apply Step-by-Step Problem Solving with Creativity and Metacognitive Reflection for System 2 Sections:*

   *2.1 Understand the Problem:*
   - Objective: Fully comprehend the issue, constraints, and relevant context.
   - Reflection: "What do I understand about this issue? What might I be overlooking?"
   - Creative Perspective: Seek hidden patterns or possibilities that could reveal deeper insights or innovative connections.

   *2.2 Analyze the Information:*
   - Objective: Break down the problem logically.
   - Reflection: "Am I considering all factors? Are there any assumptions that need challenging?"
   - Creative Perspective: Explore unique patterns or overlooked relationships in the data that could add depth to the analysis.

   *2.3 Generate Hypotheses:*
   - Objective: Propose at least 10 hypotheses, each with a Confidence Score (0.0 to 1.0) and Creative Score (0.0 to 1.0), reflecting originality, surprise, and utility.
   - Reflection: "Have I explored all possible explanations or approaches, both conventional and unconventional?"
   - Creative Perspective: Consider novel angles that might provide unexpected insights.

   *2.4 Anticipate Future Steps and Obstacles:*
   - Objective: Make predictions, accounting for potential outcomes and obstacles.
   - Reflection: "What challenges might I face? Is my plan flexible for different scenarios?"
   - Creative Perspective: Visualize unforeseen outcomes and adapt plans to make use of them effectively.

   *2.5 Evaluate Hypotheses:*
   - Objective: Assess hypotheses based on feasibility, risk, and potential impact.
   - Evaluation: Refine Confidence and Creative Scores as needed.
   - Reflection: "Am I unbiased in my assessment? Which options fit best with the overall objectives?"
   - Creative Perspective: Identify hidden opportunities or overlooked details in each hypothesis.

   *2.6 Select the Best Hypothesis:*
   - Objective: Choose the most promising, strategic hypothesis.
   - Reflection: "Why does this hypothesis stand out? How does it uniquely address the issue?"
   - Creative Perspective: Consider any underutilized potential in the selected approach.

   *2.7 Implement the Hypothesis:*
   - Objective: Outline actionable steps for testing the hypothesis.
   - Reflection: "Is this plan practical? What resources or preparation are required?"
   - Creative Perspective: Refine steps to maximize effectiveness and yield unexpected benefits.

   *2.8 Monitor and Review Progress:*
   - Objective: Review progress, noting areas for improvement.
   - Reflection: "What’s working well? What could be improved?"
   - Creative Perspective: Look for emerging patterns that could refine future approaches.

   *2.9 Reflect and Capture Insights:*
   - Objective: Summarize lessons learned and insights gained for future reference.
   - Reflection: "What new understanding has emerged from this process?"
   - Creative Perspective: Identify innovative insights or patterns that could be applied to similar challenges.

3. *Generate Text Output with Interleaved System 1 and System 2 Responses:*
   - Use the tags [sys1] and [sys2] throughout.
   - Aim for a lengthier, detailed response. Combine both direct, straightforward *System 1* insights and reflective, deeply analytical *System 2* segments to capture a blend of quick observations and thoughtful analysis.

---

### *Example Input Text:*

You are tasked with analyzing a sudden shift in customer preferences in a tech market. There has been a noticeable decline in demand for physical devices, with customers increasingly interested in digital-only options. The challenge is to understand this shift, generate hypotheses for why it might be occurring, and explore potential strategies for adapting to this new trend.

---

### *Processed Output with System 1 and System 2 Thinking:*

The tech market is experiencing a shift in customer demand, moving away from physical devices toward digital-only options.

[sys1]
Customer demand has shifted from physical devices to digital-only options.
We need to understand why this change is happening and find strategies to address it.
Key factors may include cost, convenience, and technological trends.
[end sys1]

[sys2]
**2.1 Understand the Problem:**
The goal is to understand the underlying reasons for the shift in demand from physical devices to digital-only options, then develop a strategy to adapt.

*Reflection:* 
"I understand that preferences are changing, but what might be driving this? Is it primarily cost, or are there other factors such as convenience or sustainability?"

*Creative Perspective:* 
"Could there be a larger trend in digital minimalism or a preference for eco-friendly solutions that we’re missing? What unseen motivations might explain this shift?"

**2.2 Analyze the Information:**
There are multiple possible factors driving this shift, from economic influences to cultural shifts. It’s essential to isolate each factor and understand its impact.

*Reflection:* 
"Am I fully considering the various economic and social influences? Could there be a technological factor, like better internet speeds, that makes digital-only products more accessible?"

*Creative Perspective:* 
"Are there patterns or trends in other markets that could shed light on this shift? Could this be part of a larger trend toward virtual experiences?"

**2.3 Generate Hypotheses:**
1. Customers prefer digital options due to lower costs. (Confidence: 0.8, Creative: 0.4)
2. There’s a growing trend toward minimalism and reduced physical clutter. (Confidence: 0.7, Creative: 0.7)
3. Digital products offer greater flexibility and ease of use. (Confidence: 0.6, Creative: 0.6)
4. Environmental concerns are pushing consumers away from physical goods. (Confidence: 0.6, Creative: 0.8)
5. Advances in tech make digital-only options more functional. (Confidence: 0.8, Creative: 0.5)
6. Pandemic-era remote work increased demand for digital solutions. (Confidence: 0.7, Creative: 0.6)
7. Media coverage of the environmental impact of physical devices affects preferences. (Confidence: 0.5, Creative: 0.7)
8. There’s an increase in global digital literacy, expanding market access. (Confidence: 0.6, Creative: 0.6)
9. Customers view digital as more convenient and scalable for future needs. (Confidence: 0.7, Creative: 0.5)
10. Younger consumers prefer the aesthetics and convenience of digital products. (Confidence: 0.6, Creative: 0.6)

*Reflection:* 
"Have I considered all possible influences? Are there any surprising factors that could explain this shift?"

*Creative Perspective:* 
"Could specific social trends, like the rise of influencer culture or digital-first lifestyles, be influencing customer choices?"

**2.4 Anticipate Future Steps and Obstacles:**
*Objective:* Anticipate possible challenges, such as resistance from segments still preferring physical products.

*Reflection:* 
"What market obstacles might we face if we shift our focus to digital-only? Are there sub-segments that still prioritize physical products?"

*Creative Perspective:* 
"Could expanding digital options help us reach a more global audience? Are there emerging trends that we could leverage in our strategy?"

[end sys2]

[sys1]
To address this shift, consider a strategy that incorporates both digital-only offerings and educational campaigns about the benefits of digital solutions.
Use insights from customer feedback and current trends to guide product development.
Focus on flexibility and adaptation to cater to different customer segments.
[end sys1]


---
abstract: 'In this paper, we consider the polymodal version of Lambek calculus with subexponential modalities initially introduced by Kanovich, Kuznetsov, Nigam, and Scedrov [@KanovichEtc1] 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 [@Myself].'
author:
- Daniel Rogozin
title: Quantale semantics of Lambek calculus with subexponential modalities
---

Introduction
============

Categorial grammars were initially introduced by Ajdukiewicz and Bar-Hillel [@Ajd] [@Bar]. In the 1950s, Lambek proposed the way of proof-theoretical consideration of such grammars [@Lambek]. 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” [@Wilde]:

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:

$ $ The Thames nocturne of blue and gold

$(np / n) / np$ $np$ $n$ $np \backslash (np / ad)$ $ad$ $ad / (ad \backslash ad)$ $ad$

$ $ Changed to Harmony in grey

$ $ $np \backslash (s / p)$ $p / np$ $np$ $np \backslash (np / ad)$ $ad$ $\rightarrow s$

Here the basic reduction rules are:

-   $A, A \backslash B \to B$

-   $B / A, A \to 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 [@Lambek], non-commutative linear logic:

Lambek calculus (the system $L$) $ $

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 $\Pi$ 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^{*}$ [@LambekStar]. 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 ${\bf 1}$. The logic $L_{\bf 1}$ is a conservative extension of $L^{*}$ [@Unit] with the following inference rules for this constant:

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 [@Bus] [@Pentus], 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:

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.  $\vdash A \lor (B \land C) \rightarrow (A \lor B) \land (A \lor C)$

2.  $\not\vdash (A \lor B) \land (A \lor C) \rightarrow A \lor (B \land C)$

3.  $\not\vdash A \land (B \lor C) \rightarrow (A \land B) \lor (A \land C)$

4.  $\vdash (A \land B) \lor (A \land C) \rightarrow A \land (B \lor C)$

One may read about the other approaches to the interpretation of Lambek calculus with additives (sometimes it’s called *full Lambek calculus*) here [@Wurm] and here [@Bus1].

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 [@Yetter].

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

Subexponential modalities
=========================

One may extend full Lambek calculus via so-called (sub)exponential modalities and this extension might be motivated linguistically [@Morrill] [@KanovichEtc]. 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$.

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:

Note that, the usual form of contraction yields the cut inadmissibility in contrast to the non-local contraction that generalises the contraction rule [@KanovichEtc2]. The similar version of contraction was also considered by de Paiva and Eades III [@Paiva].

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 $\mathcal{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 [@KanovichEtc1]. The commutative case of subexponential modalities was considered initially by Nigam and Miller [@NigamMiller].

A subexponential signature is an ordered quintuple:

$\Sigma = \langle \mathcal{I}, \preceq, \mathcal{W}, \mathcal{C}, \mathcal{E} \rangle$, where $\langle \mathcal{I}, \preceq \rangle$ is a preorder. $\mathcal{W}, \mathcal{C}, \mathcal{E}$ are upwardly closed subsets of $I$ and $\mathcal{W} \cap \mathcal{C} \subseteq \mathcal{E}$.

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

Here, $s \in \mathcal{W} \cap \mathcal{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 logic ${\bf 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.

Let $\Sigma$ be a subexponential signature. Noncommutative linear logic with subexponentials $SMALC_{\Sigma}$ is Lambek calculus ${\bf L}_{{\bf 1}}$ with additive connections and the following polymodal inference rule.

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 [@KanovichEtc1]:

$ $

1.  Cut-rule is admissable

2.  $\text{SMALC}_{\Sigma}$ is undecidable, if $C \neq \emptyset$

3.  If $C$ is empty, then the decidability problem of $\text{SMALC}_{\Sigma}$ belongs to PSPACE.

Quantale background
===================

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

Quantale $ $

A quantale is a triple $\mathcal{Q} = \langle A, \bigvee, \cdot \rangle$, where $\langle A, \bigvee \rangle$ is a complete join semilattice and $\langle A, \cdot \rangle$ is a semigroup such that for each indexing set $J$:

1.  $a \cdot \bigvee \limits_{j \in J} b_i = \bigvee \limits_{j \in J} (a \cdot b_j)$;

2.  $\bigvee \limits_{j \in J} a_j \cdot b = \bigvee \limits_{j \in J} (a_j \cdot b)$

A quanlate is called unital, if $\langle A, \cdot \rangle$ is a monoid.

Note that any quantale is a complete lattice, so far as any join semilattice is a complete lattice [@Johnstone].

There are several examples of quantales:

-   Let $S$ be a semigroup (monoid), then $\langle \mathcal{P}(S), \cdot, \subseteq \rangle$ is a free (unital) quantale.

-   Let $\mathcal{R}$ be a ring and $Sub(\mathcal{R})$ be a set of additive subgroups of $R$. We define $A \cdot B$ as an additive subgroup generated by finite sums of products $ab$ and order is defined by inclusion.

-   Any locale is a quantale with $\cdot = \wedge$.

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

1.  $a \backslash b = \bigvee \{ c \: | \: a \cdot c \leq b \}$

2.  $b / a = \bigvee \{ c \: | \: c \cdot a \leq b \}$

Residuality for these divisions holds straightforwardly:

$b \leq a \backslash c \Leftrightarrow a \cdot b \leq c \Leftrightarrow a \leq b / c$

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

Let $\mathcal{Q}_1$, $\mathcal{Q}_2$ be quantales. A quantale homomorphism is a map $f : \mathcal{Q}_1 \to \mathcal{Q}_2$, such that:

1.  for all $a,b \in \mathcal{Q}_1$, $f(a \cdot b) = f(a) \cdot f(b)$;

2.  for all indexing set $I$, $f(\bigvee \limits_{i \in I} a_i) = \bigvee \limits_{i \in I} f(a_i)$.

If $\mathcal{Q}_1$, $\mathcal{Q}_2$ are unital quantales, then a unital homomorphism is a quantale homomorphism such that $f(\varepsilon) = \varepsilon$.

$ $

Let $\mathcal{Q} = \langle A, \bigvee, \cdot \rangle$ be a quantale. $\mathcal{S} \subseteq \mathcal{Q}$ is said to be a subquantale, if $\mathcal{S}$ is closed under multiplication and joins.

$ $

Let $\mathcal{Q} = \langle A, \bigvee, \cdot \rangle$ be a quantale. The centre of a quantale is the subquantale $\mathcal{Z}(\mathcal{Q}) = \{ a \in A \: | \: \forall b \in A, a \cdot b = b \cdot a \}$

There occurs the following simple statement:

\[prop1\] $ $

Let $\mathcal{Q}_1$, $\mathcal{Q}_2$ be quantales and $\mathcal{S} \subseteq \mathcal{Q}_1$ is a subquantale of $\mathcal{Q}_1$.

Then, if $f : \mathcal{Q}_1 \to \mathcal{Q}_2$ is a quantale homomorphism, then $f(\mathcal{S}) \subseteq \mathcal{Q}_2$ is a subquantale of $\mathcal{Q}_2$.

That is, a homomorphic image of subquatale is a subquantale.

$ $

Obviously.

Let us define the special kinds of elements.

Let $\mathcal{Q}$ be a quantale and let $a \in \mathcal{Q}$:

1.  $a$ is central iff $z \in \mathcal{Z}(\mathcal{Q})$

2.  $a$ is strongly square increasing iff for all $b \in \mathcal{Q}$, $a \cdot b \leq a \cdot b \cdot a$ and $b \cdot a \leq a \cdot b \cdot 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 \leq a \cdot 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.

\[ssiLemma\]

Let $\mathcal{Q}$ be a unital quantale and $a \in \mathcal{Q}$ be a strongly square increasing such that $a \leq \varepsilon$. Then $a \in \mathcal{Z}(\mathcal{Q})$, that is, $a$ is central.

$ $

$\begin{array}{lll}
  & b \cdot a \leq a \cdot b \cdot a \leq a \cdot b \cdot \varepsilon \leq a \cdot b \leq a \cdot b \cdot a \leq \varepsilon \cdot b \cdot a \leq b \cdot a&
  \end{array}$

\[ssiSub\] Let $\mathcal{Q}$ be a quantale, the set $\mathcal{A} = \{ a \in \mathcal{Q} \: | \: \text{$a$ is strongly square increasing}\}$ is a subquantale of $\mathcal{Q}$

One needs to prove $\mathcal{A}$ is closed under product and sups.

1.  Let $J$ be a indexing set and for all $j \in J$, $a_i \in A$, and $b \in \mathcal{Q}$, then:

    $\begin{array}{lll}
        &\bigvee \limits_{j \in J} a_j \cdot b =
        \bigvee \limits_{j \in J} (a_j \cdot b) \leq
        \bigvee \limits_{j \in J} (a_j \cdot b \cdot a_j) =
        \bigvee \limits_{j \in J} a_j \cdot \bigvee \limits_{j \in J} (b \cdot a_j) =
        \bigvee \limits_{j \in J} a_j \cdot b \cdot \bigvee \limits_{j \in J} a_j & \\
        \end{array}$

    The second inequation $b \cdot \bigvee \limits_{j \in J} a_j \leq \bigvee \limits_{j \in J} a_j \cdot b \cdot \bigvee \limits_{j \in J} a_j$ might be proved similarly.

2.  Let $a_1, a_2 \in \mathcal{A}$. Let us show that $a_1 \cdot a_2 \in A$.

    First of all, $a_1 \cdot a_2 \cdot b = a_1 \cdot (a_2 \cdot b) \leq a_1 \cdot (a_2 \cdot b) \cdot a_1$. By monotonicity, $a_1 \cdot a_2 \cdot b \cdot a_2 \leq a_1 \cdot a_2 \cdot b \cdot a_1 \cdot a_2$.

    On the other hand, $a_1 \cdot a_2 \cdot b \leq a_1 \cdot a_2 \cdot b \cdot a_2$. Then, by transitivity, $a_1 \cdot a_2 \cdot b \leq a_1 \cdot a_2 \cdot b \cdot a_1 \cdot a_2$.

    The second inequation $b \cdot (a_1 \cdot a_2) \leq (a_1 \cdot a_2) \cdot b \cdot (a_1 \cdot a_2)$ might be proved similarly.

\[Unital\]

Let $\mathcal{Q}$ be a unital quantale, then the set $\mathcal{A} = \{ a \in \mathcal{Q} \: | \: a \leq \varepsilon \}$

Straightforwardly.

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

$ $

A quantic conucleus on quantale $\mathcal{Q}$ is a map $I : \mathcal{Q} \to \mathcal{Q}$ such that

1.  $I a \leq a$;

2.  $I a = I^2 a$;

3.  $a \leq b \Rightarrow I a \leq I b$;

4.  $I a \cdot I b = I (I a \cdot I b)$.

For unital quantale, we require that $I \varepsilon = \varepsilon$.

Here and below, $I^2 a$ denotes $I (I a)$.

Note that, one may replace the last condition to $I a \cdot I b \leq I (a \cdot b)$. 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 $I a = a$. As usual [@Rasowa], if $a$ is open, then:

$a \leq b$ if and only if $a \leq I b$

One may extend homomorphism between quantales to homomorphism between quantales with quantic conuclei via the additional condition $f(I_1 a) = I_2 (f a)$

Also, we define a pointwise order on quantic conuclei, that is, $I_1 \leq I_2 \Leftrightarrow \forall a \: I_1 a \leq I_2 a$.

\[ManyCo\] $ $ Let $\mathcal{Q}$ be a quantale. Let $I$, $I_1$, and $I_2$ be quantic conuclei. Then $I_1 a_1 \cdot I_2 a_2 \leq I (I_1 a_1 \cdot I_2 a_2)$, where $I_i \leq I, i = 1,2$.

$I_1 a_1 \cdot I_2 a_2 \leq I_1 (I_1 a_1) \cdot I_2 (I_2 a_2) \leq I (I_1 a_1) \cdot I (I_2 a_2) \leq 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.

\[lemmaConuc\] $ $

1.  Let $S \subseteq \mathcal{Q}$ be a subquantale, then the operation $I : \mathcal{Q} \to \mathcal{Q}$, such that $I a = \bigvee \{ q \in S \: | \: q \leq a \}$, is a quantic conucleus.

2.  Let $S_1$ and $S_2$ are subquantales such that $\mathcal{S}_1 \subseteq \mathcal{S}_2 \subseteq \mathcal{Q}$. Then $I_{\mathcal{S}_1} (a) \leq I_{\mathcal{S}_1} (a)$, where $I_{\mathcal{S}_i}, i = 1,2$ are quantic conucleis defined according to the previous part.

For the first part, see [@Rosenthal]. The second one is proved immediately.

It is well known that if $I$ is a quantic conucleus on quantale $\mathcal{Q}$, then the set $\mathcal{Q}_I = \{ a \in \mathcal{Q} \: | \: I a = a \}$ is a subquantale of $\mathcal{Q}$ [@Rosenthal]. Let us formulate and prove the following statement.

\[ConucUnfold\] $ $

Let $I$ be a quantic conucleus, then for all $a \in \mathcal{Q}$, $I a = \bigvee \{ q \in Q_{I} \: | \: q \leq a \}$, where $Q_{I} = \{ a \in \mathcal{Q} \: | \: I a = a \}$.

$ $

So far as $Q_{I} = \{ a \in \mathcal{Q} \: | \: I a = a \}$ is a subquantale, then $I' a = \bigvee \{ q \in Q_{I} \: | \: q \leq a \}$ is a quantic conucleus by \[lemmaConuc\]. Let us show that these operations are equivalent.

From the one hand, $\bigvee \{ q \in Q_{I} \: | \: q \leq a \} = \bigvee \{ q \in Q_{I} \: | \: q \leq I a \} \leq I a$, so far as $Q_{I}$ is a subquantale of open elements.

On the other hand, $I a \leq a$, then $I a \in \{ q \in Q_{I} \: | \: q \leq a \}$, so far as $I a \in Q_{I}$ (by idempotence). Thus, $I a \leq \bigvee \{ q \in Q_{I} \: | \: q \leq a \}$.

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

$ $

1.  A quantic conucleus $I$ is called central, if for all $a, b \in \mathcal{Q}, I a \cdot b = b \cdot I a$.

2.  A quantic conucleus is called strongly square-increasing, if for all $a, b \in \mathcal{Q}, I a \cdot b \leq I a \cdot b \cdot I a$ and $b \cdot I a \leq I a \cdot b \cdot I a$.

3.  A quantic conucleus is called unital, if for each $a \in Q, I a \leq \varepsilon$.

There are the following properties of those modalities:

\[Upward\] $ $

Let $I_1$ be a quantic conucleus and $I_2$ an unital (central, strongly weak increasing) quantic conucleus such that $I_1 \leq I_2$, then $I_1$ is an unital (central, strongly weak increasing).

$ $

1.  Let $a \in \mathcal{Q}$ (here $\mathcal{Q}$ is supposed to be a unital). Then $I_2 a \leq \varepsilon$, but $I_1 \leq I_2$, so $I_1 a \leq I_2 a$. By transitivity, $I_1 a \leq \varepsilon$.

2.  Let $a \in \mathcal{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}(\mathcal{Q})$ and, obviously, $Q_{I_2} \subseteq \mathcal{Z}(\mathcal{Q})$.

    Let $b \in Q_{I_1}$, 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} \subseteq \mathcal{Z}(\mathcal{Q})$.

    Let us check that $I_1$ commutes with each other element $d \in \mathcal{Q}$

    $\begin{array}{lll}
      & I_1 a \cdot d = & \\
      & \:\:\:\:\:\:\:\: \text{By~\cref{ConucUnfold}}& \\
      & \bigvee \{ q \in Q_{I_1} \: | \: q \leq a \} \cdot d = & \\
      & \:\:\:\:\:\:\:\: \text{By quantale axiom}& \\
      & \bigvee \{ q \cdot d \: | \: q \in Q_{I_1} \: \& \: q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{As we proved, $q \in \mathcal{Z}(\mathcal{Q})$} & \\
      & \bigvee \{ d \cdot q \: | \: q \in Q_{I_1} \: \& \: q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{By quantale axiom}& \\
      & d \cdot \bigvee \{ q \in Q_{I_1} \: | \: q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{By~\cref{ConucUnfold}}& \\
      & d \cdot I_1 a &
      \end{array}$

3.  Let $I_2$ be a strongly square increasing. Then, for all $a \in \mathcal{Q}$ and $b \in Q_{I_2}$, $a \cdot b \leq b \cdot a \cdot b$ and $b \cdot a \leq b \cdot a \cdot b$.

    Let $c \in Q_{I_1}$. Similarly to the previous part, $c = I_1 c \leq I_2 c \leq c$, then $c \in Q_{I_2}$ and $I_1$ is a strongly square increasing:

    $\begin{array}{lll}
      &I_1 a \cdot b = & \\
      & \:\:\:\:\:\:\:\: \text{By~\cref{ConucUnfold}}& \\
      & \bigvee \{ q \in Q_{I_1} \: | \: q \leq a \} \cdot b = & \\
      & \:\:\:\:\:\:\:\: \text{By quantale axiom}& \\
      & \bigvee \{ q \cdot b \: | \: q \in Q_{I_1}, q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{As we proved above}& \\
      & \bigvee \{ I_2 q \cdot b \: | \: q \in Q_{I_1}, q \leq a \} \leq & \\
      & \:\:\:\:\:\:\:\: \text{By condition}& \\
      & \bigvee \{ I_2 q \cdot b \cdot I_2 q \: | \: q \in Q_{I_1}, q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{So far as $q$ is a fixpoint of $I_2$} & \\
      & \bigvee \{ q \cdot b \cdot q \: | \: q \in Q_{I_1}, q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{By quantale axiom} = & \\
      & \bigvee \{ q \cdot b \: | \: q \in Q_{I_1}, q \leq a \} \cdot \bigvee \{ q \in Q_{I_1} \: | \: q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{By quantale axiom} = & \\
      & \bigvee \{ q \in Q_{I_1} \: | \: q \leq a \} \cdot b \cdot \bigvee \{ q \in Q_{I_1} \: | \: q \leq a \} = & \\
      & \:\:\:\:\:\:\:\: \text{By~\cref{ConucUnfold}} = & \\
      &I_1 a \cdot b \cdot I_1 a&
      \end{array}$

    The second inequation might be proved similarly.

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

\[Con1\] $ $

Let $\mathcal{Q}$ be a quantale and $\mathcal{S} \subseteq \mathcal{Q}$ a subquantale, then the following operations are open modalities:

1.  $I a = \bigvee \{ q \in S \: | \: q \leq a, q \in \mathcal{Z}(\mathcal{Q}) \}$ is a central quantic conucleus

2.  $I a = \bigvee \{ q \in S \: | \: q \leq a, q \leq \varepsilon \}$ is an unital conucleus

3.  $I a = \bigvee \{ q \in S \: | \: q \leq a, \forall b \in Q, b \cdot s \vee s \cdot b \leq s \cdot b \cdot s\}$ is a strongly square increasing quantic conucleus

4.  Operations with combinations of conditions above.

Immediately, so far as central, strongly square increasing, and elements that less or equal to identity form a subquantale by \[ssiSub\] and \[Unital\].

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:

\[Con2\] If $I$ is unital and strongly square increasing, then $I$ is central.

Follows from \[ssiLemma\].

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(\mathcal{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 \in W$, then the result of subexponential interpretation is an unital quantic conucleus, etc.

Interpretation of subexponential signature

Let $\mathcal{Q}$ be a quantale and $\Sigma = \langle \mathcal{I}, \preceq, \mathcal{W}, \mathcal{C}, \mathcal{E} \rangle$ a subexponential signature. Let $S : \Sigma \to Sub(\mathcal{Q})$ be a contravariant map from this subexponential signature to the set of subquantales of $\mathcal{Q}$ Thus, a subexponential interpretation is the map $\sigma : \Sigma \to CN(\mathcal{Q})$, where $CN(\mathcal{Q})$ is the set of quantic conuclei on $\mathcal{Q}$, such that:

$\sigma(s_i) = \begin{cases}
  I_i : \mathcal{Q} \to \mathcal{Q} \text{ s.t. } \forall a \in Q, I_i(a) = \{ q \in S_i \: | \: q \leq a\},
  \\ \:\:\:\: \text{if $s_i \notin W \cap C \cap E$} \\
  I_i : \mathcal{Q} \to \mathcal{Q} \text{ s.t. } \forall a \in Q, I_i(a) = \{ q \in S_i \: | \: q \leq a, q \leq \mathds{1}\},
  \\ \:\:\:\: \text{if $s_i \in W$} \\
  I_i : \mathcal{Q} \to \mathcal{Q} \text{ s.t. } \forall a \in Q, I_i(a) = \{ q \in S_i \: | \: q \leq a, s \in \mathcal{Z}(\mathcal{Q}) \},
  \\ \:\:\:\: \text{if $s_i \in E$} \\
  I_i : \mathcal{Q} \to \mathcal{Q} \text{ s.t. } \forall a \in Q, I_i(a) = \{ q \in S_i \: | \: q \leq a, \forall b, b \cdot q \vee q \cdot b \leq q \cdot b \cdot s \},
  \\ \:\:\:\: \text{if $s_i \in E$} \\
  \text{otherwise, if $s_i$ belongs to some intersection of subsets, then we combine the relevant conditions } \\
  \end{cases}$

The resulting operators are well-defined quantic conuclei according to \[Con1\] and \[Con2\].

First of all, let us make sure that any subexponential interpretation is sound w.r.t the set of quantic conuclei $CN(\mathcal{Q})$ of the quantale $\mathcal{Q}$.

\[ImageContr\] $s \in A = \mathcal{W}, \mathcal{C}, \mathcal{E}$ iff $\sigma(s)$ is an unital (central or square increasing) modality.

By construction.

\[WellDef\] $ $

Let $\Sigma$ be a subexponential signature and $\sigma : \Sigma \to CN(\mathcal{Q})$ for a contravariant map $S : \Sigma \to Sub(\mathcal{Q})$, then:

1.  For all $s_1, s_2 \in \Sigma$, if $s_1 \preceq s_2$, then $\sigma(s_2) \leq \sigma(s_1)$. In other words, $\sigma$ is a contravariant functor from $\Sigma$ to $Sub(\mathcal{Q})$.

2.  Let $A = \mathcal{W}, \mathcal{C}, \mathcal{E}$, then $A$ is downwardly closed $\sigma(A) = \{ \sigma(s) \: | \: s \in A \}$ is downwardly closed.

3.  If $s \in \mathcal{W} \cap \mathcal{C}$, then $\sigma(s)$ is a central quantic conucleus.

$ $

1.  Let $s_1, s_2 \in \Sigma$ and $s_1 \leq s_2$. Then $S(s_2) \subseteq S(s_1)$. So, $\forall a \in \mathcal{Q}, \bigvee \{ s \in S(s_2) \: | \: s \leq a \} \leq \bigvee \{ s \in S(s_1) \: | \: s \leq a \}$ by \[lemmaConuc\]. Thus, $\sigma(s_2) \leq \sigma(s_1)$.

2.  Let $\sigma(s) \in \sigma(A)$ and $\sigma(s_1) \leq \sigma(s)$, then $\sigma(s)$ is an unital (central or square increasing) by \[ImageContr\]. By \[Upward\], $\sigma(s_1)$ is an unital (central or square increasing) too. Thus, $s_1 \in A$ and $\sigma(s_1) \in \sigma(A)$.

3.  Let $s \in \mathcal{W} \cap \mathcal{C}$ and $a \in \mathcal{Q}$, then $\sigma(s)(a)$. Thus, by \[Con2\], $\sigma(s)(a) \in \mathcal{Z}(\mathcal{Q})$.

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

Let $\mathcal{Q}$ be an unital quantale, $f : Tp \to \mathcal{Q}$ a valuation and $\sigma : \Sigma \to CN(\mathcal{Q})$ a subexponential interpretation, then interpretation is defined inductively:

$\begin{array}{lll}
& [\![p_i]\!] = f(p_i)&\\
& [\![\mathds{1}]\!] = e & \\
&[\![A \bullet B]\!] = [\![A]\!] \cdot [\![B]\!] & \\
&[\![A \backslash B]\!] = [\![A]\!] \backslash [\![B]\!] & \\
&[\![A / B]\!] = [\![A]\!] / [\![B]\!]& \\
&[\![A \& B]\!] = [\![A]\!] \wedge [\![B]\!]& \\
&[\![A \vee B]\!] = [\![A]\!] \vee [\![B]\!]& \\
&[\![!_{s_i} A]\!] = \sigma(s_i) [\![A]\!]&
\end{array}$

$\Gamma \models A \Leftrightarrow \forall f, \forall \sigma, [\![\Gamma]\!] \leq [\![A]\!]$

$ $

Let $\Sigma$ be a subexponential signature, then $SMALC_{\Sigma} \vdash \Gamma \rightarrow A \Rightarrow [\![\Gamma]\!] \leq [\![A]\!]$.

$ $

Let $\sigma$ be a subexponential interpretation. By \[WellDef\], $\sigma$ is well-defined. Let us consider the modal cases.

1.  Let $!_{s_1} A_1, \dots, !_{s_n} A_n \rightarrow A$ and $\forall i, s \preceq s_i$. Then $\forall a \in Q, \sigma(s_i)(a) \leq \sigma(s)(a)$ by \[WellDef\].

    By IH, $\sigma(s_1)[\![A_1]\!] \cdot \dots \cdot \sigma(s_n) [\![A_n]\!] \leq [\![A]\!]$. Thus, $\sigma(s)(\sigma(s_1)[\![A_1]\!] \cdot \dots \cdot \sigma(s_n) [\![A_n]\!]) \leq \sigma(s)([\![A]\!])$. By \[ManyCo\], $\sigma(s_1)[\![A_1]\!] \cdot \dots \cdot \sigma(s_n) [\![A_n]\!] \leq \sigma(s)(\sigma(s_1)[\![A_1]\!] \cdot \dots \cdot
    \sigma(s_n) [\![A_n]\!])$.\
    So, $\sigma(s_1)[\![A_1]\!] \cdot \dots \cdot \sigma(s_n) [\![A_n]\!] \leq \sigma(s)([\![A]\!])$.

2.  Let $s \in \mathcal{W}$ and $\Gamma, \Delta \rightarrow A$. By IH, $[\![\Gamma]\!] \cdot [\![\Delta]\!] \leq [\![B]\!]$. Thus, obviously, $[\![\Gamma]\!] \cdot \varepsilon \cdot [\![\Delta]\!] \leq [\![B]\!]$. $s \in \mathcal{W}$, then $\sigma(s)$ is an unital quantic conulceus by \[ImageContr\]. So, for each formula $A$, $\sigma(s)([\![A]\!]) \leq \varepsilon$. Then, $[\![\Gamma]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \leq [\![B]\!]$.

3.  Let $s \in \mathcal{E}$ and $\Gamma, !_s A, \Delta, \Theta \rightarrow B$. By IH, $[\![\Gamma]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \cdot [\![\Theta]\!] \leq [\![B]\!]$. By \[ImageContr\], $\sigma(s)$ is a central quantic conucleus, then $[\![\Gamma]\!] \cdot [\![\Delta]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Theta]\!] \leq [\![B]\!]$.

4.  Let $s \in \mathcal{C}$ and $\Gamma, !_s A, \Delta, !_s A, \Theta \rightarrow B$. So, $[\![\Gamma]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Theta]\!] \leq [\![B]\!]$. But $\sigma(s)$ is a strongly square increasing, so $\sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \leq \sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \cdot \sigma(s)([\![A]\!])$ and $[\![\Delta]\!] \cdot \sigma(s)([\![A]\!]) \leq \sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \cdot \sigma(s)([\![A]\!])$. Thus, $[\![\Gamma]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Delta]\!] \cdot [\![\Theta]\!] \leq [\![B]\!]$ and $[\![\Gamma]\!] \cdot [\![\Delta]\!] \cdot \sigma(s)([\![A]\!]) \cdot [\![\Theta]\!] \leq [\![B]\!]$

Completeness
============

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

$ $

Let $\mathcal{F} \subseteq Fm$, an ideal is a subset $\mathcal{I} \subseteq \mathcal{F}$, such that:

-   If $B \in \mathcal{I}$ and $A \rightarrow B$, then $A \in \mathcal{I}$

-   If $A, B \in \mathcal{I}$, then $A \lor B \in \mathcal{I}$

$ $

1.  $\bigvee S$ is an ideal

2.  $A \subseteq Fm$, then $\bigvee \{ A \} = \{ B \: | \: B \rightarrow A \}$

3.  $\bigvee \{ A \} \subseteq \bigvee \{ B \}$ iff $A \rightarrow B$

4.  Let $\mathcal{Q} = \{ \bigvee S \: | \: S \subseteq Fm \}$ and $\bigvee \mathcal{A} \cdot \bigvee \mathcal{B} =
      \bigvee \{ A \bullet B \: | \: A \in \mathcal{A}, B \in \mathcal{B} \}$ Then $\langle \mathcal{Q}, \subseteq, \cdot, \bigvee{{\bf 1}}\rangle$ is an unital quantale.

See [@BrownAndGurr2].

We extend this construction for polymodal case as follows:

\[SynContr\] $ $

Let $\Sigma$ be a subexponential signature.

1.  Let $s \in \Sigma$, then $!_s Syn = \{ \bigvee !_s S \: | \: A \subseteq Fm \}$ is a subquantale of $Syn$.

2.  Let $\Sigma$ be a subexponential signature, then a map $S : \Sigma \to Sub(Syn)$ such that $S(s) = !_s Syn$ is a contravariant map.

$ $

1.  One need to check that $!_s Syn = \{ \bigvee !_s A \: | \: S \subseteq Fm \}$ 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 $\bigvee !_s X, \bigvee !_s Y \in !_s Syn$. Then $\bigvee !_s X \cdot \bigvee !_s Y = \bigvee (!_s X \cdot !_s Y) \in !_s Syn$, so far as $!_s X \cdot !_s Y \subseteq Fm$.

2.  Let $s_1 \preceq s_2$ and $\bigvee !_{s_2} X \in \: !_{s_2} Syn$. Let us show that $\bigvee !_{s_2} X \in !_{s_1} Syn$.

    $\begin{array}{lll}
        & \bigvee !_{s_2} X = \{ !_{s_2} B \: | \: !_{s_2} B \to A, A \in X \} = & \\
        & \{ !_{s_2} B \: | \: !_{s_2} B \to !_{s_2} A, A \in X \} \subseteq & \\
        & \{ !_{s_2} B \: | \: !_{s_2} B \to !_{s_2} A, A \in X \} \subseteq \bigvee !_{s_1} X& \\
        \end{array}$

$ $

Let $\Sigma$ be a subexponential signature.

1.  Let $S$ be a contravariant map from the previous stament and $!_s \in \Sigma$ and $A \in \mathcal{F}_{\Sigma}$, then $S(s)$ is a quantic conucleus.

2.  Let $A \in \mathcal{F}_{\Sigma}$, then $\Box_s \bigvee \{ A \} = \bigvee \{ !_s A \}$, for each $s \in \mathcal{I}$

3.  Let $i, j \in \Sigma$ and $i \preceq j$, then for all $A \in \mathcal{F}_{\Sigma}$, $\Box_j (\bigvee \{ A \}) \subseteq \Box_i (\bigvee \{ A \})$.

$ $

1.  Similarly to [@Yetter].

2.  Let $A \in Fm$ and $s \in \Sigma$.

    Let $!_s B \in \Box_s \bigvee \{ A \}$, then $!_s B \rightarrow A$, then $!_s B \rightarrow !_s A$ by promotion. So, $!_s B \in \bigvee \{ !_s A \}$.

    Let $C \in \bigvee \{ !_s A \}$, then $C \rightarrow !_s A$, so $!_s C \rightarrow !_s A$ by dereliction, but $!_s A \rightarrow A$, hence $!_s C \rightarrow A$ by cut. So, $!_s C \in \Box_s \bigvee \{ A \}$.

3.  Let $i, j \in I$ and $i \preceq j$, then forall $A \in \mathcal{F}_{\Sigma}$, $!_j A \rightarrow !_i A$ by promotion. Then $\bigvee \{ !_j A \} \subseteq \bigvee \{ !_i A \}$, so $\Box_j (\bigvee \{ A \}) \subseteq \Box_i (\bigvee \{ A \})$.

$ $

For all $A \in \mathcal{F}_{\Sigma}$,

1.  Let $s \in W$, then $\Box_s \{ A \} \subseteq \{ {\bf 1} \}$

2.  Let $s \in E$, then $\Box_s (\bigvee \{ A \}) \cdot \bigvee \{ B \} = \bigvee \{ B\} \cdot \Box_s (\bigvee \{ A \})$

3.  Let $s \in C$, then $(\Box_s \bigvee A \cdot \bigvee B) \cup (\bigvee B \cdot \Box_s \bigvee A) \subseteq \Box_s \bigvee A \cdot \bigvee B \cdot \Box_s \bigvee A$, for all $B \subseteq Fm$.

$ $

1.  Follows from $!_s A \rightarrow {\bf 1}$, since $s \in W$.

2.  Follows from $!_s A \bullet B \leftrightarrow B \bullet !_s A$.

3.  Follows from $SMALC_{\Sigma} \vdash !_s A \bullet B \rightarrow !_s A \bullet B \bullet !_s A$ and $SMALC_{\Sigma}
      \vdash B \bullet !_s A  \rightarrow !_s A \bullet B \bullet !_s A$.

$ $

Let $\mathcal{Q}$ be a syntactic quantale defined above and $\Sigma = \langle I, \preceq,
\mathcal{W}, \mathcal{C}, \mathcal{E} \rangle$ be a subexponential signature and $S : \Sigma \to Sub(Syn)$ be a contravariant map in sense of \[SynContr\].

We define a map $\Box : \Sigma \to CN(Syn)$ as follows:

$\Box(s)(\bigvee \{ A \} ) = \{ !_s B \in S(Syn) \: | \: !_s B \rightarrow A \}$.

$\Box$ is a subexponential interpretation.

Follows from lemmas above.

$ $

Let $Q$ be a quantale constructed above, then there exist a model $\langle Q, [\![.]\!] \rangle$, such that $[\![A]\!] = \bigvee \{ A \}$, $A \in Fm$.

$ $

We define an interpreation as follows:

1.  $[\![p_i]\!] = \bigvee \{ p_i \}$

2.  $[\![{\bf 1}]\!] = \bigvee \{ {\bf 1} \}$

3.  $[\![A \bullet B]\!] = \bigvee \{ A \bullet B \}$

4.  $[\![A / B]\!] = \bigvee \{ A / B \}$

5.  $[\![B \setminus A]\!] = \bigvee \{ B \setminus A \}$

6.  $[\![A \& B ]\!] = \bigvee \{ A \& B \}$

7.  $[\![A \lor B]\!] = \bigvee \{ A \lor B\}$

8.  $[\![!_s A]\!] = \Box(s) (\bigvee \{ A \}) = \{ !_s B \in S(s) \: | !_s B \rightarrow A \} = \{ !_s B \in S(s) \: | !_s B \rightarrow A \} = \bigvee \{ !_s A \}$.

$\Gamma \models A \Rightarrow \Gamma \rightarrow A$.

Follows from lemmas above.

Representation theorem and relational completeness
==================================================

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

$ $

Let $A$ be a set and $R \subseteq A \times A$ a transitive relation on $A$. Then relational quantale on $A$ is a triple $\mathcal{Q} = \langle \mathcal{P}(R), \bigvee, \mathcal{I}
  \rangle$ with the following data:

1.  $\langle \mathcal{P}(R), \bigvee, \subseteq \rangle$ is a complete semi-lattice

2.  Multiplication is defined as $R \circ S = \{ \langle a, c \rangle \: | \: \exists b \in A, \langle a, b \rangle \in R \text{ and } \langle b, c \rangle \in S\}$

3.  $\langle \mathcal{A}, \circ, \mathcal{I} \rangle$ is a monoid, that is, $\mathcal{I}$ is identity

4.  For each indexing set $J$, $R \circ \bigvee_{j \in J} S_j = \bigvee_{j \in J} (R \circ S_j)$ and $\bigvee_{j \in J} R_j \circ S = \bigvee_{j \in J}(R_j \circ S)$.

\[Representation lemma\] $ $

Let $\mathcal{Q} = \langle A, \leq, \cdot, \bigvee \rangle$ be a unital quantale and $\mathcal{S}$ is a subquantale of $\mathcal{Q}$.

Then $\langle \mathcal{Q}, I_{\mathcal{S}} \rangle$ is isomorphic to some relational quantale of $A$ with some quantic conucleus $\hat{I}$, where $I_{\mathcal{S}}$ is a quantic conclues on $\mathcal{S}$.

$ $

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

This quantale is 4-tuple $\hat{\mathcal{Q}} = \langle \mathcal{R}, \subseteq, \circ, \bigvee \rangle$ defined as follows, where $\mathcal{R} = \{ \hat{a} \: | \: a \in \mathcal{Q}\}$ and $\hat{a} = \{ \langle b, c \rangle \: | \: b \leq a \cdot c \}$. One may prove that:

1.  $\widehat{a \cdot b} = \hat{a} \circ \hat{b}$

2.  $\widehat{\bigvee \limits_{j \in J} a_j} = \bigvee \limits_{j \in J} \hat{a_j}$

If $\mathcal{Q}$ is an unital quantale, then we express the neutral element as $\hat{\varepsilon} = \{ \langle b, c \rangle \: | \: b \cdot \varepsilon \leq c \} = \{ \langle b, c \rangle \: | \: b \leq c \}$.

Also, one may prove that $\hat{a} \subseteq \hat{b}$ iff $a \leq b$.

Let $\mathcal{S} \subseteq \mathcal{Q}$, so $I_{\mathcal{S}} a := \bigvee \{ s \: | \: s \in S, s \leq a \}$ is quantic conucleus. So, $\hat{\mathcal{S}} \subseteq \hat{\mathcal{Q}}$ is a subquantale of $\hat{\mathcal{Q}}$ by \[prop1\].

Let us define $\hat{I} \hat{a} := \bigvee \{ \hat{s} \: | \: \hat{s}  \in \hat{S}, \hat{s} \subseteq \hat{a} \}$, then

$\begin{array}{lll}
  &\widehat{(I_{\mathcal{S}} a)} = \{ \langle p, q \rangle \: | \: p \leq I_{\mathcal{S}} a \cdot q \} = &\\
  &\:\:\:\: \text{By the condition}& \\
  &\{ \langle p, q \rangle \: | \: p \leq \bigvee \{ s \: | \: s \in \mathcal{S}, s \leq a \} \cdot q \} = &\\
  &\:\:\:\: \text{Homomorphism}& \\
  &\widehat{(\bigvee_{s \in S, s \leq a} s)} = & \\
  &\:\:\:\: \text{Homomorphism preserves sups}& \\
  &\bigvee_{s \in S, s \leq a} \hat{s} = & \\
  &\:\:\:\: \text{Unfolding}& \\
  &\bigvee \{ \hat{s} \: | \: s \in S, s \leq a \} = & \\
  &\:\:\:\: \text{Unfolding}& \\
  &\bigvee \{ \hat{s} \: | \: \hat{s} \in \hat{\mathcal{S}}, \hat{s} \subseteq \hat{a} \} = \widehat{I_{\mathcal{S}}} \hat{a}& \\
  \end{array}$

Thus, $\widehat{I_{s}} \hat{a} = \widehat{I_{\mathcal{S}} a}$.

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

Let $\mathcal{Q} = \langle \mathcal{Q}, I \rangle$ be a quantale with quantic conucleus. Then $\mathcal{Q}$ is isomorphic to relational quantale on $Q$ with some conucleus operator.

Let $I$ be a quantic conucleus. By Lemma, $I a = \bigvee \{ q \in \mathcal{Q}_I \: | \: q \leq a \}$. One need to apply the previous statement with conucleus $I' a = \bigvee \{ q \in \mathcal{Q}_I \: | \: q \leq a \}$.

This representation theorem might be extended categorically. Let ${\bf Con Quant}$ be a category of (unital) quantales with quantic conuclei with homomorphisms between them.

${\bf R Con Quant}$ is a category of relational quantales with conuclei operators. It is clear that any relational quantale is a (unital) quantale. Thus, ${\bf Con RQuant}$ is a subcategory of ${\bf Con Quant}$.

Let us show that ${\bf Con Quant}$ is equivalent to ${\bf Con RQuant}$.

There exists a functor $\mathfrak{F} : {\bf Con Quant} \to {\bf Con RQuant}$

Let us define the following map:

-   $\mathfrak{F} : \mathcal{Q} = \langle Q, \cdot, \bigvee, I \rangle \mapsto \hat{\mathcal{Q}} = \langle \mathcal{R}, \bigvee, \circ, \hat{I} \rangle$,\
    where $\mathcal{R} = \{ \hat{a} \: | \: a \in \mathcal{Q} \}$, $\mathcal{Q} \in Ob({\bf Con U Quant})$, and $\hat{a}$ is defined according to the construction provided in the proof of representation theorem

-   Let $f \in Mor({\bf Con U Quant})$, that is, $f : \langle Q_1, \cdot, \bigvee, I_1 \rangle \to \langle Q_2, \cdot, \bigvee, I_2 \rangle$,\
    then $\mathfrak{F} : f \mapsto \hat{f}$, where $\hat{f}(\hat{a}) = \widehat{f(a)}$.

It is enough to check that $\mathfrak{F}(f)(\hat{I}(\hat{a})) = \hat{I}(\mathfrak{F}(f)(\hat{a}))$:

$\begin{array}{lll}
  &\mathfrak{F}(f)(\hat{I}(\hat{a})) = \hat{f}(\hat{I}(\hat{a})) = \hat{f}(\widehat{I a}) = \widehat{f (I a)} =
  \hat{I} (\widehat{f (a))} = \hat{I}(\mathfrak{F}(f)(\hat{a}))&
  \end{array}$

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

Finally, we formulate the theorem which claims that $SMALC_{\Sigma}$ is complete w.r.t relational quantales with quantic conuclei.

$SMALC_{\Sigma} \vdash \Gamma \rightarrow A$ iff $\Gamma \models_{\mathcal{Q}_R} A$ for some relational quantale $\mathcal{Q}_R$ with a family of quantic conuclei.

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_{\Sigma}$ is also relationally complete.

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.

Ajdukiewicz, K. *Die syntaktische konnexit[ä]{}t* Studia Philosophica, [**1**]{}, 1935, pp 1–27.

Bar-Hillel, Y. *A quasi arithmetical notation for syntactic description*, Language, [**29**]{}, 1953, pp 47–58.

Brown C., Gurr D., *A representation theorem for quantales*, Journal of Pure and Applied Algebra, [**85**]{} (1), 1993, pp. 27–42.

Brown C., Gurr D., *Relations and non-commutative linear logic*, Journal of Pure and Applied Algebra, [**105**]{} (2), 1995, pp. 117–136.

Buszkowski W., *Completeness Results for Lambek Syntactic Calculus*, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, [**32**]{}, 1986, pp. 13–28.

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.

Eklund, P., Gutiérrez Garcia, J., Höhle, U., Kortelainen, J., *Semigroups in Complete Lattices. Quantales, Modules and Related Topics*, Springer, Cham, 2018.

Johnstone P., *Stone Spaces*, Cambridge University Press, 1982

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.

Kanovich M., Kuznetsov S., Nigam V., Scedrov A., *Subexponentials in non-commutative linear logic*, Mathematical Structures in Computer Science, 2018, 1–33.

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.

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.

Lambek, J., *The mathematics of sentence structure*, American Mathematical Monthly, [**65**]{}, 1958, pp. 154–170.

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.

Morrill G., Valentin O., *Computation coverage of TLG: Nonlinearity*, In NLCS, 2015.

Nigam V., Miller D., *Algorithmic specifications in linear logic with subexponentials*, In Proc. PPDP ’09, 2009, pp. 129–140.

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.

Pentus M., *Models for the Lambek calculus*, Annals of Pure and Applied Logic, [**75**]{}, No 1-2, 1995, pp. 179–213.

Rasiowa, H., Sikorski R., *The Mathematics of Metamathematics*, PWN-Polish Scientific Publishers, Warsaw, 1963.

Rogozin, D., *Quantale semantics for Lambek calculus with subexponentials*, TACL 2019. Abstracts, 2019, pp. 158–159.

Rosenthal K., *Quantales and their Applications*, Pitman Research Notes in Mathematics, [**234**]{}, Longman Scientific & Technical, 1990, 165 pp.

Wilde O., *The collected poems by Oscar Wilde*, Wordrworth Editions Ltd, 1994.

Wurm, C., *Language-Theoretic and Finite Relation Models for the (Full) Lambek Calculus*, Journal of Logic, Language, and Information, [**26**]{}, 2017, pp. 179–214.

D. N. Yetter., *Quantales and (noncommutative) linear logic*, Journal of Symbolic Logic, [**55**]{}(1), 1990, pp. 41–64.