\documentclass[11pt,reqno]{amsart}
\usepackage[utf8]{inputenc}
\usepackage[T2A]{fontenc}
\usepackage[russian,english]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage[colorlinks]{hyperref}


\usepackage{titlesec}
\titlespacing{\section}{0pt}{2.5ex}{1.5ex}
\titlespacing{\subsection}{0pt}{1.5ex}{1ex}
\titlespacing{\subsubsection}{0pt}{1.5ex}{1ex}
\titleformat{\section}{\large\bfseries\centering}{\thesection}{1em}{}
\titleformat{\subsection}[runin]{\bfseries}{\thesubsection.}{0.5em}{}[.\mbox{\ }]
\titleformat{\subsubsection}[runin]{\bfseries}{\thesubsubsection.}{0.4em}{}[.\mbox{\ }]



%%%%%---------- ORCiD
\newcommand\orcidicon[1]{\href{https://orcid.org/#1}{\includegraphics[scale=0.02]{orcid.pdf}}}

\def\udcs{510.6} %Здесь автор определяет УДК своей работы
\def\mscs{03G10} %Здесь автор определяет классификаторы AMS своей работы
\setcounter{page}{144}



\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{prop}[theorem]{Proposition}
\newtheorem{cor}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem*{definition}{Definition}


%%%%%%%%%%%%%%%
% ДОП. ПАКЕТЫ %
%%%%%%%%%%%%%%%
\usepackage{proof,mathrsfs,amssymb,yhmath}
\usepackage{url}

\usepackage{tikz}
\usetikzlibrary{tikzmark,calc,arrows.meta,patterns}

\newcommand{\MALC}{\mathbf{MALC}}
\newcommand{\ACTomega}{\mathbf{ACT}_\omega}
\newcommand{\Hc}{\mathcal{H}}
\newcommand{\Pc}{\mathcal{P}}
\newcommand{\Kc}{\mathcal{K}}
\newcommand{\Mf}{\mathcal{M}}
\newcommand{\Lc}{\mathcal{L}}
\newcommand{\Fm}{\mathrm{Fm}}

\newcommand{\NN}{\mathbb{N}}

\newcommand{\bw}{\bar{w}}

\newcommand{\Cs}{\mathscr{C}}

\newcommand{\Z}{\mathbf{0}}

\newcommand{\BS}{\mathop{\backslash}}
\newcommand{\SL}{\mathop{/}}
\newcommand{\iBS}{\mathop{\backslash\!\backslash}}
\newcommand{\iSL}{\mathop{/\!/}}

\newcommand{\eqv}{\leftrightarrow}

\newcommand{\ID}{\mathrm{Id}}
\newcommand{\CUT}{\mathrm{Cut}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\One}{\mathbf{1}}
\newcommand{\Zero}{\mathbf{0}}

%\newtheorem{lemma}{Лемма}
%\newtheorem{theorem}{Теорема}
%\newtheorem{definition}{Определение}
%\newtheorem{corollary}{Следствие}
%\newtheorem{proposition}{Предложение}


\definecolor{myblue}{rgb}{0.03, 0.27, 0.79}

\hypersetup{linkcolor=blue,filecolor=black,urlcolor=blue, citecolor=blue}

\def\logo{\textcolor{blue}{{\bf\Huge S\raisebox{0.2ex}{\hspace{0.55ex}\raisebox{0.05ex}e\hspace{-1.65ex}$\bigcirc$}MR}}}

\def\semrtop
     {
  \vbox{
     \noindent\logo \hspace{-3mm}  \parbox{12cm}{     \begin{center}
     {\LARGE \textsf{СИБИРСКИЕ ЭЛЕКТРОННЫЕ}} \\[2mm]
     {\LARGE \textsf{МАТЕМАТИЧЕСКИЕ ИЗВЕСТИЯ}} \\[2mm]
     {\Large \textsf{Siberian Electronic Mathematical Reports}} \\[1mm]
     {\Large\tt{\textcolor{blue}{http://semr.math.nsc.ru}}}\\[1mm]
     \raisebox{1ex}{ISSN 1813-3304 }
     \vspace*{-3mm}
%     {\small Институт математики им. С.Л.Соболева СО РАН}\\[-1mm]
%     {\small Sobolev Institute of Mathematics SB RAS}
     \end{center}
}
     \vspace{-1mm}
     \noindent
      \begin{tabular}{c}
     \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa!} \\
     \hline\hline
     \end{tabular}

     \vspace{3mm}
     {\flushleft\it Том ??, № ?, стр. ???--??? (2024) \hspace{\fill}{\rm\small УДК \udcs \hspace{-4mm}}}
     \newline
     	{\rm\small \textcolor{blue}{https://doi.org/10.33048/semi.2024.??.???}}\hphantom{aaaaaaaaaaaaaaaaaaaaaaaa\;}{\rm\small MSC\ \ \mscs }
  }%\vbox
}



\begin{document}
\renewcommand{\refname}{References}


\thispagestyle{empty}

\title[Fragments of Infinitary Action Logic]{Strong Conservativity and Completeness for Fragments of Infinitary Action Logic} 
\author[S.L. Kuznetsov]{{\bf \large \textsc{S.L. Kuznetsov}}\protect\orcidicon{0000-0003-0025-0133}\\ \\
\textit{Communicated by} \textsc{S.V. Sudoplatov}
%\textit{(заполняется редактором)}
}%
\address{Stepan Lvovich Kuznetsov  % Контактные данные всех авторов и место работы указываются только на английском языке
\newline\hphantom{iii} Steklov Mathematical Institute of RAS,
\newline\hphantom{iii} 8 Gubkina St.,
\newline\hphantom{iii} 119991, Moscow, Russia}%
\email{\textcolor{blue}{sk@mi-ras.ru}}%

\thanks{\sc Kuznetsov, S.L.,
Strong conservativity and completeness for fragments of infinitary action logic}
\thanks{\copyright \ 2024 Kuznetsov S.L}
\thanks{\rm This work was supported by the Russian Science Foundation under grant no.~23-11-00104, \url{https://rscf.ru/en/project/23-11-00104/}}
\thanks{\it Received February 15, 2024, Published ??? ????, 2024}%


\semrtop \vspace{1cm}
\maketitle {\small
\begin{quote}
\noindent{\bf Abstract:}  We study fragments of infinitary action logic, the algebraic logic of $*$-continuous residuated Kleene lattices, from the point of view of entailment from (possibly infinite) sets of hypotheses. The contribution of this article is twofold. First, we show, by establishing a cut normalisation result, that elementary fragments obtained by restricting the set of connectives are strongly conservative. This means that conservativity holds not just for pure derivability, but also for derivability from sets of hypotheses.
  This is proved in the presence of iterative divisions---compound connectives of a division and Kleene iteration in the denominator. Second, for the fragment with divisions, intersection, and iterative divisions, we prove strong completeness w.r.t.\ natural classes of models on language algebras and algebras of binary relations.
\medskip

\noindent{\bf Keywords:}  infinitary action logic, conservativity, strong completeness.
 \end{quote}
}

\bigskip


 \section{Introduction}

 \emph{Infinitary action logic} was introduced by Buszkowski and Palka~\cite{BuszkowskiPalka2008,Palka2007} as an axiomatisation of the equational theory of $*$-continuous residuated Kleene lattices, also called \emph{$*$-continuous action lattices.} The definition of action lattice was given in the works of Pratt~\cite{Pratt1991} and Kozen~\cite{Kozen1994act}, by adding Kleene iteration~\cite{Kleene1956} to residuated lattices defined by Krull~\cite{Krull1924} and Ward and Dilworth~\cite{WardDilworth1939}. In the $*$-continuous case, Kleene iteration is defined as the supremum of powers of an element; a more general definition uses the fixpoint construction. In whole, the definition of action lattice is as follows:

 \begin{definition}
  An action lattice (residuated Kleene lattice, RKL) is a partially ordered algebraic structure $\Kc = (\mathbf{K}; \leq, \cdot, \BS, \SL, \wedge, \vee, {}^*, 0, 1)$, where
\begin{enumerate}
\item $(\mathbf{K}; \leq, \wedge, \vee)$ is a lattice;
\item $(\mathbf{K}; \cdot, \vee, 0, 1)$ is a semiring;
\item $\BS$ and $\SL$ are residuals of $\cdot$ w.r.t.\ the $\leq$ partial order:
\[ b \leq a \BS c \iff a \cdot b \leq c \iff a \leq c \SL b;\]
\item $a^* = \max \{ b \mid 1 \leq b, a \cdot b \leq b \}$.
\end{enumerate}
 \end{definition}

 \begin{definition}
 An RKL is $*$-continuous, if $a^* = \sup \{ a^n \mid n \geq  0 \}$ for any $a \in \mathbf{K}$.
 \end{definition}

 The definition of residuated lattice is similar, but without Kleene iteration. The equational theory of residuated lattices is axiomatized by a substructural logical system called the \emph{multiplicative-additive Lambek calculus,} $\MALC$ (see the book by Galatos et al.~\cite{Galatos2007}). Infinitary action logic~$\ACTomega$ extends $\MALC$ with Kleene iteration, axiomatized by means of an omega-rule. The calculus given by Palka~\cite{Palka2007}, in a Gentzen-style sequent format, is presented in the next section.

 Completeness of $\ACTomega$ w.r.t.\ the general algebraic semantics---models on $*$-con\-tinuous action lattices---is proved by the standard Lindenbaum--Tarski construction. Moreover, the completeness result is strong. Namely, for an arbitrary (possibly infinite) set of inequations $\Hc$ and an inequation $A \le B$,  we have the following: $A \le B$ is derivable from $\Hc$ in $\ACTomega$ if and only if the corresponding semantic entailment holds on the class of $*$-continuous action lattices (i.e., any interpretation which validates all inequations from $\Hc$ should also validate $A \le B$).

  Notice that, being an infinitary logic, $\ACTomega$ does not enjoy compactness. The counter-example is readily given by the infinitary definition of Kleene iteration: while the infinite set $\Hc = \{ 1 \le q, p \le q, p^2 \le q, \ldots, p^n \le q, \ldots \}$ entails $p^* \le q$, no finite subset $\Hc_0 \subset \Hc$ does. The lack of compactness makes some of the arguments (see below) more involved. In particular, there is no way of reducing entailment from sets of equations to pure derivability (theoremhood).

 This article consists of two parts, a syntactical and a semantical one, and presents several results about the elementary fragments of $\ACTomega$. These results refine previously known ones and solve some of the open questions in the area.

 First, we address the issue of \emph{strong conservativity} for elementary fragments of $\ACTomega$. An elementary fragment of obtained by restricting the set of connectives and constants. For derivability from hypotheses, however, cut elimination does not hold, so it is not obvious that the connectives removed will not be needed inside the derivations. In order to establish strong conservativity, we prove a {\em cut normalisation} theorem, which is closely related to the {\em free cut elimination} technique (see~\cite{Takeuti1987,BeckmannBuss2011}).\footnote{Cut normalisation is a purely syntactic way towards strong conservativity results. Another, semantic approach (via models on so-called syntactic concept lattices) is sketched in the new paper~\cite{Kuzn2024WoLLIC}, which was written and published after submission of the present article.} Buszkowski~\cite{Buszkowski2007} sketches cut normalisation proof for $\ACTomega$ with hypotheses of a specific form. Before proving strong conservativity results, we extend $\ACTomega$ with extra connectives called {\em iterative divisions.}
 These are composite connectives, expressible in the language of $\ACTomega$: $A \iBS B \eqv A^* \BS B$ and $B \iSL A \eqv B \SL A^*$. We shall consider, however, fragments with iterative divisions, but without Kleene star itself, as they will enjoy completeness properties which fail for $\ACTomega$ in whole (see below). Without Kleene star in the language, iterative divisions become independent connectives.
 Iterative divisions were introduced, in a non-associative setting, by Sedl\'{a}r~\cite{Sedlar2020}, and independently in~\cite{KuznRyzh2020}. In these works, however, they appear in systems without the unit and without empty left-hand sides of sequents, so they are based on positive iteration (Kleene plus) rather than Kleene star. In our setting, we use Kleene star.
 
 Second, we prove two strong completeness results on specialised subclasses of algebraic models for fragments of $\ACTomega$. A general algebraic semantical framework for infinitary action logics is given by models on $*$-continuous action lattices (residuated Kleene lattices), with standard (Lindenbaum--Tarski) completeness arguments.
 Natural concrete examples of $*$-continuous action lattices include lattices of formal languages (over an alphabet~$\Sigma$) and lattices of binary relations (on a given set~$W$). For models on these concrete algebraic structures, however, the full $\ACTomega$ logic fails to be complete: obstacles against completeness are connected with distributivity for meet and join, constants $\Zero$ and $\One$, and others. We consider the elementary fragment of $\ACTomega$ in the language with divisions, iterative divisions, and intersection, denoted by $\ACTomega(\BS,\SL,\wedge,\iBS,\iSL)$, and prove strong completeness of this fragment w.r.t.\ both models on formal languages and on binary relations.

 For the class of all action lattices, not necessarily $*$-continuous, the corresponding algebraic logic is {\em action logic,} denoted by $\mathbf{ACT}$ (this system goes back to Pratt~\cite{Pratt1991} and Kozen~\cite{Kozen1994act}). Since natural classes of action lattices, like lattices of formal languages and lattices of binary relations, are $*$-continuous, there is no hope for $\mathbf{ACT}$ to be complete w.r.t.\ such concrete classes of models, even in the weak sense. (For an example of a sequent derivable in $\ACTomega$, but not in $\mathbf{ACT}$, see~\cite{Kuzn2018AiML}.) As for strong conservativity, $\mathbf{ACT}$ also differs from $\ACTomega$: the fragment of $\mathbf{ACT}$ with the following restricted set of connectives: $\{\BS,\SL,\cdot,{}^*\}$ is not strongly conservative in $\mathbf{ACT}$~\cite{Kuzn2020AiML}.

 
 \section{Sequent Calculus for $\ACTomega$}

 Let us recall Palka's~\cite{Palka2007} formulation of $\ACTomega$ as a Gentzen-style sequent calculus. Our formulation, however, will also include iterative divisions as primary connectives. Namely, formulae are built from variables and constants $\Z$ and $\One$ using the following operations:
 \begin{itemize}
  \item unary: $^*$ (Kleene iteration, written in postfix form: $A^*$);
  \item binary: $\cdot$ (product), $\wedge$ (meet), $\vee$ (join), $\BS$ (left division), $\SL$ (right division),
  $\iBS$ (left iterative division), $\iSL$ (right iterative division).
 \end{itemize}
In the presence of Kleene iteration and divisions, iterative divisions will be expressible by the following equivalences: $A \iBS B \eqv A^* \BS B$ and $B \iSL A \eqv B \SL A^*$. In the  fragments without Kleene iteration iterative divisions become independent operations. Such fragments will be  interesting due to strong completeness results, see Section~\ref{S:completeness} below.

Axioms and inference rules of $\ACTomega$ are as follows:
\[
\infer[\ID]{A \to A}{}
\qquad
\infer[\Zero\rL]{\Gamma, \Zero, \Delta \to C}{}
\qquad
\infer[\One\rL]{\Gamma, \One, \Delta \to C}{\Gamma, \Delta \to C}
\qquad
\infer[\One\rR]{{} \to \One}{}
\]
\[
\infer[{\BS}\rL]{\Gamma, \Pi, A \BS B, \Delta \to C}
{\Pi \to A & \Gamma, B, \Delta \to C}
\qquad
\infer[{\BS}\rR]{\Pi \to A \BS B}{A, \Pi \to B}
\qquad
\infer[{\cdot}\rL]{\Gamma, A \cdot B, \Delta \to C}
{\Gamma, A, B, \Delta \to C}
\]
\[
\infer[{\SL}\rL]{\Gamma, B \SL A, \Pi, \Delta \to C}
{\Pi \to A & \Gamma, B, \Delta \to C}
\qquad
\infer[{\SL}\rR]{\Pi \to B \SL A}{\Pi, A \to B}
\qquad
\infer[{\cdot}\rR]{\Gamma, \Delta \to A \cdot B}
{\Gamma \to A & \Delta \to B}
\]
\[
\infer{\Gamma, A \wedge B, \Delta \to C}
{\Gamma, A, \Delta \to C}
\quad
\infer[{\wedge}\rL]{\Gamma, A \wedge B, \Delta \to C}
{\Gamma, B, \Delta \to C}
\qquad
\infer[{\wedge}\rR]{\Pi \to A \wedge B}
{\Pi \to A & \Pi \to B}
\]
\[
\infer[{\vee}\rL]{\Gamma, A \vee B, \Delta \to C}
{\Gamma, A, \Delta \to C & \Gamma, B, \Delta \to C}
\qquad
\infer{\Pi \to A \vee B}{\Pi \to A}
\quad
\infer[{\vee}\rR]{\Pi \to A \vee B}{\Pi \to B}
\]
\[
\infer[{*}\rL_\omega]{\Gamma, A^*, \Delta \to C}{\bigl( \Gamma, A^n, \Delta \to C \bigr)_{n=0}^{\infty}}
\qquad
\infer[{*}\rR_n]{\Pi_1, \ldots, \Pi_n \to A^*}{\Pi_1 \to A & \ldots & \Pi_n \to A}
\]
\[
\infer[{\iBS}\rL_n]{\Gamma, \Pi_1, \ldots, \Pi_n, A \iBS B, \Delta \to C}
{\Pi_1 \to A & \ldots & \Pi_n \to A & \Gamma, B, \Delta \to C}
\qquad
\infer[{\iBS}\rR_\omega]{\Pi \to A \iBS B}
{\bigl( A^n, \Pi \to B \bigr)_{n=0}^{\infty}}
\]
\[
\infer[{\iSL}\rL_n]{\Gamma, B \iSL A, \Pi_1, \ldots, \Pi_n, \Delta \to C}
{\Pi_1 \to A & \ldots & \Pi_n \to A & \Gamma, B, \Delta \to C}
\qquad
\infer[{\iSL}\rR_\omega]{\Pi \to B \iSL A}
{\bigl( \Pi, A^n \to B \bigr)_{n=0}^{\infty}}
\]
\[
\infer[\CUT]
{\Gamma, \Pi, \Delta \to C}
{\Pi \to A & \Gamma, A, \Delta \to C}
\]

Here ${*}\rR_n$, ${\iBS}\rL_n$, and ${\iSL}\rL_n$ are three series of rules, indexed by $n \ge 0$. The rules ${*}\rL_\omega$, ${\iBS}\rR_\omega$, and ${\iSL}\rL_\omega$ are omega-rules, each of them has infinitely many premises. In the presence of omega-rules, derivations are defined as possibly infinite, but well-founded proof trees. Infinite branching at omega-rules is allowed, but each path going upwards from the goal sequent should terminate (at an axiom or hypothesis) in a finite number of steps.

The original Lambek calculus, as introduced in~\cite{Lambek1958}, has a distinctive feature called {\em Lambek's non-emptiness restriction:} in that version of the calculus, all left-hand sides of sequents are required to be non-empty. This specifically affects the division operations: in the ${\BS}\rR$ and ${\SL}\rR$ rules, $\Pi$ should be forced to be non-empty. Thus, there exist sequents which themselves have a non-empty left-hand side, but still do not have derivations obeying Lambek's restriction: e.g., $(p \BS p) \BS q \to q$. Lambek's restriction is motivated by linguistic applications (see~\cite[Sect.~2.5]{MootRetore}); algebraically it corresponds to considering structures without the unit. Lambek's restriction is obviously incompatible with constant~$\One$, so this constant is not used when Lambek's restriction is imposed. Moreover, the same problem arises with Kleene star: ${*}\rR_0$ is an axiom with an empty left-hand side. Therefore, in the presence of Lambek's restriction Kleene star is replaced by Kleene plus (positive iteration), $a^+ = \sup \{ a^n \mid n \ge 1 \}$, and the same applies to iterative divisions. The right rules for iterative divisions also have $\Pi$ forced to be non-empty.

In general, Lambek's restriction generates a parallel theory of extensions of the Lambek calculus, which shares much with the original framework, but some things there work differently. Throughout this article, we consider systems {\em without} Lambek's non-emptiness restriction. Moreover, the allowance of empty left-hand sides of sequents is crucial for our argument in Section~\ref{S:cut}. However, in some other works which we refer to this restriction is imposed, and we shall make appropriate comments on such references.


\section{Cut Normalisation and Strong Conservativity}\label{S:cut}

For a given set of connectives and constants $\Cs \subseteq \{ \Z, \One, \cdot, \wedge, \vee, \BS, \SL, \iBS, \iSL, {}^* \}$, let $\ACTomega(\Cs)$ denote the elementary fragment of $\ACTomega$ in the language restricted to $\Cs$. Namely, the axioms and rules of $\ACTomega(\Cs)$ are as follows:
\begin{enumerate}
 \item the $\ID$ axiom;
 \item the $\CUT$ rule;
 \item the logical rules operating connectives and constants from $\Cs$.
\end{enumerate}
For such elementary fragments, the following {\em conservativity} issues arise.
\begin{enumerate}
 \item Weak conservativity. Let $\Pi \to B$ be a sequent in the language restricted to $\Cs$. Is it true that if $\Pi \to B$ is derivable in $\ACTomega$, then it is also derivable in $\ACTomega(\Cs)$?
 \item Strong conservativity. Let $\Hc$ and $\Pi \to B$ be, resp., a set of sequents and a sequent in the language restricted to $\Cs$. Is it true that if $\Pi \to B$ is derivable from the set of hypotheses $\Hc$ in $\ACTomega$, then the same holds for $\ACTomega(\Cs)$?
\end{enumerate}

Similar questions may be asked for two fragments of $\ACTomega$ which extend one another: if $\Cs_1 \subset \Cs_2$, is $\ACTomega(\Cs_2)$ conservative over $\ACTomega(\Cs_1)$, in the weak or strong sense?

The first issue is resolved using cut elimination.  Indeed, as shown by Palka~\cite{Palka2007}, any sequent derivable in $\ACTomega$ is derivable without using $\CUT$. (Palka's argument did not cover iterative divisions, but they can be easily handled in the same fashion.) In the cut-free proof, all rules obey the subformula property: any formula in the premises is a subformula of the goal sequent. Therefore, any connective occurring inside the proof also occurs in the final sequent $\Pi \to B$. Since the latter sequent is in the restricted language, the proof is valid in the fragment $\ACTomega(\Cs)$.

For derivability from hypotheses, however, cut elimination does not hold. In order to obtain strong conservativity for finitary fragments (i.e., where $\Cs$ does not include Kleene iteration and iterative divisions), this can be solved~\cite{Kuzn2023LMCS} by extending the calculus with the exponential modality from linear logic, embedding the hypotheses into the goal sequent by means of a modalised deduction theorem, and finally applying cut elimination in the extended system. For this method to work it is important that $\Hc$ is finite. The whole system $\ACTomega$, however, does not enjoy compactness (see Introduction), therefore, infinite sets of hypotheses cannot be reduced to finite ones, and the aforementioned argument does not do the job.

We solve the strong conservativity issue by establishing the following {\em cut normalisation} result. (As noticed in the Introduction, the idea of cut normalisation goes back to the classical  technique of free cut elimination.)

\begin{definition}
 A derivation in $\ACTomega$, from a set of hypotheses of the form ${} \to A$, is called {\em cut-normal,} if for any application of $\CUT$ in this derivation its left premise is a hypothesis:
 \[
 \infer[\CUT]
 {\Gamma, \Delta \to C}
 {\overbrace{{} \to A}^{\in\Hc} & \Gamma, A, \Delta \to C}
 \]
\end{definition}

\begin{theorem}\label{Th:cutnorm}
 Let a sequent $\Pi \to B$ be derivable from a (possibly infinite) set of hypotheses  $\Hc$ in $\ACTomega$, where each hypothesis is of the form ${} \to A$. Then there exists a cut-normal derivation of $\Pi \to B$ from $\Hc$ in $\ACTomega$.
\end{theorem}

We shall proceed by transfinite induction, using the following ordinal parameter, which generalises the derivation case used in the finitary case.

\begin{definition}
 The rank of a derivation is defined as follows:
 \begin{enumerate}
  \item if the derivation consists of only an axiom or a hypotheses, then its rank is~1;
  \item otherwise, one takes the lowermost rule application and computes the rank a the supremum of ranks of premises' derivations, plus 1.
 \end{enumerate}
\end{definition}

The notion of derivation rank is very general, going back to the theory of inductive definitions. It can be shown that if $\Pi \to B$ is derivable from $\Hc$, then there exists a derivation with rank less than~$\omega_1^{\mathrm{CK}}$. (We shall not need this upper bound in our arguments.) See~\cite{KuznSper2022} for details.

Another parameter we shall use is a natural number:
\begin{definition}
The size of a formula, denoted by $|A|$, is the total number of variable, constant, and connective occurrences in $A$.
\end{definition}

Let us start by normalising one cut.

\begin{lemma}\label{Lm:cutnorm}
 Let $\Pi \to A$ and $\Gamma, A, \Delta \to C$ have cut-normal derivations from a set of hypotheses $\Hc$, where each hypotheses is of the form ${}\to B$. Then $\Gamma, \Pi, \Delta \to C$ also has such a derivation.
\end{lemma}

\begin{proof}
 The proof resembles much of the original Palka's argument for cut elimination in $\ACTomega$ (without hypotheses). Thus, we shall give details only for the cases which are essentially new.

 We proceed by induction on lexicographical order on triples $(|A|, \rho_1, \rho_2)$,
 where $\rho_1$ and $\rho_2$ are ranks of the derivations of $\Pi \to A$ and $\Gamma, A, \Delta \to C$ respectively.
 In what follows, we call these sequents {\em cut premises.}

 As usual, we call a logical rule (not $\CUT$) application {\em principal,} if it introduces the cut formula $A$. For this definition, the $\Zero\rL$ and $\One\rR$ axioms are considered as logical rules introducing the corresponding constants.


 Consider several cases:

 {\em Case 1.} At least one of the cut premises was introduced by a non-principal logical rule application. In this case $\CUT$ gets propagated upwards. Now it is applied to the same formula $A$, but one of $\rho_1$, $\rho_2$ became smaller, while the other did not change. We apply the induction hypothesis, and now the goal formula of each new $\CUT$ has a cut-normal derivation. Then the original non-principal rule is applied, yielding a cut-normal derivation of $\Gamma, \Pi, \Delta \to C$.

 For a detailed case analysis, see Palka's proof. The only case not covered there is the case of iterative divisions. In this case, we have the following three possibilities (we consider only $\iBS$, since $\iSL$ is symmetric).

 First, there could be an non-principal application of ${\iBS}\rL_n$ introducing $\Pi \to A$ (an application of ${\iBS}\rR_\omega$ to derive this cut premise is always principal):
 \[
  \infer[\CUT]
  {\Gamma, \Phi, \Pi_1, \ldots, \Pi_n, E \iBS F, \Psi, \Delta \to C}
  {\infer[{\iBS}\rL_n]{\Phi, \Pi_1, \ldots, \Pi_n, E \iBS F, \Psi \to A}
  {\Pi_1 \to E & \ldots & \Pi_n \to E & \Phi, F, \Psi \to A} & \Gamma, A, \Delta \to C}
 \]
This gets rebuilt as follows:
\[
 \infer[{\iBS}\rL]
  {\Gamma, \Phi, \Pi_1, \ldots, \Pi_n, E \iBS F, \Psi, \Delta \to C}
  {\Pi_1 \to E & \ldots & \Pi_n \to E & \infer[\CUT]
  {\Gamma, \Phi, F, \Psi, \Delta \to C}
  {\Phi, F, \Psi \to A & \Gamma, A, \Delta \to C}}
\]
The new $\CUT$ has the same $|A|$ and $\rho_2$, but a smaller $\rho_1$. By induction hypothesis, $\Gamma, \Phi, F, \Psi, \Delta \to C$ has a cut-normal derivation, thus so does the goal sequent.

Second, the second cut premise could be introduced by a non-principal rule application involving ${\iBS}$. The interesting case here is the right rule ${\iBS}\rR_\omega$; the left rule ${\iBS}\rL_n$ is considered exactly as above. Thus, we have the following:
\[
 \infer[\CUT]
 {\Gamma, \Pi, \Delta \to E \iBS F}
 {\Pi \to A & \infer[{\iBS}\rR_\omega]
 {\Gamma, A, \Delta \to E \iBS F}
 {\bigl( E^n, \Gamma, A, \Delta \to F \bigr)_{n=0}^{\infty}}}
\]
For each $n$, we consider the following application of $\CUT$:
\[
 \infer[\CUT]
 {E^n, \Gamma, \Pi, \Delta \to F}
 {\Pi \to A & E^n, \Gamma, A, \Delta \to F}
\]
These new applications have the same $|A|$ and $\rho_1$ parameters; $\rho_2$ got decreased. Thus, each sequent $E^n, \Gamma, \Pi, \Delta \to F$ has a cut-normal derivation, by induction hypothesis. We conclude by applying the omega-rule:
\[
 \infer[{\iBS}\rR_\omega]
 {\Gamma, \Pi, \Delta \to E \iBS F}
 {\bigl( E^n, \Gamma, \Pi, \Delta \to F \bigr)_{n=0}^{\infty}}
\]


 {\em Case 2.} Both cut premises were introduced by principal logical rule applications. Again, we consider only iterative division, for other connectives see Palka's proof.

 We have the following:
 \[
  \infer[\CUT]
  {\Gamma, \Phi_1, \ldots, \Phi_m, \Pi, \Delta \to C}
  {\infer[{\iBS}\rR_\omega]{\Pi \to E \iBS F}{\bigl( E^n, \Pi \to F \bigr)_{n=0}^{\infty}} & \infer[{\iBS}\rL_m]{\Gamma, \Phi_1, \ldots, \Phi_m, E \iBS F, \Delta \to C}{\Phi_1 \to E & \ldots & \Phi_m \to E & \Gamma, F, \Delta \to C}}
 \]
 Out of the premises of ${\iBS}\rR_\omega$ we take the one with $n = m$, and consider the following $\CUT$ applications:
 \[
 \infer[\CUT]
 {\Gamma, \Phi_1, \Phi_2, \ldots, \Phi_m, \Pi, \Delta \to C}
 {\Phi_1 \to E & \infer[\CUT]{\Gamma, E, \Phi_2, \ldots, \Phi_m, \Pi, \Delta \to C}
 {\Phi_2 \to E & \infer{\adots}{\infer[\CUT]{\Gamma, E^m, \Pi, \Delta \to C}{E^m, \Pi \to F  & \Gamma, F, \Delta \to C}}}}
 \]
 Each $\CUT$ has a smaller parameter $|A|$, thus we may gradually apply the induction hypothesis and conclude that each sequent in the derivation fragment above, including the goal one, has a cut-normal derivation.

 {\em Case 3.} One of the cut premises is the $\ID$ axiom. Then $\CUT$ disappears: the other premise coincides with the goal, and it readily has a cut-normal derivation.

 {\em Case 4.} One of the cut premises is a hypothesis. Since all hypotheses have the form ${}\to B$, it is the left cut premise. In this case, since the other premise's derivation is cut-normal, it can be extended, by adding $\CUT$ with this hypothesis, to a cut-normal derivation of the goal sequent.

 {\em Case 5.} The left cut premise is itself  derived using $\CUT$. Since its derivation is cut-normal, one of the premises of this $\CUT$ is a hypothesis. Since each hypothesis is of the form ${} \to B$, this hypothesis should be the left premise. Thus, we have the following:
 \[
 \infer[\CUT]
 {\Gamma, \Pi_1, \Pi_2, \Delta \to C}
 {\infer[\CUT]{\Pi_1, \Pi_2 \to A}{\overbrace{{} \to B}^{\in\Hc} & \Pi_1, B, \Pi_2 \to A} & \Gamma, A, \Delta \to C}
 \]
 Let us reconstruct the derivation:
 \[
 \infer[\CUT]
 {\Gamma, \Pi_1, \Pi_2, \Delta \to C}
 {\overbrace{{} \to B}^{\in\Hc} & \infer[\CUT]
 {\Gamma, \Pi_1, B, \Pi_2, \Delta \to C}
 {\Pi_1, B, \Pi_2 \to A & \Gamma, A, \Delta \to C}}
 \]
 Here the upper $\CUT$ has the same parameters $|A|$ and $\rho_2$ and a smaller $\rho_1$. By induction hypothesis, $\Gamma, \Pi_1, B, \Pi_2, \Delta \to C$ has a cut-normal derivation. Augmenting it with the lower
 $\CUT$, which is itself cut-normal, yields a cut-normal derivation of the goal sequent.

 {\em Case 6.} The right cut premise is derived using $\CUT$, whose left premises is a hypothesis of the form ${} \to B$:
 \[
 \infer[\CUT]
 {\Gamma, \Pi, \Delta_1, \Delta_2 \to C}
 {\Pi \to A & \infer[\CUT]{\Gamma, A, \Delta_1, \Delta_2 \to C}
 {\overbrace{{} \to B}^{\in\Hc} & \Gamma, A, \Delta_1, B, \Delta_2 \to C}}
 \]
 (The case where $B$ occurs to the left of $A$ is considered similarly.) The transformation here is as follows:
 \[
 \infer[\CUT]
 {\Gamma, \Pi, \Delta_1, \Delta_2 \to C}
 {\overbrace{{} \to B}^{\in\Hc} &
 \infer[\CUT]
 {\Gamma, \Pi, \Delta_1, B, \Delta_2 \to C}
 {\Pi \to A & \Gamma, A, \Delta_1, B, \Delta_2 \to C}
 }
 \]
 Here the upper $\CUT$ has a smaller $\rho_2$ with the same $|A|$ and $\rho_1$. By induction hypothesis, $\Gamma, \Pi, \Delta_1, B, \Delta_2 \to C$ has a cut-normal derivation, and adding the lower $\CUT$ yields
 a cut-normal derivation of the goal sequent.
\end{proof}


Notice that it is crucial for the argument above that our hypotheses have a specific form. If hypotheses with non-empty left-hand sides were allowed, the following problematic case could have arisen:
\[
\infer[\CUT]
{\Gamma, \Phi, \Pi, \Psi, \Delta \to C}
{ \infer[\CUT]{\Phi, \Pi, \Psi \to A}{\infer{\Pi \to B}{\text{\small principal}} &  \overbrace{\Phi, B, \Psi \to A}^{\in\Hc}} &
\infer{\Gamma, A, \Delta \to C}{\text{\small principal}}
 }
\]
Here both $\Pi \to B$ and $\Gamma, A, \Delta \to C$ are derived using principal rule applications (introducing, respectively, $B$ and $A$). This prevents from propagating cuts through these premises. The only
transformation we could have applied is swapping cuts, but it does not help, as the cut with the hypothesis keeps on top:
\[
\infer[\CUT]
{\Gamma, \Phi, \Pi, \Psi, \Delta \to C}
{\Pi \to B &
\infer[\CUT]{\Gamma, \Phi, B, \Psi, \Delta \to C}
{ \overbrace{\Phi, B, \Psi \to A}^{\in\Hc} & \Gamma, A, \Delta \to C }}
\]

Now we are ready to prove the main theorem of this section.
\begin{proof}[Proof of Theorem~\ref{Th:cutnorm}]
  Proceed by induction on the rank of the derivation and consider the lowermost rule.  If this rule is $\CUT$, then we may apply the induction hypothesis to its premises (they have derivations of smaller ranks). Therefore, these premises, $\Pi \to A$ and $\Gamma, A, \Delta \to C$, have cut-normal derivations. By Lemma~\ref{Lm:cutnorm}, the goal sequent $\Gamma, \Pi, \Delta \to C$ also has a cut-normal derivation.

  If the lowermost rule is not $\CUT$, then, again, its premises have cut-normal derivations. Combining these derivations and appending the original lowermost rule yields a cut-normal derivation of the goal sequent.
\end{proof}


Finally, let us prove the desired strong conservativity result:
\begin{theorem}\label{Th:conserv}
If $\Cs_1$ and $\Cs_2$ are sets of connectives and constants such that ${\BS} \in \Cs_1 \subseteq \Cs_2$, then $\ACTomega(\Cs_1)$ is a strongly conservative fragment of $\ACTomega(\Cs_2)$ (and, in particular, of
the full system $\ACTomega$). In other words, if a set of sequents $\Hc$ (possibly infinite) and a sequent $\Pi \to C$ are in the language of $\Cs_1$, and $\Pi \to C$ is derivable from $\Hc$ in $\ACTomega(\Cs_2)$, then $\Pi \to B$ is derivable from $\Hc$ already in the smaller system $\ACTomega(\Cs_1)$.
\end{theorem}

\begin{proof}
Let us replace each sequent of the form $A_1, \ldots, A_n \to B$ in $\Hc$ by ${} \to A_n \BS (A_{n-1} \BS \ldots \BS (A_1 \BS B) \ldots)$, and denote the new set of hypotheses by $\Hc'$. (Sequents of the form ${} \to B$
remain unchanged.) If $\Pi \to C$ is derivable from $\Hc$ in $\ACTomega(\Cs_2)$, then the same holds for $\Hc'$. Indeed, ${\BS} \in \Cs_2$, and new hypotheses are derivable from old ones as follows. First one applies ${\BS}\rL$ several times: 
\[
 \infer[{\BS}\rL]{A_1, \ldots, A_n, A_n \BS (A_{n-1} \BS \ldots \BS (A_1 \BS B) \ldots) \to B}{A_n \to A_n & \infer{A_1, \ldots, A_{n-1}, A_{n-1} \BS \ldots \BS (A_1 \BS B) \to B}{\infer{\adots}{\infer[{\BS}\rL]{A_1, A_1 \BS B \to B}{A_1 \to A_1 & B \to B}}}}
\]
Next, by $\CUT$ with the new hypothesis ${} \to A_n \BS (A_{n-1} \BS \ldots \BS (A_1 \BS B) \ldots)$, one obtains the desired old hypothesis $A_1, \ldots, A_n \to B$.

Moreover, since ${\BS} \in \Cs_1$ and all hypotheses from $\Hc$ were in the language of $\Cs_1$, hypotheses from $\Hc'$ also belong to the language of $\Cs_1$.

The new derivation is a derivation in $\ACTomega$ (even in $\ACTomega(\Cs_2)$), where all hypotheses have empty left-hand sides. Thus, Theorem~\ref{Th:cutnorm} is applicable, and we may suppose that the derivation is cut-normal. Now let us take any formula inside this derivation, and track its occurrence down. There are two possibilities: either this formula gets tracked down to the goal sequent $\Pi \to C$, or it gets cut. We claim that in both cases this formula belongs to the language of $\Cs_1$. Indeed, in the first case it is a subformula of $\Pi \to C$, which is in this restricted language. In the second case, since the derivation is cut-normal, our formula is a subformula of $B$, where $({}\to B) \in \Hc'$. Again, any sequent in $\Hc'$ is in the restricted language.

Hence, all connectives and constants in the derivation belong to $\Cs_1$, and we have a valid derivation of $\Pi \to C$ from $\Hc'$ in $\ACTomega(\Cs_1)$. Now we return to the original set of hypotheses $\Hc$: each sequent ${} \to A_n \BS (A_{n-1} \BS \ldots \BS (A_1 \BS B) \ldots)$ can be derived from $A_1, \ldots, A_n \to B$ by ${\BS}\rR$ (recall that ${\BS} \in \Cs_1$).
\end{proof}


The condition ${\BS} \in \Cs_1$ is essentially used in our argument. Symmetrically, it can also be replaced by ${\SL} \in \Cs_1$, but strong conservativity for the case where $\Cs_1$ does not include any of the two
divisions is still an open problem. The interest to this question, however, is limited, since division is the central operation of the Lambek calculus and therefore of $\ACTomega$.


 \section{Strong Relational and Language Completeness}\label{S:completeness}

In this section, we turn from syntax to semantics of $\ACTomega$ and its fragments. Let us first recall the general framework of algebraic semantics. The natural class of algebraic models for $\ACTomega$ are
models on $*$-continuous RKLs.

\begin{definition}
A model on an RKL is a pair $\Mf = (\Kc, w)$, where $\Kc$ is an RKL on a set $\mathbf{K}$ and $w \colon \mathrm{Var} \to \mathbf{K}$ is the valuation function on variables. The valuation function
is propagated to the interpretation function $\bw$ on formulae ($\bw \colon \mathrm{Fm} \to \mathbf{K}$), commuting with all operations and constants:
\begin{align*}
& \bw(p) = w(p)\mbox{ for $p \in \mathrm{Var}$;} \\
& \bw(\Zero) = 0; \\
& \bw(\One) = 1; \\
& \bw(A \odot B) = \bw(A) \odot \bw(B);\mbox{ for $\odot \subseteq \{ \cdot, \wedge, \vee, \BS, \SL \}$}; \\
& \bw(A \iBS B) = (\bw(A)^*) \BS \bw(B); \\
& \bw(B \iSL A) = \bw(B) \SL (\bw(A)^*); \\
& \bw(A^*) = \bw(A)^*.
\end{align*}
A sequent $A_1, \ldots, A_n \to B$ is true in $\Mf$, denoted by $\Mf \vDash A_1, \ldots, A_n \to B$, if $\bw(A_1) \cdot \ldots \cdot \bw(A_n) \leq \bw(B)$, and
$\Mf \vDash {} \to B$ if $1 \leq \bw(B)$.
\end{definition}


\begin{definition}
A sequent $\Pi \to B$ is semantically entailed by a set of sequents $\Hc$ on the class of all $*$-continuous RKLs (notation: $\Hc \vDash \Pi \to B$), if
for any model $\Mf$ on a $*$-continuous RKL if $\Mf \vDash \Gamma \to A$ for any $(\Gamma \to A) \in \Hc$, then $\Mf \vDash \Pi \to B$.
\end{definition}

As mentioned in the Introduction, strong soundness and completeness hold. Strong completeness is proved by the Lindenbaum -- Tarski argument.
\begin{prop}
A sequent is semantically entailed by a set of sequents on the class of all $*$-continuous RKLs if and only if the given sequent is derivable from the
given set of sequents in $\ACTomega$:
\[
\Hc \vDash \Pi \to B \iff \Hc \vdash \Pi \to B.
\]
\end{prop}
For the special case of empty $\Hc$, we obtain weak completeness.


 As noticed in the Introduction, there are two natural classes of models for $\ACTomega$, namely, relational and language models (or R- and L-models for short). These models are algebraic models on specific classes of algebras.

 \begin{definition}
 For a given non-empty set $W$ the corresponding algebra of binary relations is the RKL with $\mathbf{K} = \Pc(W \times W)$ and the operations defined as follows:
 \begin{enumerate}
 \item the lattice structure is set-theoretic: $\wedge$ is intersection, $\vee$ is union, $\leq$ is the subset relation;
 \item product is relational composition: \[R \cdot S = R \circ S = \{ (x,z) \mid \exists y \in W \: (x,y) \in R, (y,z) \in S \};\]
 \item divisions are defined as follows (in the unique way to satisfy the definition):
 \begin{align*}
 & R \BS S = \{ (y,z) \in W \times W \mid \forall x \in W \: ((x,y) \in R \Rightarrow (x,z) \in S) \};\\
 & S \SL R = \{ (x,y) \in W \times W \mid \forall z \in W \: ((y,z) \in R \Rightarrow (x,z) \in S) \};
 \end{align*}
 \item Kleene star is the reflexive-transitive closure.
 \end{enumerate}
 An R-model is a model on an algebra of binary relations.
 \end{definition}

 Accurately speaking, this is the definition of so-called ``square'' R-models; there is also a relativised variant of R-models which is used when Lambek's non-emptiness restriction is imposed.
 In relativised R-models, all relations are required to be subsets of a fixed transitive relation $U \subseteq W \times W$, and this requirement alters the definition of divisions.

 \begin{definition}
 For a given alphabet $\Sigma$ the corresponding algebra of formal languages is the RKL with $\mathbf{K} = \Pc(\Sigma^*)$ and the operations defined as follows:
 \begin{enumerate}
 \item the lattice structure is set-theoretic;
 \item product is pairwise concatenation: \[ M \cdot N = \{ uv \mid u \in M, v \in N \}; \]
 \item divisions are defined in the unique way to satisfy the residuation conditions:
 \begin{align*}
 & M \BS N = \{ v \in \Sigma^* \mid \forall u \in M \: uv \in N \};\\
 & N \SL M = \{ v \in \Sigma^* \mid \forall u \in M \: vu \in N \};
 \end{align*}
 \item Kleene star is defined in the $*$-continuous way:
 \[
 M^* = \{ u_1 \ldots u_n \mid i \geq 0; u_1, \ldots, u_n \in M \}.
 \]
 \end{enumerate}
 \end{definition}

There is also a variant of L-models with Lambek's restriction, which disallow the empty word (use $\Pc(\Sigma^+)$ instead of $\Pc(\Sigma^*)$). Divisions are modified accordingly, and
Kleene star is replaced by Kleene plus.



 Unlike abstract algebraic models, for L- and R-models there are obstacles against completeness of the whole system $\ACTomega$, even in the weak sense.

 First, one of the distributivity laws,
 \[
  (A \vee B) \wedge C \to
  (A \wedge C) \vee (B \wedge C),
 \]
 is not derivable in $\ACTomega$, but is obviously true under set-theoretic interpretation of $\vee$ and $\wedge$. (Non-derivability of this law in substructural logics without contraction was noticed by Ono and Komori~\cite{OnoKomori1985}.)

 There  also  exist corollaries of the distributivity law in narrower languages, which are not derivable in $\ACTomega$. Namely, $\ACTomega(\BS,\SL,\vee)$ is incomplete, even in the weak sense, w.r.t.\ any class of distributive models (in particular, L- or R-models)~\cite{KanKuzSce2022IC}, and the same for $\ACTomega(\BS,\cdot,\wedge,{}^*)$~\cite{Kuzn2018AiML}. Thus, distributivity causes problems with completeness in the presence of disjunction or Kleene star. This motivates replacing Kleene star with iterative divisions.

 Second, constants $\Zero$ and $\One$ also block completeness, even in the weak sense. Namely, the following sequents are true in all L- and R-models, but are not derivable in~$\ACTomega$ (see~\cite{Buszkowski2006,AndrekaMikulas2011,Kuzn2023LMCS} for R-models; for L-models, their validity is checked directly):
 \begin{align*}
 & \Zero \SL (\Zero \SL p), \Zero \SL (\Zero \SL q) \to (\Zero \SL (\Zero \SL q)) \cdot (\Zero \SL (\Zero \SL p));\\
 & \One \wedge p \wedge q \to (\One \wedge p) \cdot (\One \wedge q);\\
 & \One \SL (p \SL p) \to (\One \SL (p \SL p)) \cdot (\One \SL (p \SL p)).
 \end{align*}


Third, there are more sophisticated issues with strong completeness in the presence of product. For R-models, the counter-example is as follows. Take $\Hc = \{ a \BS a \to b \cdot c \}$ and the sequent $d \to d \cdot b \cdot ((c \cdot b) \wedge (a \BS a)) \cdot c$. This sequent is semantically entailed by $\Hc$ on the class of R-models~\cite{Mikulas2015b}, but is not derivable from $\Hc$ in $\MALC$ (and, by strong conservativity, in $\ACTomega$)~\cite{Kuzn2023LMCS}.\footnote{This example may be simplified, taking $\Hc = \{ {} \to b \cdot c \}$ and ${} \to b \cdot ((c \cdot b) \wedge (a \BS a)) \cdot c$. This example works only for systems without Lambek's non-emptiness restriction. The fragment of $\MALC$ in the language of $\{ \BS,\SL,\cdot,\wedge \}$, with Lambek's restriction imposed, is strongly complete w.r.t.\ relativised R-models~\cite{AndrekaMikulas1994}.}

For L-models, we give the following counter-example, based on an idea of Busz\-kow\-ski~\cite{Buszkowski2010}. (Buszkowski showed the failure of strong completeness w.r.t.\ L-models when Lambek's restriction is imposed.)

\begin{prop}
Let $\Hc = \{ p \to p \cdot p \}$. The sequent $(p \BS q) \cdot p \to q \cdot p$ is not derivable from $\Hc$ in $\MALC$ (and therefore in $\ACTomega$), but this sequent is semantically entailed by $\Hc$ on the class of L-models.
\end{prop}

\begin{proof}
Consider an L-model $\Mf = (\Pc(\Sigma^*), w)$. We claim that if $\Mf \vDash p \to p \cdot p$, then either $w(p) = \varnothing$ or $\varepsilon \in w(p)$ (here and further $\varepsilon$ denotes the empty word). Indeed, if neither holds, take the shortest word $u \in w(p)$; let its length be $k$. Since $w(p) \subseteq w(p) \cdot w(p)$, this word should also belong to $w(p) \cdot w(p)$. However, the shortest word in $w(p) \cdot w(p)$ has length $2k$. Since $k > 0$ ($u \ne \varepsilon$), we have $2k > k$. Contradiction.

If $w(p) = \varnothing$, we have $\bw((p \BS q) \cdot p) = \bw(p \BS q) \cdot \varnothing = \varnothing = \bw(q) \cdot \varnothing = \bw(q \cdot p)$. If $\varepsilon \in w(p)$, then $\Mf \vDash {} \to p$, and we apply the following derivation to show that $\Mf \vDash (p \BS q) \cdot p \to q \cdot p$ (using strong soundness):
\[
\infer[{\cdot}\rL]
{(p \BS q) \cdot p \to q \cdot p}
{\infer[{\cdot}\rR]{p \BS q, p \to q \cdot p}
{\infer[{\BS}\rL]{p \BS q \to q}{{} \to p & q \to q} & p \to p}}
\]
Thus, in both cases $\Mf \vDash (p \BS q) \cdot p \to q \cdot p$.

In order to show that $p \to p \cdot p \not\vdash (p \BS q) \cdot p \to q \cdot p$, let us construct an R-model satisfying $p \to p \cdot p$ and falsifying $(p \BS q) \cdot p \to q \cdot p$. Our hypothesis semantically means $w(p) \subseteq w(p) \circ w(p)$, i.e., it holds for any dense relation. Let $W = \mathbb{Q}$ be the set of all rational numbers, and consider the R-model $\Mf = ( \Pc(\mathbb{Q} \times \mathbb{Q}), w)$ defined as follows:
\begin{align*}
& w(p) = \{ (x,y)  \mid x < y \}, \\
& w(q) =
\{ (x,y)  \mid x < 0 \}.
\end{align*}
Here $w(p)$ is the $<$ relation on $\mathbb{Q}$, it is dense, therefore $\Mf \vDash p \to p \cdot p$.

By definition,
\begin{multline*}
\bw(p \BS q) = \{ (y,z) \mid \forall x \: ((x,y) \in w(p) \Rightarrow (x,z) \in w(q)) \} = \\
\{ (y,z) \mid \forall x < y \: (x < 0) \} = \{ (y,z) \mid y \leq 0 \}.
\end{multline*}
Now we have
\begin{align*}
& \bw((p \BS q) \cdot p) = 
\{ (x,z) \mid \exists y \: (x \leq 0 \mbox{ and } y < z) \} = \{ (x,z) \mid x \leq 0 \}; \\
& \bw(q \cdot p) = \{ (x,z) \mid \exists y \: (x < 0 \mbox{ and } y < z) \} = \{ (x,z) \mid x < 0 \}.
\end{align*}
(Here we use the fact that $\exists y (y < z)$ is true on $\mathbb{Q}$ for any $y$.)
Having, for example,
$(0,0) \in \bw((p \BS q) \cdot p)$ and
$(0,0) \notin \bw(q \cdot p)$,
we conclude that $\Mf \not\vDash (p \BS q) \cdot p \to q \cdot p$. By strong soundness,
$p \to p \cdot p \not\vdash (p \BS q) \cdot p \to q \cdot p$.
\end{proof}

The presence of product, however, does not block weak completeness. Namely, as shown by Mikul\'as~\cite{Mikulas2015a,Mikulas2015b}, the fragment of $\MALC$ in the language of $\{ \BS,\SL,\cdot,\wedge \}$ is weakly complete w.r.t.\ R-models; later this result was extended to $\ACTomega(\BS,\SL,\cdot,\wedge,\iBS,\iSL)$  by the author~\cite{Kuzn2023LMCS}.

For L-models, weak completeness in the multiplicative-only Lambek language ($\BS,\SL,\cdot$) was proved by Pentus, both with and without Lambek's restriction~\cite{Pentus1995,Pentus1998}. Weak completeness for the fragment of $\MALC$ in the language of $\{ \BS,\SL,\cdot,\wedge \}$, is
an open problem.

Given the obstacles listed above, we shall now carve out the fragment for which we shall prove strong completeness results (Theorems~\ref{Th:Rcompl} and~\ref{Th:Lcompl} below). This fragment is $\ACTomega(\BS,\SL,\wedge,\iBS,\iSL)$. Our strong completeness results generalise the ones of Andr\'eka and Mikul\'as~\cite{AndrekaMikulas1994} and Buszkowski~\cite{Buszkowski1982}, for R-models and L-models respectively. Namely, strong completeness w.r.t.\ L-models was previously known for the $\{ \BS,\SL, \wedge \}$-fragment; thus, the novel part is adding iterative divisions. For R-models, besides adding iterative divisions, we {\em replace} product with intersection (as having them both makes strong completeness fail).


 \begin{theorem}\label{Th:Rcompl}
  $\ACTomega(\BS,\SL,\wedge,\iBS,\iSL)$ is strongly complete w.r.t.\ R-models.
 \end{theorem}

 The proof follows the original idea of Andr\'{e}ka and Mikul\'{a}s~\cite{AndrekaMikulas1994}: construct a labelled infinite graph of a specific form. In the absence of product, this construction works without Lambek's restriction, yielding strong completeness. A similar idea was used in~\cite{Kuzn2023LMCS} for proving strong completeness in the $\BS,\SL,\wedge$ fragment. However, the construction in~\cite{Kuzn2023LMCS} internally used product, and therefore needed strong conservativity. That is why it was not extended to the infinitary system with iterative divisions. Now (see the previous section) we have strong completeness, but we also provide a proof for Theorem~\ref{Th:Rcompl} which does not need it. The trick is to use sequences of formulae as labels, instead of individual formulae.

 Throughout this section, $\Fm$ denotes the set of formulae in the language of $\BS,\SL,\wedge,\iBS,\iSL$. As usual, $\Fm^*$ denotes the set of sequences of such formulae, including the empty sequence $\Lambda$.

 \begin{lemma}\label{Lm:graph}
  There exists a directed labelled graph $G = (V,E,\Lc)$, where  $V$ is countable, $E \subseteq V \times V$, and $\Lc \colon E \to \Fm^*$ (for brevity, we shall write $\Lc(x,y)$ instead of $\Lc((x,y))$), such that the following holds:
  \begin{enumerate}
   \item $E$ is transitive, and $\Lc(x,z) = \Lc(x,y), \Lc(y,z)$ for $(x,y), (y,z) \in E$;
   \item $E$ is reflexive, and $\Lc(x,y) = \Lambda$ (the empty sequence) for each vertex $x \in V$;
   \item $E$ is antisymmetric (if $(x,y), (y,x) \in E$, then $x=y$);
   \item for each vertex $y \in V$ and each formula $A \in \Fm$ there exists a vertex $x \in V$ such that $(x,y) \in E$, $\Lc(x,y) = A$, and for each $z \in V$ we have $(x,z) \in E$ if and only if $(y,z) \in E$;
   \item for each vertex $y \in V$ and each formula $A \in \Fm$ there exists a vertex $z \in V$ such that $(y,z) \in E$, $\Lc(y,z) = A$, and for each $x \in V$ we have $(x,z) \in E$ if and only if $(x,y) \in E$.
  \end{enumerate}
 \end{lemma}

 \begin{proof}
  Let us fix a countable set of vertices $V$. The graph $G$ will be constructed as the limit of a sequence of graphs $G_n = (V_n, E_n, \Lc_n)$:
  \begin{enumerate}
   \item each $G_n$ is an induced subgraph of $G_{n+1}$;
   \item $G$ is the limit: $V = \bigcup_{n=0}^{\infty} V_n$, $E = \bigcup_{n=0}^{\infty} E_n$, $\Lc = \bigcup_{n=0}^{\infty} \Lc_n$ (a mapping is considered as a set of pairs).
  \end{enumerate}

  Each of the graphs $G_n$ will satisfy properties 1--3; properties 4 and 5 will be achieved in the limit.

  Let the elements of $V$ be enumerated: $V = \{ v_0, v_1, \ldots \}$; let $\star = v_0$.

  The starting graph consists of one vertex: $G_0 = (\{ \star \}, \{(\star,\star)\}, (\star,\star) \mapsto \Lambda)$. Next, the graph is extended by transitions of one of two types: $t = 0,1$. A transition of type $t$ is the step from $G_{2i+t}$ to $G_{2i+t+1}$.

  In order to control the transition, we introduce a bijective {\em schedule function} $\sigma \colon \NN \to (V \times \Fm) \times \NN$. The function ``visits'' pairs $(y,A)$, where $y$ is a (potential) vertex and $A$ is a formula. The third element in the output of $\sigma$ guarantees that each pair is ``visited'' infinitely many times.

  {\em Transition of type~0,} from $G_{2i}$ to $G_{2i+1}$. Let $\sigma(i) = ((y,A),k)$. If $y \notin V_{2i}$, then we skip and let $G_{2i+1} = G_{2i}$. In this case, the pair $(y,A)$ will be visited on a later stage, when $y$ becomes a vertex in some $G_{2j}$.

  Otherwise, we take the minimal $j$ such that $v_j \notin V_{2i}$ and add $x = v_j$ as a new vertex to $G_{2i}$. We also add the following new edges:
  \begin{enumerate}
   \item the loop $(x,x)$ with $\Lc(x,x) = \Lambda$;
   \item for each ``old'' edge $(y,z) \in E_{2i}$ (for the given $y$), the edge $(x,z)$ with $\Lc(x,z) = A, \Lc(y,z)$.
  \end{enumerate}
  (In particular, we add $(x,y)$ with label $A$, since $(y,y) \in E_{2i}$ and $\Lc(y,y) = \Lambda$.)
  Here we have used the same letter $\Lc$ for both $\Lc_{2i}$ and its extension $\Lc_{2i+1}$.

  {\em Transition of type~1,} from $G_{2i+1}$ to $G_{2i+2}$. Similarly, let $\sigma(i) = ((y,A),k)$. If $y \in V_{2i}$, we add the fresh vertex $z = v_j$ with the following edges:
  \begin{enumerate}
   \item the loop $(z,z)$ with $\Lc(z,z) = \Lambda$;
   \item for each ``old'' edge $(x,y) \in E_{2i}$, the edge $(x,z)$ with $\Lc(x,z) = \Lc(x,y), A$.
  \end{enumerate}
If $y \notin V_{2i}$, we skip.

Each transition obviously preserves properties~2 and~3. Let us check property~1 for transition of type~0 (type~1 is symmetric). Let $(x',y'), (y',z') \in E_{2i+1}$. The only interesting case is when $x' = x$ is the new added vertex and $y',z' \in E_{2i}$ are old ones. Then we get the following picture:
\begin{center}
 \begin{tikzpicture}[line width=.7pt]
\begin{scope}[scale=1]
 \node[circle,inner sep=2pt,draw,minimum size=7mm,dashed] (x) at (0,0) {$x$};
 \node[circle,inner sep=2pt,draw,minimum size=7mm] (y) at (1.5,2.5) {$y$};
 \node[circle,inner sep=2pt,draw,minimum size=7mm] (yx) at (4.5,2.5) {$y'$};
 \node[circle,inner sep=2pt,draw,minimum size=7mm] (zx) at (6,0) {$z'$};

 \draw (x) edge[->,dashed] node [midway,above,sloped] {$A$}  (y) ;

 \draw (y) edge[->] node[midway,above] {$\Gamma$} (yx);

 \draw (yx) edge[->] node[midway,above,sloped] {$\Delta$} (zx);

 \draw (x) edge[->,dashed] node[midway,below] {$A, \Gamma, \Delta$} (zx);

 \draw (y) edge[->] node[midway,below,sloped] {$\Gamma,\Delta$} (zx);

 \draw (x) edge[->,dashed] node[midway,below,sloped] {$A, \Gamma$} (yx);

 \draw (x) edge[in=150,out=210,looseness=8,->,dashed] node[midway,left] {$\Lambda$} (x);

 \draw (zx) edge[in=30,out=-30,looseness=8,->] node[midway,right] {$\Lambda$} (zx);

 \draw (y) edge[in=180,out=120,looseness=8,->] node[midway,left] {$\Lambda$} (y);
 \draw (yx) edge[out=60,in=0,looseness=8,->] node[midway,right] {$\Lambda$} (yx);
\end{scope}
\end{tikzpicture}
\end{center}
Here new edges are draw in dashed lines, old are sold ones.
The edge $(x,z')$, which is needed for transitivity, indeed exists and has the correct label $A,\Gamma,\Delta = \Lc(x,y'), \Lc(y',z')$.

The sequence of $V_n$ exhausts the whole set $V$. Indeed, at least each pair of the form $(\star,A)$ yields an infinite sequence of non-trivial transitions.

Now it remains to prove that the limit graph $G$ satisfies properties~4 and~5. Let us check only property~4, as property~5 is symmetric. For each vertex $y \in V_n$ and a formula $A$ there exist such $i$ and $k$ that $\sigma(i) = ((y,A),k)$ and $2i \geq k$. The transition of type~0 from $G_{2i}$ to $G_{2i+1}$ adds a vertex $x$ with the desired properties.
\end{proof}


 Now we prove strong completeness of $\ACTomega(\BS,\SL,\wedge,\iBS,\iSL)$ w.r.t.\ R-models.

 \begin{proof}[Proof of Theorem~\ref{Th:Rcompl}]
  For a given set of hypotheses $\Hc$ we construct the {\em $\Hc$-universal} R-model $\Mf_\Hc = (\Pc(W \times W), w_\Hc)$ using the graph from Lemma~\ref{Lm:graph}.  By $\Hc \vdash \Pi \to A$ we denote the fact that $\Pi \to A$ is derivable from~$\Hc$ in $\ACTomega(\BS,\SL,\wedge,\iBS,\iSL)$. Let $W = V$ and let
  \[
   w_\Hc(p) = \{ (x,y) \in E \mid \Hc \vdash \Lc(x,y) \to p \}
  \]
for each variable $p$. Now let us prove that
\[
 \bw_\Hc(A) = \{ (x,y) \in E \mid \Hc \vdash \Lc(x,y) \to A \}
\]
for each $A \in \Fm$. Proceed by induction on the structure of~$A$.

{\em Divisions.} Let $(y,z) \in \bw_\Hc(A \BS B)$, i.e., $\Hc \vdash \Lc(y,z) \to A \BS B$. Take an arbitrary $(x,y) \in \bw_\Hc(A)$, i.e., such that $\Hc \vdash \Lc(x,y) \to A$. By property~1 we have $(x,z) \in E$ and $\Lc(x,z) = \Lc(x,y),\Lc(y,z)$. The following derivation establishes $\Hc \vdash \Lc(x,y), \Lc(y,z) \to B$.
\[
 \infer[\CUT]
{\Lc(x,y),\Lc(y,z) \to B}
{\Lc(x,y) \to A &
\infer[\CUT]{A, \Lc(y,z) \to B}
{\Lc(y,z) \to A \BS B & \infer[{\BS}\rL]{A, A \BS B \to B}{A \to A & B \to B}}}
\]
Thus, $(x,z) \in \bw_\Hc(B)$, and therefore $(y,z) \in \bw_\Hc(A) \BS \bw_\Hc(B)$.

Now let $(y,z) \in \bw_\Hc(A) \BS \bw_\Hc(B)$. By property~4 of graph $G$, there exists a vertex $x$ such that $\Lc(x,y) = A$ and $(x,z') \in E$ if and only if $(y,z') \in E$. In particular, since $(x,y) \in \bw_{\Hc}(A)$ and $(y,z) \in \bw_\Hc(A) \BS \bw_\Hc(B)$, we get $(x,z) \in \bw_\Hc(B) \subseteq E$. Hence, $(y,z) \in E$, and by property~1 we have $\Lc(x,z) = \Lc(x,y),\Lc(y,z) = A,\Lc(y,z)$. Since $(x,z) \in \bw_\Hc(B)$, we have $\Hc \vdash A, \Lc(y,z) \to B$, and by ${\BS}\rR$ we derive $\Hc \vdash \Lc(y,z) \to A \BS B$. Therefore, $(y,z) \in \bw_{\Hc} (A \BS B)$.

The case of $B \SL A$ is considered similarly.


{\em Iterative divisions.} Let $(y,z) \in \bw_{\Hc}(A \iBS B)$, i.e., $\Hc \vdash \Lc(y,z) \to A \iBS B$. Take an arbitrary $(x,y)$ such that $(x,y) \in (\bw_\Hc(A))^*$. In other words, there exists a chain $x_0, x_1, \ldots, x_n \in V$, such that $n \geq 0$, $x_0 = x$, $x_n = y$, and $(x_{i-1},x_i)$ belongs to $\bw_{\Hc}(A)$ for each $i$ from 1 to $n$. By property~1 of $G$, we have $\Lc(x,z) = \Lc(x_0,x_1), \ldots, \Lc(x_{n-1},x_n), \Lc(y,z)$. Using $\CUT$, we derive $\Lc(x,z) \to B$ from the following sequents: $\Lc(x_{i-1}, x_{i}) \to A$ ($i = 1, \ldots, n$), $\Lc(y,z) \to  A \iBS B$, and $A^n, A \iBS B \to B$. (The latter is derivable by application of ${\iBS}\rL_n$.)  This concludes the proof of $(y,z) \in (\bw_{\Hc}(A))^* \BS \bw_{\Hc}(B)$.

Now let $(y,z) \in (\bw_{\Hc}(A))^* \BS \bw_{\Hc}(B)$. We have to prove $\Hc \vdash \Lc(y,z) \to A \iBS B$. Let us use the omega-rule:
\[
 \infer[{\iBS}\rR_\omega]
 {\Lc(y,z) \to A \iBS B}
 {\bigl( A^n, \Lc(y,z) \to B \bigr)_{n=0}^{\infty}}
\]
Iterating property~4, let us construct a chain of vertices $x_0, x_1, \ldots, x_n$, such that $x_0 = y$, $(x_{i+1},x_i) \in E$, and $\Lc(x_{i+1},x_i) = A$ for each $i$ from 0 to $n-1$. (Here the numeration is inverted.) By property~1, $\Lc(x_n,z) = \Lc(x_n,x_{n+1}), \ldots, \Lc(x_1,x_0), \Lc(y,z) = A^n, \Lc(y,z)$.

On the other hand,  $(x_n,y) \in (\bw_\Hc(A))^*$ and $(y,z) \in  (\bw_{\Hc}(A))^* \BS \bw_{\Hc}(B)$, whence $(x_n,z) \in \bw_{\Hc}(B)$, i.e., $\Hc \vdash \Lc(x_n,z) \to B$. This means exactly that the premises of our omega-rule are derivable from $\Hc$. Therefore, $\Hc \vdash \Lc(y,z) \to A \iBS B$, i.e., $(y,z) \in \bw_{\Hc}(A \iBS B)$.

{\em Intersection.} The sequent $\Lc(x,y) \to A \wedge B$ is derivable from $\Hc$ if and only if so are sequents $\Lc(x,y) \to A$ and $\Lc(x,y) \to B$. This is established via ${\wedge}\rR$ and its inversion using $\CUT$:
\[
 \infer[\CUT]{\Lc(x,y) \to A}
 {\Lc(x,y) \to A \wedge B & \infer[{\wedge}\rL]{A \wedge B \to A}{A \to A}}
\]
This yields the desired equality $\bw_\Hc(A \wedge B) = \bw_\Hc(A) \cap \bw_{\Hc}(B)$.


  \vskip 3pt

  Now let us show that a sequent is true in $\Mf_\Hc$ if and only if it is derivable from $\Hc$. We start with the empty left-hand side case, i.e., a sequent of the form ${} \to B$.  If $\Hc \vdash {} \to B$, we have $(x,x) \in \bw_{\Hc}(B)$ for any $x$, since $\Lc(x,x)$ is the empty sequence. The unit element of the algebra of binary relations is the diagonal relation $\delta = \{ (x,x) \mid x \in W \}$. We have $\delta \subseteq \bw_{\Hc}(B)$, whence $\Mf_{\Hc} \vDash {} \to B$.
  A sequent $A_1, \ldots, A_n \to B$ with a non-empty left-hand side is equiderivable with ${} \to A_n \BS \ldots (A_1 \BS B)$. Thus, we have
  \begin{multline*}
   \Hc \vdash A_1, \ldots, A_n \to B \iff
   \Hc \vdash {} \to A_n \BS \ldots (A_1 \BS B) \iff \\
   \Mf_{\Hc} \vDash {} \to A_n \BS \ldots (A_1 \BS B) \iff
   \Mf_{\Hc} \vDash A_1, \ldots, A_n \to B,
  \end{multline*}
  where the last equivalence is due to strong soundness: $A_1, \ldots, A_n$ is derivable from ${} \to A_n \BS \ldots (A_1 \BS B)$, and therefore semantically entailed.

  Now let a sequent $\Pi \to B$ be semantically entailed by $\Hc$ on the class of all algebras of binary relations. In particular, since $\Mf_{\Hc}$ makes all sequents from $\Hc$ true (as they are derivable from $\Hc$), we have $\Mf_{\Hc} \vDash \Pi \to B$. Therefore, $\Hc \vdash \Pi \to B$, q.e.d.
 \end{proof}


 Completeness w.r.t.\ L-models is easier, and proved by the canonical model construction going back to Buszkowski~\cite{Buszkowski1982}. We adapt the argument from~\cite{KuznRyzh2020} to the system without Lambek's non-emptiness restriction.
 
 \begin{theorem}\label{Th:Lcompl}
$\ACTomega(\BS,\SL,\wedge,\iBS,\iSL)$ is strongly complete w.r.t.\ L-models.
 \end{theorem}

 \begin{proof}
 For a given set of hypotheses $\Hc$ let us construct a universal model. Let $\Sigma = \Fm$ and let us define the interpretation of variables as follows:
 \[
 w_{\Hc}(p) = \{ \Gamma \in \Fm^* \mid \Hc \vdash \Gamma \to p \}.
 \]
 Next, we routinely check that
 \[
 \bw_{\Hc}(A) = \{ \Gamma \in \Fm^* \mid \Hc \vdash \Gamma \to A \}.
 \]
 In particular, we shall always have $A \in \bw_{\Hc}(A)$. Formally, we proceed by induction on the structure of $A$.

 {\em Division.} If $\Gamma \in \bw_{\Hc}(A \BS B)$, then for any $\Delta \in \bw_{\Hc}(A)$ we have both $\Hc \vdash \Gamma \to A \BS B$ and $\Hc \vdash \Delta \to A$, and the following derivation
 establishes the fact that $\Delta\Gamma \in \bw_{\Hc}(B)$:
 \[
 \infer[\CUT]
 {\Delta, \Gamma \to B}
 {\Gamma \to A \BS B & \infer[{\BS}\rL]{\Delta, A \BS B \to B}
 {\Delta \to A & B \to B}}
 \]
 Hence, $\Gamma \in \bw_{\Hc}(A) \BS \bw_{\Hc}(B)$. On the other hand, if $\Gamma \in \bw_{\Hc}(A) \BS \bw_{\Hc}(B)$, take $A \in \bw_{\Hc}(A)$ (by induction hypothesis). We have $A\Gamma \in \bw_{\Hc}(B)$, i.e.,
 $\Hc \vdash A, \Gamma \to B$. By ${\BS}\rR$, we get $\Hc \vdash \Gamma \to A \BS B$, that is, $\Gamma \in \bw_{\Hc}(A \BS B)$. The case of $\SL$ is analogous.

 {\em Intersection.} The sequent $\Gamma \to A \wedge B$ is derivable if and only if so are $\Gamma \to A$ and $\Gamma \to B$. Hence, $\bw_{\Hc}(A \wedge B) = \bw_{\Hc}(A) \cap \bw_{\Hc}(B)$.

 {\em Iterative division.} Let $\Gamma \in \bw_{\Hc}(A \iBS B)$, and let $\Delta_1, \ldots, \Delta_n \in \bw_{\Hc}(A)$---thus, $\Delta = \Delta_1 \ldots \Delta_n$ is an arbitrary element of $\bw_{\Hc}(A)^*$. The following derivation yields $\Delta\Gamma \in \bw_{\Hc}(B)$:
 \[
 \infer[\CUT]
 {\Delta_1, \ldots, \Delta_n, \Gamma \to B}
 {\Gamma \to A \iBS B & \infer[{\iBS}\rL_n]{\Delta_1, \ldots, \Delta_n, A \iBS B \to B}
 {\Delta_1 \to A & \ldots & \Delta_n \to A & B \to B}}
 \]
 In particular, $n$ could be zero. In this case we take the empty sequence as an element of $\bw_{\Hc}(A)^*$, and $\Delta\Gamma = \Gamma \in \bw_{\Hc}(B)$:
 \[
 \infer[\CUT]
 {\Gamma \to B}
 {\Gamma \to A \iBS B & \infer[{\iBS}\rL_0]{A \iBS B \to B}{B \to B}}
 \]
 We have proved that $\Gamma \in \bw_{\Hc}(A)^* \iBS \bw_{\Hc}(B)$. Now let us prove the other inclusion. Take an arbitrary $n \ge 0$ and $A^n \in \bw_{\Hc}(A)^*$. We have $\Hc \vdash A^n, \Gamma \to B$ for each $n$, and by application of ${\iBS}\rR_\omega$ we get $\Hc \vdash \Gamma \to A \iBS B$. Hence, $\Gamma \in \bw_{\Hc}(A \iBS B)$. The case of $\iSL$ is analogous.

 We claim that the L-model $\Mf_{\Hc} = (\Pc(\Fm^*), w)$ constructed above validates exactly the sequents derivable from $\Hc$. Let $\Hc \vdash A_1, \ldots, A_n \to B$. Take $\Delta_1 \in \bw_{\Hc}(A_1)$, \ldots $\Delta_n \in \bw_{\Hc}(A_n)$. By definition, $\Hc \vdash \Delta_i \to A_i$ for each $i$. Applying $\CUT$, we get $\Hc \vdash \Delta_1, \ldots, \Delta_n \to B$, whence $\Delta = \Delta_1 \ldots \Delta_n \in \bw_{\Hc}(B)$. Therefore, $\bw_{\Hc}(A_1) \cdot \ldots \cdot \bw_{\Hc}(A_n) \subseteq \bw_{\Hc}(B)$. In the other direction: if $\bw_{\Hc}(A_1) \cdot \ldots \cdot \bw_{\Hc}(A_n) \subseteq \bw_{\Hc}(B)$, take
 $A_1 \in \bw_{\Hc}(A_1)$, \ldots, $A_n \in \bw_{\Hc}(A_n)$. We have $A_1 \ldots A_n \in \bw_{\Hc}(B)$, whence $\Hc \vdash A_1, \ldots, A_n \to B$.

 In particular, each sequent from $\Hc$ is true in $\Mf_{\Hc}$, and if $\Pi \to B$ semantically follows from $\Hc$, then it is true in $\Mf_{\Hc}$. The latter means $\Hc \vdash \Pi \to B$, q.e.d.
 \end{proof}

Theorem~\ref{Th:Lcompl} provides strong completeness w.r.t.\ L-models over infinite alphabets ($\Sigma = \Fm$). However, this can be reduced to finite alphabets, moreover, to a two-letter alphabet $\Sigma_2 = \{ b,c \}$. (For a one-letter alphabet, commutativity becomes valid, which blocks completeness even in the weak sense.) The reduction is due to Pentus~\cite{Pentus1998}: each letter $a_j$ from a countable alphabet $\Sigma = \{ a_1, a_2, \ldots \}$ is replaced by $g(a_j) = bc^jb$. This homomorphism $g$ commutes with $\bw$, provided that $\bw(A) \ne \varnothing$ for each $A \in \Fm$~\cite[Th.~11.2]{Pentus1998}. For the model constructed above, this is indeed the case, as we always have $A \in \bw(A)$.

Due to strong conservativity (Theorem~\ref{Th:conserv}), both strong completeness results (Theorems~\ref{Th:Rcompl} and~\ref{Th:Lcompl}) get inherited by elementary fragments, provided their language includes division: 
\begin{cor}
If $\BS \in \Cs \subseteq \{\BS,\SL,\wedge,\iBS,\iSL\}$, then $\ACTomega(\Cs)$ is strongly complete w.r.t.\ L-models and w.r.t.\ R-models.
\end{cor}

We conclude with formulating an open question for future work. Is the fragment  $\ACTomega(\BS,\SL,\cdot,\iBS,\iSL)$ strongly complete w.r.t.\ R-models? On one hand, here we do not have simultaneously $\wedge$ and $\cdot$, so the aforementioned counter-example does not work. However, iterative divisions may be considered as special kinds of infinite intersections, so they could give rise to similar issues.

 
\bigskip

 \begin{thebibliography}{111}

 \bibitem{AndrekaMikulas1994} H. Andr\'eka, Sz. Mikul\'as, \href{https://doi.org/10.1007/BF01066355}{\it Lambek calculus and its relational semantics: completeness and incompleteness}, J. Logic Lang. Inform. {\bf 3}:1 (1994), 1--37. 

\bibitem{AndrekaMikulas2011} H. Andr\'eka, Sz. Mikul\'as, \href{https://doi.org/10.1007/s00012-011-0142-3}{\it Axiomatizability of positive algebras of binary relations}, Algebra Universalis, {\bf 66}:1--2 (2011), 7--34. 

\bibitem{BeckmannBuss2011} A. Beckmann, S. Buss, \href{https://doi.org/10.1016/j.tcs.2011.05.053}{\it Corrected upper bounds for free-cut elimination}, Theor. Comput. Sci., {\bf 412}:39 (2011), 5433--5445. 

\bibitem{Buszkowski1982} W. Buszkowski, \href{https://doi.org/10.1002/malq.19820281407}{\it Compatibility of a categorial grammar with an associated category system}, Z. math. Logik Grundl. Math., {\bf 28} (1982), 229--237.

\bibitem{Buszkowski2006} W. Buszkowski, \href{https://doi.org/10.1007/11828563_7}{\it On the complexity of the equational theory of relational action algebras}, in: R. A. Schmidt (ed.), {\it RelMiCS 2006: Relations and Kleene Algebra in Computer Science,} Lect. Notes Comput. Sci., {\bf 4136}, Springer, 2006, 106--119. 

\bibitem{Buszkowski2007} W. Buszkowski, \href{https://doi.org/10.1093/logcom/exl036}{\it On action logic: equational theories of action algebras}, J. Logic Comput., {\bf 17}:1 (2007), 199--217.

 \bibitem{BuszkowskiPalka2008} W. Buszkowski, E. Palka, \href{https://doi.org/10.1007/s11225-008-9116-7}{\it Infinitary action logic: complexity, models and grammars}, Studia Logica, {\bf 89}:1 (2008), 1--18.

 \bibitem{Buszkowski2010}
 W. Buszkowski, \href{http://buszko.home.amu.edu.pl/LCaSLpr.pdf}{\it Lambek calculus and substructural logics}, Linguist. Analysis {\bf 36}:1--4 (2010), 15--48.

\bibitem{Galatos2007} N. Galatos, P. Jipsen, T. Kowalski, H. Ono, \href{https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/151/}{\it Residuated lattices: an algebraic
glimpse at substructural logics}, vol.~151 of Studies in Logic and Foundations of Mathematics, Elsevier, 2007.

\bibitem{KanKuzSce2022IC}
 M. Kanovich, S. Kuznetsov, A. Scedrov, \href{https://doi.org/10.1016/j.ic.2021.104760}{\it Language models for some extensions of the Lambek calculus}, Inform. and Comput., {\bf 287} (2022), 104760. 

\bibitem{Kleene1956} S. C. Kleene, \href{https://doi.org/10.1515/9781400882618-002}{\it Representation of events in nerve nets and finite automata}, in: C. Shannon, J. McCarthy (eds.), {\it Automata Studies}, Princeton University Press, 1956, 3--41.

\bibitem{Kozen1994act} D. Kozen, \href{https://doi.org/10.7551/mitpress/4286.003.0007}{\it On action algebras,} in: J. van Eijck, A. Visser (eds.), {\it Logic and Information Flow,} MIT Press, 1994, 78--88.

\bibitem{Krull1924} W. Krull, \href{https://www.zobodat.at/pdf/Sitzber-physik-med-Soc-Erlangen_56-57_0047-0063.pdf}{\it Axiomatische Begründung der allgemeinen Idealtheorie}, Sitzber. Phys.-Med. Soc. Erlangen, {\bf 56} (1924), 47--63. 

\bibitem{Kuzn2018AiML} S. Kuznetsov, \href{http://www.aiml.net/volumes/volume12/Kuznetsov.pdf}{\it $*$-continuity vs.\ induction: divide and conquer}, in: G. Bezhanishvili et al. (eds.), Advances in Modal Logic, {\bf 12}, College Publications, London, 2018, 493--510.

\bibitem{Kuzn2020AiML} S. Kuznetsov, \href{http://www.aiml.net/volumes/volume13/Kuznetsov.pdf}{\it The `long rule' in the Lambek calculus with iteration: undecidability without meets and joins,} in: N. Olivetti et al. (eds.), Advances in Modal Logic, {\bf 13}, College Publications, London, 2020, 425--440.

\bibitem{KuznRyzh2020} S. L. Kuznetsov, N. S. Ryzhkova, \href{https://doi.org/10.1007/s10469-020-09586-9}{\it A restricted fragment of the Lambek calculus with iteration and intersection operations}, Algebra and Logic, {\bf 59}:2 (2020), 129--146. 

\bibitem{KuznSper2022} S. L. Kuznetsov, S. O. Speranski, \href{https://doi.org/10.1016/j.apal.2021.103057}{\it Infinitary action logic with exponentiation}, Ann. Pure Appl. Logic, {\bf 173}:2 (2022), 103057.

\bibitem{Kuzn2023LMCS} S. L. Kuznetsov, \href{https://doi.org/10.46298/lmcs-19(4:32)2023}{\it Relational models for the Lambek calculus with intersection and constants}, Log. Methods Comput. Sci., {\bf 19}:4 (2023), 32:1--32:27. 

\bibitem{Kuzn2024WoLLIC} S. L. Kuznetsov,
\href{https://doi.org/10.1007/978-3-031-62687-6_7}{\it Syntactic concept lattice models for infinitary action logic,} in: G. Metcalfe et al. (eds.), {\it Logic, Language, Information, and Computation. WoLLIC 2024,} Lect. Notes Comput. Sci., {\bf 14672}, Springer, 2024, 93--107.

\bibitem{Lambek1958}
J. Lambek, \href{https://doi.org/10.1080/00029890.1958.11989160}{\it The mathematics of sentence structure}, Amer. Math. Monthly, {\bf 65}:3 (1958), 154--170.

\bibitem{Mikulas2015a}
Sz. Mikul\'as, \href{https://doi.org/10.1007/s11229-014-0513-3}{\it The equational theories of representable residuated semigroups}, Synthese, {\bf 192}:7 (2015), 2151--2158. 

\bibitem{Mikulas2015b}
Sz. Mikul\'as, \href{https://doi.org/10.1007/s11225-014-9574-z}{\it Lower semilattice-ordered residuated semigroups and substructural logic}, Studia Logica, {\bf 103}:3 (2015), 453--478. 

\bibitem{MootRetore}
R. Moot, C. Retor\'e, \href{https://doi.org/10.1007/978-3-642-31555-8}{\it The logic of categorial grammars. A deductive account of natural language syntax and semantics}, vol.~6850 of Lect. Notes Comput. Sci., Springer, 2012.

\bibitem{OnoKomori1985} H. Ono, Y. Komori,
\href{https://doi.org/10.2307/2273798}
{\it Logics without the contraction rule},
J. Symb. Logic, {\bf 50}:1 (1985), 169--201.

 \bibitem{Palka2007} E. Palka, \href{https://content.iospress.com/articles/fundamenta-informaticae/fi78-2-06}{\it An infinitary sequent system for the equational theory of $*$-continuous action lattices}, Fundam. Inform., {\bf 78}:2 (2007), 295--309.

 \bibitem{Pentus1995} M. Pentus,
 \href{https://doi.org/10.1016/0168-0072(94)00063-9}
 {\it Models for the Lambek calculus}, Ann. Pure Appl. Logic, {\bf 75}:1--2 (1995), 179--213.

 \bibitem{Pentus1998} M. Pentus, \href{https://doi.org/10.1017/9781316716816.008}{\it Free monoid completeness of the Lambek calculus allowing empty premises}, in: M. Larrazabal et al. (eds.), {\it Proc. Logic Colloquium '96,} Lect. Notes Logic, {\bf 12}, Cambridge University Press, 1998, 171--209.

 \bibitem{Pratt1991} V. Pratt, \href{https://doi.org/10.1007/BFb0018436}{\it Action logic and pure induction}, in: J. van Eijck (ed.), {\it JELIA 1990: Logics in AI,} Lect. Notes Artif. Intell., {\bf 478}, Springer, 1991, 97--120. 

 \bibitem{Sedlar2020} I. Sedl\'{a}r, \href{https://doi.org/10.1007/978-3-030-38808-9_9}{\it Iterative division in the distributive full non-associative Lambek calculus}, in: L.~Soares Barbosa, A. Baltag (eds.), {\it Dynamic Logic. New Trends and Applications. DaL\'{\i} 2019,} Lect. Notes Comput. Sci.,
 {\bf 12005}, Springer, 2020, 141--154.

  \bibitem{Takeuti1987} G. Takeuti, {\it Proof theory,} 2nd ed., North-Holland, Amsterdam, 1987.

 \bibitem{WardDilworth1939} M. Ward, R. P. Dilworth, \href{https://www.ams.org/journals/tran/1939-045-03/S0002-9947-1939-1501995-3/}{\it Residuated lattices}, Trans. Amer. Math. Soc., {\bf 45} (1939), 335--354.
 \end{thebibliography}


\end{document}
