Language Models for Some Extensions of the Lambek Calculus

Max Kanovich Stepan Kuznetsov Andre Scedrov University College London Steklov Mathematical Institute of RAS University of Pennsylvania National Research University Higher School of Economics

Abstract

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.

keywords:

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

^†^†journal: Information and Computation

1 Introduction

The Lambek calculus was introduced by Joachim Lambek [1] 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 language models, or L-models 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 Lambek’s non-emptiness restriction. 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:

	$\displaystyle A\cdot B=\{uv\mid u\in A,v\in B\},$
	$\displaystyle A\mathop{\backslash}B=\{u\in\Sigma^{+}\mid(\forall v\in A)\>vu\in B\},$
	$\displaystyle B\mathop{/}A=\{u\in\Sigma^{+}\mid(\forall v\in A)\>uv\in B\}.$

The division operations, $\mathop{\backslash}$ and $\mathop{/}$ , are indeed residuals 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 [1] 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:

\Gamma,\Pi,A\mathop{\backslash}B,\Delta\vdash C\lx@proof@logical@and\Pi\vdash A\Gamma,B,\Delta\vdash C\qquad\Pi\vdash A\mathop{\backslash}BA,\Pi\vdash B

\Gamma,B\mathop{/}A,\Pi,\Delta\vdash C\lx@proof@logical@and\Pi\vdash A\Gamma,B,\Delta\vdash C\qquad\Pi\vdash B\mathop{/}A\Pi,A\vdash B

\Gamma,A\cdot B,\Delta\vdash C\Gamma,A,B,\Delta\vdash C\qquad\Gamma,\Delta\vdash A\cdot B\lx@proof@logical@and\Gamma\vdash A\Delta\vdash B

\Gamma,\Pi,\Delta\vdash C\lx@proof@logical@and\Pi\vdash A\Gamma,A,\Delta\vdash C

The cut rule is eliminable [1].

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 [2, § 2.5].

Abolishing Lambek’s restriction—that is, removing constraints “ $\Pi$ is non-empty” on $\mathop{\backslash}R$ and $\mathop{/}R$ —yields the Lambek calculus allowing empty antecedents, denoted by $\mathbf{L}^{\boldsymbol{*}}$ [3]. 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{*}}$ ,

	$\displaystyle A\mathop{\backslash}B=\{u\in\Sigma^{*}\mid(\forall v\in A)\,vu\in B\},$
	$\displaystyle B\mathop{/}A=\{u\in\Sigma^{*}\mid(\forall v\in A)\,uv\in B\}.$

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 L $\varepsilon$ -models.

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 [4, 5]. Pentus’ proofs are highly non-trivial. If one considers the fragment without $\cdot$ (the product-free fragment), however, proving L-completeness becomes much easier. This was done by Buszkowski [6]; 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 additive conjunction and disjunction. Additive operations are usually axiomatized by the following inference rules (cf. [7]):

\Gamma,A\vee B,\Delta\vdash C\lx@proof@logical@and\Gamma,A,\Delta\vdash C\Gamma,B,\Delta\vdash C\qquad\Pi\vdash A\vee B\Pi\vdash A\qquad\Pi\vdash A\vee B\Pi\vdash B

\Gamma,A\wedge B,\Delta\vdash C\Gamma,A,\Delta\vdash C\qquad\Gamma,A\wedge B,\Delta\vdash C\Gamma,B,\Delta\vdash C\qquad\Pi\vdash A\wedge B\lx@proof@logical@and\Pi\vdash A\Pi\vdash B

The Lambek calculus $\mathbf{L}$ extended with these rules is denoted by $\mathbf{MALC}$ (multiplicative-additive Lambek calculus); $\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 2, we discuss this issue in detail.

Following Abrusci [8], we put the Lambek calculus into a broader context of linear logic. Namely, $\mathbf{MALC}^{\boldsymbol{*}}$ can be viewed as a fragment of intuitionistic non-commutative 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:

\Gamma,A,B,\Delta\vdash C\Gamma,B,A,\Delta\vdash C\qquad\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 [9] linear logic notations.

Sequents are now going to be expressions of the form $\Gamma\vdash C$ , where $\Gamma$ is a multiset 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:

\Gamma,\Pi,A\multimap B\vdash C\lx@proof@logical@and\Pi\vdash A\Gamma,B\vdash C\qquad\Pi\vdash A\multimap B\Pi,A\vdash B

\Gamma,A\otimes B\vdash C\Gamma,A,B\vdash C\qquad\Gamma,\Delta\vdash A\otimes B\lx@proof@logical@and\Gamma\vdash A\Delta\vdash B

\Gamma,A\vee B\vdash C\lx@proof@logical@and\Gamma,A\vdash C\Gamma,B\vdash C\qquad\Pi\vdash A\vee B\Pi\vdash A\qquad\Pi\vdash A\vee B\Pi\vdash B

\Gamma,A\vee B\vdash C\Gamma,A\vdash C\qquad\Gamma,A\vee B\vdash C\Gamma,B\vdash C\qquad\Pi\vdash A\wedge B\lx@proof@logical@and\Pi\wedge A\Pi\wedge B

For $\mathbf{IAL}$ , the weakening rule is not officially included in the system, but is admissible:

\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}$ :

\Gamma,\Pi\vdash C\lx@proof@logical@and\Pi\vdash A\Gamma,A\vdash C

This is shown by a standard inductive argument.

Finally, let us introduce the multiplicative unit constant, $\mathbf{1}$ . The unit constant is added to systems without Lambek’s restriction extending $\mathbf{L}^{\boldsymbol{*}}$ (i.e., $\mathbf{L}^{\boldsymbol{*}}$ itself, $\mathbf{MALC}^{\boldsymbol{*}}$ , $\mathbf{AMALC}^{\boldsymbol{*}}$ , $\mathbf{ILL}$ , $\mathbf{IAL}$ ). The Lambek calculus with the unit, $\mathbf{L}_{\mathbf{1}}$ [10], is obtained from $\mathbf{L}^{\boldsymbol{*}}$ by adding one axiom, $\vdash\mathbf{1}$ (its antecedent is empty), and one inference rule,

\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)$ .

2 Distributivity Law in Fragments with One Additive

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.

(𝒟)

On one hand, this principle is obviously true in all L-models. On the other hand, as noticed by Ono and Komori [11], 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 both additive connectives, $\wedge$ and $\vee$ . We investigate fragments of $\mathbf{MALC}$ with only one additive, $\wedge$ or $\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 [12].

Let us restrict ourselves to the product-free language (with product, proving L-completeness is hard even without extra connections [4, 5]). We also consider calculi without the unit constant: issues connected with $\mathbf{1}$ are discussed in Section 3. 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 [6], $\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 both $\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$ .

2.1 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.

Definition 1.

A language $A$ is called monotone, if for any word $u_{1}u_{2}\in A$ and an arbitrary word $w$ the word $u_{1}wu_{2}$ also belongs to $A$ .

Proposition 1.

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

Proof.

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

Definition 2.

A language $A$ is called commutative, 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 multiset union, $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$ .

Proposition 2.

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

Proof.

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^{\prime}=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^{\prime}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^{\prime}\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.

Definition 3.

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

Definition 4.

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.

Proposition 3.

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)$ .

Proof.

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

Theorem 4.

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:

Calculus	Models
$\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

Proof.

The cases of $\mathbf{MALC}(\mathop{\backslash},\mathop{/},\wedge)$ and $\mathbf{MALC}^{\boldsymbol{*}}(\mathop{\backslash},\mathop{/},\wedge)$ are due to Buszkowski [6]. 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 3: 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:

	$\displaystyle w_{0}(A\mathop{\backslash}B)=w_{0}(A)\mathop{\backslash}w_{0}(B);$
	$\displaystyle w_{0}(B\mathop{/}A)=w_{0}(B)\mathop{/}w_{0}(A);$
	$\displaystyle w_{0}(A\wedge B)=w_{0}(A)\wedge w_{0}(B).$

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:

Proposition 5.

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 4; 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.

Theorem 6.

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 $\mathbf{IAL}(\multimap,\wedge)$ 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.

Proof.

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 5 it is true in all models of the corresponding class. By Theorem 4 it is derivable in, respectively, $\mathbf{MALC}(\mathop{\backslash},\mathop{/},\wedge)$ , …, $\mathbf{IAL}(\multimap,\wedge)$ . ∎

2.2 Incompleteness with Additive Disjunction Only

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

Theorem 7.

The sequent

((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

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 7 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 4).

Before proving Theorem 7, 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 [13], 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 7 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 llprover by Tamura [14]. (For the WoLLIC 2019 paper, we used a $\mathbf{MALC}$ prover by Jipsen [15], based on the algorithm by Okada and Terui [16].) 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\cr 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\cr 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 7. 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 7.

The first statement is proved using the joining (diamond) construction, the idea of which goes back to Lambek [1] and Pentus [17]. 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

((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

(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:

\not\vdash(y\multimap x)\vee w

(1)

z\not\vdash(y\multimap x)\vee w

(2)

y\not\vdash(y\multimap x)\vee w

(3)

z,y\not\vdash(y\multimap x)\vee w

(4)

z,z\not\vdash(y\multimap x)\vee w

(5)

z\not\vdash(y\multimap x)\vee(z\multimap x)\vee w

(6)

\not\vdash(y\multimap x)\vee(z\multimap x)\vee w

(7)

z,y\not\vdash(y\multimap x)\vee(z\multimap x)\vee w

(8)

Now we are ready to start proof search. First we invert $\vee L$ introducing $(y\multimap x)\vee w$ and choose $y\multimap x$ :

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),y\stackrel{{\scriptstyle 3}}{{\multimap}}x,\\ ((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash((y\vee z)\multimap x)\stackrel{{\scriptstyle 1}}{{\vee}}w

Now we have a choice of 4 principal connectives (denoted by numbers in the sequent) to be decomposed first.

Case 1. 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.

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),y\stackrel{{\scriptstyle 3}}{{\multimap}}x,\\ ((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash(y\vee z)\multimap x

Invert $\multimap R$ and $\vee L$ , choosing $z$ out of $y\vee z$ :

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),y\stackrel{{\scriptstyle 3}}{{\multimap}}x,\\ ((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w),z\vdash x

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.

Subcase 1–2. If $\Pi$ includes $y\stackrel{{\scriptstyle 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^{\prime}\subseteq\Gamma$ and the sequent is not derivable with $\Gamma$ , it is also not derivable with $\Gamma^{\prime}$ (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{{\scriptstyle 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:

((y\multimap x)\vee w)\multimap((z\multimap x)\vee w),z\vdash(y\multimap x)\vee(z\multimap x)\vee w

(9)

Decomposing $\multimap$ yields either $\vdash(y\multimap x)\vee w$ or $z\vdash(y\multimap x)\vee w$ , both not derivable by (1) and (2). 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 (3)(4).

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 (1)(2)(5).

Subcase 1–3. Apply $\multimap L$ for $\stackrel{{\scriptstyle 3}}{{\multimap}}$ and consider its left premise with the maximal possible $\Pi$ :

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w),z\vdash y.

(10)

Subsubcase 1–3–2. Decompose $\stackrel{{\scriptstyle 2}}{{\multimap}}$ . If the big formula with $\stackrel{{\scriptstyle 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 (6)(7). If the formula with $\stackrel{{\scriptstyle 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$ .

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

Subcase 1–4. If $\Pi$ includes $y\stackrel{{\scriptstyle 3}}{{\multimap}}x$ , then the right premise is, at maximum,

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 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{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),z,w\vdash x

Now we have to use $\stackrel{{\scriptstyle 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{{\scriptstyle 3}}{{\multimap}}x$ is in $\Gamma$ , then the maximal version of the left premise is

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),z\vdash(y\multimap x)\vee w.

(11)

Applying $\stackrel{{\scriptstyle 2}}{{\multimap}}$ right now is impossible: its left premise gets falsified by (7) or (6). 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{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),z,y\vdash x.

Here the left premise of $\stackrel{{\scriptstyle 2}}{{\multimap}}$ is also falsified by (7), (6), or (8).

Case 2. Consider again two cases, depending on whether $y\stackrel{{\scriptstyle 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{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash((y\vee z)\multimap x)\stackrel{{\scriptstyle 1}}{{\vee}}w.

Invert $\vee L$ and choose $y\multimap x$ :

y\stackrel{{\scriptstyle 5}}{{\multimap}}x,((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash((y\vee z)\multimap x)\stackrel{{\scriptstyle 1}}{{\vee}}w.

(12)

For reusal of our reasoning in further cases, we shall falsify a stronger sequent

y\stackrel{{\scriptstyle 5}}{{\multimap}}x,((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash((y\vee z)\multimap x)\stackrel{{\scriptstyle 1}}{{\vee}}w.

(13)

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 (12) happens to be derivable then, by cut, so will be (13).

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

Subcase 2– $\Pi$ –1. Recall that we never choose $w$ in $\vee R$ , and invert $\multimap R$ :

y\stackrel{{\scriptstyle 5}}{{\multimap}}x,((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w),y\vee z\vdash x.

Invert $\vee L$ and choose $z$ :

y\stackrel{{\scriptstyle 5}}{{\multimap}}x,((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w),z\vdash x.

Subsubcase 2– $\Pi$ –1–5. The left premise is, at maximum,

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w),z\vdash y.

Applying $\stackrel{{\scriptstyle 4}}{{\multimap}}L$ is impossible, since its right premise is falsified by choosing $w$ : $w,z\not\vdash y$ and $w\not\vdash y$ .

Subsubcase 2– $\Pi$ –1–4. Again, if $y\stackrel{{\scriptstyle 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 left premise is, at maximum, $z\vdash(y\multimap x)\vee(z\multimap x)\vee w$ , which is not derivable by (6).

Subcase 2– $\Pi$ –4. If the new $\Pi$ is empty, then the left premise is falsified by (7). 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$ .

Subcase 2– $\Pi$ –5. 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{{\scriptstyle 3}}{{\multimap}}x$ go to $\Gamma$ . Then the left premise is, at maximum,

((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash(y\multimap x)\vee(z\multimap x)\vee w.

This sequent is stronger than (9)—that is, (9) can be obtained from it by weakening. Therefore, it cannot be derivable, since we’ve already falsified (9) in Case 1.

Case 3. Take the maximal possible $\Pi$ and consider the left premise:

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),((y\multimap x)\vee w)\stackrel{{\scriptstyle 4}}{{\multimap}}((z\multimap x)\vee w)\vdash y.

This sequent is stronger than (10), and therefore not derivable: (10) was falsified in Case 1.

Case 4. If $y\stackrel{{\scriptstyle 3}}{{\multimap}}x$ goes to $\Pi$ , then the maximal version of the right premise of $\stackrel{{\scriptstyle 4}}{{\multimap}}L$ is

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),(z\multimap x)\vee w\vdash((y\vee z)\multimap x)\stackrel{{\scriptstyle 1}}{{\vee}}w.

Invert $\vee L$ and choose $z\multimap x$ :

((y\multimap x)\vee(z\multimap x)\vee w)\stackrel{{\scriptstyle 2}}{{\multimap}}((y\multimap x)\vee w),z\stackrel{{\scriptstyle 6}}{{\multimap}}x\vdash((y\vee z)\multimap x)\stackrel{{\scriptstyle 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 (13), up to commutativity; (13) was falsified in Case 2.

Finally, if $y\stackrel{{\scriptstyle 3}}{{\multimap}}x$ , in Case 4, goes to $\Gamma$ , then the maximal version of the left premise of $\stackrel{{\scriptstyle 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 (11) and therefore cannot be derivable. ∎

3 Undecidability with $\mathop{\backslash}$ , $\wedge$ , and $\mathbf{1}$

3.1 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 [6], 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:

A\vdash A\qquad A,\mathbf{1}\vdash A

\Gamma,\Pi,A\mathop{\backslash}B,\Delta\vdash C\lx@proof@logical@and\Pi\vdash A\Gamma,B,\Delta\vdash C\qquad\Pi\vdash A\mathop{\backslash}BA,\Pi\vdash B

\Gamma,A\vee B\vdash C\Gamma,A\vdash C\qquad\Gamma,A\vee B\vdash C\Gamma,B\vdash C\qquad\Pi\vdash A\wedge B\lx@proof@logical@and\Pi\wedge A\Pi\wedge B

\Gamma,\mathbf{1}\wedge G,A,\Delta\vdash C\Gamma,A,\mathbf{1}\wedge G,\Delta\vdash C\quad\Gamma,A,\mathbf{1}\wedge G,\Delta\vdash C\Gamma,\mathbf{1}\wedge G,A,\Delta\vdash C\quad\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 [10], 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 [18] 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 [19] 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 [20] 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. [21]. The system considered in [20] 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. [22]). 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}$ .

Theorem 8.

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 [23]. 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. [24, 25, 16], 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 relative double negation 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$ (ex falso) 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 final 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:

Instruction $I$	Formula $A_{I}$
inc $(L_{i},1,L_{j})$	$l_{i}\mathop{\backslash}(p_{1},l_{j})^{bb}$
inc $(L_{i},2,L_{j})$	$l_{i}\mathop{\backslash}(l_{j},p_{2})^{bb}$
dec $(L_{i},1,L_{j})$	$(p_{1},l_{i})\mathop{\backslash}l_{j}^{bb}$
dec $(L_{i},2,L_{j})$	$(l_{i},p_{2})\mathop{\backslash}l_{j}^{bb}$
jz $(L_{i},1,L_{j})$	$(e_{1},l_{i})\mathop{\backslash}(e_{1},l_{j})^{bb}$
jz $(L_{i},2,L_{j})$	$(l_{i},e_{2})\mathop{\backslash}(l_{j},e_{2})^{bb}$

Here instruction inc $(L_{i},r,L_{j})$ (increment) means “at state $L_{i}$ , increase $c_{r}$ by 1 and go to $L_{j}$ ” ( $r=1,2$ ). Instruction dec $(L_{i},r,L_{j})$ (decrement) 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, jz $(L_{i},r,L_{j})$ (zero-test) means “at state $L_{i}$ , if $k_{r}=0$ , go to $L_{j}$ .” Now if $k_{r}\neq 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 jzdec $(L_{i},r,L_{j_{1}},L_{j_{2}})$ instruction from Minsky’s original formalism [26], meaning “at state $L_{i}$ , if $k_{r}\neq 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: dec $(L_{i},r,L_{j_{1}})$ and jz $(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.

Theorem 9.

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.

(*)

Theorem 10.

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 9 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 8 (our undecidability result) immediately follows from Theorems 9 and 10. 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 9, and the “only if” direciton is by Theorem 10. Since reachability in Minsky computations is undecidable, we get undecidability of $\mathcal{L}$ .

Before proving Theorems 9 and 10, 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 9, is as follows.

Lemma 11.

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$ .

Proof.

The derivation is as follows:

\mathbf{1}\wedge G,\Delta,\Psi\vdash b\mathbf{1}\wedge G,\mathbf{1}\wedge G,\Delta,\Psi,\vdash b\mathbf{1}\wedge G,\mathbf{1}\wedge(\Psi\mathop{\backslash}\Phi^{bb}),\Delta,\Psi\vdash b\mathbf{1}\wedge G,\Delta,\Psi,\mathbf{1}\wedge(\Psi\mathop{\backslash}\Phi^{bb})\vdash b\mathbf{1}\wedge G,\Delta,\Psi,\Psi\mathop{\backslash}\Phi^{bb}\vdash b\lx@proof@logical@and\Psi\vdash\Psi\mathbf{1}\wedge G,\Delta,(\Phi\mathop{\backslash}b)\mathop{\backslash}b\vdash B\mathbf{1}\wedge G,\Delta\vdash\Phi\mathop{\backslash}b\lx@proof@logical@and\Phi,\mathbf{1}\wedge G,\Delta\vdash b\mathbf{1}\wedge G,\Phi,\Delta\vdash bb\vdash b

∎

Corollary 12 (“Post-ish productions”).

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$ .

Proof.

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 11 with $\Phi=\Psi=q$ . ∎

Corollary 13 (One step of Minsky computation).

Suppose the Minsky machine $\mathfrak{M}$ can make a computation step from configuration $(L_{i},k_{1},k_{2})$ to configuration $(L_{i^{\prime}},k^{\prime}_{1},k^{\prime}_{2})$ , and let $(*^{\prime})$ be the instance of $(*)$ for $(L_{i^{\prime}},k^{\prime}_{1},k^{\prime}_{2})$ . Then $(*)$ is derivable from $(*^{\prime})$ in $\mathbf{L}^{+\varepsilon}(\mathop{\backslash},\wedge,\mathbf{1})$ .

Proof.

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, $(*^{\prime})$ is obtained from $(*)$ by replacing $\Psi$ with $\Phi$ in the antecedent.

For example, for the instruction inc $(L_{i},1,L_{j})$ in the center of $(*)$ we have $l_{i}=\Psi$ , which is replaced with $p_{1},l_{j}=\Phi$ in $(*^{\prime})$ . 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 jz, 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 $(*^{\prime})$ is $\mathbf{1}\wedge G,\Delta_{1},\Phi,\Delta_{2}\vdash b$ . Now we derive $(*)$ from $(*^{\prime})$ in the following way:

\mathbf{1}\wedge G,\Delta_{1},\Psi,\Delta_{2}\vdash b\mathbf{1}\wedge G,\Delta_{2},\Delta_{1},\Psi\vdash b\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 9.

Proof of Theorem 9.

Using Corollary 13 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

(*_{0})

This sequent $(*_{0})$ is derived as follows:

\mathbf{1}\wedge G,e_{1},l_{0},e_{2}\vdash be_{1},l_{0},e_{2},\mathbf{1}\wedge G\vdash be_{1},l_{0},e_{2},e_{2}\mathop{\backslash}(l_{0}\mathop{\backslash}(e_{1}\mathop{\backslash}b))\vdash b\lx@proof@logical@and e_{2}\vdash e_{2}e_{1},l_{0},l_{0}\mathop{\backslash}(e_{1}\mathop{\backslash}b)\vdash b\lx@proof@logical@and l_{0}\vdash l_{0}e_{1},e_{1}\mathop{\backslash}b\vdash b\lx@proof@logical@and e_{1}\vdash e_{1}b\vdash b

∎

The backwards direction, Theorem 10, 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:

	$\displaystyle w(q)=\{q\}\qquad\mbox{for $q\in\mathcal{V}$;}$
	$\displaystyle w(b)=\{\Xi\Upsilon\mid\mbox{ $\Xi$ and $\Upsilon$ are words over $\Sigma$ such that $\Upsilon\Xi\in B_{\mathfrak{M}}$ }\}.$

Lemma 14.

$w(\mathbf{1}\wedge G)=\{\varepsilon\}$ .

Proof.

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^{\prime}},k^{\prime}_{1},k^{\prime}_{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^{\prime}},k^{\prime}_{1},k^{\prime}_{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^{\prime}},k^{\prime}_{1},k^{\prime}_{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^{\prime}},k^{\prime}_{1},k^{\prime}_{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 10.

Proof of Theorem 10.

If $(*)$ is true in all L $\varepsilon$ -models, it is true in the specific model defined above. By Lemma 14, $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})$ . ∎

3.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 complete theory 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 [22], 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 8 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:

	$\displaystyle\mathscr{L}(0)=\varnothing;$
	$\displaystyle\mathscr{L}(1)=\{\varepsilon\};$
	$\displaystyle\mathscr{L}(A\cdot B)=\mathscr{L}(A)\cdot\mathscr{L}(B);$
	$\displaystyle\mathscr{L}(A+B)=\mathscr{L}(A)\cup\mathscr{L}(B);$
	$\displaystyle\mathscr{L}(A^{})=\bigl{(}\mathscr{L}(A)\bigr{)}^{}=\{u_{1}\ldots u_{n}\mid n\geq 0,u_{i}\in\mathscr{L}(A)\}.$

Languages described by regular expressions are called regular languages.

By Lreg $\varepsilon$ -models let us denote a subclass of L $\varepsilon$ -models in which every variable as interpreted as a regular 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, [27, Theorem 2.8]). Moreover, it is also closed under division:

Proposition 15.

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

Proof.

A more well-known fact (see, for example, [27, 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{5.0pt}{\rotatebox{-60.0}{${\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{5.0pt}{\rotatebox{-60.0}{${\sim}$}}}}$ by the complement operation: $A\mathop{\backslash}B=\overline{A\mathop{\mbox{\raisebox{5.0pt}{\rotatebox{-60.0}{${\sim}$}}}}\overline{B}}$ , where $\overline{X}=\Sigma^{*}-X$ . Since the class of regular languages is closed under $\mathop{\mbox{\raisebox{5.0pt}{\rotatebox{-60.0}{${\sim}$}}}}$ and complement (again, see [27, Theorem 2.8]), it is also closed under $\mathop{\backslash}$ . The $\mathop{/}$ case is symmetric. ∎

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

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

Proposition 16.

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

Proof.

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 [28], it is complete w.r.t. a class of models which is even narrower than the class of Lreg $\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 4, but also no equivalence between theories of all L $\varepsilon$ -models and Lreg $\varepsilon$ -models.

Theorem 17.

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

Proof.

As follows from Theorem 8, $\mathrm{Th}(\mbox{L$\varepsilon$-models};\mathop{\backslash},\wedge,\mathbf{1})$ is $\Sigma_{1}^{0}$ -hard. On the other hand, following Buszkowski [29], 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 Lreg $\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:

\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{)}.

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 Lreg $\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})\neq\mathrm{Th}(\mbox{L$\varepsilon$-models};\mathop{\backslash},\wedge,\mathbf{1}).

∎

Notice that our proof of Theorem 8 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 Lreg $\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 17, 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 Lreg $\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 arbitrary 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})$ .

4 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 2), 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 3, 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 Lreg $\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 [13]. Let us briefly list the results which are new in this article, compared to the WoLLIC paper.

1.

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}$ .
2.

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}$ .
3.

We prove that, in the language including $\mathbf{1}$ , the theory of all L $\varepsilon$ -models is different from the theory of LReg $\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 [28].

While in Section 2 we have presented a quite completed study, Section 3 leaves many questions open for further investigations. Among these, we would like to emphasize the following ones.

1.

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 17) and that for $\mathrm{Th}(\mbox{{\sc Lreg}$\varepsilon$-models};\mathop{\backslash},\wedge,\mathbf{1})$ enumerability will immediately mean decidability.
2.

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 17.

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 [4, 5], 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 Lreg $\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.

References

[1] J. Lambek, The mathematics of sentence structure, Amer. Math. Monthly 65 (1958) 154–170.
[2] R. Moot, C. Retoré, The logic of categorial grammars: a deductive account of natural language syntax and semantics, Vol. 6850 of LNCS, Springer, 2012.
[3] J. Lambek, On the calculus of syntactic types, in: Structure of Language and Its Mathematical Aspects, Vol. 12 of Proc. Symposia Appl. Math., AMS, 1961, pp. 166–178.
[4] M. Pentus, Models for the Lambek calculus, Annals of Pure and Applied Logic 75 (1–2) (1995) 179–213.
[5] M. Pentus, Free monoid completeness of the Lambek calculus allowing empty premises, in: Proc. Logic Colloquium ’96, Vol. 12 of Lect. Notes Logic, Springer, 1998, pp. 171–209.
[6] W. Buszkowski, Compatibility of a categorial grammar with an associated category system, Zeitschr. Math. Logik Grundl. Math. (Math. Logic Q.) 28 (1982) 229–238.
[7] M. Kanazawa, The Lambek calculus enriched with additional connectives, J. Logic Lang. Inform. 1 (2) (1992) 141–171.
[8] V. M. Abrusci, A comparison between Lambek syntactic calculus and intuitionistic linear logic, Zeitschr. math. Logik Grundl. Math. (Math. Logic Q.) 36 (1990) 11–15.
[9] J.-Y. Girard, Linear logic, Theor. Comput. Sci. 50 (1) (1987) 1–102.
[10] J. Lambek, Deductive systems and categories II. Standard constructions and closed categories, in: Category Theory, Homology Theory and Their Applications I, Vol. 86 of Lect. Notes Math., Springer, 1969, pp. 76–122.
[11] H. Ono, Y. Komori, Logics without contraction rule, J. Symb. Log. 50 (1) (1985) 169–201.
[12] M. Kozak, Distributive full Lambek calculus has the finite model property, Studia Logica 91 (2009) 201–216.
[13] M. Kanovich, S. Kuznetsov, A. Scedrov, L-models and R-models for Lambek calculus enriched with additives and the multiplicative unit, in: WoLLIC 2019: Logic, Language, Information, and Computation, Vol. 11541 of Lect. Notes Comput. Sci., 2019, pp. 373–391.
[14] N. Tamura, A linear logic prover (llprover), http://bach.istc.kobe-u.ac.jp/llprover/ (1998–2007).
[15] P. Jipsen, Deciding equations in residuated lattices, http://www1.chapman.edu/~jipsen/reslat/.
[16] M. Okada, K. Terui, The finite model property for various fragments of intuitionistic linear logic, J. Symb. Log. 64 (2) (1999) 790–802.
[17] M. Pentus, The conjoinability relation in Lambek calculus and linear logic, J. Log. Lang. Inform. 3 (1994) 121–140.
[18] H. Andréka, S. Mikulás, I. Németi, The equational theory of Kleene lattices, Theoretical Computer Science 412 (52) (2011) 7099–7108.
[19] H. Andréka, S. Mikulás, Axiomatizability of positive algebras of binary relations, Algebra Universalis 66 (2011) 7–34.
[20] H. Andréka, I. Németi, I. Sain, Some new landmarks on the roadmap of two dimensional logics, in: J. van Eijck, A. Visser (Eds.), Logic and Information Flow, MIT Press, 1994, pp. 163–169.
[21] A. Kurucz, I. Németi, I. Sain, A. Simon, Undecidable varieties of semilattice-ordered semigroups, of Boolean algebras with operators, and logics extending Lambek calculus, Bulletin of the IGPL 1 (1) (1993) 91–98.
[22] S. L. Kuznetsov, Trivalent logics arising from L-models for the Lambek calculus with constants, Journal of Applied Non-Classical Logics 24 (1–2) (2014) 132–137.
[23] M. Kanovich, The direct simulation of Minsky machines in linear logic, in: Advances in Linear Logic, Vol. 222 of London Mathematical Society Lecture Notes, Cambridge University Press, 1995, pp. 123–145.
[24] Y. Lafont, The undecidability of second order linear logic without exponentials, Journal of Symbolic Logic 61 (2) (1996) 541–548.
[25] Y. Lafont, A. Scedrov, The undecidability of second order multiplicative linear logic, Information and Computation 125 (1) (1996) 46–51.
[26] M. L. Minsky, Recursive unsolvability of Post’s problem of “Tag” and other topics in theory of Turing machines, Annals of Mathematics 74 (3) (1961) 437–455.
[27] A. V. Aho, J. D. Ullman, The theory of parsing, translation, and compiling. Vol. I: Parsing, Prentice-Hall, 1972.
[28] W. Buszkowski, The finite model property for BCI and related systems, Studia Logica 57 (1996) 303–323.
[29] W. Buszkowski, On the complexity of the equational theory of relational action algebras, in: RelMiCS 2006: Relations and Kleene Algebra in Computer Science, Vol. 4136 of LNCS, Springer, 2006, pp. 106–119.

Language Models for Some Extensions of the Lambek Calculus

Abstract

keywords:

1 Introduction

2 Distributivity Law in Fragments with One Additive

2.1 Completeness with Additive Conjunction Only

Definition 1.

Proposition 1.

Proof.

Definition 2.

Proposition 2.

Proof.

Definition 3.

Definition 4.

Proposition 3.

Proof.

Theorem 4.

Proof.

Proposition 5.

Theorem 6.

Proof.

2.2 Incompleteness with Additive Disjunction Only

Theorem 7.

Proof of Theorem 7.

3 Undecidability with \\mathop{\backslash}, ∧\wedge, and 𝟏\mathbf{1}

3.1 The System 𝐋+ε​(\,∧,𝟏)\mathbf{L}^{+\varepsilon}(\mathop{\backslash},\wedge,\mathbf{1}) and Its Undecidability

Theorem 8.

Theorem 9.

Theorem 10.

Lemma 11.

Proof.

Corollary 12 (“Post-ish productions”).

Proof.

Corollary 13 (One step of Minsky computation).

Proof.

Proof of Theorem 9.

Lemma 14.

Proof.

Proof of Theorem 10.

3.2 Models on Regular Languages with the Unit Constant

Proposition 15.

Proof.

Proposition 16.

Proof.

Theorem 17.

Proof.

4 Concluding Remarks

References

3 Undecidability with $\mathop{\backslash}$ , $\wedge$ , and $\mathbf{1}$

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