*This article is an extended version of the conference paper presented at RAMiCS 2021.

# Relational Models for the Lambek Calculus
with Intersection and Constants*

Stepan L. Kuznetsov0000-0003-0025-0133  Steklov Mathematical Institute of RAS,
8 Gubkina St., Moscow, Russia<EMAIL_ADDRESS>
###### Abstract.

We consider relational semantics (R-models) for the Lambek calculus extended
with intersection and explicit constants for zero and unit. For its variant
without constants and a restriction which disallows empty antecedents, Andréka
and Mikulás (1994) prove strong completeness. We show that it fails without
this restriction, but, on the other hand, prove weak completeness for non-
standard interpretation of constants. For the standard interpretation, even
weak completeness fails. The weak completeness result extends to an infinitary
setting, for so-called iterative divisions (Kleene star under division). We
also prove strong completeness results for product-free fragments.

###### Key words and phrases:

Lambek calculus, relational semantics, completeness

The author is grateful to Daniel Rogozin for fruitful discussions. The work
was supported by the Theoretical Physics and Mathematics Advancement
Foundation “BASIS”

## Introduction

The Lambek calculus was originally introduced back in 1958 for mathematical
modelling of natural languages [Lam58]. Lambek’s approach involves using
division operations on formal languages, defined as follows:

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

In other words, the language $A\mathop{\backslash}B$ (resp., $B\mathop{/}A$)
consists of words which lack a word from $A$ on the left (resp., on the
right), to become a word from $B$. This interpretation suggests understanding
the Lambek calculus as the atomic (inequational) theory of multiplication and
division of languages; corresponding completeness results were proved by
Pentus [Pen95, Pen98]. Models of the Lambek calculus on the algebra of formal
languages are called language models, or L-models for short.

There is, however, a different class of interpretations for the Lambek
calculus. These are relational models, or R-models. In an R-model, Lambek
formulae (built from variables using multiplication and two division
operations) are interpreted as binary relations on a non-empty set $W$.
Multiplication is composition, and divisions are defined as follows:

$\displaystyle R\mathop{\backslash}S=\\{(y,z)\mid(\forall x\in W)\,((x,y)\in
R\Rightarrow(x,z)\in S\\},$ $\displaystyle S\mathop{/}R=\\{(x,y)\mid(\forall
z\in W)\,((y,z)\in R\Rightarrow(x,z)\in S\\}.$

The idea here is basically the same as in L-models. An arrow $(y,z)$ belongs
to $R\mathop{\backslash}S$ if, being prepended by an arrow $(x,y)$ from $R$,
it yields an arrow $(x,y)$ from $S$; symmetrically for $S\mathop{/}R$. On the
other side, there is a significant difference: in L-models, any two words may
be concatenated, while in R-models composing two arrows is possible only if
the end of the first one coincides with the beginning of the second one.

Both L-models and R-models are particular cases of general algebraic semantics
for the Lambek calculus, namely, models on residuated semigroups. A residuated
semigroup is a semigroup with a partial order $\preceq$ and division
operations $\mathop{\backslash}$ and $\mathop{/}$ obeying the following
equivalences:

$b\preceq a\mathop{\backslash}c\iff a\cdot b\preceq c\iff a\preceq
c\mathop{/}b.$

(In L-models and R-models, $\preceq$ is the subset relation.)

More precisely, L-models and R-models are interpretations on residuated
monoids, since multiplication there has a unit. Namely, the unit language is
$\\{\varepsilon\\}$, the singleton of the empty word, and the unit relation is
the diagonal $\delta=\\{(x,x)\mid x\in W\\}$. Notice that in the language of
the original Lambek calculus there is no explicit constant for the unit.
Adding such a constant causes issues with completeness, which we shall discuss
later.

However, even without an explicit constant for the unit the atomic theory of
residuated monoids differs from that of residuated semigroups. This difference
is witnessed, for example, by the statement
$(a\mathop{\backslash}a)\mathop{\backslash}b\preceq b$, which is true in all
residuated monoids, but not in all residuated semigroups. Thus, the Lambek
calculus comes in two variants: the original Lambek calculus $\mathbf{L}$
[Lam58] for residuated semigroups, and its variant called the Lambek calculus
allowing empty antecedents [Lam61] for residuated monoids. The latter is
commonly denoted by $\mathbf{L}^{\\!\mathbf{*}}$, but we prefer an alternative
notation, $\mathbf{L}^{\\!\Lambda}$, in order to avoid notation conflicts with
Kleene star. The term “… allowing empty antecedents” comes from the sequential
(Gentzen-style) formulation, see Section 1.

In order to obtain completeness for $\mathbf{L}$, one needs to modify
definitions of L-models and R-models. For L-models, it is sufficient just to
remove the empty word from all languages. Importantly, this involves
modification of division operations, since, e.g., $A\mathop{\backslash}A$ in
the original formulation always included the empty word (even if $A$ did not).
(By the way, refraining from the empty word is motivated by linguistic
applications, see [MR12, § 2.5].) For R-models, the corresponding modification
is relativising. Namely, we restrict all relations to subsets of a fixed
transitive relation $U$, which is called the universal one. By transitivity,
composition (product) keeps this relativisation in place; for divisions,
again, one needs to impose it implicitly:

$R\mathop{\backslash}\nolimits_{U}S=\\{(y,z)\in U\mid(\forall x\in
W)\;((x,y)\in R\Rightarrow(x,z)\in S\\},$

and similarly for $S\mathop{/}\nolimits_{\\!U}R$.

Andréka and Mikulás [AM94] proved both completeness of
$\mathbf{L}^{\\!\Lambda}$ w.r.t. unrelativised (also called “square”) R-models
(i.e., with $U=W\times W$) and that of $\mathbf{L}$ w.r.t. relativised ones.
Both results are strong completeness results, i.e., completeness holds for
derivability and semantic entailment from sets of hypotheses (non-logical
axioms), not only for “pure” derivability and general truth (this is called
weak completeness). Notice that, since the Lambek calculus is a substructural
logic and does not enjoy deduction theorem, the difference between strong and
weak completeness is essential already for derivability from finite sets of
hypotheses.

In this article, we consider relational semantics for the extension of
$\mathbf{L}^{\\!\Lambda}$ with intersection, denoted by $\wedge$, and
constants $\mathbf{0}$ and $\mathbf{1}$. In abstract algebraic models
(residuated semigroups), intersection corresponds to the meet operation,
giving the preorder a structure of meet-semilattice. Constant $\mathbf{1}$ is
the unit for multiplication, and $\mathbf{0}$ is simultaneously the smallest
element of the preorder and the zero for multiplication. This extension was
introduced already in Lambek’s 1969 paper [Lam69]; later on, the Lambek
calculus with intersection was considered by van Benthem [Ben91] and Kanazawa
[Kan92].

As noticed by Abrusci [Abr90], the Lambek calculus can be viewed as a non-
commutative variant of Girard’s [Gir87] linear logic. From this point of view,
intersection corresponds to additive conjunction (as opposed to product, which
is multiplicative conjunction). This suggests considering also the dual
additive disjunction, i.e., union, which is also natural in algebraic
semantics, where it corresponds to lattice-theoretic join (this gives rise to
residuated lattices; for more information on these structures and their
logics, see [GJKO07]). Additive disjunction, however, raises problems with
completeness connected with the distributivity law [OK85, KKS22]. Due to this
reason, we consider only intersection, not union.

The rest of the article is organised as follows.

  * •

In Section 1, we give accurate definitions of the calculus in question,
denoted by $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$, and R-models
for it. Here we also formulate known completeness results, by Andréka and
Mikulás [AM94, Mik15a, Mik15b].

  * •

In Section 2, we provide examples showing that each of the explicit constants
$\mathbf{0}$ and $\mathbf{1}$ ruins completeness, even in the weak sense (the
example for $\mathbf{1}$ is not a new one). As a workaround, we relax the
definition of R-models and define R-models with non-standard interpretations
of constants.

  * •

For these non-standard models, in Section 3 we prove weak completeness of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. As a corollary, we
obtain a simpler proof of Mikulás’ completeness result [Mik15a, Mik15b] for
the fragment of $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ without
constants.

  * •

Strong completeness fails, as proved in Section 4. The counterexample used in
this section was suggested by Mikulás [Mik15b], but without proof. Here we
fill this gap.

  * •

In Section 5, we extend our weak completeness result to an infinitary setting.
Namely, we consider so-called iterative divisions, which are Kleene stars in
denominators of division operations. Being axiomatised by $\omega$-rules,
iterative divisions are in fact infinite intersections.

  * •

The last two sections are devoted to the product-free fragment of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. We show (Section 7)
that if one removes the product that strong completeness can be restored, but
w.r.t. a modified class of models. However, inside the proof we essentially
use product, which raises a conservativity issue. Conservativity is proved in
Section 6 in the strong form, i.e., for derivability from hypotheses, using an
extension of $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ with the
exponential modality (which allows a modalised variant of deduction theorem,
cf. [LMSS92]). An important corollary of the strong completeness result is
that if we consider the product-free fragment without constants (that is, in
the language of $\mathop{\backslash}$, $\mathop{/}$, and $\wedge$), then it
will be strongly complete w.r.t. square R-models in the standard sense.

This journal article is an extended version of the conference paper [Kuz21],
presented at RAMiCS 2021 and published in its proceedings. The extension here
is twofold. First, along with constant $\mathbf{1}$, now we also consider
constant $\mathbf{0}$. We show that this constant also raises issues with
completeness, and resolve them using a non-standard interpretation for
$\mathbf{0}$ also. Second, we add Section 7 (and Section 6 supporting it) with
the strong completeness result for the product-free fragment. This result was
presented as a short talk at AiML 2022, without formal publication.

##  1\. The Lambek Calculus with Intersection and R-Models

Let us recall the formulation of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$, the Lambek calculus
with intersection and constants, in the form of a Gentzen-style sequent
calculus. Formulae are constructed from variables ($p,q,r,\ldots$) and
constants $\mathbf{0}$ (zero) and $\mathbf{1}$ (unit) using four binary
connectives: $\cdot$ (multiplication), $\mathop{\backslash}$ (left division),
$\mathop{/}$ (right division), and $\wedge$ (intersection). The set of all
formulae is denoted by $\mathrm{Fm}$. Formulae are denoted by capital Latin
letters. Capital Greek letters denote sequences of formulae; $\Lambda$ stands
for the empty sequence. Sequents are expressions of the form $\Pi\to B$. (Due
to the non-commutative nature of the Lambek calculus, order in $\Pi$ matters.)
Here $\Pi$ is called the antecedent and $B$ the succedent of the sequent.

The axioms and inference rules are as follows:

$A\to A\qquad\Gamma,\Pi,\Delta\to C\lx@proof@logical@and\Pi\to
A\Gamma,A,\Delta\to C$ $\Gamma,\Pi,A\mathop{\backslash}B,\Delta\to
C\lx@proof@logical@and\Pi\to A\Gamma,B,\Delta\to C\qquad\Pi\to
A\mathop{\backslash}BA,\Pi\to B\qquad\Gamma,A\cdot B,\Delta\to
C\Gamma,A,B,\Delta\to C$ $\Gamma,B\mathop{/}A,\Pi,\Delta\to
C\lx@proof@logical@and\Pi\to A\Gamma,B,\Delta\to C\qquad\Pi\to
B\mathop{/}A\Pi,A\to B\qquad\Pi,\Delta\to A\cdot B\lx@proof@logical@and\Pi\to
A\Delta\to B$ $\Gamma,A\wedge B,\Delta\to C\Gamma,A,\Delta\to
C\qquad\Gamma,A\wedge B,\Delta\to C\Gamma,B,\Delta\to C\qquad\Pi\to A\wedge
B\lx@proof@logical@and\Pi\to A\Pi\to B$ $\Gamma,\mathbf{0},\Delta\to
C\qquad\Gamma,\mathbf{1},\Delta\to C\Gamma,\Delta\to
C\qquad\Lambda\to\mathbf{1}$

We consider both pure derivability of sequents and derivability from
hypotheses. For the latter, having a set of sequents $\mathcal{H}$, we add
them as extra non-logical axioms, and derive a given sequent $\Pi\to B$ using
both the new axioms and axioms and inference rules of the original calculus.
In this case, we say that $\Pi\to B$ is derivable, or syntactically follows
from $\mathcal{H}$. Pure derivability is derivability from an empty
$\mathcal{H}$, i.e., using only axioms and rules of the original calculus.

For pure derivability, $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$
enjoys cut elimination, that is, any derivable sequent can be derived without
using $Cut$. The proof of cut elimination is standard, being an easy extension
of Lambek’s argument [Lam58] for the Lambek calculus. For derivability from
hypotheses, cut elimination, in general, does not hold.

Besides $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ itself, we
consider its elementary fragments with restricted sets of connectives and
constants. Such a fragment is obtained by merely removing all axioms and rules
which operate the connectives and constants which do not belong to the
restricted set. In particular, we shall use the notation
$\mathbf{L}^{\\!\Lambda}{\wedge}$ for the fragment of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ without constants
$\mathbf{0}$ and $\mathbf{1}$ and $\mathbf{L}^{\\!\Lambda}$ for the fragment
with only $\mathop{\backslash}$, $\mathop{/}$, and $\cdot$.

Such a definition of elementary fragment raises issues of conservativity. For
pure derivability, this issue is resolved by cut elimination. All rules,
except $Cut$, enjoy the subformula property, therefore the set of theorems of
an elementary fragment coincides with the set of sequents in the corresponding
restricted language which are derivable in the full system
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. For derivability from
hypotheses, the issue is more subtle. In principle, a derivation of $\Pi\to B$
from $\mathcal{H}$ which uses $Cut$ could involve connectives or constants
which do not belong to the restricted language of $\mathcal{H}$ and $\Pi\to
B$. We address this question below in Section 6.

The original Lambek calculus $\mathbf{L}$ is obtained from
$\mathbf{L}^{\\!\Lambda}$ by imposing the so-called Lambek’s non-emptiness
restriction, that is, requiring non-emptiness of $\Pi$ in the
$\mathop{\backslash}R$ and $\mathop{/}R$ rules. This condition ensures that
antecedents of all sequents in $\mathbf{L}$ are non-empty
($\mathop{\backslash}R$ and $\mathop{/}R$ are the only two rules which could
possibly produce an empty antecedent). As noticed in the Introduction,
Lambek’s restriction has linguistic motivation [MR12, § 2.5]. One can also
consider a version of $\mathbf{L}^{\\!\Lambda}{\wedge}$ with Lambek’s
restriction, denoted by $\mathbf{L}{\wedge}$. On the other hand, constant
$\mathbf{1}$ is incompatible with Lambek’s restriction, so we shall not add
constants to $\mathbf{L}$ or $\mathbf{L}{\wedge}$.

It is important to keep in mind that $\mathbf{L}$ is not a conservative
fragment of $\mathbf{L}^{\\!\Lambda}$, neither $\mathbf{L}{\wedge}$ is such of
$\mathbf{L}^{\\!\Lambda}{\wedge}$. Even if the sequent has a non-empty
antecedent, empty antecedents could be necessary inside its derivation. An
example is $(p\mathop{\backslash}p)\mathop{\backslash}q\to q$, which is
derivable in $\mathbf{L}^{\\!\Lambda}$, but not in $\mathbf{L}$. Therefore,
there is no easy way of translating results between $\mathbf{L}$ and
$\mathbf{L}^{\\!\Lambda}$, and certain properties of these systems differ, as
we shall see below.

Now let us define relational semantics. Here we define it for calculi without
constants $\mathbf{0}$ and $\mathbf{1}$; those are handled in the next
section.

A relativised relational model (R-model) is a triple $\mathcal{M}=(W,U,v)$,
where $W$ is a non-empty set, $U\subseteq W\times W$ is a transitive relation
on $W$ called the universal one, and $v\colon\mathrm{Fm}\to\mathcal{P}(U)$ is
a valuation function mapping formulae to subrelations of $U$. The valuation
function should obey the following conditions:

$\displaystyle v(A\cdot B)=v(A)\circ v(B)=\\{(x,z)\mid\exists y\in
W\>\bigl{(}(x,y)\in v(A)\mbox{ and }(y,z)\in v(B)\bigr{)}\\};$ $\displaystyle
v(A\mathop{\backslash}B)=v(A)\mathop{\backslash}\nolimits_{U}v(B)=\\{(y,z)\in
U\mid\forall x\in W\>\bigl{(}(x,y)\in v(A)\Rightarrow(x,z)\in
v(B)\bigr{)}\\};$ $\displaystyle
v(B\mathop{/}A)=v(B)\mathop{/}\nolimits_{\\!U}v(A)=\\{(x,y)\in U\mid\forall
z\in W\>\bigl{(}(y,z)\in v(A)\Rightarrow(x,z)\in v(B)\bigr{)}\\};$
$\displaystyle v(A\wedge B)=v(A)\cap v(B)=\\{(x,y)\mid(x,y)\in v(A)\mbox{ and
}(x,y)\in v(B)\\}.$

An R-model $\mathcal{M}=(W,U,v)$ is a square one if $U=W\times W$.

Arbitrary R-models and square R-models form natural classes of models for
$\mathbf{L}{\wedge}$ and $\mathbf{L}^{\\!\Lambda}{\wedge}$ respectively (and,
thus, for $\mathbf{L}$ and $\mathbf{L}^{\\!\Lambda}$). Let us define the truth
condition of sequents in R-models.

A sequent of the form $A_{1},\ldots,A_{n}\to B$ is true in model
$\mathcal{M}=(W,U,v)$, if $v(A_{1})\circ\ldots\circ v(A_{n})\subseteq v(B)$.
For sequents with empty antecedents, truth is defined only in square R-models:
$\Lambda\to B$ is true in $\mathcal{M}=(W,W\times W,v)$, if
$\delta=\\{(x,x)\mid x\in W\\}\subseteq v(B)$.

Let us also recall the general notion of strong soundness and completeness of
a logic $\mathcal{L}$ (formulated as a sequent calculus) w.r.t. a class of
models $\mathcal{K}$.

Let $\Pi\to B$ and $\mathcal{H}$ be, respectively, a sequent and a set of
sequents in the language of $\mathcal{L}$. The sequent $\Pi\to B$ semantically
follows from $\mathcal{H}$ on the class of models $\mathcal{K}$, if for any
model from $\mathcal{K}$ in which all sequents from $\mathcal{H}$ are true,
the sequent $\Pi\to B$ is also true. This is denoted by
$\mathcal{H}\vDash_{\mathcal{K}}\Pi\to B$.

In the notations of the previous definition, $\Pi\to B$ syntactically follows
from $\mathcal{H}$ in the logic $\mathcal{L}$, if $\Pi\to B$ is derivable in
the calculus for $\mathcal{L}$ extended with sequents from $\mathcal{H}$ as
extra axioms. This is denoted by $\mathcal{H}\vdash_{\mathcal{L}}\Pi\to B$.

The logic $\mathcal{L}$ is strongly sound w.r.t. the class of models
$\mathcal{K}$, if $\mathcal{H}\vdash_{\mathcal{L}}\Pi\to B$ entails
$\mathcal{H}\vDash_{\mathcal{K}}\Pi\to B$ for any $\Pi\to B$ and
$\mathcal{H}$.

The logic $\mathcal{L}$ is strongly complete w.r.t. the class of models
$\mathcal{K}$, if $\mathcal{H}\vDash_{\mathcal{K}}\Pi\to B$ entails
$\mathcal{H}\vdash_{\mathcal{L}}\Pi\to B$ for any $\Pi\to B$ and
$\mathcal{H}$.

The Lambek calculus is a substructural system which does not enjoy deduction
theorem. Therefore, strong soundness and completeness, even for finite sets
$\mathcal{H}$, are significantly different from their more usual weak
counterparts (that derivability of a sequent without hypotheses yields its
truth in all models from the given class, and the other way round).

One can easily check that $\mathbf{L}{\wedge}$ and
$\mathbf{L}^{\\!\Lambda}{\wedge}$ are strongly sound w.r.t. the corresponding
class of R-models: namely, all R-models for $\mathbf{L}$ and square ones for
$\mathbf{L}^{\\!\Lambda}$. The situation with completeness is non-trivial.
Andréka and Mikulás [AM94] proved the following strong completeness results:

######  Theorem 1 (Andréka, Mikulás 1994).

The calculus $\mathbf{L}{\wedge}$ is strongly complete w.r.t. the class of all
R-models.

######  Theorem 2 (Andréka, Mikulás 1994).

The calculus $\mathbf{L}^{\\!\Lambda}$ is strongly complete w.r.t. the class
of square R-models.

The arguments used for proving these two theorems, being similar, are yet not
completely identical. In particular, Theorem 1 is valid for the calculus with
intersection, while the proof of Theorem 2 cannot be easily extended to such a
calculus, i.e., to $\mathbf{L}^{\\!\Lambda}{\wedge}$.

Later on, however, Mikulás [Mik15a, Mik15b] managed to modify the proof of
Theorem 2 for $\mathbf{L}^{\\!\Lambda}{\wedge}$, but this modification
establishes only weak completeness:

######  Theorem 3 (Mikulás 2015).

111Here “Mikulás 2015” refers both to [Mik15a] and [Mik15b], which feature
different proofs of Theorem 1. If a sequent (in the language of
$\cdot,\mathop{\backslash},\mathop{/},\wedge$) is true in all square R-models,
then it is derivable in $\mathbf{L}^{\\!\Lambda}{\wedge}$.

In Section 4 we shall show that strong completeness for
$\mathbf{L}^{\\!\Lambda}{\wedge}$ fails.

##  2\. Constants Zero and One: Nonstandard Models

The situation with constants $\mathbf{0}$ and $\mathbf{1}$ is tricky.
Naturally, $\mathbf{1}$ should be interpreted as the neutral element for
multiplication (since $A\cdot\mathbf{1}\leftrightarrow
A\leftrightarrow\mathbf{1}\cdot A$) and $\mathbf{0}$ as the smallest element
in the preorder (due to derivability of $\mathbf{0}\to A$). This suggests the
following interpretation of constants in R-models, which we call the standard
interpretation:

$\displaystyle v(\mathbf{0})=\varnothing;$ $\displaystyle
v(\mathbf{1})=\delta=\\{(x,x)\mid x\in W\\}.$

Unfortunately, under the standard interpretation completeness fails, even in
the weak sense, for each of the constants. Let us start with constant
$\mathbf{0}$.

######  Proposition 4.

The sequent

$\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p),\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)\to(\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q))\cdot(\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p))$

is true in all square R-models (under the standard interpretation of
$\mathbf{0}$), but not derivable in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$.

######  Proof 2.1.

Let us first check that sequent is generally true on R-models. For an
arbitrary relation $R$ we have:

$\varnothing\mathop{/}R=\\{(x,y)\in W\times W\mid\forall z\in
W\>\bigl{(}(y,z)\in R\Rightarrow(x,z)\in\varnothing\bigr{)}\\}=\\\ \\{(x,y)\in
W\times W\mid\forall z\in W\>(y,z)\notin R\\}.$

Further,

$\varnothing\mathop{/}(\varnothing\mathop{/}R)=\\{(x,y)\in W\times
W\mid\forall z\in W\>(y,z)\notin\varnothing\mathop{/}R\\}=\\\ \\{(x,y)\in
W\times W\mid\forall z\in W\>\exists w\in W\>(z,w)\in R\\}.$

The condition on $(x,y)$ here does not depend on $(x,y)$ itself. Hence,
$\varnothing\mathop{/}(\varnothing\mathop{/}R)$ is either $\varnothing$ or
$W\times W$, for any relation $R$. For these two relations, composition is
commutative:

$\varnothing\circ(W\times W)=\varnothing=(W\times W)\circ\varnothing.$

This yields
$(\varnothing\mathop{/}(\varnothing\mathop{/}P))\circ(\varnothing\mathop{/}(\varnothing\mathop{/}Q))\subseteq(\varnothing\mathop{/}(\varnothing\mathop{/}Q))\circ(\varnothing\mathop{/}(\varnothing\mathop{/}P))$
for any $P,Q$. Taking $P=v(p)$, $Q=v(q)$, and recalling that
$v(\mathbf{0})=\varnothing$ (standard interpretation), we conclude that the
desired sequent is true.

Now let us perform cut-free proof search in order to show that this sequent is
not derivable in $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. Two
possible cases for the lowermost rule are $\mathop{\backslash}L$ and $\cdot
R$. In the first case, the left premise of this rule should be
$\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)\to\mathbf{0}\mathop{/}p$ (since
$\Lambda\to\mathbf{0}\mathop{/}p$ and $\Lambda\to\mathbf{0}\mathop{/}q$ are
obviously not derivable). The only non-trivial attempt to derive this sequent
is as follows:

$\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)\to\mathbf{0}\mathop{/}p\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q),p\to\mathbf{0}\lx@proof@logical@and
p\to\mathbf{0}\mathop{/}qp,q\to\mathbf{0}\mathbf{0}\to\mathbf{0}$

and it fails.

The second possibility is $\cdot R$. One can easily see that
$\Lambda\to\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)$ is not derivable,
neither is $\Lambda\to\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p)$. Hence, the
only remaining attempt is as follows:

$\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p),\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)\to(\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q))\cdot(\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p))\lx@proof@logical@and\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p)\to\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p),\mathbf{0}\mathop{/}q\to\mathbf{0}\lx@proof@logical@and\mathbf{0}\mathop{/}q\to\mathbf{0}\mathop{/}p\mathbf{0}\mathop{/}q,p\to\mathbf{0}\mathbf{0}\to\mathbf{0}\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}q)\to\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}p)$

The top sequent $\mathbf{0}\mathop{/}q,p\to\mathbf{0}$ is not derivable.

Next, we recall two previously known counterexamples to weak completeness with
constant $\mathbf{1}$, in square R-models with standard interpretation of this
constant.

One example,

$\mathbf{1}\wedge p\wedge q\to(\mathbf{1}\wedge p)\cdot(\mathbf{1}\wedge q),$

was given by Andréka and Mikulás [AM11]. In the particular case of $p=q$, this
yields the contraction (“doubling”) principle for formulae of the form
$\mathbf{1}\wedge A$, that is, $\mathbf{1}\wedge A\to(\mathbf{1}\wedge
A)\cdot(\mathbf{1}\wedge A)$. Another such example was given by Buszkowski
[Bus06]:

$\mathbf{1}\mathop{/}(p\mathop{/}p)\to(\mathbf{1}\mathop{/}(p\mathop{/}p))\cdot(\mathbf{1}\mathop{/}(p\mathop{/}p)).$

This example uses division instead of intersection, and again it is a form of
contraction.

Thus, constructing a complete axiomatisation for the standard interpretation
of constants $\mathbf{0}$ and $\mathbf{1}$ in R-models, even if this is
possible, is a non-trivial open question.

We overcome this issue by extending the class of models being considered, thus
restoring completeness for the original system
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. The idea is as follows:
while $\delta$ is the only neutral element for the set of all binary relations
on $W$, for a set which includes only some relations (and does not include
$\delta$), the neutral element could be a different relation. Similarly for
zero, a designated subclass of binary relations could have the smallest
element which is not $\varnothing$. This leads to the following definition.

Let $\mathfrak{A}\subseteq\mathcal{P}(W\times W)$ be a family of binary
relations over $W$, closed under $\circ$, $\mathop{\backslash}$, $\mathop{/}$,
and $\cap$. Relation $\mathbf{1}_{\mathfrak{A}}\in\mathfrak{A}$ is called the
$\mathfrak{A}$-unit if $\mathbf{1}_{\mathfrak{A}}\circ
R=R\circ\mathbf{1}_{\mathfrak{A}}=R$ for any $R\in\mathfrak{A}$. Relation
$\mathbf{0}_{\mathfrak{A}}\in\mathfrak{A}$ is called the $\mathfrak{A}$-zero
if $\mathbf{0}_{\mathfrak{A}}\subseteq R$ for any $R\in\mathfrak{A}$.

A standard algebraic argument shows that the $\mathfrak{A}$-unit, if it
exists, is unique. Indeed, for another $\mathfrak{A}$-unit
$\mathbf{1}_{\mathfrak{A}}^{\prime}\in\mathfrak{A}$ we have
$\mathbf{1}_{\mathfrak{A}}^{\prime}=\mathbf{1}_{\mathfrak{A}}^{\prime}\circ\mathbf{1}_{\mathfrak{A}}=\mathbf{1}_{\mathfrak{A}}$.
For $\mathfrak{A}$-zero, uniqueness is obvious.

However, $\mathbf{1}_{\mathfrak{A}}$ is not necessarily the diagonal relation
$\delta=\\{(x,x)\mid x\in W\\}$, as the latter may be outside $\mathfrak{A}$.
For example, let $W$ be a non-empty set and let $W^{\prime}=W\times\\{1,2\\}$.
For each relation $R$ on $W$ let us define a relation $R^{\prime}$ as follows:
$(x,i)R^{\prime}(y,j)$, if $xRy$ and $i\leq j$. Let $\mathfrak{A}$ be the
class of relations of the form $R^{\prime}$. Then
$\mathbf{1}_{\mathfrak{A}}=\delta^{\prime}=\\{((x,i),(x,j))\mid i\leq j\\}$.
Similarly, $\mathbf{0}_{\mathfrak{A}}$ is not necessarily $\varnothing$; in
fact, it is just the intersection of all relations from $\mathfrak{A}$.

Let us prove two properties of $\mathbf{0}_{\mathfrak{A}}$ and
$\mathbf{1}_{\mathfrak{A}}$.

######  Lemma 5.

If $\mathbf{0}_{\mathfrak{A}}$ is the $\mathfrak{A}$-zero, then it is the zero
for relation composition, i.e., $\mathbf{0}_{\mathfrak{A}}\circ
R=R\circ\mathbf{0}_{\mathfrak{A}}=\mathbf{0}_{\mathfrak{A}}$ for any
$R\in\mathfrak{A}$.

######  Proof 2.2.

Let us show $\mathbf{0}_{\mathfrak{A}}\circ R=\mathbf{0}_{\mathfrak{A}}$, the
other equality is symmetric. First, since $\mathfrak{A}$ is closed under
composition, we have $\mathbf{0}_{\mathfrak{A}}\circ R\in\mathfrak{A}$, and
therefore $\mathbf{0}_{\mathfrak{A}}\subseteq\mathbf{0}_{\mathfrak{A}}\circ
R$. For the opposite inclusion, we notice that
$\mathbf{0}_{\mathfrak{A}}\mathop{/}R$ is also in $\mathfrak{A}$, whence
$\mathbf{0}_{\mathfrak{A}}\subseteq\mathbf{0}_{\mathfrak{A}}\mathop{/}R$,
which is equivalent to $\mathbf{0}_{\mathfrak{A}}\circ
R\subseteq\mathbf{0}_{\mathfrak{A}}$.

######  Lemma 6.

If $R\in\mathfrak{A}$ and $\mathbf{1}_{\mathfrak{A}}$ is the
$\mathfrak{A}$-unit, then $\mathbf{1}_{\mathfrak{A}}\subseteq R$ if and only
if $\delta\subseteq R$. In particular,
$\delta\subseteq\mathbf{1}_{\mathfrak{A}}$.

######  Proof 2.3.

Let us first show that for any $R\in\mathfrak{A}$ we have
$R=R\mathop{/}\mathbf{1}_{\mathfrak{A}}$. One inclusion is easy:
$R\circ\mathbf{1}_{\mathfrak{A}}\subseteq R$ yields $R\subseteq
R\mathop{/}\mathbf{1}_{\mathfrak{A}}$. For the other inclusion, we first
notice that
$(R\mathop{/}\mathbf{1}_{\mathfrak{A}})\circ\mathbf{1}_{\mathfrak{A}}\subseteq
R$ (this follows from $R\mathop{/}\mathbf{1}_{\mathfrak{A}}\subseteq
R\mathop{/}\mathbf{1}_{\mathfrak{A}}$). Now, since
$(R\mathop{/}\mathbf{1}_{\mathfrak{A}})\in\mathfrak{A}$, we have
$R\mathop{/}\mathbf{1}_{\mathfrak{A}}=(R\mathop{/}\mathbf{1}_{\mathfrak{A}})\circ\mathbf{1}_{\mathfrak{A}}\subseteq
R$. Using $R=R\mathop{/}\mathbf{1}_{\mathfrak{A}}$, we build a chain of
equivalences: $\mathbf{1}_{\mathfrak{A}}\subseteq
R\iff\delta\circ\mathbf{1}_{\mathfrak{A}}\subseteq R\iff\delta\subseteq
R\mathop{/}\mathbf{1}_{\mathfrak{A}}\iff\delta\subseteq R.$

Due to this lemma, we may keep the truth definition for sequents with empty
antecedents the same. That is, we do not need to replace $\delta$ with
$\mathbf{1}_{\mathfrak{A}}$.

Now we are ready to define our non-standard models.

A non-standard square R-model is a structure
$\mathcal{M}^{\mathfrak{A}}=(W,\mathfrak{A},\mathbf{1}_{\mathfrak{A}},\mathbf{0}_{\mathfrak{A}},v)$,
where $W$ is a non-empty set; $\mathfrak{A}\subseteq\mathcal{P}(W\times W)$ is
a family of binary relations on $W$, closed under $\circ$,
$\mathop{\backslash}$, $\mathop{/}$, and $\cap$; $\mathbf{1}_{\mathfrak{A}}$
is the $\mathfrak{A}$-unit; $\mathbf{0}_{\mathfrak{A}}$ is the
$\mathfrak{A}$-unit; $v\colon\mathrm{Fm}\to\mathfrak{A}$ is a valuation
function mapping formulae to relations from the family $\mathfrak{A}$. The
valuation function should obey the conditions from Definition 1, with
$U=W\times W$, and, additionally, $v(\mathbf{1})=\mathbf{1}_{\mathfrak{A}}$
and $v(\mathbf{0})=\mathbf{0}_{\mathfrak{A}}$. The truth of a sequent in a
non-standard square R-model is defined exactly as in Definition 1.

######  Proposition 7.

The calculus $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is strongly
sound w.r.t. the class of non-standard square R-models.

######  Proof 2.4.

As usual, we proceed by induction on the derivation. The interesting cases are
$\mathbf{1}L$, $\mathbf{1}R$, and $\mathbf{0}L$, as others are copied from the
standard strong soundness proof of $\mathbf{L}^{\\!\Lambda}{\wedge}$ w.r.t.
square R-models (without constants $\mathbf{0}$ and $\mathbf{1}$).

For $\mathbf{1}R$, we have to show that $\Lambda\to\mathbf{1}$ is true, that
is, $\delta\subseteq v(\mathbf{1})=\mathbf{1}_{\mathfrak{A}}$. This is a
particular case of Lemma 6.

For $\mathbf{1}L$, we consider two cases. If both $\Gamma$ and $\Delta$ are
empty, then our induction hypothesis gives $\delta\subseteq v(C)$. By Lemma 6,
this is equivalent to $\mathbf{1}_{\mathfrak{A}}\subseteq v(C)$ (recall that
$v(C)\in\mathfrak{A}$), which is the truth of $\mathbf{1}\to C$. If, say,
$\Delta$ is non-empty, then let $D_{1}$ be the first formula of $\Delta$. By
definition of the $\mathfrak{A}$-unit, we have $v(\mathbf{1})\circ
v(D_{1})=\mathbf{1}_{\mathfrak{A}}\circ v(D_{1})=v(D_{1})$. Thus,
interpretations of left-hand sides of the premise and the conclusion are
identical. The case of non-empty $\Gamma$ is symmetric.

For $\mathbf{0}L$, since the antecedent includes $\mathbf{0}$, its
interpretation is $\mathbf{0}_{\mathfrak{A}}$ by Lemma 5. By definition of
$\mathfrak{A}$-zero, $\mathbf{0}_{\mathfrak{A}}\subseteq v(C)$, where $C$ is
the succedent.

As for completeness, we prove only its weak version (Section 3). For strong
completeness, there is a counterexample (Section 4).

##  3\. Weak Completeness

We prove weak completeness of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ w.r.t. the class of non-
standard square R-models, as defined in the previous section.

######  Theorem 8.

If a sequent (in the language of
$\mathop{\backslash},\mathop{/},\cdot,\wedge,\mathbf{1},\mathbf{0}$) is true
in all non-standard square R-models, then it is derivable in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$.

Our proof follows the line of the proof of Theorem 1 (suprisingly, not Theorem
2, see Remark 11 below): we build a labelled graph with specific properties
and use it to construct a universal model.

Throughout this section, $\vdash A\to B$ means “$A\to B$ is derivable in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$.”

######  Lemma 9.

There exists a labelled directed graph $G=(V,E,\ell)$, where
$V\neq\varnothing$, $E\subseteq V\times V$, and $\ell\colon E\to\mathrm{Fm}$,
such that the following holds:

  1. (1)

$E$ is transitive;

  2. (2)

$E$ is reflexive and $\ell(x,x)=\mathbf{1}$ for any $x\in V$;

  3. (3)

$E$ is antisymmetric: if $x\neq y$ and $(x,y)\in E$, then $(y,x)\notin E$;

  4. (4)

if $(x,y)\in E$ and $(y,z)\in E$, then
$\vdash\ell(x,z)\to\ell(x,y)\cdot\ell(y,z)$;

  5. (5)

if $\vdash\ell(x,z)\to B\cdot C$, then there exists such $y\in V$ that
$(x,y)\in E$, $(y,z)\in E$, $\vdash\ell(x,y)\to B$, and $\vdash\ell(y,z)\to
C$;

  6. (6)

for any $y\in V$ and any formula $A$ there exists such $x\in V$ that for any
$z\in V$ if $(y,z)\in E$, then $\ell(x,z)=A\cdot\ell(y,z)$;

  7. (7)

for any $y\in V$ and any formula $A$ there exists such $z\in V$ that for any
$x\in V$ if $(x,y)\in E$, then $\ell(x,z)=\ell(x,y)\cdot A$.

Before proving Lemma 9, let us use it to establish Theorem 8.

######  Proof 3.1 (Proof of Theorem 8).

Using graph $G$ provided by Lemma 9, we construct a universal non-standard
square R-model
$\mathcal{M}_{0}^{\mathfrak{A}}=(W,\mathfrak{A},\mathbf{1}_{\mathfrak{A}},\mathbf{0}_{\mathfrak{A}},v)$
in the following way:

$\displaystyle W=V;$ $\displaystyle v(A)=\\{(x,y)\in E\mid\ \vdash\ell(x,y)\to
A\\};$ $\displaystyle\mathfrak{A}=\\{v(A)\mid A\in\mathrm{Fm}\\};$
$\displaystyle\mathbf{1}_{\mathfrak{A}}=v(\mathbf{1});\
\mathbf{0}_{\mathfrak{A}}=v(\mathbf{0}).$

Let us show that $\mathcal{M}_{0}^{\mathfrak{A}}$ is indeed a well-defined
model.

Multiplication. If $(x,z)\in v(B\cdot C)$, then $\vdash\ell(x,z)\to B\cdot C$.
By property 5 of graph $G$, there exists such $y$ that $(x,y)\in v(B)$ and
$(y,z)\in v(C)$. Therefore, $(x,z)\in v(B)\circ v(C)$. This establishes the
inclusion $v(B\cdot C)\subseteq v(B)\circ v(C)$.

For the opposite inclusion, take $(x,y)\in v(B)$ and $(y,z)\in v(C)$. By
transitivity, $(x,z)\in E$. By property 4 of $G$,
$\vdash\ell(x,z)\to\ell(x,y)\cdot\ell(y,z)$. We derive $\ell(x,z)\to B\cdot C$
as follows:

$\ell(x,z)\to B\cdot
C\lx@proof@logical@and\ell(x,z)\to\ell(x,y)\cdot\ell(y,z)\ell(x,y)\cdot\ell(y,z)\to
B\cdot C\ell(x,y),\ell(y,z)\to B\cdot C\lx@proof@logical@and\ell(x,y)\to
B\ell(y,z)\to C$

Therefore, $(x,z)\in v(B\cdot C)$.

Division. Let $(y,z)\in v(A\mathop{\backslash}B)$, that is,
$\vdash\ell(y,z)\to A\mathop{\backslash}B$. Take an arbitrary $x\in W$ such
that $(x,y)\in v(A)$, that is, $\vdash\ell(x,y)\to A$. Now by transitivity
$(x,z)\in E$, and $\ell(x,z)\to B$ is derived using two cuts, with
$\ell(x,z)\to\ell(x,y)\cdot\ell(y,z)$ (property 4 of $G$) and
$A\cdot(A\mathop{\backslash}B)\to B$. This establishes the inclusion
$v(A\mathop{\backslash}B)\subseteq v(A)\mathop{\backslash}v(B)$.

For the opposite inclusion, take $(y,z)\in v(A)\mathop{\backslash}v(B)$ and
apply property 6 to $y$ and $A$. For the vertex $x\in W$ given by this
property, we have $\ell(x,y)=A\cdot\ell(y,y)=A\cdot\mathbf{1}$ and
$\ell(x,z)=A\cdot\ell(y,z)$. The first condition gives $(x,y)\in v(A)$
(because $\vdash A\cdot\mathbf{1}\to A$). Hence, $(x,z)\in v(B)$, i.e.,
$(x,z)\in E$ and $\vdash\ell(x,z)\to B$. In particular, $(x,z)\in E$ gives
$(y,z)\in E$ (which was not guaranteed in advance). Since
$\ell(x,z)=A\cdot\ell(y,z)$, we may proceed as follows:

$\ell(y,z)\to A\mathop{\backslash}BA,\ell(y,z)\to B\lx@proof@logical@and
A,\ell(y,z)\to A\cdot\ell(y,z)\lx@proof@logical@and A\to
A\ell(y,z)\to\ell(y,z)A\cdot\ell(y,z)\to B$

This establishes $(y,z)\in v(A\mathop{\backslash}B)$. Thus, we get
$v(A)\mathop{\backslash}v(B)=v(A\mathop{\backslash}B)$.

The equality $v(B\mathop{/}A)=v(B)\mathop{/}v(A)$ is established
symmetrically.

Intersection. We have $v(A\wedge B)=\\{(x,y)\in E\mid\ \vdash\ell(x,y)\to
A\wedge B\\}=\\{(x,y)\in E\mid\ \vdash\ell(x,y)\to A\mbox{ and
}\vdash\ell(x,y)\to B\\}=v(A)\cap v(B)$. In the second equality, the
$\supseteq$ inclusion is by $\wedge R$, and the $\subseteq$ one is by cut with
$A\wedge B\to A$ and $A\wedge B\to B$.

Unit. Here we have $v(\mathbf{1})=\mathbf{1}_{\mathfrak{A}}$ by definition,
and $\mathbf{1}_{\mathfrak{A}}$ is the $\mathfrak{A}$-unit. Indeed, since $A$
is equivalent to $\mathbf{1}\cdot A$ and any relation in $\mathfrak{A}$ is of
the form $v(A)$, we have $\mathbf{1}_{\mathfrak{A}}\circ
v(A)=v(\mathbf{1})\circ v(A)=v(\mathbf{1}\cdot A)=v(A)$. Similarly for
$v(A)\circ\mathbf{1}_{\mathfrak{A}}$.

Zero. By definition $v(\mathbf{0})=\mathbf{0}_{\mathfrak{A}}$, let us show
that it is indeed the $\mathfrak{A}$-zero. Each relation in $\mathfrak{A}$ is
of the form $v(A)$ for some $A\in\mathrm{Fm}$, so we need to show that
$v(\mathbf{0})\subseteq v(A)$ for any formula $A$. Let $(x,y)\in
v(\mathbf{0})$, that is, $\vdash\ell(x,y)\to\mathbf{0}$. By cut with
$\mathbf{0}\to A$ (which is an instance of $\mathbf{0}L$), we get
$\vdash\ell(x,y)\to A$, therefore $(x,y)\in v(A)$.

Now let us show that $\mathcal{M}^{\mathfrak{A}}_{0}$ is indeed a universal
model, that is, a sequent is true in this model if and only if it is derivable
in $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. The interesting
direction is of course the “only if” one (the “if” direction is just weak
soundness).

Moreover, we may consider only sequents of the form $\Lambda\to B$, since from
$A_{1},\ldots,A_{n}\to B$ one can derive $\Lambda\to
A_{n}\mathop{\backslash}(A_{n-1}\mathop{\backslash}\ldots\mathop{\backslash}(A_{1}\mathop{\backslash}B)\ldots)$,
and vice versa, and by strong soundness these two sequents are true or false
in $\mathcal{M}_{0}^{\mathfrak{A}}$ simultaneously.

Let $\Lambda\to B$ be true in $\mathcal{M}_{0}^{\mathfrak{A}}$, that is,
$\delta\subseteq v(B)$. Take an arbitrary $x\in V$. We have $(x,x)\in v(B)$,
that is, $\vdash\ell(x,x)\to B$. On the other hand, $\ell(x,x)=\mathbf{1}$ by
property 2 of $G$. Applying cut with $\Lambda\to\mathbf{1}$ (axiom), we derive
the desired sequent $\Lambda\to B$.

Existence of a universal model yields weak completeness: if a sequent is true
in all models, then it is true in the universal one, and therefore derivable
in the calculus.

Now we finish our argument by proving Lemma 9. The spirit of this proof is the
same as the central lemma of the proof of Theorem 1 by Andréka and Mikulás.
However, for the step-by-step construction we use the countable schedule
function, as in [KR20], which is sufficient for enumerating formulae, rather
than consider abstract algebras of arbitrary cardinality, as in [AM94]; see
Remark 10 below. The presentation of the proof closely follows the line of
[KR20, Lemma 14]; the figures are adaptations of those by Andréka and Mikulás
[AM94] to the reflexive situation.

######  Proof 3.2 (Proof of Lemma 9).

We construct a growing sequence of labelled graphs
$G_{n}=(V_{n},E_{n},\ell_{n})$, where each $G_{n}$ is an induced subgraph of
$G_{n+1}$. The countable set of vertices $V=\bigcup_{n=0}^{\infty}V_{n}$ is
fixed before the process starts. Our aim is the union graph
$G=\left(\bigcup_{n=0}^{\infty}V_{n},\bigcup_{n=0}^{\infty}E_{n},\bigcup_{n=0}^{\infty}\ell_{n}\right)$.

The desired properties 1–4 are maintained along the sequence, that is, they
will hold for each $G_{n}$. In contrast, properties 5–7 are achieved only in
the limit; each transition from $G_{n}$ to $G_{n+1}$ is a step towards
satisfying one of these properties (in a particular case).

The initial graph $G_{0}$ is just a reflexive point with the required unit
label on the loop:
$G_{0}=(\\{\star\\},\\{(\star,\star)\\},(\star,\star)\mapsto\mathbf{1})$.
Properties 1–4 are trivially satisfied.

Each step is a transition of one of three types: for $t=0,1,2$, a transition
of type $t$ is a step from $G_{3i+t}$ to $G_{3i+t+1}$. In order to ensure that
all necessary transitions are eventually performed, let us define two
bijective schedule functions:

$\displaystyle\sigma\colon\mathbb{N}\to(V\times\mathrm{Fm})\times\mathbb{N}$
$\displaystyle\varsigma\colon\mathbb{N}\to(V\times
V\times\mathrm{Fm}\times\mathrm{Fm})\times\mathbb{N}$

Here $\sigma$ enumerates pairs of a (possible) vertex and a formula, and the
second component (a natural number) ensures that each such pair is “visited”
infinitely many times. The second function, $\varsigma$, does the same for
quadruples including two vertices and two formulae. Now let us define our
transitions.

Transition of type 0, from $G_{3i}$ to $G_{3i+1}$. Let $\sigma(i)=((y,A),k)$.
If $y\notin V_{3i}$, we skip: $G_{3i+1}=G_{3i}$. Otherwise we add a new vertex
$x\in V-V_{3i}$ (such a vertex always exists, since $V$ is countable and
$V_{3i}$ is finite) with a loop edge $(x,x)$, $\ell(x,x)=\mathbf{1}$, and for
each $z\in V_{3i}$, such that $(y,z)\in E_{3i}$, an edge $(x,z)$ with
$\ell(x,z)=A\cdot\ell(y,z)$. (In particular, we add an edge $(x,y)$ with label
$A\cdot\mathbf{1}$.)

Let us show that properties 1–4 keep valid for $G_{3i+1}$. Indeed, the new
vertex $x$ is reflexive, and the loop has the correct label $\mathbf{1}$.
Antisymmetricity is also maintained: the new vertex $x$ has no ingoing edges,
except the loop.

Transitivity and property 4 are checked as follows. We have to verify that for
any $x^{\prime},y^{\prime},z^{\prime}\in V_{3i+1}$ if
$(x^{\prime},y^{\prime})\in E_{3i+1}$ and $(y^{\prime},z^{\prime})\in
E_{3i+1}$, then $(x^{\prime},z^{\prime})\in E_{3i+1}$ and
$\vdash\ell(x^{\prime},z^{\prime})\to\ell(x^{\prime},y^{\prime})\cdot\ell(y^{\prime},z^{\prime})$.
The interesting case is when at least one of these vertices is new (that is,
not from $V_{3i}$). This means $x^{\prime}=x$. If $y^{\prime}=x$, we trivially
get $(x^{\prime},z^{\prime})=(y^{\prime},z^{\prime})\in E_{3i+1}$, and
$\vdash\ell(x^{\prime},z^{\prime})\to\ell(x^{\prime},y^{\prime})\cdot\ell(y^{\prime},z^{\prime})$,
since $\ell(x^{\prime},y^{\prime})=\ell(x,x)=\mathbf{1}$. Now let
$y^{\prime},z^{\prime}$ be old vertices (from $V_{3i}$). Since
$(x,y^{\prime})$ and $(x,z^{\prime})$ were added, edges $(y,y^{\prime})$ and
$(z,z^{\prime})$ are in $E_{3i}$. Let $\ell(y,y^{\prime})=B$,
$\ell(y^{\prime},z^{\prime})=C$, and $\ell(y,z^{\prime})=D$ (the latter edge
exists by transitivity of $G_{3i}$). Then the picture is as follows (new edges
are dashed):

$x$$y$$y^{\prime}$$z^{\prime}$$A\cdot\mathbf{1}$$B$$C$$A\cdot D$$D$$A\cdot
B$$\mathbf{1}$$\mathbf{1}$$\mathbf{1}$$\mathbf{1}$

(Notice that some of the vertices $y$, $y^{\prime}$, $z^{\prime}$ could
coincide; in this case, the corresponding edges are loops with label
$\mathbf{1}$.)

We have indeed added the necessary edge $(x,z^{\prime})$, and it remains to
check that
$\vdash\ell(x,z^{\prime})\to\ell(x,y^{\prime})\cdot\ell(y^{\prime},z^{\prime})$,
that is, $A\cdot D\to(A\cdot B)\cdot C$. By associativity, we may replace
$(A\cdot B)\cdot C$ with $A\cdot(B\cdot C)$, and then $A\cdot D\to
A\cdot(B\cdot C)$ is derived from $D\to B\cdot C$ by applying $\cdot R$ and
$\cdot L$. The sequent $D\to B\cdot C$ is derivable by property 4 of the old
graph $G_{3i}$.

Transition of type 1, from $G_{3i+1}$ to $G_{3i+2}$, is similar. Let
$\sigma(i)=((y,A),k)$. If $y\notin V_{3i}$, we skip, and otherwise add a new
vertex $z$ with its loop and for each $x\in V_{3i}$, if $(x,y)\in E_{3i}$, add
an edge $(x,z)$ with $\ell(x,z)=\ell(x,y)\cdot A$. As for type 0, properties
1–4 keep valid.

Transition of type 2, from $G_{3i+2}$ to $G_{3i+3}$. Let
$\varsigma(i)=((x,z,B,C),k)$. If $x$ or $z$ is not in $V_{3i+2}$ or if
$\not\vdash\ell(x,z)\to B\cdot C$, we skip. We also skip if $x=z$: in this
case, we do not need to add a new vertex to satisfy property 5, see below.
Otherwise, we add a new vertex $y$, with its loop $(y,y)$,
$\ell(y,y)=\mathbf{1}$, and the following edges:

  * •

edge $(r,y)$, with $\ell(r,y)=\ell(r,x)\cdot B$, for each $r$ such that
$(r,x)\in E_{3i+2}$;

  * •

edge $(y,s)$, with $\ell(y,s)=C\cdot\ell(z,s)$, for each $s$ such that
$(z,s)\in E_{3i+2}$.

(In particular, we add edges $(x,y)$ and $(y,z)$ with labels $\mathbf{1}\cdot
B$ and $C\cdot\mathbf{1}$ respectively.) The picture in this situation is as
follows:

$x$$r$$z$$s$$y$$\mathbf{1}\cdot
B$$C\cdot\mathbf{1}$$\ell(r,x)$$\ell(z,s)$$\ell(x,z)$$\ell(r,x)\cdot
B$$C\cdot\ell(z,s)$$\mathbf{1}$$\mathbf{1}$$\mathbf{1}$$\mathbf{1}$$\mathbf{1}$

In this picture, it is possible that $r=x$, or $z=s$, or even both. In such a
case, the corresponding edge is a loop with label $\mathbf{1}$. However,
$x\neq z$ by assumption, and also $r\neq s$ (for any $r$, $s$ in question).
Indeed, if $r=s$, then by transitivity we get $(z,x)\in E_{3i+2}$, which
violates antisymmetry of the old graph $G_{3i+2}$. Also, the new vertex $y$ is
a distinct one.

The $r\neq s$ condition yields antisymmetry of the new graph $G_{3i+3}$.
Indeed, a possible violation of antisymmetry should involve the new vertex
$y$, but then the other vertex should be $r$ and $s$ at the same time.

Reflexivity of the new graph, with $\mathbf{1}$ labels on the loops, is by
construction.

Let us check transitivity and property 4. Take
$x^{\prime},y^{\prime},z^{\prime}$ such that edges $(x^{\prime},y^{\prime})$
and $(y^{\prime},z^{\prime})$ belong to $E_{3i+3}$. The interesting case is
when $x^{\prime}\neq y^{\prime}$ and $y^{\prime}\neq z^{\prime}$ (otherwise we
just add a unit), and at least one of $x^{\prime},y^{\prime},z^{\prime}$ is
the new vertex $y$. Moreover, by antisymmetry, which we have already proved,
we have $x^{\prime}\neq z^{\prime}$.

Consider three cases.

Case 1: $x^{\prime}=y$. Denote $s_{1}=y^{\prime}$ and $s_{2}=z^{\prime}$.
Since $(y,s_{1})\in E_{3i+3}$ and $s_{1}\neq y$, we have $(z,s_{1})\in
E_{3i+2}$ and $\ell(y,s_{1})=C\cdot\ell(z,s_{1})$. (Possibly, $s_{1}=z$.) For
$s_{2}$, since it is also not $y$, we have $(s_{1},s_{2})\in E_{3i+2}$, and by
transitivity of $G_{3i+2}$ we get $(z,s_{2})\in E_{3i+2}$. Therefore,
$(y,s_{2})\in E_{3i+3}$ and $\ell(y,s_{2})=C\cdot\ell(z,s_{2})$. Now by
property 4 of the old graph we have
$\vdash\ell(z,s_{2})\to\ell(z,s_{1})\cdot\ell(s_{1},s_{2})$, and via $\cdot
R$, $\cdot L$, and associativity we obtain $\vdash
C\cdot\ell(z,s_{2})\to(C\cdot\ell(z,s_{1}))\cdot\ell(s_{1},s_{2})$. This is
the necessary sequent $\ell(y,s_{2})\to\ell(y,s_{1})\cdot\ell(y,s_{2})$.

Notice that here antisymmetry is crucial: otherwise, we could have
$z^{\prime}=s_{2}=y$ (i.e., $s_{1}$ plays both as $s$ and $r$), in which case
$\ell(y,s_{2})$ would be $\mathbf{1}$, not $C\cdot\ell(z,s_{2})$.

Case 2: $z^{\prime}=y$. Considered symmetrically.

Case 3: $y^{\prime}=y$. Denote $r=x^{\prime}$ and $s=z^{\prime}$; they are
both distinct from $y$. We have $\ell(r,y)=\ell(r,x)\cdot B$ and
$\ell(y,s)=C\cdot\ell(z,s)$. By shortcutting the path $r$–$x$–$z$–$s$ using
transitivity, we see that $(r,s)$ is an edge of the old graph and
$\vdash\ell(r,s)\to\ell(r,x)\cdot\ell(x,z)\cdot\ell(z,s)$. Now we recall that
$\vdash\ell(x,z)\to B\cdot C$ by assumption and by cut and monotonicity
conclude that $\vdash\ell(r,s)\to\ell(r,x)\cdot B\cdot C\cdot\ell(z,s)$. This
is exactly (up to associativity) what we need:
$\vdash\ell(r,s)\to\ell(r,y)\cdot\ell(y,s)$.

Our construction shows that properties 1–4 hold for each $G_{n}$. Therefore,
they also hold for the limit graph $G$. Also notice that this graph is
infinite, because, e.g., transitions of type 0 are used infinitely often.
Hence, the set of vertices of $G$ is indeed the whole $V$. Thus, it remains to
show that $G$ also enjoys properties 5–7.

Let us start with property 6. The vertex $y\in V$ belongs to $V_{n}$ for some
$n$. Using the bijectivity of $\sigma$, we conclude that there exists such $i$
that $3i\geq n$ and $\sigma(i)=((y,A),k)$ (for some $k$). Therefore, $y\in
V_{3i}$, and at the transition of type 0 from $G_{3i}$ to $G_{3i+1}$ we added
a vertex $x$, the properties of which are exactly the ones required. Property
7 is symmetric, using a transition of type 1.

Finally, let us prove property 5. Let us first consider the case where $x\neq
z$. Again, vertices $x$ and $z$ belong to some $V_{n}$. There exists such $i$
that $\varsigma(i)=((x,z,B,C),k)$ and $3i+2\geq n$. Since we indeed have
$\vdash\ell(x,z)\to B\cdot C$ and $x\neq z$, the corresponding transition of
type 2 is not skipped. This transition introduces $y$ with the desired
properties. Indeed, $\ell(x,y)=\mathbf{1}\cdot A$ and
$\ell(y,z)=B\cdot\mathbf{1}$, which yields $\vdash\ell(x,y)\to B$ and
$\vdash\ell(y,z)\to C$.

Now let $x=z$. Then $\ell(x,z)=\ell(x,x)=\mathbf{1}$, and we have
$\vdash\mathbf{1}\to B\cdot C$. By cut with $\Lambda\to\mathbf{1}$ (axiom), we
get $\vdash\Lambda\to B\cdot C$. Let us eliminate the cut rule in this
proof.222As noticed in Section 1, cut elimination for
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is standard. Below, in
the proof of Theorem 12, we sketch the cut elimination proof for an extension
of $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. The lowermost rule
in the cut-free proof is nothing but $\cdot R$. Therefore, we get
$\vdash\Lambda\to B$ and $\vdash\Lambda\to C$. In its turn, by $\mathbf{1}L$,
this yields $\vdash\mathbf{1}\to B$ and $\vdash\mathbf{1}\to C$, or, in other
words, $\vdash\ell(x,x)\to B$ and $\vdash\ell(x,x)\to C$. Thus, taking $y=x$
satisfies property 5. Notice that this is the only place in the proof where we
cannot allow extra axioms from $\mathcal{H}$ and fail to prove strong
completeness.333This failure is actually even not due to the absence of cut
elimination in the presence of $\mathcal{H}$. Indeed, one could just add
$\mathbf{1}\to b\cdot c$ ($b$ and $c$ are variables) as an axiom, while
$\mathbf{1}\to b$ and $\mathbf{1}\to c$ are not derivable. The extra axiom
$\mathbf{1}\to b\cdot c$ can be reformulated as a good sequent calculus rule,
see Section 4 for more details.

######  Remark 10.

Andréka and Mikulás [AM94] in their proof of Theorem 1 use a more abstract
algebraic framework: labels on graph edges are not formulae but elements of a
residuated semi-lattice (that is, algebraic model for $\mathbf{L}$, see
[GJKO07] for details). In other words, strong completeness appears as a
corollary of a purely algebraic representation theorem. In our case, however,
the representation theorem holds only for the Lindenbaum–Tarski algebra, which
consists of equivalence classes of formulae. Indeed, the representation
theorem for arbitrary algebras would have yielded strong completeness, which
does not hold (see Section 4 below). Thus, it does not matter whether to use
formulae (as we do) or elements of this algebra as labels.

######  Remark 11.

If one takes the reduct of a non-standard square R-model by removing constants
$\mathbf{0}$ and $\mathbf{1}$, the result will be a square R-model in the
usual sense. In particular, this holds for our universal model
$\mathcal{M}_{0}^{\mathfrak{A}}$. Thus, we get Mikulás’ Theorem 1 as a
corollary of our Theorem 8. Labels in our proof are formulae, while Mikulás
used filters, which are sets of formulae. The reason was that without an
explicit unit constant there are incompatible formulae which should be labels
of the same loop (e.g., $p\mathop{\backslash}p$ and $q\mathop{\backslash}q$
for different variables $p$ and $q$). Using the explicit unit resolves this
issue and makes things simpler.

##  4\. Counter-Example to Strong Completeness

Unlike the case with Lambek’s restriction, for
$\mathbf{L}^{\\!\Lambda}{\wedge}$ strong completeness w.r.t. square R-models
does not hold. We prove one result for both $\mathbf{L}^{\\!\Lambda}{\wedge}$
and its extension $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. For
the latter, strong completeness fails w.r.t. the class of non-standard models
defined in Section 2. A series of potential counterexamples to strong
completeness was given by Mikulás [Mik15b]. Here we prove that the first one
of them is indeed such a counterexample.

######  Theorem 12.

Let $a,b,c,d$ be distinct variables. Then $a\mathop{\backslash}a\to b\cdot
c\vDash_{\text{\rm square R-models}}d\to d\cdot b\cdot\bigl{(}(c\cdot
b)\wedge(a\mathop{\backslash}a)\bigr{)}\cdot c$, but not
$a\mathop{\backslash}a\to b\cdot
c\vdash_{\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}}d\to d\cdot
b\cdot\bigl{(}(c\cdot b)\wedge(a\mathop{\backslash}a)\bigr{)}\cdot c$.
Therefore, neither $\mathbf{L}^{\\!\Lambda}{\wedge}$ is not strongly complete
w.r.t. square R-models (since non-derivability in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ implies that in
$\mathbf{L}^{\\!\Lambda}{\wedge}$), nor
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is strongly complete
w.r.t. non-standard square R-models (since the sequent does not include
constants and does not feel non-standardness of models).

######  Proof 4.1.

The first part (semantic entailment) is due to Mikulás [Mik15b, Remark 5.3].
We reproduce it here in order to keep our exposition self-contained. Let us
show that $(y,y)\in v(b\cdot((c\cdot b)\wedge(a\mathop{\backslash}a))\cdot c)$
for any $y\in W$. Then for any $(x,y)\in v(d)$ we shall have $(x,y)\in
v(d\cdot b\cdot((c\cdot b)\wedge(a\mathop{\backslash}a))\cdot c)$.

We have $(y,y)\in v(a\mathop{\backslash}a)$, since $\delta\subseteq
v(a)\mathop{\backslash}v(a)$ for any $v(a)$. Therefore, since
$a\mathop{\backslash}a\to b\cdot c$ is true in $\mathcal{M}$, we get $(y,y)\in
v(b)\circ v(c)$. This means that there exists such $z\in W$ that $(y,z)\in
v(b)$ and $(z,y)\in v(c)$. In its turn, this gives $(z,z)\in v(c\cdot b)$; we
also have $(z,z)\in v(a\mathop{\backslash}a)$, therefore $(z,z)\in v((c\cdot
b)\wedge(a\mathop{\backslash}a))$.

$y$$z$$a\mathop{\backslash}a$$b$$c$$(c\cdot b)\wedge(a\mathop{\backslash}a)$

This yields $(y,y)\in v(b)\circ v((c\cdot
b)\wedge(a\mathop{\backslash}a))\circ v(c)$, q.e.d.

Now let us show that $d\to d\cdot b\cdot\bigl{(}(c\cdot
b)\wedge(a\mathop{\backslash}a)\bigr{)}\cdot c$ is not derivable from
$a\mathop{\backslash}a\to b\cdot c$ in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ We do it in a syntactic
way. Suppose the contrary and let the sequent be derivable from our
hypotheses. In this derivation, let us substitute $\mathbf{1}$ for $a$ and
$d$. This yields derivability of $\mathbf{1}\to\mathbf{1}\cdot
b\cdot\bigl{(}(c\cdot
b)\wedge(\mathbf{1}\mathop{\backslash}\mathbf{1})\bigr{)}\cdot c$ from
$\mathbf{1}\mathop{\backslash}\mathbf{1}\to b\cdot c$.

Next, we notice that $\mathbf{1}\mathop{\backslash}\mathbf{1}\to b\cdot c$ is
derivable from $\Lambda\to b\cdot c$ using $\mathbf{1}L$, $\mathbf{1}R$, and
$\mathop{\backslash}L$. On the other hand, given in
$\mathbf{1}\to\mathbf{1}\cdot b\cdot\bigl{(}(c\cdot
b)\wedge(\mathbf{1}\mathop{\backslash}\mathbf{1})\bigr{)}\cdot c$, we apply
cut with $\Lambda\to\mathbf{1}$ (axiom) and $\mathbf{1}\cdot
b\cdot\bigl{(}(c\cdot
b)\wedge(\mathbf{1}\mathop{\backslash}\mathbf{1})\bigr{)}\cdot c\to
b\cdot\bigl{(}(c\cdot b)\wedge\mathbf{1}\bigr{)}\cdot c$ (derivable in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$). This argument gives
the following: $\Lambda\to b\cdot\bigl{(}(c\cdot
b)\wedge\mathbf{1}\bigr{)}\cdot c$ is derivable in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$, extended with
$\Lambda\to b\cdot c$ as an extra axiom.

Let us introduce an auxiliary calculus
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}bc$, which is
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ extended with the
following inference rule:

$\Gamma,\Delta\to F\Gamma,b,c,\Delta\to F$

(Notice that here $b$ and $c$ are concrete variables, not meta-symbols.)

Adding this new rule to
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}bc$ is equivalent to
adding $\Lambda\to b\cdot c$ as an axiom. Indeed, $\Lambda\to b\cdot c$ can be
derived using the $bc$ rule and the $bc$ rule can be simulated using
$\Lambda\to b\cdot c$ and cut.

The new calculus $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}bc$,
however, enjoys cut elimination. The proof is standard (going back to Lambek’s
original paper [Lam58]) and proceeds by nested induction: (1) on the
complexity of the formula $A$ being cut; (2) on the height of the derivation
tree above the cut.

At each step we consider the lowermost rules in the derivations of the
premises of cut. The only new situation here is when at least one of these
rules is $bc$; other cases are standard.

For $bc$ on the left, we propagate cut as follows:

$\Gamma,\Pi^{\prime},\Pi^{\prime\prime},\Delta\to
B\lx@proof@logical@and\Pi^{\prime},\Pi^{\prime\prime}\to
A\Pi^{\prime},b,c,\Pi^{\prime\prime}\to A\Gamma,A,\Delta\to
B\quad\raisebox{10.00002pt}{$\leadsto$}\quad\Gamma,\Pi^{\prime},\Pi^{\prime\prime},\Delta\to
B\Gamma,\Pi^{\prime},b,c,\Pi^{\prime\prime},\Delta\to
B\lx@proof@logical@and\Pi^{\prime},b,c,\Pi^{\prime\prime}\to
A\Gamma,A,\Delta\to B$

For $bc$ on the right:

$\Gamma^{\prime},\Gamma^{\prime\prime},\Pi,\Delta\to
B\lx@proof@logical@and\Pi\to
A\Gamma^{\prime},\Gamma^{\prime\prime},A,\Delta\to
B\Gamma^{\prime},b,c,\Gamma^{\prime\prime},A,\Delta\to
B\quad\raisebox{10.00002pt}{$\leadsto$}\quad\Gamma^{\prime},\Gamma^{\prime\prime},\Pi,\Delta\to
B\Gamma^{\prime},b,c,\Gamma^{\prime\prime},\Pi,\Delta\to
B\lx@proof@logical@and\Pi\to
A\Gamma^{\prime},b,c,\Gamma^{\prime\prime},A,\Delta\to B$

and similarly in the case when $b,c$ appear in $\Delta$.

Now we may suppose that $\Lambda\to b\cdot\bigl{(}(c\cdot
b)\wedge\mathbf{1}\bigr{)}\cdot c$ has a cut-free proof in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}bc$. Let us track this
proof from the goal sequent to the application of $\wedge R$ which introduces
$(c\cdot b)\wedge\mathbf{1}$. Below this $\wedge R$ there are only two
applications of $\cdot R$ and several ones of $bc$. Therefore, the application
of $\wedge R$ derives $\Pi\to(c\cdot b)\wedge\mathbf{1}$ from $\Pi\to c\cdot
b$ and $\Pi\to\mathbf{1}$, where $\Pi$ is a sequence of $b$’s and $c$’s.

However, $\Pi\to\mathbf{1}$, if $\Pi$ contains no connectives, is derivable
only if $\Pi$ is empty. Thus, we get derivability of $\Lambda\to c\cdot b$.
Let us again track its derivation up to the application of $\cdot R$, which
derives $\Phi,\Psi\to c\cdot b$ from $\Phi\to c$ and $\Psi\to b$. Here the
sequence $\Phi,\Psi$ was obtained by several applications of the $bc$ rule.
Therefore, either $\Phi$ is empty, or the first element of $\Phi$ is $b$. On
the other hand, $\Phi\to c$, where $\Phi$ is a sequence of $b$’s and $c$’s, is
derivable only if $\Phi=c$. Contradiction.

##  5\. An Infinite Conjunction: Iterative Division

Now let us return to our weak completeness result (Section 3). As noted above
(Remark 11), adding an explicit unit constant allowed us to label each edge in
our graphs by just one formula, not a set of formulae.444In the setting of
Mikulaś [Mik15b, Mik15a], this formula generates a principal filter of all
formulae which are “valid” on the edge. Besides making the construction
simpler, this has one more interesting consequence. Namely, we can easily
extend our proof to the case of infinite conjunctions. In contrast, for
Mikulás’ proofs [Mik15a, Mik15b] this is not so easy, since the sets which are
used as labels are filters, and filters are closed only under finite meets.
Possibly, this issue could be overcome by modifying the notion of filter and
making it closed under (specific kinds of) infinite meets, but our approach is
much clearer and simpler.

In order to make our syntax simpler, we shall not consider arbitrary infinite
conjunctions, since this would require development of an infinitary formula
language. We concentrate on one important particular case, in which the
formula language is finitary (while proofs could be infinitary). This
particular case of infinitary conjunction is connected to the Kleene star.

In relational models, the Kleene star is the operation of taking the
reflexive-transitive closure of a relation. Thus, it can be represented as an
infinite union:

$R^{*}=\delta\cup R\cup(R\circ R)\cup(R\circ R\circ R)\cup\ldots$

Adding a union-like connective, however, causes incompleteness issues
connected with distributivity. A concrete corollary of the distributivity law,
using meet and the Kleene star, which is not derivable without distributivity,
is given in [Kuz18, Theorem 4.1].

When put under division, however, the infinite union turns into an infinite
intersection:

$S\mathop{/}R^{*}=S\cap(S\mathop{/}R)\cap((S\mathop{/}R)\mathop{/}R)\cap\ldots,$

and similarly for $R^{*}\mathop{\backslash}S$. Thus, instead of one
unrestricted Kleene star, we consider two composite connectives:
$A^{*}\mathop{\backslash}B$ and $B\mathop{/}A^{*}$. Following Sedlár [Sed20],
who introduced similar connectives in a non-associative setting and with
positive iteration (Kleene plus) instead of Kleene star (due to Lambek’s
restriction), we call these connectives iterative divisions. Independently
from Sedlár, such connectives were introduced in [KR20]. The system considered
there is associative, but still has Lambek’s restriction, so Kleene plus is
used instead of Kleene star. In [KR20] it was proved that the Lambek calculus
$\mathbf{L}$ extended with meet and iterative divisions is strongly complete
w.r.t. the class of all R-models. In this paper, we shall prove a weak
counterpart of that result for the system without Lambek’s restriction.

An infinitary proof system for the Lambek calculus with Kleene star, or
infinitary action logic, was introduced by Buszkowski and Palka [Pal07, BP08].
We present a version of this system for iterative divisions, following [KR20]:

$\Gamma,\Pi_{1},\ldots,\Pi_{n},A^{*}\mathop{\backslash}B,\Delta\to
C\lx@proof@logical@and\Pi_{1}\to A\ldots\Pi_{n}\to A\Gamma,B,\Delta\to
C\qquad\Pi\to A^{*}\mathop{\backslash}B\bigl{(}A^{n},\Pi\to
B\bigr{)}_{n=0}^{\infty}$
$\Gamma,B\mathop{/}A^{*},\Pi_{1},\ldots,\Pi_{n},\Delta\to
C\lx@proof@logical@and\Pi_{1}\to A\ldots\Pi_{n}\to A\Gamma,B,\Delta\to
C\qquad\Pi\to B\mathop{/}A^{*}\bigl{(}\Pi,A^{n}\to B\bigr{)}_{n=0}^{\infty}$

The system obtained by adding these rules to
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ will be denoted by
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}\mathrm{ItD}$. A version
of this system with Lambek’s restriction is undecidable (namely,
$\Pi^{0}_{1}$-complete) [KR20]. For
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}\mathrm{ItD}$, we also
conjecture $\Pi^{0}_{1}$-completeness, thus using infinitary proof machinery
(omega-rules or similar) becomes inevitable.

In square R-models, the Kleene star is interpreted as the reflexive-transitive
closure operation: $v(A^{*})=(v(A))^{*}$. Thus, the interpretation of
iterative divisions is as follows:
$v(A^{*}\mathop{\backslash}B)=(v(A))^{*}\mathop{\backslash}v(B)$ and
$v(B\mathop{/}A^{*})=v(B)\mathop{/}(v(A))^{*}$.

We extend the notion of non-standard square R-model with the unit (Definition
2) with this interpretation for iterative divisions. A routine check provides
strong soundness. Notice that the usage of $\delta$ in the interpretation of
the Kleene star does not conflict with the non-standard unit
$\mathbf{1}_{\mathfrak{A}}$, since they are equivalent in the denominator:
$R\mathop{/}\delta=R=R\mathop{/}\mathbf{1}_{\mathfrak{A}}$ (see the proof of
Lemma 6).

Below we prove weak completeness. The strong one fails by Theorem 12. The
reduct to the language without the unit yields “standard” square R-models with
iterative divisions, thus we get soundness and weak completeness for them
also.

######  Theorem 13.

If a sequent in the language with iterative divisions is true in all non-
standard square R-models, the it is derivable in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}\mathrm{ItD}$.

######  Proof 5.1.

This extension of Theorem 8 is proved in the same way as we do in [KR20] for
the case with Lambek’s restriction. First, in Lemma 9 we replace the set
$\mathrm{Fm}$ of formulae used as labels by the one with iterative divisions.
Thus, we get a new labelled graph $G$ using the same step-by-step construction
(that is, we do not need to re-prove Lemma 9). Next, the only thing we need to
modify in the proof of Theorem 8 is to add one more case, iterative division,
in the check that $\mathcal{M}_{0}^{\mathfrak{A}}$ is a well-defined model.
Everything else remains the same.

Thus, we have to prove that
$v(A^{*}\mathop{\backslash}B)=(v(A))^{*}\mathop{\backslash}v(B)$ and
$v(B\mathop{/}A^{*})=v(B)\mathop{/}(v(A))^{*}$. We shall prove only the
former, since the latter is symmetric. Let us first establish the $\subseteq$
inclusion.

Suppose that $(y,z)\in v(A^{*}\mathop{\backslash}B)$ and take an arbitrary
$x\in W$ such that $(x,y)\in(v(A))^{*}$. Our aim is to show that $(x,z)\in
v(B)$. The statement $(x,y)\in(v(A))^{*}$ means that there exists a number
$n\geq 0$ and a sequence $x_{0},x_{1},\ldots,x_{n}\in W$ such that $x_{0}=x$,
$x_{n}=y$, and $(x_{i-1},x_{i})\in v(A)$ for each $i=1,\ldots,n$. In
particular, if $n=0$, then we have $x=y$. For $n>0$, we iterate property 4 of
$G$ and get $\vdash\ell(x,y)\to A^{n}$ and proceed as follows:

$\ell(x,z)\to
B\lx@proof@logical@and\ell(x,z)\to\ell(x,y)\cdot\ell(y,z)\ell(x,y)\cdot\ell(y,z)\to
B\ell(x,y),\ell(y,z)\to B\lx@proof@logical@and\ell(x,y)\to
A^{n}A^{n},\ell(y,z)\to B\lx@proof@logical@and\ell(y,z)\to
A^{*}\mathop{\backslash}BA^{n},A^{*}\mathop{\backslash}B\to
B\lx@proof@logical@and\overbrace{A\to A\ \ldots}^{\text{$n$ times}}B\to B$

In the case of $n=0$ we have $\ell(x,z)=\ell(y,z)$, and the sequent
$\ell(y,z)\to B$ is derived using cut with $\ell(y,z)\to
A^{*}\mathop{\backslash}B$ and the ${*}{\mathop{\backslash}}L$ rule with
$n=0$.

Now let us establish the $\supseteq$ inclusion. Suppose that
$(y,z)\in(v(A))^{*}\mathop{\backslash}v(B)$. We need to show that $(y,z)\in
v(A^{*}\mathop{\backslash}B)$, that is, $\vdash\ell(y,z)\to
A^{*}\mathop{\backslash}B$. The latter is derived using the omega-rule
${*}{\mathop{\backslash}}R$ from the infinite series of sequents
$\bigl{(}A^{n},\ell(y,z)\to B\bigr{)}_{n=0}^{\infty}$. For $n=0$, take
$\delta\in(v(A))^{*}$ and conclude that $(y,z)\in v(B)$, thus,
$\vdash\ell(y,z)\to B$. For $n>0$, we iterate property 6 of $G$ and construct
a sequence $x_{0},x_{1},\ldots,x_{n}$ such that $x_{0}=y$, $(x_{i+1},x_{i})\in
E$ and $\ell(x_{i+1},t)=A\cdot\ell(x_{i},t)$ for any $t$ such that
$(x_{i},t)\in E$. Having $\ell(x_{0},z)=\ell(y,z)$ and
$\ell(x_{0},y)=\ell(y,y)=\mathbf{1}$, by induction we get
$\ell(x_{n},z)=A^{n}\cdot\ell(y,z)$ and $\ell(x_{n},y)=A^{n}\cdot\mathbf{1}$.

The latter yields $(x_{n},y)\in v(A^{n})=v(A)\circ\ldots\circ
v(A)\subseteq(v(A))^{*}$. Thus, since
$(y,z)\in(v(A))^{*}\mathop{\backslash}v(B)$, we have $(x_{n},z)\in v(B)$, that
is, $\vdash\ell(x_{n},z)\to B$. Now the derivation of $A^{n},\ell(y,z)\to B$
is as follows:

$A^{n},\ell(y,z)\to B\lx@proof@logical@and
A^{n},\ell(y,z)\to\ell(x_{n},z)\lx@proof@logical@and A^{n}\to
A^{n}\ell(y,z)\to\ell(y,z)\ell(x_{n},z)\to B$

##  6\. The Exponential Modality and Strong Conservativity

In the next section, we are going to prove a strong completeness result for
the product-free fragment of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. This fragment will be
denoted by
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$
and, as defined in Section 1, it is obtained from
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ by simply removing rules
for product, $\cdot L$ and $\cdot R$. Another interesting fragment is
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$, which also
lacks axioms and rules for constants: $\mathbf{1}L$, $\mathbf{1}R$,
$\mathbf{0}L$.

However, inside the proofs in Section 7 we are going to use formulae with
multiplication. This makes conservativity an acute question. Otherwise, we
would prove completeness not for
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$,
but for a potentially bigger system in which, despite the set of hypotheses
$\mathcal{H}$ and the goal sequent $\Pi\to B$ are product-free, the
derivations are allowed to use product. So, let us formulate and prove the
strong conservativity statement.

######  Theorem 14.

If $\mathcal{H}$ and $\Pi\to B$ are in the product-free language (i.e.,
constructed using $\mathop{\backslash}$, $\mathop{/}$, $\wedge$, $\mathbf{0}$,
and $\mathbf{1}$) and $\Pi\to B$ syntactically follows from $\mathcal{H}$ in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$, then it also does so in
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$.
Moreover, if $\mathcal{H}$ and $\Pi\to B$ do not include constants
$\mathbf{0}$ and $\mathbf{1}$, then $\Pi\to B$ syntactically follows from
$\mathcal{H}$ in
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$.

Wishing to use cut elimination and the subformula property, we are going to
internalise sequents from $\mathcal{H}$ into the goal sequent using a
modalised version of deduction theorem. (Deduction theorem itself does not
hold for $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ due to the
substructural nature of the calculus.) The modality which will be used for
this purpose is the exponential borrowed from linear logic, see [Gir87,
LMSS92]. The exponential extension of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ will be denoted by
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$.

The new system
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is
obtained from $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ in the
following way. The language of formulae is extended by the exponential as a
unary connective, written in the prefix form: ${!}A$. The set of inference
rules are extended by the following rules for the exponential:

$\Gamma,{!}A,\Delta\to C\Gamma,A,\Delta\to
C\qquad{!}A_{1},\ldots,{!}A_{n}\to{!}B{!}A_{1},\ldots,{!}A_{n}\to
B\qquad\Gamma,{!}A,\Delta\to C\Gamma,\Delta\to C$ $\Gamma,{!}A,\Phi,\Delta\to
C\Gamma,\Phi,{!}A,\Delta\to C\qquad\Gamma,\Phi,{!}A,\Delta\to
C\Gamma,{!}A,\Phi,\Delta\to C\qquad\Gamma,{!}A,\Delta\to
C\Gamma,{!}A,{!}A,\Delta\to C$

Notice that ${!}$ allows all structural rules, namely weakening, permutation,
and contraction. In other words, formulae of the form ${!}A$ behave like
intuitionistic formulae rather than Lambek ones. This will allow reducing
derivability from hypotheses in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ to pure derivability in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$.

The key feature of pure derivability in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is cut
elimination: any sequent derivable in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is
derivable without using $Cut$. The proof of cut elimination is a non-
commutative variant of cut elimination in linear logic. For an accurate
presentation of this proof, see [KKNS19]. Our system
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is a
fragment of the $\mathbf{SMALC}_{\Sigma}$ calculus considered in [KKNS19].

Now let us return to proving Theorem 14. For simplicity, we transform sequents
in $\mathcal{H}$ into sequents with empty antecedents. Indeed, replacing
$A_{1},\ldots,A_{n}\to B$ with $\Lambda\to
A_{n}\mathop{\backslash}\ldots(A_{n-1}\mathop{\backslash}\ldots\mathop{\backslash}(A_{1}\mathop{\backslash}B)\ldots)$
(as we already did in the proof of Theorem 8) in $\mathcal{H}$ does not change
derivability from $\mathcal{H}$. Moreover, this holds for each system
considered, since the rules used here are only $Cut$, $\mathop{\backslash}R$,
and $\mathop{\backslash}L$. Thus, from this points $\mathcal{H}$ consists of
sequents with empty antecedents.

For a finite set of hypotheses $\mathcal{H}^{\prime}=\\{\Lambda\to
A_{1},\ldots,\Lambda\to A_{n}\\}$, let us define the following sequence of
formulae in the language of
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$:

${!}\mathcal{H}^{\prime}=\\{{!}A_{1},\ldots,{!}A_{n}\\}.$

The order of $A_{i}$’s here is arbitrary, since ${!}\mathcal{H}^{\prime}$ will
be used in antecedents where permutation rules are available for
${!}$-formulae.

Let us formulate and prove the version of deduction theorem we need for strong
conservativity. The idea here is not new, and it goes back to [LMSS92,
KKNS19].

######  Lemma 15.

Let $\mathcal{H}$ and $\Pi\to B$ be, resp., a set of sequents (possibly
infinite) and a sequent in the product-free language. Then the following
holds.

  1. (1)

If $\Pi\to B$ syntactically follows from $\mathcal{H}$ in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$, then there exists a
finite $\mathcal{H}^{\prime}\subseteq\mathcal{H}$ such that the following
sequent is derivable in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$:

${!}\mathcal{H}^{\prime},\Pi\to B.$

  2. (2)

If the sequent ${!}\mathcal{H}^{\prime},\Pi\to B$ is derivable in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$, then
$\Pi\to B$ syntactically follows from $\mathcal{H}^{\prime}$ (and, therefore,
from $\mathcal{H}$) in
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$.

  3. (3)

Moreover, if $\mathcal{H}$ and $\Pi\to B$ do not contain constants, then this
holds also for
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$.

######  Proof 6.1.

For (1), we proceed by induction on the derivation of $\Pi\to B$ from
$\mathcal{H}$. For axioms $Id$, $\mathbf{1}R$, and $\mathbf{0}R$, we take
$\mathcal{H}^{\prime}=\varnothing$ and get just the same axiom. For a sequent
of the form $\Lambda\to A$ from $\mathcal{H}$, which can be also used as an
axiom, we take $\mathcal{H}^{\prime}=\\{\Lambda\to A\\}$ and obtain ${!}A\to
A$, which is derivable using ${!}L$. For one-premise rule, we just keep the
same ${!}\mathcal{H}^{\prime}$, possibly moving it using ${!}P_{2}$ (this is
necessary for the $\mathop{\backslash}R$ rule). Finally, for two-premise rules
we have two subsets of $\mathcal{H}$, which we denote by
$\mathcal{H}^{\prime}_{1}$ and $\mathcal{H}^{\prime}_{2}$. The new
$\mathcal{H}^{\prime}$ is their union. We apply the same rule as in the
original derivation, moving the ${!}$-formulae using permutation rules and in
the end contracting duplicated formulae of the form ${!}A$ where
$A\in\mathcal{H}^{\prime}_{1}\cap\mathcal{H}^{\prime}_{2}$ (if any). In
particular, this also happens for $Cut$ (which is a two-premise rule), so the
resulting derivation in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ could
include cuts. However, as noticed above, $Cut$ can be eliminated. Since the
original derivation was finite, $\mathcal{H}^{\prime}$ is also always finite.
Namely, it includes all sequents from $\mathcal{H}$ actually used at least
once.

Statements (2) and (3) are proved by the same argument. Consider a cut-free
derivation of ${!}\mathcal{H}^{\prime},\Pi\to B$ in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. Cut-free
derivations enjoy the subformula property, whence this derivation does not
include rules for product, $\cdot L$ and $\cdot R$. For (3), it also does not
include axioms and rules for constants: $\mathbf{1}L$, $\mathbf{1}R$,
$\mathbf{0}L$. Now let us erase all formulae of the form ${!}A$ from this
derivation. This trivialises all rules for ${!}$, except ${!}L$ (the ${!}R$
rule is never used, since $!$-formulae never appear in antecedents). For
${!}L$, we have $A\in\mathcal{H}^{\prime}$, whence it translates to the
following application of $Cut$:

$\Gamma,\Delta\to C\lx@proof@logical@and\Lambda\to A\Gamma,A,\Delta\to C$

(the instance of ${!}A$ in the conclusion was erased). All other rules are
translated directly to the corresponding rules of
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$
(for (2) or $\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$
(for (3). This gives the desired derivation of $\Pi\to B$ from $\mathcal{H}$.

Notice that this argument does not work for infinitary systems, like our
system with iterated divisions
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}\mathrm{ItD}$. For this
system, we leave strong conservativity an open question, as well as strong
completeness of the product-free fragment (see next section).

######  Remark 16.

In fact, the weakening rule ${!}W$ was never used in the proof of Lemma 15.
Therefore, the full-power exponential modality here may be replaced by the so-
called relevant modality [KKS16], which has the same set of rules as the
exponential, except ${!}W$. Indeed, our $\mathcal{H}^{\prime}$ set collects
exactly those sequents from $\mathcal{H}$ which are really used for deriving
$\Pi\to B$, thus, we are talking about entailment in the sense of relevant
logic rather than, say, intuitionistic one.

Now we are ready to prove strong conservativity.

######  Proof 6.2 (Proof of Theorem 14).

Let $\Pi\to B$ semantically follow from $\mathcal{H}$ in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. Then by statement (1)
of Lemma 15, the sequent ${!}\mathcal{H}^{\prime},\Pi\to B$ is derivable in
$\boldsymbol{!}\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ for some
finite $\mathcal{H}^{\prime}\subseteq\mathcal{H}$. By statement (2), $\Pi\to
B$ is derivable from $\mathcal{H}$ in the smaller system
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$.
In the case where $\mathcal{H}$ and $\Pi\to B$ also do not contain constants
$\mathbf{0}$ and $\mathbf{1}$, we use statement (3) and get derivability of
$\Pi\to B$ from $\mathcal{H}$ in
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$.

##  7\. Strong Completeness without Product

In this section we are going to prove strong completeness results for the
product-free fragments of
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ and
$\mathbf{L}^{\\!\Lambda}{\wedge}$. For the first one, denoted by
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$,
strong completeness will be proved for a modified class of non-standard square
R-models, which we call product-free non-standard square R-models. This class
could look ad hoc and artificial, but using such models will allow proving
strong completeness of
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$ (the
product-free calculus without constants $\mathbf{0}$ and $\mathbf{1}$) w.r.t.
square R-models in the standard sense.

In order to define product-free non-standard square R-models, we first relax
the definition of $\mathfrak{A}$-unit and $\mathfrak{A}$-zero (Definition 2)
by allowing $\mathfrak{A}$ not to be closed under composition. (At the same
time, $\mathfrak{A}$ should still be closed under $\mathop{\backslash}$,
$\mathop{/}$, $\cap$.) The definition of $\mathbf{1}_{\mathfrak{A}}$ and
$\mathbf{0}_{\mathfrak{A}}$ remains the same: $\mathbf{1}_{\mathfrak{A}}\circ
R=R\circ\mathbf{1}_{\mathfrak{A}}=R$ and $\mathbf{0}_{\mathfrak{A}}\subseteq
R$ for any $R\in\mathfrak{A}$. Uniqueness of $\mathbf{1}_{\mathfrak{A}}$ and
$\mathbf{0}_{\mathfrak{A}}$ (if they exist) still holds.

As for properties of $\mathbf{0}_{\mathfrak{A}}$ and
$\mathbf{1}_{\mathfrak{A}}$, the situation is trickier. Lemma 6 still holds,
with the same proof. As for Lemma 5, we prove only one inclusion:

######  Lemma 17.

If $\mathbf{0}_{\mathfrak{A}}$ is the $\mathfrak{A}$-zero, where
$\mathfrak{A}$ is not necessarily closed under composition, then
$\mathbf{0}_{\mathfrak{A}}\circ R\subseteq\mathbf{0}_{\mathfrak{A}}$ and
$R\circ\mathbf{0}_{\mathfrak{A}}\subseteq\mathbf{0}_{\mathfrak{A}}$ for any
$R\in\mathfrak{A}$.

######  Proof 7.1.

Exactly as the corresponding part of the proof of Lemma 5.

######  Corollary 18.

If $\mathbf{0}_{\mathfrak{A}}$ is the $\mathfrak{A}$-zero, where
$\mathfrak{A}$ is not necessarily closed under composition, then
$R_{1}\circ\ldots\circ R_{m}\circ\mathbf{0}_{\mathfrak{A}}\circ
S_{1}\circ\ldots\circ S_{k}\subseteq\mathbf{0}_{\mathfrak{A}}$ for any
$R_{1},\ldots,R_{m},S_{1},\ldots,S_{k}\in\mathfrak{A}$.

######  Proof 7.2.

By Lemma 17, using monotonicity of $\circ$ w.r.t. $\subseteq$.

The definition of our modified models, product-free non-standard square
R-models, is the same as Definition 2, but $\mathfrak{A}$ is not required to
be closed under composition, and the $\mathfrak{A}$-unit and
$\mathfrak{A}$-zero are understood also in this relaxed version of definition.

######  Proposition 19.

The calculus
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$
is strongly sound w.r.t. the class of product-free non-standard square
R-models.

######  Proof 7.3.

Again, we basically repeat the proof of Proposition 7. First we notice that
for any product-free formula $A$ we have $v(A)\in\mathfrak{A}$. (For formulae
with product, this is now, in general, not true.) This allows considering the
cases of $\mathbf{1}R$ and $\mathbf{1}L$ exactly as in the proof of
Proposition 7, using Lemma 6. For $\mathbf{0}L$, we use Corollary 18 and show
that the interpretation $R$ of the antecedent is a subset of
$\mathbf{0}_{\mathfrak{A}}$. Since $C$, the succedent, is cut-free, we have
$R\subseteq\mathbf{0}_{\mathfrak{A}}\subseteq v(C)$.

Notice that the original calculus
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ is, in general, not
sound w.r.t. these models even in the weak sense. For example, Lemma 17 lacks
the other implication,
$\mathbf{0}_{\mathfrak{A}}\subseteq\mathbf{0}_{\mathfrak{A}}\circ R$, which
prevents from validating the sequent $\mathbf{0}\to\mathbf{0}\cdot r$.
Fortunately, this sequent is not a product-free one.

Now we are ready to prove strong completeness for
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$.

######  Theorem 20.

The calculus
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$
is strongly complete w.r.t. the class of product-free non-standard square
R-models.

As mentioned in the previous section, inside our proofs we shall use
multiplication. Due to this reason, the set $\mathrm{Fm}$ still denotes the
set of all $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ formulae. Let
us fix a set $\mathcal{H}$ of product-free sequents and prove a weaker version
of Lemma 9 for derivability from $\mathcal{H}$. Namely, in the presence of a
non-empty set of hypotheses we are unable to maintain property 5 of the graph,
so we just omit it. By $\mathcal{H}\vdash A\to B$ we mean “$A\to B$ is
derivable from $\mathcal{H}$ in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$.”

######  Lemma 21.

There exists a labelled directed graph $G=(V,E,\ell)$ where
$V\neq\varnothing$, $E\subseteq V\times V$, and $\ell\colon E\to\mathrm{Fm}$,
such that the following holds:

  1. (1)

$E$ is transitive;

  2. (2)

$E$ is reflexive and $\ell(x,x)=\mathbf{1}$ for any $x\in V$;

  3. (3)

$E$ is antisymmetric: if $x\neq y$ and $(x,y)\in E$, then $(y,x)\notin E$;

  4. (4)

if $(x,y)\in E$ and $(y,z)\in E$, then
$\mathcal{H}\vdash\ell(x,z)\to\ell(x,y)\cdot\ell(y,z)$;

  5. (5)

for any $y\in V$ and any formula $A$ there exists such $x\in V$ that for any
$z\in V$ if $(y,z)\in E$, then $\ell(x,z)=A\cdot\ell(y,z)$;

  6. (6)

for any $y\in V$ and any formula $A$ there exists such $z\in V$ that for any
$x\in V$ if $(x,y)\in E$, then $\ell(x,z)=\ell(x,y)\cdot A$.

######  Proof 7.4.

We go through the same infinite procedure as in the proof of Lemma 9, but
apply only transitions of types 0 and 1, not of type 2. As transitions of type
2 were necessary exactly for obtaining property 5 of graph $G$, without them
we shall obtain a graph obeying all other properties, w.r.t. derivability from
$\mathcal{H}$ instead of pure derivability.

Now we prove strong completeness for
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$.

######  Proof 7.5 (Proof of Theorem 20).

Given a set of hypotheses $\mathcal{H}$, let us construct an
$\mathcal{H}$-universal product-free non-standard square R-model
$\mathcal{M}_{\mathcal{H}}^{\mathfrak{A}}=(W,\mathfrak{A},\mathbf{1}_{\mathfrak{A}},\mathbf{0}_{\mathfrak{A}},v_{\mathcal{H}})$
in a way similar to how we did it in the proof of Theorem 8, using the graph
$G$ given by Lemma 21.

We take $W=V$ and define $v_{\mathcal{H}}(A)=\\{(x,y)\in
E\mid\mathcal{H}\vdash\ell(x,y)\to A\\}$ where $A$ is a variable or constant
($\mathbf{0}$ or $\mathbf{1}$). Below we shall prove that this equality holds
for any product-free formula $A$. Then we may define
$\mathfrak{A}=\\{v_{\mathcal{H}}(A)\mid\mbox{$A$ is a product-free
formula}\\}$ and assert that $\mathfrak{A}$ is closed under
$\mathop{\backslash}$, $\mathop{/}$, and $\cap$ (but possibly not under
$\circ$). Finally, we shall show that $v_{\mathcal{H}}(\mathbf{1})$ and
$v_{\mathcal{H}}(\mathbf{0})$ are indeed the $\mathfrak{A}$-unit and the
$\mathfrak{A}$-zero, respectively.

The fact that $v_{\mathcal{H}}(A)=\\{(x,y)\mid\mathcal{H}\vdash\ell(x,y)\to
A\\}$ is proved by induction on the structure of $A$ exactly as in the proof
of Theorem 8. Indeed, now we do not need to handle multiplication, so the
omitted property of graph $G$ is not used. As for the differences connected to
$\mathfrak{A}$ (which is now not closed under composition), this proof has
nothing to do with $\mathfrak{A}$, so these differences are irrelevant.
Finally, the shift from pure derivability to derivability from $\mathcal{H}$
does not affect the argument.

Finally, we check that $v_{\mathcal{H}}(\mathbf{1})$ is the
$\mathfrak{A}$-unit and $v_{\mathcal{H}}(\mathbf{0})$ is the
$\mathfrak{A}$-zero. The latter is simpler:
$v_{\mathcal{H}}(\mathbf{0})=\\{(x,y)\mid\mathcal{H}\vdash\ell(x,y)\to\mathbf{0}\\}\subseteq\\{(x,y)\mid\mathcal{H}\vdash\ell(x,y)\to
A\\}=v_{\mathcal{H}}(A)$ for any product-free formula $A$.

For the former, formally we cannot use the argument from the proof of Theorem
8, since it uses $v_{\mathcal{H}}(\mathbf{1}\cdot A)$, and $\mathbf{1}\cdot A$
is not product-free. Let us provide an explicit argument for
$v_{\mathcal{H}}(\mathbf{1})\circ v_{\mathcal{H}}(A)=v_{\mathcal{H}}(A)$ (the
other equality, $v_{\mathcal{H}}(A)\circ
v_{\mathcal{H}}(\mathbf{1})=v_{\mathcal{H}}(A)$, is symmetric). First, we have
$\ell(x,x)=\mathbf{1}$ for any $x$, whence $\delta\subseteq
v_{\mathcal{H}}(\mathbf{1})$. This establishes one inclusion:
$v_{\mathcal{H}}(A)=\delta\circ v_{\mathcal{H}}(A)\subseteq
v_{\mathcal{H}}(\mathbf{1})\circ v_{\mathcal{H}}(A)$. For the opposite
inclusion, let $(x,y)\in v_{\mathcal{H}}(\mathbf{1})\circ v_{\mathcal{H}}(A)$.
This means that, for some $w$, we have $(x,w)\in v_{\mathcal{H}}(\mathbf{1})$
and $(w,y)\in v_{\mathcal{H}}(A)$. Thus, we have
$\mathcal{H}\vdash\ell(x,w)\to\mathbf{1}$, $\mathcal{H}\vdash\ell(w,y)\to A$,
and, by property 4 of graph $G$,
$\mathcal{H}\vdash\ell(x,y)\to\ell(x,w)\cdot\ell(w,y)$. Now we give the
following derivation:

$\ell(x,y)\to
A\lx@proof@logical@and\ell(x,y)\to\ell(x,w)\cdot\ell(w,y)\ell(x,w)\cdot\ell(w,y)\to
A\lx@proof@logical@and\ell(x,w)\cdot\ell(w,y)\to\mathbf{1}\cdot
A\ell(x,w),\ell(w,y)\to\mathbf{1}\cdot
A\lx@proof@logical@and\ell(x,w)\to\mathbf{1}\ell(w,y)\to A\mathbf{1}\cdot A\to
A\mathbf{1},A\to AA\to A$

which establishes $(x,y)\in v_{\mathcal{H}}(A)$.

Now, using our $\mathcal{H}$-universal model
$\mathcal{M}_{\mathcal{H}}^{\mathfrak{A}}$, we show strong completeness.
Again, we restrict ourselves to sequents with empty antecedents, both in
$\mathcal{H}$ and as the goal sequent. Suppose $\mathcal{H}$ semantically
entails a sequent of the form $\Lambda\to B$ on the class of product-free non-
standard square R-models.

Let us show that all sequents from $\mathcal{H}$ are true in
$\mathcal{M}_{\mathcal{H}}^{\mathfrak{A}}$. Take one such sequent, $\Lambda\to
A$. For any $x$, we have $\ell(x,x)=\mathbf{1}$, and
$\mathcal{H}\vdash\mathbf{1}\to A$ by application of $\mathbf{1}L$. This means
$(x,x)\in v_{\mathcal{H}}(A)$ for any $x$, that is, $\delta\subseteq
v_{\mathcal{H}}(A)$.

Now, by semantic entailment, $\Lambda\to B$ is also true in
$\mathcal{M}_{\mathcal{H}}^{\mathfrak{A}}$, that is, $\delta\subseteq
v_{\mathcal{H}}(B)$. This means $\mathcal{H}\vdash\mathbf{1}\to B$ (since $W$
is non-empty, we take an arbitrary $x$ with $(x,x)\in\delta$ and
$\ell(x,x)=\mathbf{1}$), and by cut with $\Lambda\to\mathbf{1}$ we get
$\mathcal{H}\vdash\Lambda\to B$.

The final issue is that derivability here is understood as derivability in
$\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$. Using Theorem 14
(strong conservativity), we transform it into derivability in
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}\mathbf{0}\mathbf{1}$.

Finally, as promised above, as a corollary we obtain strong completeness of
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$ w.r.t.
square R-models, in the most standard sense (Definition 1), cf. Remark 11
above.

######  Theorem 22.

The calculus
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$ is strongly
complete w.r.t. the class of square R-models.

######  Proof 7.6.

Let a sequent $\Lambda\to B$ semantically follow from $\mathcal{H}$ on square
R-models, provided that $\Lambda\to B$ and $\mathcal{H}$ do not include
$\cdot$, $\mathbf{1}$, and $\mathbf{0}$. Then we take the
$\mathcal{H}$-universal model $\mathcal{M}_{\mathcal{H}}^{\mathfrak{A}}$ from
the proof of Theorem 20 and consider its reduct to the language without
constants. This reduct is a standard square R-model which satisfies all
sequents from $\mathcal{H}$. Therefore, it also validated $\Lambda\to B$,
whence $\mathcal{H}\vdash\Lambda\to B$. Using Theorem 14, we transform
derivability in $\mathbf{L}^{\\!\Lambda}{\wedge}\mathbf{0}\mathbf{1}$ into
derivability in
$\mathbf{L}^{\\!\Lambda}_{\mathop{\backslash},\mathop{/}}{\wedge}$.

Along with Theorem 2 by Andréka and Mikulás this shows that $\cdot$ or
$\wedge$ on its own does not leads to failure of strong completeness of
$\mathbf{L}^{\\!\Lambda}{\wedge}$, but together they do.

## Concluding Remarks

The completeness and incompleteness results presented in this article reveal
the following peculiarities of relational semantics for the Lambek calculus
and its extensions. First, Lambek’s non-emptiness restriction indeed matters,
and without it strong completeness surprisingly fails when the system includes
both multiplicative and additive conjunctions (i.e., product and
intersection). Weak completeness still holds. One of the conjunctions is fine
for strong completeness. Second, adding one or both explicit constants
$\mathbf{0}$ and $\mathbf{1}$ ruins completeness even in the weak sense.
Fortunately, there are easy and arguably natural ways of modifying the models
which restore completeness.

The counterexamples to weak completeness with constants are actually very deep
ones. They show that these constants allow building constructions (e.g.,
$\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}A)$, $\mathbf{1}\wedge B$, or
$\mathbf{1}\mathop{/}(C\mathop{/}C)$) which obey structural rules not
available for arbitrary formulae. In particular, formulae of the form
$\mathbf{0}\mathop{/}(\mathbf{0}\mathop{/}A)$ even obey classical Boolean
logic! This suggests that axiomatising the standard interpretations for these
constants is probably a hard problem. Here one would have to somehow hybridise
the Lambek calculus itself and a structurally richer calculus (for comparison,
see [Kuz14] where such attempts were made for constants $\mathbf{0}$ and
$\mathbf{1}$ in the language semantics).

From the point of view of complexity, we see that these constructions using
constants behave much like exponential or subexponential modalities (i.e.,
enable structural rules, including contraction), which would probably make the
complete theories for standard interpretations undecidable, cf. [LMSS92,
CH16]. These undecidability conjectures are supported by the analogous
situation with constant $\mathbf{1}$ in language models where undecidability
was established [KKS22]. Even more interesting things in complexity could
happen if we add some sort of infinitary operations, like Kleene star or
iterated divisions, cf. [KS22]. By now, we leave these questions aside as an
interesting area of further research.

## References

  * [Abr90] V. Michele Abrusci.  A comparison between Lambek syntactic calculus and intuitionistic linear propositional logic.  Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 36:11–15, 1990.  doi:10.1002/malq.19900360103.
  * [AM94] Hajnal Andréka and Szabolcs Mikulás.  Lambek calculus and its relational semantics: completeness and incompleteness.  Journal of Logic, Language, and Information, 3(1):1–37, 1994.  doi:10.1007/BF01066355.
  * [AM11] Hajnal Andréka and Szabolcs Mikulás.  Axiomatizability of positive algebras of binary relations.  Algebra Universalis, 66:7–34, 2011.  doi:10.1007/s00012-011-0142-3.
  * [Ben91] Johan van Benthem.  Language in Action: Categories, Lambdas, and Dynamic Logic.  North Holland, Amsterdam, 1991.
  * [BP08] Wojciech Buszkowski and Ewa Palka.  Infinitary action logic: complexity, models and grammars.  Studia Logica, 89(1):1–18, 2008.  doi:10.1007/s11225-008-9116-7.
  * [Bus06] Wojciech Buszkowski.  On the complexity of the equational theory of relational action algebras.  In R. A. Schmidt, editor, RelMiCS 2006: Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science, pages 106–119. Springer, 2006.  doi:10.1007/11828563_7.
  * [CH16] Karel Chvalovský and Rostislav Horčík.  Full Lambek calculus with contraction is undecidable.  Journal of Symbolic Logic, 81(2):524–540, 2016.
  * [Gir87] Jean-Yves Girard.  Linear logic.  Theoretical Computer Science, 50(1):1–102, 1987.  doi:10.1016/0304-3975(87)90045-4.
  * [GJKO07] Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono.  Residuated Lattices: An Algebraic Glimpse at Substructural Logics, volume 151 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 2007.
  * [Kan92] Makoto Kanazawa.  The Lambek calculus enriched with additional connectives.  Journal of Logic, Language, and Information, 1(2):141–171, 1992\.  doi:10.1007/BF00171695.
  * [KKNS19] Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov.  Subexponentials in non-commutative linear logic.  Mathematical Structures in Computer Science, 29(8):1217–1249, 2019\.  doi:10.1017/S0960129518000117.
  * [KKS16] Max Kanovich, Stepan Kuznetsov, and Andre Scedrov.  Undecidability of the lambek calculus with a relevant modality.  In A. Foret, G. Morrill, R. Muskens, R. Osswald, and S. Pogodalla, editors, FG 2015, FG 2016: Formal Grammar, volume 9804 of Lecture Notes in Computer Science, pages 240–256. Springer, 2016.  doi:10.1007/978-3-662-53042-9_14.
  * [KKS22] Max Kanovich, Stepan Kuznetsov, and Andre Scedrov.  Language models for some extensions of the Lambek calculus.  Information and Computation, 287:104760, 2022.  doi:10.1016/j.ic.2021.104760.
  * [KR20] S. L. Kuznetsov and N. S. Ryzhkova.  A restricted fragment of the Lambek calculus with iteration and intersection operations.  Algebra and Logic, 59(2):190–241, 2020.  doi:10.1007/s10469-020-09586-9.
  * [KS22] Stepan L. Kuznetsov and Stanislav O. Speranski.  Infinitary action logic with exponentiation.  Annals of Pure and Applied Logic, 173:103057, 2022.  doi:10.1016/j.apal.2021.103057.
  * [Kuz14] S. L. Kuznetsov.  Trivalent logics arising from L-models for the Lambek calculus with constants.  Journal of Applied Non-Classical Logics, 24(1–2):132–137, 2014\.  doi:10.1080/11663081.2014.911522.
  * [Kuz18] Stepan Kuznetsov.  *-continuity vs. induction: divide and conquer.  In G. Bezhanishvili, G. D’Agostino, G. Metcalfe, and T. Studer, editors, AiML 2018, volume 12 of Advances in Modal Logic, pages 493–510. College Publications, 2018.
  * [Kuz21] Stepan L. Kuznetsov.  Relational models for the Lambek calculus with intersection and unit.  In U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter, editors, RAMiCS 2021: Relational and Algebraic Methods in Computer Science, volume 13027 of Lecture Notes in Computer Science, pages 258–274. Springer, 2021.  doi:10.1007/978-3-030-88701-8_16.
  * [Lam58] Joachim Lambek.  The mathematics of sentence structure.  American Mathematical Monthly, 65:154–170, 1958.  doi:10.1080/00029890.1958.11989160.
  * [Lam61] Joachim Lambek.  On the calculus of syntactic types.  In R. Jakobson, editor, Structure of Language and Its Mathematical Aspects, pages 166–178. AMS, 1961.
  * [Lam69] Joachim Lambek.  Deductive systems and categories II: standard constructions and closed categories.  In P. Hilton, editor, Category Theory, Homology Theory, and Their Applications I, volume 86 of Lecture Notes in Mathematics, pages 76–122. Springer, 1969.  doi:10.1007/BFb0079385.
  * [LMSS92] Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar.  Decision problems for propositional linear logic.  Annals of Pure and Applied Logic, 56(1–3):239–311, 1992.  doi:10.1016/0168-0072(92)90075-B.
  * [Mik15a] Szabolcs Mikulás.  The equational theories of representable residuated semigroups.  Synthese, 192:2151–2158, 2015.  doi:10.1007/s11229-014-0513-3.
  * [Mik15b] Szabolcs Mikulás.  Lower semilattice-ordered residuated semigroups and substructural logics.  Studia Logica, 103:453–478, 2015.  doi:10.1007/s11225-014-9574-z.
  * [MR12] Richard Moot and Christian Retoré.  The logic of categorial grammars: a deductive account of natural language syntax and semantics, volume 6850 of Lecture Notes in Computer Science.  Springer, 2012.  doi:10.1007/978-3-642-31555-8.
  * [OK85] Hiroakira Ono and Yuichi Komori.  Logics without contraction rule.  Journal of Symbolic Logic, 50(1):169–201, 1985.  doi:10.2307/2273798.
  * [Pal07] Ewa Palka.  An infinitary sequent system for the equational theory of *-continuous action lattices.  Fundamenta Informaticae, 78(2):295–309, 2007.
  * [Pen95] Mati Pentus.  Models for the Lambek calculus.  Annals of Pure and Applied Logic, 75(1–2):179–213, 1995.  doi:10.1016/0168-0072(94)00063-9.
  * [Pen98] Mati Pentus.  Free monoid completeness of the Lambek calculus allowing empty premises.  In J. M. Larrazabal, D. Lascar, and G. Mints, editors, Proceedings of Logic Colloquium ’96, volume 12 of Lecture Notes in Logic, pages 171–209. Springer, 1998.
  * [Sed20] Igor Sedlár.  Iterative division in the distributive full non-associative Lambek calculus.  In L. Soares Barbosa and A. Baltag, editors, DaLí 2019: Dynamic Logic. New Trends and Applications, volume 12005 of Lecture Notes in Computer Science, pages 141–154. Springer, 2020.  doi:10.1007/978-3-030-38808-9_9.