anguage Models for Some Extensions of the Lambek Calculu

We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For extensions with additive connectives, we show that conjunction and disjunction behave differently. Adding both of them leads to incompleteness due to the distributivity law. We show that with conjunction only no issues with distributivity arise. In contrast, there exists a corollary of the distributivity law in the language with disjunction only which is not derivable in the non-distributive system. Moreover, this difference keeps valid for systems with permutation and/or weakening structural rules, that is, intuitionistic linear and affine logics and affine multiplicative-additive Lambek calculus. For the extension of the Lambek with the unit constant, we present a calculus which reflects natural algebraic properties of the empty word. We do not claim completeness for this calculus, but we prove undecidability for the whole range of systems extending this minimal calculus and sound w.r.t.language models. As a corollary, we show that in the language with the unit there exissts a sequent that is true if all variables are interpreted by regular language, but not true in language models in general.

Lambek calculus ,language models ,relational models ,distributive law ,incompleteness ,undecidability

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

The Lambek calculus was introduced by Joachim Lambek @Lambek58 for mathematical modelling of natural language syntax. This suggests the natural interpretation of the Lambek calculus as the algebraic logic of operations on formal languages. Such interpretations of the Lambek calculus are called <span>*language models,*</span> or <span>*L-models*</span> for short.

The Lambek calculus, as originally formulated by Lambek, includes three operations: $\cdot$ (product), ${\mathop{\backslash}}$ (left division), and ${\mathop{/}}$ (right division). A distinctive feature of the Lambek calculus is the so-called <span>*Lambek's non-emptiness restriction.*</span> In terms of L-models, this means that the empty word is disallowed, and we consider, for a given alphabet $\Sigma$, subsets of $\Sigma^+$. Lambek operations on languages are defined as follows: $$\begin{aligned}
 & A \cdot B = \{ uv \mid u \in A, v \in B \}, \\
 & A {\mathop{\backslash}}B = \{ u \in \Sigma^+ \mid (\forall v \in A) \: 
 vu \in B \}, \\
 & B {\mathop{/}}A = \{ u \in \Sigma^+ \mid (\forall v \in A) \: 
 uv \in B \}.\end{aligned}$$

The division operations, ${\mathop{\backslash}}$ and ${\mathop{/}}$, are indeed <span>*residuals*</span> of the product w.r.t. the subset relation: $$B \subseteq  A {\mathop{\backslash}}C \iff
A \cdot B \subseteq C \iff 
A \subseteq C {\mathop{/}}B.$$ These equivalences form the core of the Lambek calculus. Along with transitivity ($A \subseteq B \subseteq C \Rightarrow A \subseteq C$), reflexivity ($A \subseteq A$), and associativity ($A \cdot (B \cdot C) = (A \cdot B) \cdot C$), they form a complete axiomatization of all generally true atomic statements about Lambek operations on formal languages. This axiomatization is the Lambek calculus in its non-sequential form.

The sequential formulation of the Lambek calculus @Lambek58 is as follows. Formulae are constructed from variables ($p,q,r,\ldots$) using three connectives: $\cdot$, ${\mathop{\backslash}}$, ${\mathop{/}}$. (We use capital Latin letters both for languages and for Lambek formulae.) Sequents are expressions of the form $\Gamma \vdash C$, where the antecedent $\Gamma$ is a sequence of formulae and the succedent $C$ is one formula (intuitionistic style). The calculus ${\mathbf{L}}$ includes axioms of the form $A \vdash A$ and the following rules of inference:

$$\infer[{\mathop{\backslash}}L]{\Gamma, \Pi, A {\mathop{\backslash}}B, \Delta \vdash C}
{\Pi \vdash A & \Gamma, B, \Delta \vdash C}
\qquad
\infer[{\mathop{\backslash}}R;\mbox{ $\Pi$ is non-empty}]{\Pi \vdash A {\mathop{\backslash}}B}
{A, \Pi \vdash B}$$ $$\infer[{\mathop{/}}L]{\Gamma, B {\mathop{/}}A, \Pi, \Delta \vdash C}
{\Pi \vdash A & \Gamma, B, \Delta \vdash C}
\qquad
\infer[{\mathop{/}}R;\mbox{ $\Pi$ is non-empty}]{\Pi \vdash B {\mathop{/}}A}
{\Pi, A \vdash B}$$ $$\infer[\cdot L]
{\Gamma, A \cdot B, \Delta \vdash C}{\Gamma, A, B, \Delta \vdash C}
\qquad
\infer[\cdot R]
{\Gamma, \Delta \vdash A \cdot B}
{\Gamma \vdash A & \Delta \vdash B}$$ $$\infer[Cut]
{\Gamma, \Pi, \Delta \vdash C}{\Pi \vdash A &
\Gamma, A, \Delta \vdash C}$$ The cut rule is eliminable @Lambek58.

An L-model, formally, is a mapping $w$ of Lambek formulae to subsets of $\Sigma^+$ (languages without the empty word), which commutes with Lambek operations: $w(A \cdot B) = w(A) \cdot w(B)$, $w(A {\mathop{\backslash}}B) = w(A) {\mathop{\backslash}}w(B)$, and $w(B {\mathop{/}}A) = w(B) {\mathop{/}}w(A)$. A sequent $A_1, \ldots, A_n \vdash B$ is true in this model, if $w(A_1) \cdot \ldots \cdot w(A_n) \subseteq w(B)$.

According to Lambek's non-emptiness restriction, all sequents in derivations are required to have non-empty antecedents. This constraint is motivated by linguistic applications: without it, Lambek categorial grammars generate ungrammatical sentences @MootRetore [§2.5].

Abolishing Lambek's restriction—that is, removing constraints "$\Pi$ is non-empty" on ${\mathop{\backslash}}R$ and ${\mathop{/}}R$—yields <span>*the Lambek calculus allowing empty antecedents,*</span> denoted by ${\mathbf{L}^{\boldsymbol{*}}}$ @Lambek61. Language models are easily adapted for the case of ${\mathbf{L}^{\boldsymbol{*}}}$: now we consider languages, which are subsets of $\Sigma^*$ (that is, they are allowed to include the empty word $\varepsilon$). The definition of division operations is also modified: for models of ${\mathbf{L}^{\boldsymbol{*}}}$, $$\begin{aligned}
 & A {\mathop{\backslash}}B = \{ u \in \Sigma^* \mid (\forall v \in A) \, vu \in B \},\\
 & B {\mathop{/}}A = \{ u \in \Sigma^* \mid (\forall v \in A) \, uv \in B \}.\end{aligned}$$ This modification can alter the values of $A {\mathop{\backslash}}B$ and $B {\mathop{/}}A$ even if $A$ and $B$ do not contain the empty word. For example, $A {\mathop{\backslash}}A$ now always includes $\varepsilon$, and therefore $(A {\mathop{\backslash}}A) {\mathop{\backslash}}B$ is always a subset of $B$. Hence, ${\mathbf{L}^{\boldsymbol{*}}}$ is not a conservative extension of ${\mathbf{L}}$: the sequent $(p {\mathop{\backslash}}p) {\mathop{\backslash}}q \vdash q$ has a non-empty antecedent, but is derivable only in ${\mathbf{L}^{\boldsymbol{*}}}$, not in ${\mathbf{L}}$. For these modified L-models, let us use the term <span>*L$\varepsilon$-models.*</span>

In an L$\varepsilon$-model $w$, a sequent of the form $A_1, \ldots, A_n \vdash B$ is true if $w(A_1) \cdot \ldots \cdot w(A_n) \subseteq w(B)$, and a sequent of the form $\vdash B$, with an empty antecedent, is true if $\varepsilon \in w(B)$.

Completeness theorems for ${\mathbf{L}}$ and ${\mathbf{L}^{\boldsymbol{*}}}$ w.r.t. corresponding versions of L-models were proved by Pentus @PentusAPAL [@PentusFmonov]. Pentus' proofs are highly non-trivial. If one considers the fragment without $\cdot$ (the <span>*product-free*</span> fragment), however, proving L-completeness becomes much easier. This was done by Buszkowski @Buszko1982; Buszkowski's proof applies both to ${\mathbf{L}}$ and ${\mathbf{L}^{\boldsymbol{*}}}$, w.r.t. L-models and L$\varepsilon$-models, respectively.

Besides product and two divisions, natural operations on formal languages include set-theoretic intersection and union. These operations correspond to so-called <span>*additive*</span> conjunction and disjunction. Additive operations are usually axiomatized by the following inference rules (cf. @KanazawaJoLLI): $$\infer[\vee L]
{\Gamma, A \vee B, \Delta \vdash C}
{\Gamma, A, \Delta \vdash C & \Gamma, B, \Delta \vdash C}
\qquad
\infer[\vee R_l]
{\Pi \vdash A \vee B}{\Pi \vdash A}
\qquad
\infer[\vee R_r]
{\Pi \vdash A \vee B}{\Pi \vdash B}$$ $$\infer[\wedge L_l]
{\Gamma, A \wedge B, \Delta \vdash C}
{\Gamma, A, \Delta \vdash C}
\qquad
\infer[\wedge L_r]
{\Gamma, A \wedge B, \Delta \vdash C}
{\Gamma, B, \Delta \vdash C}
\qquad
\infer[\wedge R]
{\Pi \vdash A \wedge B}
{\Pi \vdash A & \Pi \vdash B}$$ The Lambek calculus ${\mathbf{L}}$ extended with these rules is denoted by ${\mathbf{MALC}}$ (<span>*multiplicative-additive Lambek calculus*</span>); ${\mathbf{MALC}^{\boldsymbol{*}}}$ is the variant of ${\mathbf{MALC}}$ without Lambek's restriction (that is, allowing empty antecedents). L-completeness, however, fails for ${\mathbf{MALC}}$ in general. Further, in Section \[S:distr\], we discuss this issue in detail.

Following Abrusci @Abrusci, we put the Lambek calculus into a broader context of linear logic. Namely, ${\mathbf{MALC}^{\boldsymbol{*}}}$ can be viewed as a fragment of intuitionistic <span>*non-commutative*</span> linear logic. (This fragment includes multiplicative and additive operations, but lacks the exponential and constants.) We also consider commutative systems: intuitionistic linear logic ${\mathbf{ILL}}$ and intuitionistic affine logic ${\mathbf{IAL}}$.

Calculi ${\mathbf{ILL}}$ and ${\mathbf{IAL}}$ can be obtained from ${\mathbf{MALC}^{\boldsymbol{*}}}$ by adding structural rules: permutation for ${\mathbf{ILL}}$ and permutation and weakening for ${\mathbf{IAL}}$. In the language of ${\mathbf{MALC}}$, the rules of permutation and weakening are formulated as follows: $$\infer[P]{\Gamma, A, B, \Delta \vdash C}{\Gamma, B, A, \Delta \vdash C}
\qquad
\infer[W]{\Gamma, A, \Delta \vdash C}{\Gamma, \Delta \vdash C}$$ Adding only weakening yields non-commutative intuitionistic affine logic, or affine (monotone) multiplicative-additive Lambek calculus. We denote this system by ${\mathbf{AMALC}^{\boldsymbol{*}}}$ (in the presence of extra structural rules, we do not impose Lambek's restriction).

We shall also use alternative calculi for the commutative systems ${\mathbf{ILL}}$ and ${\mathbf{IAL}}$, in which structural rules are hidden in axioms and in the format of sequents. First, we change the language of formulae, introducing one connective $A {\multimap}B$ instead of $A {\mathop{\backslash}}B$ and $B {\mathop{/}}A$ (these are equivalent in ${\mathbf{ILL}}$ and ${\mathbf{IAL}}$). We also write $A \otimes B$ instead of $A \cdot B$, following Girard's @Girard linear logic notations.

Sequents are now going to be expressions of the form $\Gamma \vdash C$, where $\Gamma$ is a <span>*multiset*</span> of formulae. Further $\Gamma, A$ means $\Gamma \uplus \{ A \}$, and $\Gamma, \Pi$ means $\Gamma \uplus \Pi$, where $\uplus$ is multiset union.

Axioms are of the form $p \vdash p$, for each variable $p$, in the case of ${\mathbf{ILL}}$, and of the form $\Gamma, p \vdash p$ for ${\mathbf{IAL}}$. Inference rules for both systems are as follows: $$\infer[{\multimap}L]{\Gamma, \Pi, A {\multimap}B \vdash C}
 {\Pi \vdash A & \Gamma, B \vdash C}
 \qquad 
 \infer[{\multimap}R]{\Pi \vdash A {\multimap}B}{\Pi, A \vdash B}$$ $$\infer[{\otimes}L]{\Gamma, A {\otimes}B \vdash C}{\Gamma, A, B \vdash C}
 \qquad
 \infer[{\otimes}R]{\Gamma, \Delta \vdash A {\otimes}B}
 {\Gamma \vdash A & \Delta \vdash B}$$ $$\infer[\vee L]{\Gamma, A \vee B \vdash C}{\Gamma, A \vdash C &
 \Gamma, B \vdash C}
 \qquad
 \infer[\vee R_l]{\Pi \vdash A \vee B}{\Pi \vdash A}
 \qquad
 \infer[\vee R_r]{\Pi \vdash A \vee B}{\Pi \vdash B}$$ $$\infer[\wedge L_l]{\Gamma, A \vee B \vdash C}{\Gamma, A \vdash C}
 \qquad
 \infer[\wedge L_r]{\Gamma, A \vee B \vdash C}{\Gamma, B \vdash C}
 \qquad 
 \infer[\wedge R]{\Pi \vdash A \wedge B}{\Pi \wedge A & \Pi \wedge B}$$

For ${\mathbf{IAL}}$, the weakening rule is not officially included in the system, but is admissible: $$\infer[W]{\Gamma, A \vdash C}{\Gamma \vdash C}$$ (it is hidden in axioms).

The cut rule of the following form is admissible both in ${\mathbf{ILL}}$ and ${\mathbf{IAL}}$: $$\infer[Cut]{\Gamma, \Pi \vdash C}{\Pi \vdash A & \Gamma, A \vdash C}$$ This is shown by a standard inductive argument.

Finally, let us introduce the <span>*multiplicative unit constant,*</span> ${\mathbf{1}}$. The unit constant is added to systems without Lambek's restriction extending ${\mathbf{L}^{\boldsymbol{*}}}$ (<span>*i.e.,*</span> ${\mathbf{L}^{\boldsymbol{*}}}$ itself, ${\mathbf{MALC}^{\boldsymbol{*}}}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}$, ${\mathbf{ILL}}$, ${\mathbf{IAL}}$). The <span>*Lambek calculus with the unit,*</span> ${{\mathbf{L}}_{\mathbf{1}}}$ @Lambek69, is obtained from ${\mathbf{L}^{\boldsymbol{*}}}$ by adding one axiom, $\vdash {\mathbf{1}}$ (its antecedent is empty), and one inference rule, $$\infer[{\mathbf{1}}L]{\Gamma, {\mathbf{1}}, \Delta \vdash C}
{\Gamma, \Delta \vdash C}$$ L-completeness, however, does not hold for ${{\mathbf{L}}_{\mathbf{1}}}$. Indeed, since ${\mathbf{1}}$ should be the unit w.r.t. $\cdot$, that is $A \cdot {\mathbf{1}}= A = {\mathbf{1}}\cdot A$ for any $A$, in L$\varepsilon$-models it should be interpreted as $\{ \varepsilon \}$. The following sequent is a counter-example for L-completeness: ${\mathbf{1}}{\mathop{/}}p, {\mathbf{1}}{\mathop{/}}p \vdash {\mathbf{1}}{\mathop{/}}p$. This sequent is true in all models for any interpretation of $p$, but is not derivable in ${{\mathbf{L}}_{\mathbf{1}}}$.

Throughout this paper, we shall frequently consider fragments of the calculi defined above in languages with restricted sets of connectives. Such a fragment will be denoted by the name of the calculus, followed by the list of connectives in parentheses: e.g., ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$.

Distributivity Law in Fragments with One Additive {#S:distr}
=================================================

It is well known, that ${\mathbf{MALC}}$ is incomplete w.r.t. L-models. The reason is the distributivity principle, $$(A \vee C) \wedge (B \vee C) \vdash (A \wedge B) \vee C.
\eqno{(\mathcal{D})}$$ On one hand, this principle is obviously true in all L-models. On the other hand, as noticed by Ono and Komori @OnoKomori, one needs the structural rules of contraction and weakening to derive it. In particular, the distributivity principle is not derivable in ${\mathbf{MALC}}$, ${\mathbf{MALC}^{\boldsymbol{*}}}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}$, ${\mathbf{ILL}}$, and ${\mathbf{ILL}}$.

The distributivity principle, as formulated above, includes <span>*both*</span> additive connectives, $\wedge$ and $\vee$. We investigate fragments of ${\mathbf{MALC}}$ with only one additive, $\wedge$ <span>*or*</span> $\vee$. The result of our study is that with respect to distributivity $\wedge$ and $\vee$ behave in opposite ways.

Let ${\mathbf{MALC}+\mathcal{D}}$ denote ${\mathbf{MALC}}$ with the distributivity principle added as an extra axiom scheme. In the presence of this axiom scheme, we have to keep cut as an official rule of the system (it is now not eliminable). A hypersequential system for ${\mathbf{MALC}+\mathcal{D}}$ was developed by Kozak @Kozak. Let us restrict ourselves to the product-free language (with product, proving L-completeness is hard even without extra connections @PentusAPAL [@PentusFmonov]). We also consider calculi without the unit constant: issues connected with ${\mathbf{1}}$ are discussed in Section \[S:unit\]. Thus, we consider two fragments of the multiplicative-additive Lambek calculus: ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ and ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\vee)$, and the corresponding fragments of bigger system up to ${\mathbf{IAL}}$. (For commutative calculi, we have only one implication, that is, consider fragments in the language of ${\multimap}, \wedge$ and ${\multimap}, \vee$.)

As shown by Buszkowski @Buszko1982, ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ is complete w.r.t. L-models. This yields the following corollary: ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ is a conservative fragment of <span>*both*</span> ${\mathbf{MALC}}$ and ${\mathbf{MALC}+\mathcal{D}}$. Indeed, any sequent provable in ${\mathbf{MALC}+\mathcal{D}}$ is true in all L-models; if it is in the language of ${\mathop{\backslash}},{\mathop{/}},\wedge$, it is derivable in ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ by L-completeness. In other words, the distributivity principle has no non-trivial corollaries in the language of ${\mathop{\backslash}},{\mathop{/}},\wedge$.

The situation with ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\vee)$ is opposite. Namely, we present a corollary of the distributivity principle in the language of ${\mathop{\backslash}},{\mathop{/}},\vee$, which is not provable in ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\vee)$. Thus, ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\vee)$ is not a conservative fragment of ${\mathbf{MALC}+\mathcal{D}}$, and is therefore incomplete w.r.t. L-models. Moreover, we show that this effect is of a more general nature. Namely, the same holds for the corresponding fragments of ${\mathbf{MALC}^{\boldsymbol{*}}}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}$, ${\mathbf{ILL}}$, and ${\mathbf{IAL}}$: distributivity has no new corollaries in the language with $\wedge$, but has such in the language with $\vee$.

Completeness with Additive Conjunction Only
-------------------------------------------

For the first series of results, concerning $\wedge$, we give a semantic proof. For each system, we consider a specific version of L-semantics. For ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ and ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, these are L-models and L$\varepsilon$-models respectively. For other systems, let us first give some definitions and prove correctness statements for them.

A language $A$ is called <span>*monotone,*</span> if for any word $u_1 u_2 \in A$ and an arbitrary word $w$ the word $u_1 w u_2$ also belongs to $A$.

If $A$ and $B$ are both monotone, then so are $A {\mathop{\backslash}}B$, $B {\mathop{/}}A$, and $A \wedge B$.

Let $u  = u_1 u_2 \in A {\mathop{\backslash}}B$. Then for any $v \in A$ we have $v u_1 u_2 \in B$. Now take $u' = u_1 w u_2$ for an arbitrary $w$. By monotonicity of $B$, the word $vu' = v u_1 w u_2$ is also in $B$. Since this holds for any $v \in A$, we get $u' \in A {\mathop{\backslash}}B$. The reasoning for $B {\mathop{/}}A$ is symmetric. The case of $A \wedge B$ is trivial.

A language $A$ is called <span>*commutative,*</span> if for any word $u = a_1 \ldots a_n$ belonging to $A$ and an arbitrary transposition $\sigma \in \mathbf{S}_n$ on $\{ 1, \ldots, n \}$ the word $a_{\sigma(1)} \ldots a_{\sigma(n)}$ also belongs to $A$.

Commutative languages are in one-to-one correspondence with multisets of letters from $\Sigma$. Thus, we can define the operation of <span>*multiset union,*</span> $A \uplus B$, for two commutative languages $A$ and $B$, which can be expressed as follows: $$A \uplus B = \{ a_{\sigma(1)} \ldots a_{\sigma(n)} \mid
\sigma \in \mathbf{S}_n \mbox{ and } 
a_1 \ldots a_n \in A \cdot B \}.$$

If $A$ is a commutative language, then $vu \in A$ if and only if $uv \in A$. Therefore, for commutative $A$ and $B$, we have $A {\mathop{\backslash}}B = B {\mathop{/}}A$; we denote this language by $A {\multimap}B$.

If $A$ and $B$ are commutative, then so is $A {\multimap}B$ and $A \wedge B$.

Commutativity of $A \wedge B$ is obvious. For $A {\multimap}B$, take any $u = a_1 \ldots a_n \in A {\multimap}B = B {\mathop{/}}A$ and let $u' = u_{\sigma(1)} \ldots u_{\sigma(n)}$. Now for any $v = a_{n+1} \ldots a_{m} \in A$. By definiton of $B {\mathop{/}}A$, we have $uv \in B$. Now by commutativity of $B$, the word $u'v$ also belongs to $B$. Indeed, it is obtained from $uv$ by the following transposition: $$\tilde{\sigma} =
 \left(
 \begin{matrix}
  1 & 2 & \ldots & n & n+1 & \ldots & m \\
  \sigma(1) & \sigma(2) & \ldots & \sigma(n) & n+1 & \ldots & m
 \end{matrix}\right).$$ Since $v \in A$ was taken arbitrarily, we conclude that $u' \in B {\mathop{/}}A = A {\multimap}B$.

Having the class of monotone languages and the class of commutative languages closed under our operations (${\mathop{\backslash}}$, ${\mathop{/}}$, $\wedge$), we can define the classes of restricted L$\varepsilon$-models for all our systems.

An L$\varepsilon$-model is monotone, if all languages in it are monotone. Truth of sequents is defined as in ordinary L$\varepsilon$-models.

A commutative L$\varepsilon$-model is an L$\varepsilon$-model, where all languages are commutative.

In commutative models $\uplus$ actually plays the role of product (while we do not have product as a connective, we still have the sequential comma, which is a hidden product), due to the following fact.

\[P:commtruth\] In a commutative L$\varepsilon$-model $w$, a sequent $A_1, \ldots, A_n \vdash B$ is true if and only if $w(A_1) \uplus \ldots \uplus w(A_n) \subseteq w(B)$.

The "if" part is due to the fact that $w(A_1) \cdot \ldots \cdot w(A_n) \subseteq w(A_1) \uplus \ldots \uplus w(A_n)$. The "only if" part holds since $w(B)$ is closed under transpositions.

Now we prove an extension of Buszkowski's completeness result

\[Th:compl\] Each of ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, ${\mathbf{AMALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, ${\mathbf{ILL}}({\multimap},\wedge)$, ${\mathbf{IAL}}({\multimap},\wedge)$ is sound and complete w.r.t. the corresponding class of models, according to the following table:

                              <span>*Calculus*</span>                                                   <span>*Models*</span>
  -------------------------------------------------------------------------------- ----------------------------------------------------------------
            ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$                                       L-models
   ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$                        L$\varepsilon$-models
   ${\mathbf{AMALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$                   monotone L$\varepsilon$-models
                        ${\mathbf{ILL}}({\multimap},\wedge)$                                      commutative L$\varepsilon$-models
                        ${\mathbf{IAL}}({\multimap},\wedge)$                        L$\varepsilon$-models, which are both monotone and commutative

The cases of ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ and ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ are due to Buszkowski @Buszko1982. Let us consider the remaining three systems.

The soundness part is easy: our conditions on models were specifically designed to reflect structural rules. In a monotone model, if $w(A_1) \cdot \ldots \cdot w(A_k) \cdot w(A_{k+1}) \cdot \ldots \cdot w(A_n) \subseteq w(B)$, then also $w(A_1) \cdot \ldots \cdot w(A_k) \cdot w(A) \cdot w(A_{k+1}) \cdot \ldots \cdot w(A_n) \subseteq w(B)$, thus the weakening rule is valid. If we have a commutative L$\varepsilon$-model, then the permutation rule is valid. This is obvious from Proposition \[P:commtruth\]: unlike $\cdot$, $\uplus$ is just commutative. All other rules and axioms are valid in arbitrary L$\varepsilon$-models.

Completeness is proved by Buszkowski's canonical model argument. We do it uniformly for all systems. In the canonical model, the alphabet $\Sigma$ is the set of all formulae of the given calculus, and for any formula $A$ let $$w_0(A) = \{ \Gamma \mid \Gamma \vdash A \mbox{ is derivable in the given system} \}.$$

First we show that $w_0$ is indeed an L${\varepsilon}$-model: $$\begin{aligned}
   & w_0(A {\mathop{\backslash}}B) = w_0(A) {\mathop{\backslash}}w_0(B); \\
   & w_0(B {\mathop{/}}A) = w_0(B) {\mathop{/}}w_0(A); \\
   & w_0(A \wedge B) = w_0(A) \wedge w_0(B).
  \end{aligned}$$ This is performed exactly as in Buszkowski's proof. Indeed, if $\Gamma \in w_0(A {\mathop{\backslash}}B)$, then for an arbitrary $\Delta \in w_0(A)$ we have $\Gamma \vdash A {\mathop{\backslash}}B$ and $\Delta \vdash A$. Applying cut with $A, A {\mathop{\backslash}}B \vdash B$, we get $\Delta, \Gamma \vdash A$ derivable in our system. Thus, $\Delta\Gamma \in w_0(B)$, therefore $\Gamma \in w_0(A) {\mathop{\backslash}}w_0(B)$. Notice that cut is available in all systems we consider. Dually, if $\Gamma \in w_0(A) {\mathop{\backslash}}w_0(B)$, then, since $A \in w_0(A)$ by the axiom, $A\Gamma \in w_0(B)$. This means derivability $A, \Gamma \vdash B$, thus $\Gamma \vdash A {\mathop{\backslash}}B$. Hence, $\Gamma \in w_0(A {\mathop{\backslash}}B)$.

The ${\mathop{/}}$ case is symmetric. For $\wedge$, we use the equivalence $\Gamma \vdash A \wedge B$ if and only if $\Gamma \vdash A$ and $\Gamma \vdash B$. Here the "if" part is an application of $\wedge R$, and the "only if" part is by cut with $A \wedge B \vdash A$ and $A \wedge B \vdash B$.

Next, is easy to see that the canonical model $w_0$ belongs to the corresponding class of models: monotone for ${\mathbf{AMALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, commutative for ${\mathbf{ILL}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, commutative and monotone for ${\mathbf{IAL}}({\mathop{\backslash}},{\mathop{/}},\wedge)$.

Finally, suppose a sequent $\Pi \vdash B$ is not derivable. Consider two cases. If $\Pi = A_1, \ldots, A_n$ is non-empty, then, since each $A_i$ belongs to $w(A_i)$, we have $\Gamma \in w(A_1) \cdot \ldots \cdot w(A_n)$. On the other hand, $\Gamma \notin w(B)$. This falsifies $\Pi \vdash B$ under interpretation $w_0$. If $\Pi$ is empty, then we have $\varepsilon \notin w(B)$, which again falsifies $\Pi \vdash B$. This finishes the completeness proof.

It is easy to see that soundness actually extends to the language with $\vee$ (interpreted as set-theoretic union). Unions of monotone languages are also monotone, the same for commutative languages. The situation with product is a bit more complicated for commutative systems, since $A \cdot B$ is usually not commutative, even for commutative $A$ and $B$. Thus, we have to alter the definition of language models in the commutative case, requiring $w(A \cdot B) = w(A) \uplus w(B)$ instead of $w(A \cdot B) = w(A) \cdot w(B)$. Under this modification, soundness holds for product also. Finally, notice that in all models we consider $\vee$ and $\wedge$ are interpreted set-theoretically, thus, obey the distributivity law. These considerations yield the following soundness result:

\[P:sound\] Each of ${\mathbf{MALC}}+ \mathcal{D}$, ${\mathbf{MALC}^{\boldsymbol{*}}}+ \mathcal{D}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}+ \mathcal{D}$, ${\mathbf{ILL}}+ \mathcal{D}$, ${\mathbf{IAL}}+ \mathcal{D}$ is sound w.r.t. the corresponding class of models, according to the table in Theorem \[Th:compl\]; for ${\mathbf{ILL}}$ and ${\mathbf{IAL}}$ in the models we use $\uplus$ to interpret $\cdot$.

Now we are ready to state and prove our conservativity result.

\[Th:conservdisj\] The systems in the restricted language without $\vee$, ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, ${\mathbf{AMALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, ${\mathbf{ILL}}({\multimap},\wedge)$, and are conservative fragments of ${\mathbf{MALC}}+ \mathcal{D}$, ${\mathbf{MALC}^{\boldsymbol{*}}}+ \mathcal{D}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}+ \mathcal{D}$, ${\mathbf{ILL}}+ \mathcal{D}$, and ${\mathbf{IAL}}+ \mathcal{D}$ respectively.

Let $\Pi \vdash B$ be a sequent in the language of ${\mathop{\backslash}}, {\mathop{/}}, \wedge$ (in the commutative case, ${\multimap}, \wedge$). Suppose it is derivable in one of the distributive systems, ${\mathbf{MALC}}+ \mathcal{D}$, …, ${\mathbf{IAL}}+ \mathcal{D}$. Then by Proposition \[P:sound\] it is true in all models of the corresponding class. By Theorem \[Th:compl\] it is derivable in, respectively, ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$, …, ${\mathbf{IAL}}({\multimap},\wedge)$.

Incompleteness with Additive Disjunction Only
---------------------------------------------

If we take $\vee$ instead of $\wedge$, however, no analog of the conservativity result like Theorem \[Th:conservdisj\] is possible, due to the following counter-example.

\[Th:disj\] The sequent $$\begin{gathered}
  ((x {\mathop{/}}y) \vee w) {\mathop{/}}((x {\mathop{/}}y) \vee (x {\mathop{/}}z) \vee w),
  (x {\mathop{/}}y) \vee w, \\ 
  ((x {\mathop{/}}y) \vee w) {\mathop{\backslash}}((x {\mathop{/}}z) \vee w) \vdash (x {\mathop{/}}(y \vee z)) \vee w
  \end{gathered}$$ is derivable in ${\mathbf{MALC}+\mathcal{D}}$ but this sequent is not derivable in ${\mathbf{IAL}}$.

This sequent is in the language of ${\mathop{\backslash}},{\mathop{/}},\vee$. The theorem states that it is derivable in ${\mathbf{MALC}}+ \mathcal{D}$, and therefore in all its extensions up to ${\mathbf{IAL}}+ \mathcal{D}$, but not in the corresponding (${\mathop{\backslash}},{\mathop{/}},\vee$) fragments without the distributivity law added. Thus, this is a non-trivial corollary of $\mathcal{D}$ in the language without $\wedge$. In particular, Theorem \[Th:disj\] implies that ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\vee)$ is incomplete w.r.t. L-models, as well as ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\vee)$, ${\mathbf{AMALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\vee)$, ${\mathbf{ILL}}({\multimap},\vee)$, ${\mathbf{IAL}}({\multimap},\vee)$ are incomplete w.r.t. the corresponding modifications of L-models (compare with Theorem \[Th:compl\]).

Before proving Theorem \[Th:disj\], let us make some remarks. First, let us notice that the sequent in this theorem is slightly different from the one in our WoLLIC 2019 paper @KanKuzSceWoLLICLMod, where one variable is used for $x$ and $w$. The reason is that the old example happens to be derivable in ${\mathbf{IAL}}$ (but still not in ${\mathbf{ILL}}$ and weaker systems).

Second, the hard part of Theorem \[Th:disj\] is, of course, the second one (non-derivability). Fortunately, the derivability problem in ${\mathbf{MALC}}$ is algorithmically decidable (belongs to PSPACE), thus, it is possible to establish non-derivability by exhaustive proof search. This proof search was first performed, as a pre-verification of the result, automatically using an affine modification of <span>llprover</span> by Tamura @Tamura. (For the WoLLIC 2019 paper, we used a ${\mathbf{MALC}}$ prover by Jipsen @Jipsenprover, based on the algorithm by Okada and Terui @OkadaTerui.) In order to make this article self-contained and independent from proof-search software, here we present a complete manual proof search.

One of the WoLLIC 2019 reviewers suggested a shorter method of proving non-derivability of the given sequent in ${\mathbf{MALC}}$, via an algebraic counter-model. This counter-model is a commutative residuated lattice on the set $R = \{ 0, a, b, c, 1 \}$. The order is defined as follows: $0 \prec a,b,c \prec 1$; $a,b,c$ are incomparable. Product and residual are defined as follows: $$\begin{array}{c|ccccc}
\cdot&0&a&b&c&1\\\hline
0&0&0&0&0&0\\
a&0&a&b&c&1\\
b&0&b&a&c&1\\
c&0&c&c&0&c\\
1&0&1&1&c&1\\
\end{array}
\qquad
\begin{array}{c|ccccc}
{\multimap}&0&a&b&c&1\\\hline
0&1&1&1&1&1\\
a&0&a&b&c&1\\
b&0&b&a&c&1\\
c&c&c&c&1&1\\
1&0&0&0&c&1\\
\end{array}$$ (In the commutative situation, we have only one residual, which we denote by ${\multimap}$.) Variables are interpreted as follows: $y$ as $b$, $z$ as $c$, $x$ and $w$ both as $a$. This algebraic model falsifies the sequent in Theorem \[Th:disj\]. However, is insufficient for our new purposes. The reason is that in this model $a \cdot b = b \not\preceq a$, while in the presence of weakening $A \cdot B \vdash A$ should be true. Thus, in order to establish non-derivability of our sequent not only in ${\mathbf{MALC}}$, but also in ${\mathbf{IAL}}$, we use the good old syntactic method.

\[Proof of Theorem \[Th:disj\]\] The first statement is proved using the joining (diamond) construction, the idea of which goes back to Lambek @Lambek58 and Pentus @PentusJoLLI. Indeed, let $A = (x {\mathop{/}}y) \vee w$ and $B = (x {\mathop{/}}z) \vee w$. Then $A \vee B$ is equivalent to $(x {\mathop{/}}y) \vee (x {\mathop{/}}z) \vee w$. One can easily check derivability of $A {\mathop{/}}(A \vee B), A, A {\mathop{\backslash}}B \vdash A$ and $A {\mathop{/}}(A \vee B), A, A {\mathop{\backslash}}B \vdash B$ in ${\mathbf{MALC}}$. Notice that the antecedent of this sequent is exactly the one in the sequent of our theorem. Next, we derive $A {\mathop{/}}(A \vee B), A, A {\mathop{\backslash}}B \vdash A \wedge B$, and further by distributivity $A \wedge B \equiv ((x {\mathop{/}}y) \wedge (x {\mathop{/}}z)) \vee w \equiv
 (x {\mathop{/}}(y \vee z)) \wedge w$.

The second statement is proved by an exhaustive proof search for the sequent $$\begin{gathered}
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) {\multimap}((y {\multimap}x) \vee w),
 (y {\multimap}x) \vee w, \\
 ((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w)
 \vdash ((y \vee z) {\multimap}x) \vee w
 \end{gathered}$$ (the translation of our sequent into the commutative language) in ${\mathbf{IAL}}$.

In order to facilitate proof search, we take into account the following considerations.

First, the rules $\vee L$ and ${\multimap}R$ are invertible. Thus, we can suppose they are applied immediately. Moreover, $\vee L$ has two premises, and when disproving derivability we have the right to choose one and establish non-derivability there.

Second, we can suppose that in our (hypothetic) derivation instances of $\vee L_r$ of the form $\dfrac{\Gamma \vdash w}{\Gamma \vdash F \vee w}$ are directly preceded by axioms. Indeed, such instances are interchangeable upwards with ${\multimap}L$ and $\vee L$, and ${\multimap}R$ cannot appear before this $\vee L_r$, since $w$ is a variable. Other rules are impossible by the polarized subformula property.

Third, we establish non-derivability of several sequents, which will appear frequently in our proof search: $$\label{yxw}
 \not\vdash (y {\multimap}x) \vee w$$ $$\label{zyxw}
  z \not\vdash (y {\multimap}x) \vee w$$ $$\label{yyxw}
 y \not\vdash (y {\multimap}x) \vee w$$ $$\label{zyyxw}
  z,y \not\vdash (y {\multimap}x) \vee w$$ $$\label{zzyxw}
  z,z \not\vdash (y {\multimap}x) \vee w$$ $$\label{zyxzxw}
 z \not\vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$$ $$\label{yxzxw}
 \not\vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$$ $$\label{zyyxzxw}
 z, y \not\vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$$

Now we are ready to start proof search. First we invert $\vee L$ introducing $(y {\multimap}x) \vee w$ and choose $y {\multimap}x$: $$\begin{gathered}
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w),
 y \stackrel{3}{{\multimap}} x, \\
 ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w)
 \vdash ((y \vee z) {\multimap}x) \stackrel{1}{\vee} w
 \end{gathered}$$ Now we have a choice of 4 principal connectives (denoted by numbers in the sequent) to be decomposed first.

<span>**Case 1.**</span> In this case, we use $\vee R_l$, thanks to our consideration that $\vee R_r$ with $w$ should be applied immediately after an axiom. $$\begin{gathered}
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w),
 y \stackrel{3}{{\multimap}} x, \\
 ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w)
 \vdash (y \vee z) {\multimap}x
 \end{gathered}$$ Invert ${\multimap}R$ and $\vee L$, choosing $z$ out of $y \vee z$: $$\begin{gathered}
((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w),
 y \stackrel{3}{{\multimap}} x,\\
 ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w), z \vdash x\end{gathered}$$

Now we can decompose (by ${\multimap}L$) one of the implications 2–4, and for each we have a choice of $8 = 2^3$ ways of splitting the rest of the antecedent into $\Pi$ and $\Gamma$. Making use of the weakening rule, however, we can reduce the number of cases.

<span>**Subcase 1–2.**</span> If $\Pi$ includes $y \stackrel{3}{{\multimap}x}$, then the right premise is $\Gamma, (y {\multimap}x) \vee w \vdash x$, where $\Gamma$ is a subset of $z, ((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w)$. Notice that if $\Gamma' \subseteq \Gamma$ and the sequent is not derivable with $\Gamma$, it is also not derivable with $\Gamma'$ (otherwise we could derive it with $\Gamma$ using the weakening rule). However, the sequent is not derivable even with the maximal $\Gamma$: $$z, ((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w), (y {\multimap}x) \vee w
\not\vdash x.$$ Indeed, invert $\vee L$ and choose $w$: $$z, w, ((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w) \not \vdash x.$$ Here one should use ${\multimap}L$, but then in its right premise we can again invert $\vee L$ choosing $w$, which yields one of: $$w \vdash x \qquad z,w \vdash x \qquad w,w \vdash x \qquad
 z,w,w \vdash x.$$ None of these is derivable.

If $\Pi$ does not include $y \stackrel{3}{{\multimap}} x$, then $\Pi$ is a subset of $((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w), z$, and we again take the maximal $\Pi$ in the left premise: $$\label{three}
 ((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w), z \vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$$ Decomposing ${\multimap}$ yields either $\vdash (y {\multimap}x) \vee w$ or $z \vdash (y {\multimap}x) \vee w$, both not derivable by (\[yxw\]) and (\[zyxw\]). Thus, we have to decompose $\vee$ on the right.

Taking $y {\multimap}x$ (and inverting ${\multimap}R$) yields $$((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w), z, y \vdash x.$$ Now we again have to use ${\multimap}L$. The new cases are $y \vdash (y {\multimap}x) \vee w$ and $z, y \vdash (y {\multimap}x) \vee w$, both not derivable (\[yyxw\])(\[zyyxw\]).

Taking $z {\multimap}x$ and inverting ${\multimap}R$ gives $$((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w), z, z \vdash x.$$ Decomposing ${\multimap}$ fails due to (\[yxw\])(\[zyxw\])(\[zzyxw\]).

<span>**Subcase 1–3.**</span> Apply ${\multimap}L$ for $\stackrel{3}{{\multimap}}$ and consider its left premise with the maximal possible $\Pi$: $$\label{vorpal}
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w), ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}}
 ((z {\multimap}x) \vee w), z \vdash y.$$

<span>*Subsubcase 1–3–2.*</span> Decompose $\stackrel{2}{{\multimap}}$. If the big formula with $\stackrel{4}{{\multimap}}$ goes to the new $\Gamma$, then the new $\Pi$ is either $z$ or empty. However, neither $z \vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$ nor $\vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$ is derivable (\[zyxzxw\])(\[yxzxw\]). If the formula with $\stackrel{4}{{\multimap}}$ goes to the new $\Pi$, then the new $\Gamma$ is either $z$ or empty. This gives, at maximum, $z, (y {\multimap}x) \vee w \vdash y$, which is falsified by choosing $w$ in the inverted $\vee L$: $z, w \not\vdash y$.

<span>*Subsubcase 1–3–4.*</span> Decompose $\stackrel{4}{{\multimap}}$. Again, if the big formula (now with $\stackrel{2}{{\multimap}}$) goes to the new $\Gamma$, we falsify the left premise by (\[yxw\]) or (\[zyxw\]). Otherwise, the right premise is, at maximum, $z, (z {\multimap}x) \vee w \vdash y$, which is again falsified by choosing $w$.

<span>**Subcase 1–4.**</span> If $\Pi$ includes $y \stackrel{3}{{\multimap}} x$, then the right premise is, at maximum, $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w), z, (z {\multimap}x) \vee w \vdash x$$ Invert $\vee L$ and choose $w$: $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w), z, w \vdash x$$ Now we have to use $\stackrel{2}{{\multimap}} L$. Its right premise is, at maximum, $z,w,(y {\multimap}x) \vee w \vdash x$. Choosing $w$ falsifies it.

If $y \stackrel{3}{{\multimap}} x$ is in $\Gamma$, then the maximal version of the <span>*left*</span> premise is $$\label{jujub}
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w), z \vdash (y {\multimap}x) \vee w.$$ Applying $\stackrel{2}{{\multimap}}$ right now is impossible: its left premise gets falsified by (\[yxzxw\]) or (\[zyxzxw\]). Apply $\vee R_l$ (recall that $\vee R_r$ is used only directly below axiom) and invert ${\multimap}R$: $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
 ((y {\multimap}x) \vee w), z, y \vdash x.$$ Here the left premise of $\stackrel{2}{{\multimap}}$ is also falsified by (\[yxzxw\]), (\[zyxzxw\]), or (\[zyyxzxw\]).

<span>**Case 2.**</span> Consider again two cases, depending on whether $y \stackrel{3}{{\multimap}} x$ goes to $\Pi$ or to $\Gamma$. If it goes to $\Pi$, then the right premise is, at maximum, $$(y {\multimap}x) \vee w,
 ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w) \vdash
 ((y \vee z) {\multimap}x) \stackrel{1}{\vee} w.$$ Invert $\vee L$ and choose $y {\multimap}x$: $$\label{alice}
 y \stackrel{5}{{\multimap}} x, ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w) \vdash
 ((y \vee z) {\multimap}x) \stackrel{1}{\vee} w.$$

For reusal of our reasoning in further cases, we shall falsify a stronger sequent $$\label{rabbit}
 y \stackrel{5}{{\multimap}} x, ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w) \vdash
 ((y \vee z) {\multimap}x) \stackrel{1}{\vee} w.$$

Indeed, $(y {\multimap}x) \vee w \vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$, and therefore $((y {\multimap}x) \vee (z {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w) \vdash ((y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w)$ is derivable in ${\mathbf{IAL}}$. Thus, if (\[alice\]) happens to be derivable then, by cut, so will be (\[rabbit\]).

Now we decompose one of $\stackrel{1}{\vee}$, $\stackrel{4}{{\multimap}}$, $\stackrel{5}{{\multimap}}$ in (\[rabbit\]).

<span>**Subcase 2–$\Pi$–1.**</span> Recall that we never choose $w$ in $\vee R$, and invert ${\multimap}R$: $$y \stackrel{5}{{\multimap}} x, 
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w), 
 y \vee z \vdash x.$$ Invert $\vee L$ and choose $z$: $$y \stackrel{5}{{\multimap}} x, 
 ((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w), 
  z \vdash x.$$

<span>*Subsubcase 2–$\Pi$–1–5.*</span> The left premise is, at maximum, $$((y {\multimap}x) \vee (z {\multimap}x) \vee w)
 \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w), z \vdash y.$$ Applying $\stackrel{4}{{\multimap}} L$ is impossible, since its right premise is falsified by choosing $w$: $w,z \not\vdash y$ and $w \not\vdash y$.

<span>*Subsubcase 2–$\Pi$–1–4.*</span> Again, if $y \stackrel{5}{{\multimap}} x$ goes to the new $\Pi$, then the right premise is, at maximum, $z, (z {\multimap}x) \vee w \vdash x,$ which is falsified by choosing $w$. If it goes to the new $\Gamma$, then the new <span>*left*</span> premise is, at maximum, $z \vdash (y {\multimap}x) \vee (z {\multimap}x) \vee w$, which is not derivable by (\[zyxzxw\]).

<span>**Subcase 2–$\Pi$–4.**</span> If the new $\Pi$ is empty, then the left premise is falsified by (\[yxzxw\]). Otherwise, the right premise is $$(z {\multimap}x) \vee w \vdash ((y \vee z) {\multimap}x) \vee w.$$ Invert $\vee L$ and choose $z {\multimap}x$: $$z {\multimap}x \vdash ((y \vee z) {\multimap}x) \vee w.$$ Applying ${\multimap}L$ is impossible ($\not\vdash z$); also $z {\multimap}x \not\vdash w$. Thus, we have to use $\vee R_l$, and we can immediately apply ${\multimap}R$ afterwards: $
 z {\multimap}x, y \vee z \vdash x.
 $ Inverting $\vee L$ and choosing $y$ falsifies this sequent: $z {\multimap}x, y \not\vdash x$.

<span>**Subcase 2–$\Pi$–5.**</span> The left premise is, at maximum, $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w) \vdash y.$$ This is not derivable.

Now let, in Case 2, $y \stackrel{3}{{\multimap}} x$ go to $\Gamma$. Then the left premise is, at maximum, $$((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} ((z {\multimap}x) \vee w) \vdash
(y {\multimap}x) \vee (z {\multimap}x) \vee w.$$ This sequent is stronger than (\[three\])—that is, (\[three\]) can be obtained from it by weakening. Therefore, it cannot be derivable, since we've already falsified (\[three\]) in Case 1.

<span>**Case 3.**</span> Take the maximal possible $\Pi$ and consider the left premise: $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}}
((y {\multimap}x) \vee w), ((y {\multimap}x) \vee w) \stackrel{4}{{\multimap}} 
((z {\multimap}x) \vee w) \vdash y.$$ This sequent is stronger than (\[vorpal\]), and therefore not derivable: (\[vorpal\]) was falsified in Case 1.

<span>**Case 4.**</span> If $y \stackrel{3}{{\multimap}} x$ goes to $\Pi$, then the maximal version of the right premise of $\stackrel{4}{{\multimap}} L$ is $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}} ((y {\multimap}x) \vee w), (z {\multimap}x) \vee w \vdash ((y \vee z) {\multimap}x) 
\stackrel{1}{\vee} w.$$ Invert $\vee L$ and choose $z {\multimap}x$: $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) \stackrel{2}{{\multimap}} ((y {\multimap}x) \vee w), z \stackrel{6}{{\multimap}} x \vdash ((y \vee z) {\multimap}x) 
\stackrel{1}{\vee} w.$$ Suppose this sequent is derivable. Then it will also be derivable after swapping variables $y$ and $z$: $$((z {\multimap}x) \vee (y {\multimap}x) \vee w) {\multimap}((z {\multimap}x) \vee w), y {\multimap}x \vdash ((z \vee y) {\multimap}x) 
\vee w.$$ This sequent, however, is exactly (\[rabbit\]), up to commutativity; (\[rabbit\]) was falsified in Case 2.

Finally, if $y \stackrel{3}{{\multimap}} x$, in Case 4, goes to $\Gamma$, then the maximal version of the left premise of $\stackrel{4}{{\multimap}} L$ is $$((y {\multimap}x) \vee (z {\multimap}x) \vee w) {\multimap}((y {\multimap}x) \vee w) \vdash ((y \vee z) {\multimap}x) \vee w.$$ This sequent is stronger than (\[jujub\]) and therefore cannot be derivable.

Undecidability with ${\mathop{\backslash}}$, $\wedge$, and ${\mathbf{1}}$ {#S:unit}
=========================================================================

The System ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$ and Its Undecidability
----------------------------------------------------------------------------------------------------------

In this section we consider the extension of the Lambek calculus with the multiplicative unit constant. The language of our fragment will be as follows: ${\mathop{\backslash}}$, $\wedge$, ${\mathbf{1}}$. As shown by Buszkowski @Buszko1982, in the fragment of ${\mathop{\backslash}}$ and $\wedge$ the Lambek calculus with empty antecedents is complete w.r.t. L$\varepsilon$-models. As noticed in the Introduction, however, this is not the case if we add ${\mathbf{1}}$. In L$\varepsilon$-models, because of the principle $A \cdot {\mathbf{1}}\vdash {\mathbf{1}}$, the unit constant ${\mathbf{1}}$ is necessarily interpreted as the singleton set $\{\varepsilon\}$, where $\varepsilon$ is the empty word. (In the presence of the unit constant, we allow the empty word to belong to our languages and abolish Lambek's non-emptiness restriction.) This particular interpretation of ${\mathbf{1}}$ satisfies certain principles, including $A \cdot \{ \varepsilon \} = \{ \varepsilon \} \cdot A$ and $\{ \varepsilon \} \cdot \{ \varepsilon \} = \{ \varepsilon \}$. Moreover, these principles keep valid for languages of the form $\{\varepsilon\} \cap B$ (for any $B$). Indeed, this language is either $\{\varepsilon\}$ or $\varnothing$, and for the empty set $\varnothing$ we also have $A \cdot \varnothing = \varnothing \cdot A$ and $\varnothing \cdot \varnothing = \varnothing$.

Below we present a calculus denoted by ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$, which reflects these principles as sequential rules: $$\infer[Id]{A \vdash A}{}
\qquad
\infer[{\mathbf{1}}]{A, {\mathbf{1}}\vdash A}{}$$ $$\infer[{\mathop{\backslash}}L]{\Gamma, \Pi, A {\mathop{\backslash}}B, \Delta \vdash C}
{\Pi \vdash A & \Gamma, B, \Delta \vdash C}
\qquad
\infer[{\mathop{\backslash}}R]{\Pi \vdash A {\mathop{\backslash}}B}
{A, \Pi \vdash B}$$ $$\infer[\wedge L_l]{\Gamma, A \vee B \vdash C}{\Gamma, A \vdash C}
 \qquad
 \infer[\wedge L_r]{\Gamma, A \vee B \vdash C}{\Gamma, B \vdash C}
 \qquad 
 \infer[\wedge R]{\Pi \vdash A \wedge B}{\Pi \wedge A & \Pi \wedge B}$$ $$\infer[L\varepsilon]
{\Gamma, {\mathbf{1}}\wedge G, A, \Delta \vdash C}
{\Gamma, A, {\mathbf{1}}\wedge G, \Delta \vdash C}
\quad
\infer[R\varepsilon]
{\Gamma, A, {\mathbf{1}}\wedge G, \Delta \vdash C}
{\Gamma, {\mathbf{1}}\wedge G, A, \Delta \vdash C}
\quad
\infer[D\varepsilon]
{\Gamma, {\mathbf{1}}\wedge G, \Delta \vdash C}
{\Gamma, {\mathbf{1}}\wedge G, {\mathbf{1}}\wedge G, \Delta \vdash C}$$

The rules $L\varepsilon$ and $R\varepsilon$ are called "commuting" rules; they reflect the fact that, for any set $X$, $X \cdot \{\varepsilon\} = \{\varepsilon\} \cdot X$ and $X \cdot \varnothing = \varnothing \cdot X$. The "doubling" rule $D \varepsilon$ is caused by $\{\varepsilon\} \cdot \{\varepsilon\} = \{\varepsilon\}$ and $\varnothing \cdot \varnothing =
\varnothing$. Thus, these rules express natural algebraic properties of the interpretation of ${\mathbf{1}}$ as $\varnothing$. However, we emphasize that they are not admissible in the standard calculus ${{\mathbf{L}}_{\mathbf{1}}}$, introduced by Lambek @Lambek69, that is, non-commutative intuitionistic multiplicative-additive linear logic.

The rules $L\varepsilon$, $R\varepsilon$, and $D \varepsilon$ are not new. Their underlying principles, namely, $({\mathbf{1}}\wedge G) \cdot A \equiv A \cdot ({\mathbf{1}}\wedge G)$ and $({\mathbf{1}}\wedge G) \cdot ({\mathbf{1}}\wedge G) \equiv {\mathbf{1}}\wedge G$ appear in works of the Hungarian school (Andréka, Mikulás, Németi). Namely, in @Andreka2011TCS one can find the first of these equivalences (denoted there as formula 3.2), as one of the principles which is true in language algebras, but not in algebras of binary relations. The second equivalence is true for binary relations also; formula (CbI) in @Andreka2011AlgUniv is actually its stronger version, $({\mathbf{1}}\wedge G) \cdot ({\mathbf{1}}\wedge F) \equiv {\mathbf{1}}\wedge G \wedge F$. We get our $({\mathbf{1}}\wedge G) \cdot ({\mathbf{1}}\wedge G) \equiv {\mathbf{1}}\wedge G$ by taking $F = G$.

Andréka, Mikulás, and Sain @Andreka1994LIF also sketch an undecidability proof for a system related to the one considered here. Their proof is based on the technique of Kurucz et al. @Kurucz1993. The system considered in @Andreka1994LIF is the logic of residuated distributive lattices over monoids. Unlike the case we consider in this section, their system requires product, the unit and also the zero constant (the minimal element of the lattice) to be present in the language. Here we require only division, additive conjunction, and the unit. The trade-off is that we consider a narrower class of models. Namely, we consider only L$\varepsilon$-models, and these models, as shown above, allow extra principles for ${\mathbf{1}}$.

We do not claim that ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$ is an L$\varepsilon$-complete system. Indeed, the L$\varepsilon$-complete extension of ${{\mathbf{L}}_{\mathbf{1}}}$ happens to be quite involved (cf. @KuznJANCL). In particular, it is still an open problem whether such a complete system is recursively enumerable. The cut rule is not included in ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$, so all our derivations will be cut-free. We do not claim that cut is admissible in this system.

We prove undecidability for the whole range of systems between ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$ and the L$\varepsilon$-complete system in the language of ${\mathop{\backslash}}$, $\wedge$, ${\mathbf{1}}$.

\[Th:undec\] Let $\mathcal{L}$ be an L$\varepsilon$-sound logic which includes ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$. Then the derivability problem for $\mathcal{L}$ is undecidable.

Our undecidability proof is based on encoding computations of 2-counter Minsky machines @Kanovich1995Minsky. In the forward encoding, from Minsky computations to derivations in our calculus, we present explicit derivations in ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$. For the backwards direction, from derivations to computations, we use a semantic approach using L-models (cf. @Lafont [@LafontScedrov; @OkadaTerui], where phase semantics was used for similar purposes). Thus, we get undecidability not only for ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$ itself, but for the whole range of its L$\varepsilon$-sound extensions.

Before going further, let us introduce the <span>*relative double negation*</span> construction. We fix a variable (atomic proposition) $b$ and define relative negation $A^b$ as $$A^b = A {\mathop{\backslash}}b.$$ The term "negation" here is motivated as follows. In linear logic with the falsity constant $\bot$, negation is expressed as $A^\bot = A {\multimap}\bot$. Here we do the same non-commutatively, but due to lack of the $\bot$ constant we replace it by a fixed variable. This is the minimal logic approach: variable $b$ can be read as "false," but no specific axioms like $b \vdash A$ (<span>*ex falso*</span>) are imposed for $b$.

The relative double negation now is $$A^{bb} = (A {\mathop{\backslash}}b) {\mathop{\backslash}}b.$$ Notice the difference from the more usual in the Lambek calculus "type raising" version of something like double negation: ${}^b A^{b} = b {\mathop{/}}(A {\mathop{\backslash}}b)$. In our setting, we have neither $A^{bb} \vdash A$ (due to the intuitionistic nature of the Lambek calculus), nor $A \vdash A^{bb}$ (due to non-commutativity; in contrast, $A \vdash {}^b A^{b}$ is derivable). Nevertheless, $A^{bb}$ will be useful for our construction.

Given a sequence of formulae $\Phi = A_1, A_2, \ldots, A_{m-1}, A_m$ and a formula $C$, we introduce the notation $$\Phi {\mathop{\backslash}}C = A_m {\mathop{\backslash}}(A_{m-1} {\mathop{\backslash}}\ldots {\mathop{\backslash}}(A_2 {\mathop{\backslash}}(A_1 {\mathop{\backslash}}C)) \ldots ).$$ In particular, $$\Phi^b = A_m {\mathop{\backslash}}(A_{m-1} {\mathop{\backslash}}\ldots {\mathop{\backslash}}(A_2 {\mathop{\backslash}}(A_1 {\mathop{\backslash}}b)) \ldots )$$ and $$\Phi^{bb} = \bigl( A_m {\mathop{\backslash}}(A_{m-1} {\mathop{\backslash}}\ldots {\mathop{\backslash}}(A_2 {\mathop{\backslash}}(A_1 {\mathop{\backslash}}b)) \ldots ) \bigr) {\mathop{\backslash}}b.$$

In what follows, we suppose that the $^{bb}$ operation has a higher priority than ordinary division ${\mathop{\backslash}}$.

Consider a non-deterministic Minsky machine $\mathfrak{M}$ with a finite set of states $\{ L_0, L_1, \ldots, L_n \}$. A configuration of $\mathfrak{M}$ is a triple $(L_i, k_1, k_2)$, where $L_i$ is the current state and $k_1$ and $k_2$ are the current values of $\mathfrak{M}$'s two counters. The counters themselves are denoted by $c_1$ and $c_2$. The configuration $(L_0,0,0)$ is considered the <span>*final*</span> one; the initial configuration can be taken arbitrarily.

Configurations of Minsky machines are encoded as follows. We introduce distinct variables $e_1$, $e_2$, $p_1$, $p_2$, $l_0$, $l_1$, …, $l_n$ and represent configuration $(L_i, k_1, k_2)$ as $$e_1, \underbrace{p_1, \ldots, p_1}_{\text{$k_1$ times}}, l_i,
\underbrace{p_2, \ldots, p_2}_{\text{$k_2$ times}}, e_2.$$ In particular, the final configuration $(L_0,0,0)$ is represented as $e_1, l_0, e_2$.

Minsky instructions are encoded according to the following table:

   <span>*Instruction $I$*</span>             <span>*Formula $A_I$*</span>
  -------------------------------- ---------------------------------------------------
   <span>inc</span>$(L_i,1,L_j)$       $l_i {\mathop{\backslash}}(p_1, l_j)^{bb}$
   <span>inc</span>$(L_i,2,L_j)$       $l_i {\mathop{\backslash}}(l_j, p_2)^{bb}$
   <span>dec</span>$(L_i,1,L_j)$       $(p_1, l_i) {\mathop{\backslash}}l_j^{bb}$
   <span>dec</span>$(L_i,2,L_j)$       $(l_i, p_2) {\mathop{\backslash}}l_j^{bb}$
   <span>jz</span>$(L_i, 1, L_j)$   $(e_1, l_i) {\mathop{\backslash}}(e_1, l_j)^{bb}$
   <span>jz</span>$(L_i, 2, L_j)$   $(l_i, e_2) {\mathop{\backslash}}(l_j, e_2)^{bb}$

Here instruction <span>inc</span>$(L_i,r,L_j)$ <span>*(increment)*</span> means "at state $L_i$, increase $c_r$ by 1 and go to $L_j$" ($r = 1,2$). Instruction <span>dec</span>$(L_i,r,L_j)$ <span>*(decrement)*</span> means "at state $L_i$, decrease $c_r$ by 1 and go to $L_j$." If $k_r = 0$, then this instruction cannot be applied. Finally, <span>jz</span>$(L_i,r,L_j)$ <span>*(zero-test)*</span> means "at state $L_i$, if $k_r = 0$, go to $L_j$." Now if $k_r \ne 0$, then the instruction cannot be applied.

Notice that our version of zero-test and decrement instructions are very restrictive. Once the counter has a wrong value (zero for decreasing or non-zero for zero-test), the machine just fails to proceed. Usually, in such cases the machine is allowed to perform conditional branching (e.g., zero-test jumps to $L_j$ if the counter is zero and safely stays at $L_i$ if not). These restrictions, however, are compensated by the allowed non-determinism of $\mathfrak{M}$. Indeed, the compound <span>jzdec</span>$(L_i, r, L_{j_1}, L_{j_2})$ instruction from Minsky's original formalism @Minsky1961, meaning "at state $L_i$, if $k_r \ne 0$, decrease $c_r$ by one and go to $L_{j_1}$, and if $k_r = 0$, go to $L_{j_2}$," is modelled by adding simultaneously two instructions: <span>dec</span>$(L_i, r, L_{j_1})$ and <span>jz</span>$(L_i, r, L_{j_2})$. This non-deterministically branches computation; however, exactly one branch (depending on whether $k_r = 0$) could be successful, the other one immediately fails.

Let us denote the set of our variables, except $b$, by ${\mathcal{V}}$: $${\mathcal{V}}= \{ e_1, e_2, p_1, p_2, l_0, l_1, \ldots, l_n \}.$$

Finally, the Minsky machine $\mathfrak{M}$ is represented by the following formula $$G = ((e_1, l_0, e_2) {\mathop{\backslash}}b) \wedge \bigwedge_{I} A_I \wedge \bigwedge_{q \in {\mathcal{V}}} (q {\mathop{\backslash}}q^{bb}).$$ Here in the first big conjunction $I$ ranges among all instructions of $\mathfrak{M}$.

Now we are ready to state our main encoding theorems.

\[Th:encforw\] If $\mathfrak{M}$ can reach the final configuration $(L_0,0,0)$, starting from $(L_i,k_1,k_2)$, then the following sequent is derivable in ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$: $${\mathbf{1}}\wedge G, e_1, \underbrace{p_1, \ldots, p_1}_{\text{$k_1$ times}}, l_i,
\underbrace{p_2, \ldots, p_2}_{\text{$k_2$ times}}, e_2 \vdash b.\eqno{(*)}$$

\[Th:encback\] If the sequent $(*)$ is true in all L$\varepsilon$-models, then $\mathfrak{M}$ can reach $(L_0,0,0)$ from $(L_i,k_1,k_2)$.

Notice that our encodings are in a sense "upside-down": the starting configuration corresponds to the goal sequent in our derivation, and the sequent encoding the final configuration $(L_0,0,0)$ is on the top of the derivation, very close to axioms (see proof of Theorem \[Th:encforw\] below). The right intuition here is to consider the derivation in the direction of proof search, developing from the goal up to axioms. This direction correctly reflects the direction of Minsky computation.

Theorem \[Th:undec\] (our undecidability result) immediately follows from Theorems \[Th:encforw\] and \[Th:encback\]. Indeed, if ${\mathcal{L}}$ is a logic which is L$\varepsilon$-sound and includes ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$, then $(*)$ is provable in ${\mathcal{L}}$ if and only if ${\mathfrak{M}}$ can reach $(L_0,0,0)$ from $(L_1,k_1,k_2)$. Indeed, the "if" direction is by Theorem \[Th:encforw\], and the "only if" direciton is by Theorem \[Th:encback\]. Since reachability in Minsky computations is undecidable, we get undecidability of ${\mathcal{L}}$.

Before proving Theorems \[Th:encforw\] and \[Th:encback\], we establish several technical results.

Notice that each formula in the big conjunction $G$, except the first one, is of the form $G_{\Phi,\Psi} = \Psi {\mathop{\backslash}}\Phi^{bb}$. The key lemma for such formulae, in the view of Theorem \[Th:encforw\], is as follows.

\[Lm:G\] If the big conjunction $G$ includes $G_{\Phi,\Psi}$ and ${\mathbf{1}}\wedge G, \Phi, \Delta \vdash b$ is derivable in ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$, then so is ${\mathbf{1}}\wedge G, \Delta, \Psi \vdash b$.

The derivation is as follows: $$\infer[D\varepsilon]{{\mathbf{1}}\wedge G, \Delta, \Psi \vdash b}
 {\infer[\wedge L\text{ \small several times}]
 {{\mathbf{1}}\wedge G, {\mathbf{1}}\wedge G, \Delta, \Psi, \vdash b}
 {\infer[L\varepsilon\text{ \small several times}]
 {{\mathbf{1}}\wedge G, {\mathbf{1}}\wedge (\Psi {\mathop{\backslash}}\Phi^{bb}), \Delta, \Psi \vdash b}
 {\infer[\wedge L_r]{{\mathbf{1}}\wedge G, \Delta, \Psi, {\mathbf{1}}\wedge (\Psi {\mathop{\backslash}}\Phi^{bb}) \vdash b}
 {\infer[{\mathop{\backslash}}L]{{\mathbf{1}}\wedge G, \Delta, \Psi, \Psi {\mathop{\backslash}}\Phi^{bb} \vdash b}
 {\Psi \vdash \Psi & 
 \infer[{\mathop{\backslash}}L]{{\mathbf{1}}\wedge G, \Delta, (\Phi {\mathop{\backslash}}b) {\mathop{\backslash}}b \vdash B}
 {\infer[{\mathop{\backslash}}R]{{\mathbf{1}}\wedge G, \Delta \vdash \Phi {\mathop{\backslash}}b}
 {\infer[R \varepsilon\text{ \small several times}]{\Phi, {\mathbf{1}}\wedge G, \Delta \vdash b}
 {{\mathbf{1}}\wedge G, \Phi, \Delta \vdash b} & b \vdash b}}}}}}}$$

\["Post-ish productions"\]\[Cor:Postish\] Let $\Delta_1$ and $\Delta_2$ be sequences of variables from ${\mathcal{V}}$ (no complex formulae). Then, provided that $G$ includes $q {\mathop{\backslash}}q^{bb}$ for any $q \in {\mathcal{V}}$, the sequent ${\mathbf{1}}\wedge G, \Delta_2, \Delta_1 \vdash b$ is derivable in ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$ from ${\mathbf{1}}\wedge G, \Delta_1, \Delta_2 \vdash b$.

It is sufficient to consider the case of $\Delta_1 = q$; then we proceed by induction on the length of $\Delta_1$. For $\Delta_1 = q$, we apply Lemma \[Lm:G\] with $\Phi = \Psi = q$.

\[One step of Minsky computation\]\[Cor:step\] Suppose the Minsky machine $\mathfrak{M}$ can make a computation step from configuration $(L_i, k_1, k_2)$ to configuration $(L_{i'}, k'_1, k'_2)$, and let $(*')$ be the instance of $(*)$ for $(L_{i'}, k'_1, k'_2)$. Then $(*)$ is derivable from $(*')$ in ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$.

The proof is performed uniformly for all Minsky instructions. For any instruction $I$, the corresponding formula $A_I$ is of the form $G_{\Phi,\Psi} = \Psi {\mathop{\backslash}}\Phi^{bb}$. On the other hand, $(*')$ is obtained from $(*)$ by replacing $\Psi$ with $\Phi$ in the antecedent.

For example, for the instruction <span>inc</span>$(L_i,1,L_j)$ in the center of $(*)$ we have $l_i = \Psi$, which is replaced with $p_1, l_j = \Phi$ in $(*')$. This exactly corresponds to the computation step: the number of $p_1$'s (that is, the value of $c_1$) gets increased by 1, and the state is changed to $l_j$. For <span>jz</span>, the replacement happens at the edge of the antecedent, involving $e_1$ or $e_2$.

Thus, $(*)$ is of the form ${\mathbf{1}}\wedge G, \Delta_1, \Psi, \Delta_2 \vdash b$ and $(*')$ is ${\mathbf{1}}\wedge G, \Delta_1, \Phi, \Delta_2 \vdash b$. Now we derive $(*)$ from $(*')$ in the following way: $$\infer
 [\text{\small Corollary~\ref{Cor:Postish}}]
 {{\mathbf{1}}\wedge G, \Delta_1, \Psi, \Delta_2 \vdash b}
 {\infer
 [\text{\small Lemma~\ref{Lm:G}}]
 {{\mathbf{1}}\wedge G, \Delta_2, \Delta_1, \Psi \vdash b}
 {\infer[\text{\small Corollary~\ref{Cor:Postish}}]
 {{\mathbf{1}}\wedge G, \Phi, \Delta_2, \Delta_1 \vdash b}
 {{\mathbf{1}}\wedge G, \Delta_1, \Phi, \Delta_2 \vdash b}}}$$

Now we are ready to prove Theorem \[Th:encforw\].

\[Proof of Theorem \[Th:encforw\]\] Using Corollary \[Cor:step\] and induction on the number of steps in Minsky computation from $(L_i, k_1, k_2)$ to $(L_0,0,0)$, we derive $(*)$ from $${\mathbf{1}}\wedge G, e_1, l_0, e_2 \vdash b
 \eqno{(*_0)}$$ This sequent $(*_0)$ is derived as follows: $$\infer[L\varepsilon\text{ \small 3 times}]
 {{\mathbf{1}}\wedge G, e_1, l_0, e_2 \vdash b}
 {\infer
 [\wedge L\text{ \small several times}]
 {e_1, l_0, e_2, {\mathbf{1}}\wedge G \vdash b}
 {\infer[{\mathop{\backslash}}L]{e_1, l_0, e_2, e_2 {\mathop{\backslash}}(l_0 {\mathop{\backslash}}(e_1 {\mathop{\backslash}}b)) \vdash b}
 {e_2 \vdash e_2 & 
 \infer[{\mathop{\backslash}}L]{e_1, l_0, l_0 {\mathop{\backslash}}(e_1 {\mathop{\backslash}}b) \vdash b}
 {l_0 \vdash l_0 &
 \infer[{\mathop{\backslash}}L]{e_1, e_1 {\mathop{\backslash}}b \vdash b}
 {e_1 \vdash e_1 & b \vdash b}}}}}$$

The backwards direction, Theorem \[Th:encback\], is proved by constructing a specific L$\varepsilon$-model. Let $\Sigma = {\mathcal{V}}$ and fefine $B_{\mathfrak{M}}$ as the set of "terminating words" for $\mathfrak{M}$, defined as follows: $$B_{\mathfrak{M}} = 
\{ e_1 \underbrace{p_1 \ldots p_1}_{\text{$k_1$ times}} l_i
\underbrace{p_2 \ldots p_2}_{\text{$k_2$ times}} e_2 \mid
\mbox{ $\mathfrak{M}$ can reach $(L_0,0,0)$ from $(L_i,k_1,k_2)$ }\}.$$ Now define the interpreting function $w$ on variables as follows: $$\begin{aligned}
 & w(q) = \{ q \} \qquad\mbox{for $q \in {\mathcal{V}}$;}\\
 & w(b) = \{ \Xi\Upsilon \mid \mbox{ $\Xi$ and $\Upsilon$ are words over
 $\Sigma$ such that $\Upsilon\Xi \in B_{\mathfrak{M}}$ } \}.\end{aligned}$$

\[Lm:Geps\] $w({\mathbf{1}}\wedge G) = \{ \varepsilon \}$.

It is sufficient to show that $\varepsilon \in w(G)$, that is, $\varepsilon$ belongs to interpretation of all formulae in the big conjunction $G$.

First, $\varepsilon \in w((e_1, l_0, e_2) {\mathop{\backslash}}b)$. Indeed, $w((e_1,l_0,e_2) {\mathop{\backslash}}b) = 
 \{ e_1 l_0 e_2 \} {\mathop{\backslash}}w(b)$, thus, we have to show that $e_1 l_0 e_2 \varepsilon = e_1 l_0 e_2 \in w(b)$. This is indeed so by the definition of $B_{\mathfrak{M}}$, since $(L_0,0,0)$ is reachable from itself in zero steps.

Second, we prove that $\varepsilon \in w(A_I)$ for each instruction $I$ of $\mathfrak{M}$. Recall that $A_I = \Psi {\mathop{\backslash}}\Phi^{bb} = \Psi {\mathop{\backslash}}((\Phi {\mathop{\backslash}}b) {\mathop{\backslash}}b)$, and if instruction $I$ changes the configuration from $(L_i, k_1, k_2)$ to $(L_{i'}, k'_1, k'_2)$, then the code of the second configuration is obtained from the code of the first one by replacing $\Psi$ with $\Phi$. In other words, the code of $(L_i, k_1, k_2)$ is $\Delta_1 \Psi \Delta_2$ and the code of $(L_{i'}, k'_1, k'_2)$ is $\Delta_1 \Phi \Delta_2$. We have to prove that $\varepsilon \in w(\Psi) {\mathop{\backslash}}w((\Phi {\mathop{\backslash}}b) {\mathop{\backslash}}b)$. Since $w(\Psi) = \{ \Psi \}$ ($\Psi$ contains only letters from ${\mathcal{V}}$), this means that $\Psi$ should belong to $w((\Phi {\mathop{\backslash}}b) {\mathop{\backslash}}b)$.

In turn, $\Psi \in w((\Phi {\mathop{\backslash}}b) {\mathop{\backslash}}b)$ means that for any word $\Delta \in w(\Phi {\mathop{\backslash}}b)$ we have $\Delta \Psi \in w(b)$. The fact that $\Delta \in w(\Phi {\mathop{\backslash}}b)$, since $w(\Phi) = \{ \Phi \}$, actually means that $\Phi\Delta \in w(b)$. Thus, we have to prove, for an arbitrary $\Delta$, that if $\Phi\Delta \in w(b)$, then $\Delta\Psi \in w(b)$.

If $\Phi\Delta \in w(b)$, then we have $\Delta = \Delta_1\Delta_2$, and $\Delta_2 \Phi \Delta_1 \in B_{\mathfrak{M}}$. Here $\Phi$ cannot be split between $\Xi$ and $\Upsilon$, because any word in $B_{\mathfrak{M}}$ should begin with $e_1$ and end on $e_2$. This means that $\Delta_2 \Phi \Delta_1$ is a code of some configuration $(L_{i'}, k'_1, k'_2)$, from which $\mathfrak{M}$ can reach the final configuration. As noticed above, this means that $\Delta_2 \Psi \Delta_1$ encodes a configuration $(L_i, k_1, k_2)$, which transforms into $(L_{i'}, k'_1, k'_2)$ by applying instruction $I$. Therefore, from $(L_i, k_1, k_2)$ our Minsky machine can also reach the final state, hence $\Delta_2 \Psi \Delta_1 \in B_{\mathfrak{M}}$. This yields $\Delta\Psi = \Delta_1 \Delta_2 \Psi \in w(b)$, which is our goal.

Third, consider $q {\mathop{\backslash}}q^{bb}$, where $q \in {\mathcal{V}}$. We have to show that $\varepsilon \in w(q) {\mathop{\backslash}}w(q^{bb})$, that is, $q \in w(q^{bb})$. The latter means that for any $\Delta \in w(q {\mathop{\backslash}}b)$ the word $\Delta q$ should belong to $w(b)$. This is indeed so: if $\Delta \in w(q {\mathop{\backslash}}b)$, then $q \Delta \in w(b)$, and since $w(b)$ is closed under cyclic transpositions, also $\Delta q \in w(b)$.

Now we are ready to prove Theorem \[Th:encback\].

\[Proof of Theorem \[Th:encback\]\] If $(*)$ is true in all L$\varepsilon$-models, it is true in the specific model defined above. By Lemma \[Lm:Geps\], $w({\mathbf{1}}\wedge G) = \{ \varepsilon \}$; $w(q) = \{ q \}$ for any $q \in {\mathcal{V}}$. Thus, we have $$e_1 \underbrace{p_1 \ldots p_1}_{\text{$k_1$ times}} l_i 
 \underbrace{p_2 \ldots p_2}_{\text{$k_2$ times}} e_2 \in w(b),$$ and therefore $$e_1 \underbrace{p_1 \ldots p_1}_{\text{$k_1$ times}} l_i 
 \underbrace{p_2 \ldots p_2}_{\text{$k_2$ times}} e_2 \in B_{\mathfrak{M}}.$$ (No cyclic transposition is possible, since $e_1$ and $e_2$ should start and end the word.)

By definition of $B_{\mathfrak{M}}$, this means that $\mathfrak{M}$ can reach the final state $(L_0,0,0)$, starting from $(L_i,k_1,k_2)$.

Models on Regular Languages with the Unit Constant
--------------------------------------------------

Let ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ denote the set of all sequents in the language of ${\mathop{\backslash}}$, $\wedge$, ${\mathbf{1}}$ which are true in all L$\varepsilon$-models, that is, the <span>*complete theory*</span> of this class of models.

As noticed above, the question of axiomatizing this theory is quite involved. We know that this theory includes ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$, introduced in the previous section, but it is probably much more complicated. For example, as shown in @KuznJANCL, Sobociński's 3-valued logic $\mathbf{RM}_3$ can be embedded into ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$.

It follows from Theorem \[Th:undec\] that ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ is undecidable. More precisely, it is $\Sigma_1^0$-hard (hard w.r.t. the class of recursively enumerable sets). The upper complexity bound, however, is not known: this theory could possibly be even not recursively enumerable. Having the algorithmic complexity question for ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ open, we can still obtain an interesting corollary of our complexity estimations.

Recall the standard notion of regular expression. Regular expressions are constructed from constants $0$ and $1$ using two binary operations, $\cdot$ and $+$, and one unary operation, ${}^*$. The language $\mathscr{L}(R)$ described by a given regular expression $R$ is defined recursively: $$\begin{aligned}
 & \mathscr{L}(0) = \varnothing; \\
 & \mathscr{L}(1) = \{ \varepsilon \}; \\
 & \mathscr{L}(A \cdot B) = \mathscr{L}(A) \cdot \mathscr{L}(B);\\
 & \mathscr{L}(A + B) = \mathscr{L}(A) \cup \mathscr{L}(B); \\
 & \mathscr{L}(A^*) = \bigl(\mathscr{L}(A)\bigr)^* = 
 \{ u_1 \ldots u_n \mid n \ge 0, u_i \in \mathscr{L}(A) \}.\end{aligned}$$ Languages described by regular expressions are called regular languages.

By <span>Lreg</span>$\varepsilon$-models let us denote a subclass of L$\varepsilon$-models in which every variable as interpreted as a <span>*regular*</span> language, that is, a set of words described by a regular expression. It is well-known that the class of regular languages is closed under intersection (see, for example, @AhoUllman [Theorem 2.8]). Moreover, it is also closed under division:

If $A$ and $B$ are regular languages, then so are $A {\mathop{\backslash}}B$ and $B {\mathop{/}}A$.

A more well-known fact (see, for example, @AhoUllman [Exercise 2.3.17a]) is that the class of regular languages is closed under the following modified division operation with the existential quantifier instead of the universal one: $A {\mathop{\mbox{\raisebox{5pt}{\rotatebox{-60}{${\sim}$}}}}}B = 
\{ u \in \Sigma^* \mid (\exists v \in A) \, vu \in B\}$. Our "normal" division ${\mathop{\backslash}}$ can be reduced to ${\mathop{\mbox{\raisebox{5pt}{\rotatebox{-60}{${\sim}$}}}}}$ by the complement operation: $A {\mathop{\backslash}}B = \overline{A {\mathop{\mbox{\raisebox{5pt}{\rotatebox{-60}{${\sim}$}}}}}\overline B}$, where $\overline{X} = \Sigma^* - X$. Since the class of regular languages is closed under ${\mathop{\mbox{\raisebox{5pt}{\rotatebox{-60}{${\sim}$}}}}}$ and complement (again, see @AhoUllman [Theorem 2.8]), it is also closed under ${\mathop{\backslash}}$. The ${\mathop{/}}$ case is symmetric.

Thus, in <span>Lreg</span>$\varepsilon$-models interpretations of all formulae are regular languages.

In the language without the unit constant, namely, ${\mathop{\backslash}}$, ${\mathop{/}}$, $\wedge$, the theory of <span>Lreg</span>$\varepsilon$-models coincides with the theory of all L$\varepsilon$-models:

$
{\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, {\mathop{/}}, \wedge) =
{\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, {\mathop{/}}, \wedge).
$

On the one hand, the calculus ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ is sound w.r.t. all L$\varepsilon$-models. On the other hand, as shown by Buszkowski @Buszkowski1996, it is complete w.r.t. a class of models which is even narrower than the class of <span>Lreg</span>$\varepsilon$-models. Namely, ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ is complete w.r.t. the class of L$\varepsilon$-models in which variables are interpreted by cofinite languages. (A cofinite language is a language which includes all words over a given alphabet, except for a finite set.) In this case, formulae are interpreted by cofinite or finite languages, and any finite or cofinite language is regular. Therefore, both ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, {\mathop{/}}, \wedge)$ and ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, {\mathop{/}}, \wedge)$ are axiomatized by the same calculus ${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)$.

The unit changes things dramatically. With the unit, there is no completeness result, like Theorem \[Th:compl\], but also no equivalence between theories of all L$\varepsilon$-models and <span>Lreg</span>$\varepsilon$-models.

\[Th:regdiff\] ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}) \ne
{\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}).$

As follows from Theorem \[Th:undec\], ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ is $\Sigma_1^0$-hard. On the other hand, following Buszkowski @Buszko2006RelMiCS, we can show that ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ belongs to the $\Pi_1^0$ class. Indeed, a sequent belongs to this theory if and only if it is true in all <span>Lreg</span>$\varepsilon$-models. A concrete sequent includes only a finite number of variables, $p_1$, …, $p_n$. Thus, a model for this sequent is defined by a finite number of regular expressions $R_1$, …, $R_n$, which describe the languages $w(p_1)$, …, $w(p_n)$. This means that the general truth condition for this sequent can be written down as the following formula: $$\begin{gathered}
 \forall R_1 \, \ldots \, \forall R_n \bigl(
 \mbox{the sequent is true under interpretation} \\ \mbox{where $w(p_i)$ is the language of $R_i$} \bigr).
 \end{gathered}$$ Quantifiers $\forall R_1$, …, $\forall R_n$ can be encoded as quantifiers over natural numbers representing the regular expressions. The quantifier-free part of the formula (truth condition under a concrete $w$) is decidable, because all necessary operations on regular expressions are computable. Thus, we get a $\Pi_1^0$ representation of the set of sequents which are true in all <span>Lreg</span>$\varepsilon$-models.

It is well known that a set cannot belong to $\Pi_1^0$ and be $\Sigma_1^0$-hard at the same time. (Otherwise, for any set in $\Sigma_1^0$ there would be a computable reduction to a set in $\Pi_1^0$, which would yield $\Sigma_1^0 \subseteq \Pi_1^0$, which is not the case.) Therefore, $${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}) \ne
{\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}).$$

Notice that our proof of Theorem \[Th:undec\] does not apply to ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; \linebreak {\mathop{\backslash}}, \wedge, {\mathbf{1}})$, because the language $w(b)$ there is non-regular (in fact, it is undecidable).

Since the class of <span>Lreg</span>$\varepsilon$-models is narrower than the class of all L$\varepsilon$-models, we have (by Galois connection) an inverted inclusion of theories: $${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}) \supset
{\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}).$$ By our Theorem \[Th:regdiff\], this inclusion is strict. Thus, the other inclusion should fail: $${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}) \not\subset
{\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}}).$$ In other words, there exists a sequent which is true in all <span>Lreg</span>$\varepsilon$-models, but not in all L$\varepsilon$-models. Our proof, however, is non-constructive, and we do not present a concrete example of such sequent. Constructing such a concrete example is left for further research.

Notice that if we apply the reasoning establishing the upper $\Pi_1^0$ bound of ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ to ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$, we shall have to quantify over <span>*arbitrary*</span> formal languages $w(p_1)$, …, $w(p_n)$. This results in hyperarithmetical quantifiers, and yields only a very high, $\Pi_1^1$ complexity upper bound for ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$.

Concluding Remarks
==================

In this article, we have investigated language interpretations of natural extensions of the Lambek calculus: with additive operations ($\vee$ and $\wedge$) and with additive conjunction ($\wedge$) and the unit constant (${\mathbf{1}}$).

For extensions with additive connectives (Section \[S:distr\]), we have shown that conjunction and disjunction show significantly different behaviour. It is known that adding both conjunction and disjunction leads to incompleteness due to the distributivity law $\mathcal{D}$. This law is true in all language models, but not derivable in the multiplicative-additive Lambek calculus (${\mathbf{MALC}}$). Adding only conjunction, however, still provides completeness. Any sequent in the language of ${\mathop{\backslash}}$, ${\mathop{/}}$, $\wedge$ (but not $\vee$) that is derivable with the help of $\mathcal{D}$, is also derivable without it. For disjunction the situation is opposite: there exists a sequent in the language of ${\mathop{\backslash}}$, ${\mathop{/}}$, $\vee$, which is derivable using $\mathcal{D}$, but not derivable without it.

Moreover, this difference between $\wedge$ and $\vee$ keeps valid for systems with permutation and/or weakening structural rules, that is, intuitionistic linear (${\mathbf{ILL}}$), and affine (${\mathbf{IAL}}$) logics and affine ${\mathbf{MALC}}$.

For the extension of the Lambek calculus with the unit, ${\mathbf{1}}$, it is well-known that its standard axiomatization in the style of linear logic does not give an L$\varepsilon$-complete system. In Section \[S:unit\], we present a system in the language ${\mathop{\backslash}}, \wedge, {\mathbf{1}}$, where rules for ${\mathbf{1}}$ reflect natural algebraic properties of the empty word in the algebra of formal languages. This system is denoted by ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$. We do not claim L$\varepsilon$-completeness of ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$. Instead, we consider the whole range of logics between ${\mathbf{L}^{+\varepsilon}}({\mathop{\backslash}},\wedge,{\mathbf{1}})$ and the L$\varepsilon$-complete system denoted by ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$. For any logic within this range, we show that it is undecidable; more precisely, $\Sigma_1^0$-complete. As a corollary, we also show that, in the language of ${\mathop{\backslash}}, \wedge, {\mathbf{1}}$, the complete theory of all L$\varepsilon$-models is different from that of <span>Lreg</span>$\varepsilon$-models, where formulae are interpreted by regular languages.

A preliminary version of this article was presented at WoLLIC 2019 and published in its lecture notes @KanKuzSceWoLLICLMod. Let us briefly list the results which are new in this article, compared to the WoLLIC paper.

-   In the language without additive conjunction, we show incompleteness not only for ${\mathbf{MALC}}$, but also for its extensions: ${\mathbf{MALC}^{\boldsymbol{*}}}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}$, ${\mathbf{ILL}}$, and ${\mathbf{IAL}}$.

-   We prove that ${\mathbf{MALC}}({\mathop{\backslash}},{\mathop{/}},\wedge)$ is a conservative fragment of ${\mathbf{MALC}}$ extended with the distributity law $\mathcal{D}$. Moreover, we prove similar results for ${\mathbf{MALC}^{\boldsymbol{*}}}$, ${\mathbf{AMALC}^{\boldsymbol{*}}}$, ${\mathbf{ILL}}$, and ${\mathbf{IAL}}$.

-   We prove that, in the language including ${\mathbf{1}}$, the theory of all L$\varepsilon$-models is different from the theory of L<span>Reg</span>$\varepsilon$-models, in which formulae are interpreted by regular languages. In the language of ${\mathop{\backslash}}, {\mathop{/}}, \wedge$ (without ${\mathbf{1}}$), the corresponding theories coincide due to a completeness result by Buszkowski @Buszkowski1996.

While in Section \[S:distr\] we have presented a quite completed study, Section \[S:unit\] leaves many questions open for further investigations. Among these, we would like to emphasize the following ones.

-   The question of axiomatization, or even recursive enumerability for complete theories ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ and ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ is still open, and potentially very hard. Notice that these theories are different (Theorem \[Th:regdiff\]) and that for ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ enumerability will immediately mean decidability.

-   A possibly easier question would be to construct a concrete formula distinguishing ${\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$ and ${\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, \wedge, {\mathbf{1}})$. That is, we are looking for an explicit example for Theorem \[Th:regdiff\].

-   Without the unit, we know that $${\mathbf{MALC}^{\boldsymbol{*}}}({\mathop{\backslash}},{\mathop{/}},\wedge)= {\mathrm{Th}}(\mbox{L$\varepsilon$-models}; {\mathop{\backslash}}, {\mathop{/}}, \wedge) = {\mathrm{Th}}(\mbox{{\sc Lreg}$\varepsilon$-models}; {\mathop{\backslash}}, {\mathop{/}}, \wedge).$$ By the completeness theorem of Pentus @PentusAPAL [@PentusFmonov], the first equality is also true for the language of ${\mathop{\backslash}},{\mathop{/}},\cdot$ (with product instead of additive conjunction). There are two open questions. First, whether Pentus' theorem is true for the language with both conjunctions (${\mathop{\backslash}},{\mathop{/}},\cdot,\wedge$). Second, whether Pentus' theorem is true for <span>Lreg</span>$\varepsilon$-models. Both questions are questions of making Pentus' result stronger. Recalling that Pentus' proofs are quite sophisticated, these questions are also probably very hard.

{'source': 'arXiv_out/2008'}