# Semi-Substructural Logics with Additives

Niccolò Veltri Cheng-Syuan Wan Tallinn University of Technology, Estonia
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

This work concerns the proof theory of (left) skew monoidal categories and
their variants (e.g. closed monoidal, symmetric monoidal), continuing the line
of work initiated in recent years by Uustalu et al. Skew monoidal categories
are a weak version of Mac Lane’s monoidal categories, where the structural
laws are not required to be invertible, they are merely natural
transformations with a specific orientation. Sequent calculi which can be
modelled in such categories can be identified as deductive systems for
restricted substructural fragments of intuitionistic linear logic. These
calculi enjoy cut elimination and admit a focusing strategy, sharing
resemblance with Andreoli’s normalization technique for linear logic. The
focusing procedure is useful for solving the coherence problem of the
considered categories with skew structure.

Here we investigate possible extensions of the sequent calculi of Uustalu et
al. with additive connectives. As a first step, we extend the sequent calculus
with additive conjunction and disjunction, corresponding to studying the proof
theory of skew monoidal categories with binary products and coproducts
satisfying a left-distributivity condition. We introduce a new focused sequent
calculus of derivations in normal form, which employs tag annotations to
reduce non-deterministic choices in bottom-up proof search. The focused
sequent calculus and the proof of its correctness have been formalized in the
Agda proof assistant. We also discuss extensions of the logic with additive
units, a form of skew exchange and linear implication.

##  1 Introduction

Substructural logics are logical systems in which the usage of one or more
structural rules is disallowed or restricted. A well-known example is the
syntactic calculus of Lambek [14], in which all the structural rules of
exchange, weakening and contraction are disallowed. Variants of the Lambek
calculus allow exchange or a cyclic form of exchange, while others disallow
even associativity [17]. In Girard’s linear logic, which has been studied both
in the presence and absence of an exchange rule [10, 2], selective versions of
weakening and contraction can be recovered via the use of modalities.
Applications of substructural logics are abundant in a variety of different
fields, from computational investigations of natural languages to the design
of resource-sensitive programming languages.

In recent years, in collaboration with Tarmo Uustalu and Noam Zeilberger, we
initiated a program intended to study a family of _semi-substructural_ logics,
inspired by developments in category theory by Szlachányi, Street, Bourke,
Lack and many others [20, 12, 19, 13, 8, 5, 6, 7]. Kornél Szlachányi
introduced _skew monoidal categories_ as a weakening of MacLane’s monoidal
categories in which the structural morphisms of associativity and unitality
(often also called associator and unitors) are not required to be invertible,
they are just natural transformation in a particular direction. As such, they
can be regarded as _semi-associative_ and _semi-unital_ variants of monoidal
categories. Bourke and Lack also introduced notions of braiding and symmetry
for skew monoidal categories which involve three objects instead of two [7].
Skew monoidal categories arise naturally in semantics of programming languages
[3] and semi-associativity has strong connections with combinatorial
structures such as the Tamari lattice and Stasheff associahedra [27, 16].

Semi-substructural logics correspond to the internal languages of skew
monoidal categories and their extensions, therefore sitting in between
(certain fragments of) non-associative and associative intuitionistic linear
logic. Semi-associativity and semi-unitality can be hard-coded in the sequent
calculus following a two-step recipe. First, consider sequents of the form
$S\mid\Gamma\vdash A$, where the antecedent is split into an optional formula
$S$, called stoup, and an ordered list of formulae $\Gamma$. The succedent
consists of a single formula $A$. Then restrict the application of
introduction rules to allow only one of the directions of associativity and
unitality, the one in the definition of skew monoidal category. For example,
left-introduction rules are allowed to act only on the formula in stoup
position, not on formulae in $\Gamma$.

In our previous investigations we have explored deductive systems for $(i)$
skew semigroup [27], $(ii)$ skew monoidal [24], $(iii)$ skew (prounital)
closed [22] and $(iv)$ skew monoidal closed categories [21, 26], corresponding
to skew variants of the fragments of non-commutative intuitionistic linear
logic consisting of connectives $(i)$ $\otimes$, $(ii)$
$(\mathsf{I},\otimes)$, $(iii)$ $\multimap$ and $(iv)$
$(\mathsf{I},\otimes,\multimap)$. We have also studied partial normality
conditions, when one or more among associator and unitors is allowed to have
an inverse [23], and extensions with exchange à la Bourke and Lack [25].

When studying meta-theoretic properties of these semi-structural deductive
systems, we have been mostly interested in categorical and proof-theoretic
semantics. In the latter, we have particularly investigated normalization
strategies inspired by Andreoli’s focused sequent calculus for classical
linear logic [4] and employed the resulting normal forms to solve the
_coherence problem_ for the corresponding categories with skew structure. For
these categories, the word problem is more nuanced than in the normal non-skew
case studied by MacLane [15]. Our study additionally revealed that the focused
sequent calculi of semi-substructural logics can serve as cornerstones for a
compositional and modular understanding of normalization techniques for other
richer substructural logics.

In this work we begin the investigation of semi-substructural logics with
_additive connectives_. We start in Section 2 by considering a fragment of
non-commutative linear logic consisting of skew multiplicative unit
$\mathsf{I}$ and conjunction $\otimes$, and additive conjunction $\land$ and
disjunction $\lor$. We describe a cut-free sequent calculus and a congruence
relation $\circeq$ identifying derivations up-to $\eta$-equivalence and
permutative conversions. In Section 3, we discuss categorical semantics in
terms of skew monoidal categories with binary products and coproducts
satisfying a left-distributivity condition.

In Section 4, we introduce a sequent calculus of proofs in normal form, i.e.
canonical representative of the equivalence relation on derivations $\circeq$.
The design of the latter calculus is again inspired by the ideas of Andreoli
and it describes a sound and complete root-first proof search strategy for the
original sequent calculus. Completeness is achieved by marking sequents with
lists of _tags_ , a mechanism introduced by Uustalu et al. [21] and inspired
by Scherer and Rémy’s saturation technique [18], which helps to completely
eliminate all undesired non-determinism in proof search and faithfully capture
normal forms wrt. the congruence relation on derivations in the original
sequent calculus.

To showcase the modularity of our normalization strategy, in Section 5 we
discuss extensions of the logic with other connectives, such as additive
units, the structural rule of exchange in the style of Bourke and Lack and
linear implication. This provides evidence that our normalization technique is
potentially scalable to other richer substructural logics arising as
extensions of ours, e.g. full Lambek calculus or intuitionistic linear logic.
Moreover, we conjecture that a similar use of tags can be ported to fragments
of classical linear logic, such as MALL. The resulting notion of normal form
should correspond to maximally multi-focused proofs [9] and therefore proof
nets.

The sequent calculi of Sections 2 and 4, as well as the effective
normalization procedure, have been fully formalized in the Agda proof
assistant. The code is freely available at

https://github.com/cswphilo/SkewMonAdd.

##  2 Sequent Calculus

We start by describing a sequent calculus for a skew variant of non-
commutative multiplicative intuitionistic linear logic with additive
conjunction and disjunction.

Formulae are inductively generated by the grammar $A,B::=X\ |\ \mathsf{I}\ |\
A\otimes B\ |\ A\land B\ |\ A\lor B$, where $X$ comes from a set $\mathsf{At}$
of atomic formulae. We use $\mathsf{I},\otimes,\land$ and $\lor$ to denote
multiplicative verum, multiplicative conjunction, additive conjunction and
additive disjunction, respectively. The additives are traditionally named $\&$
and $\oplus$ in linear logic literature.

A sequent is a triple of the form $S\mid\Gamma\vdash A$. The antecedent is
split in two parts: an optional formula $S$, called _stoup_ [11], and an
ordered list of formulae $\Gamma$, called _context_. The succedent $A$ is a
single formula. The peculiar design of sequents, involving the presence of the
stoup in the antecedent, comes from our previous work on deductive systems
with skew structure in collaboration with Uustalu and Zeilberger [24, 23, 22,
25, 21, 26]. The metavariable $S$ always denotes a stoup, i.e., $S$ can be a
single formula or empty, in which case we write $S={-}$. Metavariables $X,Y,Z$
are always names of atomic formulae.

Derivations of a sequent $S\mid\Gamma\vdash A$ are inductively generated by
the following rules:

$\begin{array}[]{c}A\mid\quad\vdash A\qquad{-}\mid A,\Gamma\vdash
CA\mid\Gamma\vdash C\qquad\mathsf{I}\mid\Gamma\vdash C{-}\mid\Gamma\vdash
C\qquad{-}\mid\quad\vdash\mathsf{I}\\\ \qquad A\otimes B\mid\Gamma\vdash
CA\mid B,\Gamma\vdash C\qquad S\mid\Gamma,\Delta\vdash A\otimes
B\lx@proof@logical@and S\mid\Gamma\vdash A{-}\mid\Delta\vdash B\\\ A\land
B\mid\Gamma\vdash CA\mid\Gamma\vdash C\qquad A\land B\mid\Gamma\vdash
CB\mid\Gamma\vdash C\qquad S\mid\Gamma\vdash A\land B\lx@proof@logical@and
S\mid\Gamma\vdash AS\mid\Gamma\vdash B\\\ A\lor B\mid\Gamma\vdash
C\lx@proof@logical@and A\mid\Gamma\vdash CB\mid\Gamma\vdash C\qquad
S\mid\Gamma\vdash A\lor BS\mid\Gamma\vdash A\qquad S\mid\Gamma\vdash A\lor
BS\mid\Gamma\vdash B\end{array}$ (1)

The inference rules are similar to the ones in non-commutative intuitionistic
linear logic [2], but with some essential differences.

  1. 1.

The left logical rules $\mathsf{IL}$, $\otimes\mathsf{L}$,
$\land\mathsf{L}_{i}$ and $\lor\mathsf{L}$, when read bottom-up, can only be
applied on the formula in the stoup position. That is, it is generally not
possible to remove a unit $\mathsf{I}$, or decompose a tensor $A\otimes B$ or
a disjunction $A\lor B$, when these formulae are located in the context.

  2. 2.

The right tensor rule $\otimes\mathsf{R}$, when read bottom-up, splits the
antecedent of the conclusion but the formula in the stoup, whenever this is
present, always moves to the left premise. The stoup formula of the conclusion
is prohibited to move to the second premise even if $\Gamma$ is empty.

  3. 3.

The presence of the stoup implies a distinction between antecedents of the
form $A\mid\Gamma$ and ${-}\mid A,\Gamma$. The structural rule $\mathsf{pass}$
(for ‘passivation’), when read bottom-up, allows the moving of the leftmost
formula in the context to the stoup position whenever the stoup is initially
empty.

These restrictions allow the derivability of sequents $(A\otimes B)\otimes
C\mid~{}\vdash A\otimes(B\otimes C)$ (semi-associativity), $\mathsf{I}\otimes
A\mid~{}\vdash A$ and $A\mid~{}\vdash A\otimes\mathsf{I}$ (semi-unitality),
while forbidding the derivability of their inverses, where the formulae in the
stoup and in the succedent have been swapped. This is in line with the
intended categorical semantics, see Section 3.

Notice that, similarly to the case of non-commutative intuitionistic linear
logic [2], all structural rules of exchange, contraction and weakening are
absent. We give names to derivations and we write $f:S\mid\Gamma\vdash A$ when
$f$ is a particular derivation of the sequent $S\mid\Gamma\vdash A$.

######  Theorem 2.1.

The sequent calculus enjoys cut admissibility: the following two cut rules are
admissible

$S\mid\Gamma,\Delta\vdash C\lx@proof@logical@and S\mid\Gamma\vdash
AA\mid\Delta\vdash C\qquad S\mid\Delta_{\\_}0,\Gamma,\Delta_{\\_}1\vdash
C\lx@proof@logical@and{-}\mid\Gamma\vdash
AS\mid\Delta_{\\_}0,A,\Delta_{\\_}1\vdash C$

While the left $\land$-rules only act on the formula in stoup position (as all
the other left logical rules), other $\land$-rules
$\land\mathsf{L}_{i}^{\mathsf{C}}$ acting on formulae in context are
admissible.

$\begin{array}[]{c}\begin{tabular}[]{l}$S\mid\Gamma,A\land B,\Delta\vdash
CS\mid\Gamma,A,\Delta\vdash
C$\end{tabular}\quad\begin{tabular}[]{l}$S\mid\Gamma,A\land B,\Delta\vdash
CS\mid\Gamma,B,\Delta\vdash C$\end{tabular}\end{array}$

However, this is not the case for the other left logical rules. For example,
there is no way of constructing a general left $\lor$-rule
$\lor\mathsf{L}^{\mathsf{C}}$ acting on a disjunction in context. This rule
should be forbidden since it would make some inadmissible sequents provable in
the sequent calculus. For example, the sequent $X\land Y\mid Y\lor
X\vdash(X\otimes Y)\lor(Y\otimes X)$ is not admissible (this can be proved
using the normalization procedure of Section 4) but a proof could be found
using $\lor\mathsf{L}^{\mathsf{C}}$:

$\footnotesize\begin{array}[]{c}X\land Y\mid Y\lor X\vdash(X\otimes
Y)\lor(Y\otimes X)\lx@proof@logical@and X\land Y\mid Y\vdash(X\otimes
Y)\lor(Y\otimes X)X\land Y\mid Y\vdash X\otimes YX\mid Y\vdash X\otimes
Y\lx@proof@logical@and X\mid\quad\vdash X-\mid Y\vdash YY\mid\quad\vdash
YX\land Y\mid X\vdash(X\otimes Y)\lor(Y\otimes X)X\land Y\mid X\vdash Y\otimes
XY\mid X\vdash Y\otimes X\lx@proof@logical@and Y\mid\quad\vdash Y-\mid X\vdash
XX\mid\quad\vdash X\end{array}$

We introduce a congruence relation $\circeq$ on the sets of cut-free
derivations:

$\small\begin{array}[]{rlll}\mathsf{ax}_{\\_}{\mathsf{I}}&\circeq\mathsf{IL}\text{
}(\mathsf{IR})\\\ \mathsf{ax}_{\\_}{A\otimes B}&\circeq\otimes\mathsf{L}\text{
}(\otimes\mathsf{R}\text{ }(\mathsf{ax}_{\\_}{A},\mathsf{pass}\text{
}\mathsf{ax}_{\\_}{B}))\\\ \mathsf{ax}_{\\_}{A\land B}&\circeq\land\mathsf{R}\
(\land\mathsf{L}_{1}\ \mathsf{ax}_{\\_}A,\land\mathsf{L}_{2}\
\mathsf{ax}_{\\_}B)\\\ \mathsf{ax}_{\\_}{A\lor B}&\circeq\lor\mathsf{L}\
(\lor\mathsf{R}_{1}\ \mathsf{ax}_{\\_}A,\lor\mathsf{R}_{2}\
\mathsf{ax}_{\\_}B)\\\ \otimes\mathsf{R}\text{ }(\mathsf{pass}\text{
}f,g)&\circeq\mathsf{pass}\text{ }(\otimes\mathsf{R}\text{
}(f,g))&&(f:A^{\prime}\mid\Gamma\vdash A,g:{-}\mid\Delta\vdash B)\\\
\otimes\mathsf{R}\text{ }(\mathsf{IL}\text{ }f,g)&\circeq\mathsf{IL}\text{
}(\otimes\mathsf{R}\text{ }(f,g))&&(f:{-}\mid\Gamma\vdash
A,g:{-}\mid\Delta\vdash B)\\\ \otimes\mathsf{R}\text{
}(\otimes\mathsf{L}\text{ }f,g)&\circeq\otimes\mathsf{L}\text{
}(\otimes\mathsf{R}\text{ }(f,g))&&(f:A^{\prime}\mid B^{\prime},\Gamma\vdash
A,g:{-}\mid\Delta\vdash B)\\\ \otimes\mathsf{R}\ (\land\mathsf{L}_{i}\
f,g)&\circeq\land\mathsf{L}_{i}\ (\otimes\mathsf{R}\
(f,g))&&(f:A^{\prime}\mid\Gamma\vdash A,g:-\mid\Delta\vdash B)\\\
\otimes\mathsf{R}\ (\lor\mathsf{L}\
(f_{\\_}1,f_{\\_}2),g)&\circeq\lor\mathsf{L}\ (\otimes\mathsf{R}\
(f_{\\_}1,g),\otimes\mathsf{R}\
(f_{\\_}2,g))&&(f_{\\_}1:A^{\prime}\mid\Gamma\vdash
A,f_{\\_}2:B^{\prime}\mid\Gamma\vdash A,\\\ &&&\;\;g:-\mid\Delta\vdash B)\\\
\mathsf{pass}\ (\land\mathsf{R}\ (f,g))&\circeq\land\mathsf{R}\
(\mathsf{pass}\ f,\mathsf{pass}\ g)&&(f:A^{\prime}\mid\Gamma\vdash
A,g:A^{\prime}\mid\Gamma\vdash B)\\\ \mathsf{IL}\ (\land\mathsf{R}\
(f,g))&\circeq\land\mathsf{R}\ (\mathsf{IL}\ f,\mathsf{IL}\
g)&&(f:-\mid\Gamma\vdash A,g:-\mid\Gamma\vdash B)\\\ \otimes\mathsf{L}\
(\land\mathsf{R}\ (f,g))&\circeq\land\mathsf{R}\ (\otimes\mathsf{L}\
f,\otimes\mathsf{L}\ g)&&(f:A^{\prime}\mid B^{\prime},\Gamma\vdash
A,g:A^{\prime}\mid B^{\prime},\Gamma\vdash B)\\\ \land\mathsf{L}_{i}\
(\land\mathsf{R}\ (f,g))&\circeq\land\mathsf{R}\ (\land\mathsf{L}_{i}\
f,\land\mathsf{L}_{i}\ g)&&(f:A^{\prime}\mid\Gamma\vdash
A,g:A^{\prime}\mid\Gamma\vdash B)\\\ \lor\mathsf{L}\ (\land\mathsf{R}\
(f_{\\_}1,g_{\\_}1),\land\mathsf{R}\
(f_{\\_}2,g_{\\_}2))&\circeq\land\mathsf{R}\ (\lor\mathsf{L}\
(f_{\\_}1,f_{\\_}2),\lor\mathsf{L}\
(g_{\\_}1,g_{\\_}2))&&(f_{\\_}1:A^{\prime}\mid\Gamma\vdash
A,f_{\\_}2:B^{\prime}\mid\Gamma\vdash A,\\\
&&&\;\;g_{\\_}1:A^{\prime}\mid\Gamma\vdash
B,g_{\\_}2:B^{\prime}\mid\Gamma\vdash B)\\\ \lor\mathsf{R}_{i}\
(\mathsf{pass}\ f)&\circeq\mathsf{pass}\ (\lor\mathsf{R}_{i}\
f)&&(f:A^{\prime}\mid\Gamma\vdash A)\\\ \lor\mathsf{R}_{i}\ (\mathsf{IL}\
f)&\circeq\mathsf{IL}\ (\lor\mathsf{R}_{i}\ f)&&(f:-\mid\Gamma\vdash A)\\\
\lor\mathsf{R}_{i}\ (\otimes\mathsf{L}\ f)&\circeq\otimes\mathsf{L}\
(\lor\mathsf{R}_{i}\ f)&&(f:A^{\prime}\mid B^{\prime},\Gamma\vdash A)\\\
\lor\mathsf{R}_{i}\ (\land\mathsf{L}_{i}\ f)&\circeq\land\mathsf{L}_{i}\
(\lor\mathsf{R}_{i}\ f)&&(f:A^{\prime}\mid\Gamma\vdash A)\\\
\lor\mathsf{R}_{i}\ (\lor\mathsf{L}\ (f,g))&\circeq\lor\mathsf{L}\
(\lor\mathsf{R}_{i}\ f,\lor\mathsf{R}_{i}\ g)&&(f:A^{\prime}\mid\Gamma\vdash
A,g:B^{\prime}\mid\Gamma\vdash A)\end{array}$ (2)

The first four equations ($\eta$-conversions) characterize the $\mathsf{ax}$
rule for non-atomic formulae. The remaining equations are permutative
conversions. The congruence $\circeq$ has been carefully chosen to serve as
the proof-theoretic counterpart of the equational theory of certain categories
with skew structure, which we introduce in the next section.

##  3 Categorical Semantics

A _skew monoidal category_ [20, 12, 13] is a category $\mathbb{C}$ with a unit
object $\mathsf{I}$, a functor
$\otimes:\mathbb{C}\times\mathbb{C}\rightarrow\mathbb{C}$ and three natural
transformations $\lambda$, $\rho$, $\alpha$ typed
$\lambda_{\\_}A:\mathsf{I}\otimes A\to A$, $\rho_{\\_}A:A\to
A\otimes\mathsf{I}$ and $\alpha_{\\_}{A,B,C}:(A\otimes B)\otimes C\to
A\otimes(B\otimes C)$, satisfying the following equations due to Mac Lane
[15]:

${{\mathsf{I}\otimes\mathsf{I}}}$${\mathsf{I}}$${\mathsf{I}}$$\scriptstyle{\rho_{\\_}{\mathsf{I}}}$$\scriptstyle{\lambda_{\\_}{\mathsf{I}}}$${{(A\otimes\mathsf{I})\otimes
B}}$${{A\otimes(\mathsf{I}\otimes B)}}$${{A\otimes B}}$${{A\otimes
B}}$$\scriptstyle{\rho_{\\_}A\otimes
B}$$\scriptstyle{A\otimes\lambda_{\\_}{B}}$$\scriptstyle{\alpha_{\\_}{A,\mathsf{I},B}}$${{(\mathsf{I}\otimes
A)\otimes B}}$${{\mathsf{I}\otimes(A\otimes B)}}$${{A\otimes
B}}$$\scriptstyle{\alpha_{\\_}{\mathsf{I},A,B}}$$\scriptstyle{\lambda_{\\_}{A\otimes
B}}$$\scriptstyle{\lambda_{\\_}{A}\otimes B}$${{(A\otimes
B)\otimes\mathsf{I}}}$${{A\otimes(B\otimes\mathsf{I})}}$${{A\otimes
B}}$$\scriptstyle{\alpha_{\\_}{A,B,\mathsf{I}}}$$\scriptstyle{A\otimes\rho_{\\_}B}$$\scriptstyle{\rho_{\\_}{A\otimes
B}}$${{(A\otimes(B\otimes C))\otimes D}}$${{A\otimes((B\otimes C)\otimes
D)}}$${{((A\otimes B)\otimes C)\otimes D}}$${{(A\otimes B)\otimes(C\otimes
D)}}$${{A\otimes(B\otimes(C\otimes D))}}$$\scriptstyle{\alpha_{\\_}{A,B\otimes
C,D}}$$\scriptstyle{A\otimes\alpha_{\\_}{B,C,D}}$$\scriptstyle{\alpha_{\\_}{A,B,C\otimes
D}}$$\scriptstyle{\alpha_{\\_}{A\otimes
B,C,D}}$$\scriptstyle{\alpha_{\\_}{A,B,C}\otimes D}$

A skew monoidal category with binary coproducts is _(binary) left-
distributive_ if the canonical morphism typed $(A\otimes C)+(B\otimes
C)\to(A+B)\otimes C$ has an inverse $l:(A+B)\otimes C\to(A\otimes C)+(B\otimes
C)$. We will be interested in skew monoidal categories with binary products
and coproducts, which moreover are left-distributive. We simply call these
distributive skew monoidal categories.

A _(strict) skew monoidal functor_ $F:\mathbb{C}\rightarrow\mathbb{D}$ between
skew monoidal categories $(\mathbb{C},\mathsf{I},\otimes)$ and
$(\mathbb{D},\mathsf{I}^{\prime},\otimes^{\prime})$ is a functor from
$\mathbb{C}$ to $\mathbb{D}$ satisfying $F\mathsf{I}=\mathsf{I}^{\prime}$ and
$F(A\otimes B)=FA\otimes^{\prime}FB$, also preserving the structural laws
$\lambda$, $\rho$ and $\alpha$ on the nose. This means that
$F\lambda_{\\_}A^{\mathbb{C}}=\lambda_{\\_}{FA}^{\mathbb{D}}$, where
$\lambda^{\mathbb{C}}$ and $\lambda^{\mathbb{D}}$ are left-unitors of
$\mathbb{C}$ and $\mathbb{D}$ respectively, and similar equations hold for
$\rho$ and $\alpha$. A skew monoidal functor is _distributive_ if it also
strictly preserves products, coproducts and (consequently also) left-
distributivity.

The formulae, derivations and the equivalence relation $\circeq$ of the
sequent calculus determine a _syntactic_ distributive skew monoidal category
$\mathsf{FDSkM}(\mathsf{At})$ (an acronym for Free Distributive Skew Monoidal
category on the set $\mathsf{At}$). Its objects are formulae. The operations
$\mathsf{I}$ and $\otimes$ are the logical connectives. The set of maps
between objects $A$ and $B$ is the set of derivations $A\mid~{}\vdash B$
quotiented by the equivalence relation $\circeq$. The identity map on $A$ is
the equivalence class of $\mathsf{ax}_{\\_}A$, while composition is given by
$\mathsf{scut}$. The structural laws $\lambda$, $\rho$, $\alpha$ are all
admissible. Products and coproducts are the additive connectives $\land$ and
$\lor$. Left-distributivity follows from the logical rules of $\lor$ and
$\otimes$.

Distributive skew monoidal categories form models of our sequent calculus.
Moreover the sequent calculus, as a presentation of a distributive skew
monoidal category, is the _initial_ one among these models. Equivalently,
$\mathsf{FDSkM}(\mathsf{At})$ is the _free_ such category on the set
$\mathsf{At}$.

######  Theorem 3.1.

Let $\mathbb{D}$ be a distributive skew monoidal category. Given a function
$F_{\\_}{\mathsf{At}}:\mathsf{At}\rightarrow|\mathbb{D}|$ evaluating atomic
formulae as objects of $\mathbb{D}$, there exists a unique distributive skew
monoidal functor $F:\mathsf{FDSkM}(\mathsf{At})\rightarrow\mathbb{D}$ for
which $FX=F_{\\_}{\mathsf{At}}X$, for any atom $X$.

The construction of the functor $F$ and the proof of uniqueness proceed
similarly to the proofs of Theorems 3.1 and 3.2 in [21].

##  4 A Focused Sequent Calculus with Tag Annotations

When oriented from left-to-right, the equations in (2) become a rewrite
system, which is locally confluent and strongly normalizing, thus confluent
with unique normal forms. Here we provide an explicit description of the
normal forms of (1) wrt. this rewrite system.

For any sequent $S\mid\Gamma\vdash A$, a root-first proof search procedure can
be defined as follows. First apply right invertible rules on the sequent until
the principal connective of the succedent is non-negative, then apply left
invertible rules until the stoup becomes either empty or non-positive. At this
point, if we do not insist on focusing on a particular formula (either in the
stoup or succedent, since no rule acts on formulae in context) as in
Andreoli’s focusing procedure [4], we obtain a sequent calculus with a reduced
proof search space, that looks like this:

$\begin{array}[]{lc}\text{(right
invertible)}&\begin{tabular}[]{l}$S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A\land
B\lx@proof@logical@and
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}AS\mid\Gamma\vdash_{\\_}{\mathsf{RI}}B$
\qquad$S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}PS\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$\end{tabular}\\\\[10.0pt]
\text{(left
invertible)}&\begin{tabular}[]{l}$\mathsf{I}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P{-}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$
\qquad$A\otimes B\mid\Gamma\vdash_{\\_}{\mathsf{LI}}PA\mid
B,\Gamma\vdash_{\\_}{\mathsf{LI}}P$\\\ $A\lor
B\mid\Gamma\vdash_{\\_}\mathsf{LI}P\lx@proof@logical@and
A\mid\Gamma\vdash_{\\_}\mathsf{LI}PB\mid\Gamma\vdash_{\\_}\mathsf{LI}P$
\qquad$T\mid\Gamma\vdash_{\\_}{\mathsf{LI}}PT\mid\Gamma\vdash_{\\_}{\mathsf{F}}P$\end{tabular}\\\\[10.0pt]
\text{(focusing)}&\begin{tabular}[]{l}${-}\mid
A,\Gamma\vdash_{\\_}{\mathsf{F}}PA\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$
\qquad$X\mid\quad\vdash_{\\_}{\mathsf{F}}X$
\qquad${-}\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}$\end{tabular}\\\\[10.0pt]
\lx@intercol\hfil T\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{F}}A\otimes
B\lx@proof@logical@and
T\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}B\qquad
T\mid\Gamma\vdash_{\\_}{\mathsf{F}}A\lor
BT\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A\qquad
T\mid\Gamma\vdash_{\\_}{\mathsf{F}}A\lor
<EMAIL_ADDRESS>\lx@intercol\hfil A\land
B\mid\Gamma\vdash_{\\_}{\mathsf{F}}PA\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P\qquad
A\land
B\mid\Gamma\vdash_{\\_}{\mathsf{F}}PB\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P\hfil\lx@intercol\end{array}$
(3)

In the rules above, $P$ is a non-negative formula, i.e. its principal
connective is not $\land$, and $T$ is a non-positive stoup (also called
_irreducible_), i.e. it is not $\mathsf{I}$ and its principal connective is
neither $\otimes$ nor $\lor$.

This calculus is too permissive. The same sequent
$S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$ may have multiple derivations which
correspond to $\circeq$-related derivations in the original sequent calculus.
This happens since certain sequents in phase $\vdash_{\\_}\mathsf{F}$ can be
alternatively proved by an application of a left non-invertible rule
($\mathsf{pass}$, $\land\mathsf{L}_{1}$ and $\land\mathsf{L}_{2}$) or an
application of a right non-invertible rule ($\otimes\mathsf{R}$,
$\lor\mathsf{R}_{1}$ and $\lor\mathsf{R}_{2}$). As concrete examples, both
sequents $-\mid X,Y\vdash_{\\_}{\mathsf{F}}X\otimes Y$ and $X\land
Y\mid~{}\vdash_{\\_}{\mathsf{F}}X\lor Y$ have multiple distinct proofs in this
calculus, but their corresponding proofs in the original calculus are
$\circeq$-related.

In phase $\vdash_{\\_}\mathsf{F}$, only non-invertible rules can be applied,
so the question is: how to arrange the order between non-invertible rules
without causing undesired non-determinism and losing completeness with respect
to the sequent calculus in (1) and its equivalence relation $\circeq$?
Similarly to [21], our strategy is to prioritize left non-invertible rules
over right ones, unless this does not lead to a valid derivation and the other
way around is necessary. For example, consider the sequent $X\land
Y\mid\quad\vdash_{\\_}{\mathsf{F}}(X\land Y)\lor Z$. Proof search fails if we
apply $\land\mathsf{L}_{i}$ before $\lor\mathsf{R}_{1}$. A valid proof is
obtained only when applying $\lor\mathsf{R}_{1}$ before $\land\mathsf{L}_{i}$.
Rule $\mathsf{sw}$ is an abbreviation for the application of multiple
consecutive phase switching rules.

$\small\begin{array}[]{c}X\land Y\mid\quad\vdash_{\\_}\mathsf{F}(X\land Y)\lor
ZX\land Y\mid\quad\vdash_{\\_}\mathsf{RI}X\land Y\lx@proof@logical@and X\land
Y\mid\quad\vdash_{\\_}\mathsf{RI}XX\land
Y\mid\quad\vdash_{\\_}\mathsf{F}XX\mid\quad\vdash_{\\_}\mathsf{LI}XX\mid\quad\vdash_{\\_}\mathsf{F}XX\land
Y\mid\quad\vdash_{\\_}\mathsf{RI}YX\land
Y\mid\quad\vdash_{\\_}\mathsf{F}YY\mid\quad\vdash_{\\_}\mathsf{LI}YY\mid\quad\vdash_{\\_}\mathsf{F}Y\end{array}$
(4)

In this example it was possible to first apply $\lor\mathsf{R}_{1}$ since,
after the application of $\land\mathsf{R}$, different left $\land$-rules are
applied in different branches of the proof tree. If we would have applied the
same rule $\land\mathsf{L}_{1}$ to both premises (imagine that $X=Y$ for this
to be possible), then we could have obtained a $\circeq$-equivalent derivation
by moving the application of $\land\mathsf{L}_{1}$ to the bottom of the proof
tree.

It is also possible that the two premises of $\land\mathsf{R}$ correspond to
$\circeq$-inequivalent derivations. For example, consider the following proof
of sequent $-\mid\mathsf{I}\otimes X\vdash_{\\_}\mathsf{F}((I\otimes
X)\land(\mathsf{I}\otimes X))\lor Y$:

$\small\begin{array}[]{c}-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{F}((\mathsf{I}\otimes X)\land(\mathsf{I}\otimes X))\lor
Y-\mid\mathsf{I}\otimes X\vdash_{\\_}\mathsf{RI}(\mathsf{I}\otimes
X)\land(\mathsf{I}\otimes X)\lx@proof@logical@and-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{RI}\mathsf{I}\otimes X-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{F}\mathsf{I}\otimes X\mathsf{I}\otimes
X\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}\otimes X\mathsf{I}\mid
X\vdash_{\\_}\mathsf{LI}\mathsf{I}\otimes X-\mid
X\vdash_{\\_}\mathsf{LI}\mathsf{I}\otimes X-\mid
X\vdash_{\\_}\mathsf{F}\mathsf{I}\otimes
X\lx@proof@logical@and-\mid\quad\vdash_{\\_}\mathsf{RI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{F}\mathsf{I}-\mid
X\vdash_{\\_}\mathsf{RI}X-\mid
X\vdash_{\\_}\mathsf{F}XX\mid\quad\vdash_{\\_}\mathsf{LI}XX\mid\quad\vdash_{\\_}\mathsf{F}X-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{RI}\mathsf{I}\otimes X-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{F}\mathsf{I}\otimes
X\lx@proof@logical@and-\mid\quad\vdash_{\\_}\mathsf{RI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{F}\mathsf{I}-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{RI}X-\mid\mathsf{I}\otimes
X\vdash_{\\_}\mathsf{F}X\mathsf{I}\otimes
X\mid\quad\vdash_{\\_}\mathsf{LI}X\mathsf{I}\mid
X\vdash_{\\_}\mathsf{LI}X-\mid X\vdash_{\\_}\mathsf{LI}X-\mid
X\vdash_{\\_}\mathsf{F}XX\mid\quad\vdash_{\\_}\mathsf{LI}XX\mid\quad\vdash_{\\_}\mathsf{F}X\end{array}$

In this case, the right non-invertible rule $\lor\mathsf{R}_{1}$ must be
applied before the left non-invertible rule $\mathsf{pass}$. This is because
$\mathsf{pass}$ is used in the proof of the left branch of $\land\mathsf{R}$,
but it is not used in the proof of the right branch, $\otimes\mathsf{R}$ is
used instead. If both left and right proofs would have used $\mathsf{pass}$
(for example, they could have been the same exact proof), then it would have
been possible to apply $\mathsf{pass}$ before $\lor\mathsf{R}_{1}$.

In general, a right non-invertible rule should be applied before a left non-
invertible one if, after the possible application of some $\land\mathsf{R}$
rules, either: $(i)$ a right non-invertible rule or the $\mathsf{ax}$ rule is
applied to one of the premises; $(ii)$ $\land\mathsf{L}_{1}$ and
$\land\mathsf{L}_{2}$ are applied to different premises. Therefore, we have to
make sure that in the focused sequent calculus, after the application of a
right non-invertible rule, not all premises use the same left non-invertible
rule, because in this case the latter rule could be applied first.

In order to keep track of this, we use a system of _tag annotations_ and we
introduce new phases of proof search where sequents are annotated by _list of
tags_. There are four tags:
$\mathbb{P},\mathbb{C}_{1},\mathbb{C}_{2},\mathbb{R}$. Intuitively, they
respectively correspond to rules
$\mathsf{pass},\land\mathsf{L}_{1},\land\mathsf{L}_{2}$ and all the remaining
non-invertible rules in phase $\vdash_{\\_}\mathsf{F}$. A list of tags $l$ is
called _valid_ if it is non-empty and either $(i)$ $\mathbb{R}\in l$ or $(ii)$
both $\mathbb{C}_{1}\in l$ and $\mathbb{C}_{2}\in l$.

Derivations in the focused sequent calculus with tag annotations are generated
by the rules

$\begin{array}[]{lc}\text{(right
invertible)}&\begin{tabular}[]{l}$S\mid\Gamma\vdash^{l_{\\_}1?,l_{\\_}2?}_{\\_}{\mathsf{RI}}A\land
B\lx@proof@logical@and
S\mid\Gamma\vdash^{l_{\\_}1?}_{\\_}{\mathsf{RI}}AS\mid\Gamma\vdash^{l_{\\_}2?}_{\\_}{\mathsf{RI}}B$
\qquad$S\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{RI}}PS\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{LI}}P$\end{tabular}\\\\[10.0pt]
\text{(left
invertible)}&\begin{tabular}[]{l}$\mathsf{I}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P{-}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$
\qquad$A\otimes B\mid\Gamma\vdash_{\\_}{\mathsf{LI}}PA\mid
B,\Gamma\vdash_{\\_}{\mathsf{LI}}P$\\\ $A\lor
B\mid\Gamma\vdash_{\\_}\mathsf{LI}P\lx@proof@logical@and
A\mid\Gamma\vdash_{\\_}\mathsf{LI}PB\mid\Gamma\vdash_{\\_}\mathsf{LI}P$
\qquad$T\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{LI}}PT\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{F}}P$\end{tabular}\\\\[10.0pt]
\text{(focusing)}&\begin{tabular}[]{l}${-}\mid
A,\Gamma\vdash^{\mathbb{P}?}_{\\_}{\mathsf{F}}PA\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$
\qquad$X\mid\quad\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}X$
\qquad${-}\mid\quad\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}\mathsf{I}$\end{tabular}\\\\[10.0pt]
\lx@intercol\hfil
T\mid\Gamma,\Delta\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}A\otimes
B\lx@proof@logical@and
T\mid\Gamma\vdash^{l}_{\\_}{\mathsf{RI}}A{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}Bl\
\text{valid}\quad T\mid\Gamma\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}A\lor
B\lx@proof@logical@and T\mid\Gamma\vdash^{l}_{\\_}{\mathsf{RI}}Al\
\text{valid}\quad T\mid\Gamma\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}A\lor
B\lx@proof@logical@and T\mid\Gamma\vdash^{l}_{\\_}{\mathsf{RI}}Bl\
<EMAIL_ADDRESS>\lx@intercol\hfil A\land
B\mid\Gamma\vdash^{\mathbb{C}_{1}?}_{\\_}{\mathsf{F}}PA\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P\qquad
A\land
B\mid\Gamma\vdash^{\mathbb{C}_{2}?}_{\\_}{\mathsf{F}}PB\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P\hfil\lx@intercol\end{array}$
(5)

We use $l$ for lists of tags and $t$ for single tags. The notation $l?$
indicates that the sequent is either untagged or assigned the list of tags
$l$. Similarly for notation $t?$. We discuss the proof search procedures of
untagged and tagged sequents separately. The proof search of a sequent
$S\mid\Gamma\vdash_{\\_}\mathsf{RI}A$ proceeds as follows:

  * ($\vdash_{\\_}{\mathsf{RI}}$)

We apply the right invertible rule $\land\mathsf{R}$ eagerly to decompose the
succedent until its principal connective is not $\land$, then we move to the
left invertible phase $\vdash_{\\_}\mathsf{LI}$ with an application of
$\mathsf{LI}2\mathsf{RI}$.

  * ($\vdash_{\\_}{\mathsf{LI}}$)

We apply left invertible rules until the stoup becomes irreducible, then move
to the focusing phase $\vdash_{\\_}\mathsf{F}$ with an application of
$\mathsf{F}2\mathsf{LI}$.

  * ($\vdash_{\\_}{\mathsf{F}}$)

We apply one of the remaining rules. Since the sequents are not marked by tags
at this point, rules $\mathsf{pass}$, $\mathsf{ax}$ , $\mathsf{IR}$ and
$\land\mathsf{L}_{i}$ can be directly applied when stoups, contexts and
succedents are of the appropriate form. If we decide to apply a right non-
invertible rule, we need to come up with a valid list of tags $l$ and
subsequently continue proof search in tagged right invertible phase
$\vdash^{l}_{\\_}{\mathsf{RI}}$, which is described below. Notice that only
the first premise of $\otimes\mathsf{R}$ is tagged, the second premise is not,
i.e. its proof search continues in phase $\vdash_{\\_}{\mathsf{RI}}$.

The proof search of a sequent $T\mid\Gamma\vdash^{l}_{\\_}\mathsf{RI}A$
proceeds as follows (notice that at this point in proof search the stoup $T$
is necessarily irreducible):

  * ($\vdash^{l}_{\\_}{\mathsf{RI}}$)

We apply the $\land\mathsf{R}$ rule to decompose the succedent and split the
list of tags carefully until the succedent becomes non-negative and the list
of tags becomes a singleton $t$, then we move to phase
$\vdash_{\\_}\mathsf{LI}^{t}$ with an application of
$\mathsf{LI}2\mathsf{RI}$.

  * ($\vdash^{t}_{\\_}{\mathsf{LI}}$)

Since the stoup is either empty or a negative formula, we immediately switch
to phase $\vdash_{\\_}\mathsf{F}$ with an application of
$\mathsf{F}2\mathsf{LI}$. This motivates why sequents in rules $\mathsf{IL}$,
$\otimes\mathsf{L}$, $\lor\mathsf{L}$ are not tagged.

  * ($\vdash^{t}_{\\_}{\mathsf{F}}$)

If $t=\mathbb{R}$ we can apply either $\mathsf{ax}$, $\mathsf{IR}$ or another
right non-invertible rule. Again, when applying right non-invertible rules we
need to come up with a new valid list of tags. Left non-invertible rules can
be applied only when the tag is correct, i.e. $\mathsf{pass}$ with tag
$\mathbb{P}$, $\land\mathsf{L}_{1}$ with tag $\mathbb{C}_{1}$, and
$\land\mathsf{L}_{2}$ with tag $\mathbb{C}_{2}$.

The derivation in (4) can be reconstructed in the focused calculus with tag
annotations.

$\begin{array}[]{c}X\land Y\mid\quad\vdash_{\\_}{\mathsf{F}}(X\land Y)\lor
ZX\land
Y\mid\quad\vdash^{\mathbb{C}_{1},\mathbb{C}_{2}}_{\\_}{\mathsf{RI}}X\land
Y\lx@proof@logical@and X\land
Y\mid\quad\vdash^{\mathbb{C}_{1}}_{\\_}{\mathsf{RI}}XX\land
Y\mid\quad\vdash^{\mathbb{C}_{1}}_{\\_}{\mathsf{F}}XX\mid\quad\vdash_{\\_}{\mathsf{LI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}XX\land
Y\mid\quad\vdash^{\mathbb{C}_{2}}_{\\_}{\mathsf{RI}}YX\land
Y\mid\quad\vdash^{\mathbb{C}_{2}}_{\\_}{\mathsf{F}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y\end{array}$
(6)

Notice that the list of tags is not predetermined when a right non-invertible
rule is applied, we have to come up with one ourselves. Practically, the list
$l$ can be computed by continuing proof search until, in each branch, we hit
the first application of a rule in phase $\vdash_{\\_}\mathsf{F}$, each with
its own (necessarily uniquely determined) single tag $t$. Take $l$ as the
concatenation of the resulting $t$s and check whether it is valid. If it is
not, backtrack and apply a left non-invertible rule instead.

######  Theorem 4.1.

The focused sequent calculus with tag annotations in (5) is sound and complete
with respect to the sequent calculus in (1).

Soundness is immediate because there exist functions
$\mathsf{emb}_{\\_}{ph}:S\mid\Gamma\vdash^{l?}_{\\_}{ph}A\to S\mid\Gamma\vdash
A$, for all $ph\in\\{\mathsf{RI},\mathsf{LI},\mathsf{F}\\}$, which erase all
phase and tag annotations. Completeness follows from the fact that the
following rules are all admissible:

$\small\begin{array}[]{c}\mathsf{I}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C{-}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\quad
A\otimes B\mid\Gamma\vdash_{\\_}{\mathsf{RI}}CA\mid
B,\Gamma\vdash_{\\_}{\mathsf{RI}}C\quad{-}\mid
A,\Gamma\vdash_{\\_}{\mathsf{RI}}CA\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\quad
A\mid\quad\vdash_{\\_}{\mathsf{RI}}A\quad{-}\mid\quad\vdash_{\\_}{\mathsf{RI}}\mathsf{I}\\\\[6.0pt]
A\lor B\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\lx@proof@logical@and
A\mid\Gamma\vdash_{\\_}{\mathsf{RI}}CB\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\qquad
S\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{RI}}A\otimes B\lx@proof@logical@and
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}B\\\\[6.0pt]
A\land
B\mid\Gamma\vdash_{\\_}{\mathsf{RI}}CA\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\qquad
A\land
B\mid\Gamma\vdash_{\\_}{\mathsf{RI}}CB\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\qquad
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A\lor
BS\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A\qquad
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A\lor
BS\mid\Gamma\vdash_{\\_}{\mathsf{RI}}B\end{array}$ (7)

The admissibility of the rules in (7), apart from the right non-invertible
ones, is proved by structural induction on derivations. The same strategy
cannot be applied to right non-invertible rules. For example, if the premise
of $\lor\mathsf{R}_{1}^{\mathsf{RI}}$ ends with an application of
$\land\mathsf{R}$, we get immediately stuck:

$\begin{array}[]{c}\small\begin{tabular}[]{l}$S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}(A^{\prime}\land
B^{\prime})\lor BS\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A^{\prime}\land
B^{\prime}\lx@proof@logical@and
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A^{\prime}fS\mid\Gamma\vdash_{\\_}{\mathsf{RI}}B^{\prime}g$\end{tabular}\quad=\quad??\end{array}$

The inductive hypothesis applied to $f$ and $g$ would produce wrong sequents
for the target conclusion. This is fixed by proving the admissibility of more
general rules. In order to state and prove this, we need to first introduce a
few lemmata. The first one shows that applying several $\land\mathsf{R}$ rules
in one step is admissible.

Let $\mathsf{conj}(A)$ be the list of formulae obtained by decomposing
additive conjunctions $\land$ in the formula $A$. Concretely,
$\mathsf{conj}(A)=\mathsf{conj}(A^{\prime}),\mathsf{conj}(B^{\prime})$ if
$A=A^{\prime}\land B^{\prime}$ and $\mathsf{conj}(A)=A$ otherwise.

######  Lemma 4.2.

The following rules

$T\mid\Gamma\vdash^{l}_{\\_}{\mathsf{RI}}A[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}\qquad
T\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A[T\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}$

are admissible, where $\mathsf{conj}(A)=[P_{\\_}1,\dots,P_{\\_}n]$ and
$l=[t_{\\_}1,\dots,t_{\\_}n]$.

###### Proof.

We show the case of $\land\mathsf{R}^{*}_{\\_}{t}$, the other one is similar.
Let $fs:[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}i$ be a
list of derivations. The proof proceeds by induction on $A$.

  * •

If $A\neq A^{\prime}\land B^{\prime}$, then $fs$ consists of a single
derivation $f$. Define $\land\mathsf{R}^{*}_{\\_}{t}\text{
}fs=\mathsf{F}2\mathsf{LI}\text{ }(\mathsf{LI}2\mathsf{RI}\text{ }f)$.

  * •

If $A=A^{\prime}\land B^{\prime}$, then there exist lists of derivations
$fs_{\\_}1:[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}A^{\prime}_{\\_}i]_{\\_}{i\in[1,\dots,m]}$
and
$fs_{\\_}2:[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}B^{\prime}_{\\_}i]_{\\_}{i\in[m+1,\dots,n]}$,
and lists of tags $l_{\\_}1=t_{\\_}1,\dots,t_{\\_}m$ and
$l_{\\_}2=t_{\\_}{m+1},\dots,t_{\\_}n$, so that $fs$ is the concatenation of
$fs_{\\_}1$ and $fs_{\\_}2$ and $l$ is the concatenation of $l_{\\_}1$ and
$l_{\\_}2$. Apply $\land\mathsf{R}$ at the bottom, then proceed recursively:

$\small\begin{array}[]{cc}\begin{tabular}[]{l}$T\mid\Gamma\vdash^{l}A^{\prime}\land
B^{\prime}[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs$\end{tabular}&=\begin{tabular}[]{l}$T\mid\Gamma\vdash^{l_{\\_}1,l_{\\_}2}_{\\_}{\mathsf{RI}}A^{\prime}\land
B^{\prime}\lx@proof@logical@and
T\mid\Gamma\vdash^{l_{\\_}1}_{\\_}{\mathsf{RI}}A^{\prime}[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}{i\in[1,\dots,m]}fs_{\\_}1T\mid\Gamma\vdash^{l_{\\_}2}_{\\_}{\mathsf{RI}}B^{\prime}[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}{i\in[m+1,\dots,n]}fs_{\\_}2$\end{tabular}\end{array}$

∎

The second lemma corresponds to the invertibility of phase
$\vdash_{\\_}\mathsf{RI}$.

######  Lemma 4.3.

Given $f:S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$, there is a list of
derivations
$fs:[S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}$
with $f=\land\mathsf{R}^{*}fs$.

###### Proof.

The proof proceeds by structural induction on
$f:S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$.

  * •

If $f=\mathsf{LI}2\mathsf{RI}\text{ }f_{\\_}1$, then $A$ is non-negative. Take
$fs$ as the singleton list consisting exclusively of $f_{\\_}1$.

  * •

If $f=\land\mathsf{R}\ (f_{\\_}1,f_{\\_}2)$, then by inductive hypothesis we
have
$fs_{\\_}1:[S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}$
and
$fs_{\\_}2:[S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P^{\prime}_{\\_}i]_{\\_}{i\in[1,\dots,m]}$.
Take $fs$ as the concatenation of $fs_{\\_}1$ and $fs_{\\_}2$.

∎

######  Proposition 4.4.

The following rules

$\begin{array}[]{c}S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
B[S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs\quad
S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
B[S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}Q_{\\_}i]_{\\_}{i\in[1,\dots,m]}fs\quad
S\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{LI}}A\otimes
B^{\prime}\lx@proof@logical@and[S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs-\mid\Delta\vdash_{\\_}{\mathsf{RI}}B^{\prime}\end{array}$

are admissible, where $\mathsf{conj}(A)=[P_{\\_}1,\dots,P_{\\_}n]$ and
$\mathsf{conj}(B)=[Q_{\\_}1,\dots,Q_{\\_}m]$.

###### Proof.

The list of derivations $fs$ is non-empty, so we let
$fs=[f_{\\_}1,fs^{\prime}]$. We proceed by induction on $f_{\\_}1$. We only
present the proof for $\lor\mathsf{R}_{1}^{\mathsf{LI}}$, the admissibility of
$\lor\mathsf{R}_{2}^{\mathsf{LI}}$ and $\otimes\mathsf{R}^{\mathsf{LI}}$ is
proved similarly.

If $f_{\\_}1$ ends with the application of a left invertible rule, then all
the derivations in $fs^{\prime}$ necessarily end with the same rule as well.
Therefore, we permute this rule with $\lor\mathsf{R}_{1}^{\mathsf{LI}}$ and
apply the inductive hypothesis.

If $f_{\\_}1=\mathsf{F}2\mathsf{LI}\,f^{\prime}_{\\_}1$, then all the
derivations in $fs^{\prime}$ necessarily end with $\mathsf{F}2\mathsf{LI}$ as
well. We generate a list of tags $l$ by examining the shape of each derivation
in $fs$: we add $\mathbb{P}$ for each $\mathsf{pass}$, $\mathbb{C}_{1}$ for
each $\land\mathsf{L}_{1}$, $\mathbb{C}_{2}$ for each $\land\mathsf{L}_{2}$
and $\mathbb{R}$ for the remaining rules. There are two possibilities:

  * •

The resulting list $l$ is valid. We switch to phase $\vdash_{\\_}\mathsf{F}$
and apply $\lor\mathsf{R}_{1}^{\mathsf{LI}}$ followed by
$\land\mathsf{R}^{*}_{\\_}{t}$:

$\begin{array}[]{cc}\begin{tabular}[]{l}$T\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
B[T\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}[T\mid\Gamma\vdash_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs^{*}$\end{tabular}&=\begin{tabular}[]{l}$T\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
BT\mid\Gamma\vdash_{\\_}{\mathsf{F}}A\lor
BT\mid\Gamma\vdash^{l}_{\\_}{\mathsf{RI}}A[T\mid\Gamma\vdash^{t_{\\_}i}_{\\_}{\mathsf{F}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}{fs^{*}}^{\prime}$\end{tabular}\end{array}$

A rule wrapped in square brackets, like $[\mathsf{F}2\mathsf{LI}]$ above,
denotes the application of the rule to the conclusion of each derivation in
the list. The list of derivations $fs^{*}$ is obtained from $fs$ by applying
$[\mathsf{F}2\mathsf{LI}]$, i.e. $fs=[\mathsf{F}2\mathsf{LI}]\,fs^{*}$, while
${fs^{*}}^{\prime}$ is a list of derivations whose conclusions are tagged
version of those in $fs^{*}$, which can be easily constructed from $fs^{*}$.

  * •

The list $l$ is invalid. In this case, all elements in $fs$ end with the same
left non-invertible rule, so we permute the rule down with
$\lor\mathsf{R}_{1}^{\mathsf{LI}}$ and continue recursively. Here is an
example where all derivations in $fs$ end with an application of
$\mathsf{pass}$, i.e.
$fs=[\mathsf{F}2\mathsf{LI}]\,([\mathsf{pass}]\,fs^{*})$:

$\begin{array}[]{cc}\begin{tabular}[]{l}$-\mid
A^{\prime},\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor B[-\mid
A^{\prime},\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}[-\mid
A^{\prime},\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}[A^{\prime}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs^{*}$\end{tabular}&=\begin{tabular}[]{l}$-\mid
A^{\prime},\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor B-\mid
A^{\prime},\Gamma\vdash_{\\_}{\mathsf{F}}A\lor
BA^{\prime}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
B[A^{\prime}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs^{*}$\end{tabular}\end{array}$

∎

Finally, a right non-invertible rule in (7) is defined as follows: first
invert its premises (for $\otimes\mathsf{R}^{\mathsf{RI}}$, only the left
premise) using Lemma 4.3. Then apply the corresponding generalized rule in
Proposition 4.4.

We can construct a function $\mathsf{focus}:S\mid\Gamma\vdash A\to
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$ by structural recursion on the input
derivation. Each inference rule in (1) is sent to the corresponding admissible
rule in (7). For example, $\mathsf{focus}\ (\lor\mathsf{R}_{1}\
f)=\lor\mathsf{R}_{1}^{\mathsf{RI}}\ (\mathsf{focus}\ f)$. Furthermore, it can
be shown that $\mathsf{emb}_{\\_}{\mathsf{RI}}$ and $\mathsf{focus}$ are each
other inverses, in the sense made precise by the following theorem.

######  Theorem 4.5.

The functions $\mathsf{emb}_{\\_}{\mathsf{RI}}$ and $\mathsf{focus}$ define a
bijective correspondence between the set of derivations of $S\mid\Gamma\vdash
A$ quotiented by the equivalence relation $\circeq$ and the set of derivations
of $S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$:

  * •

For all $f,g:S\mid\Gamma\vdash A$, if $f\circeq g$ then $\mathsf{focus}\text{
}f=\mathsf{focus}\text{ }g$.

  * •

For all $f:S\mid\Gamma\vdash A$, $\mathsf{emb}_{\\_}{\mathsf{RI}}\text{
}(\mathsf{focus}\text{ }f)\circeq f$.

  * •

For all $f:S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$, $\mathsf{focus}\text{
}(\mathsf{emb}_{\\_}{\mathsf{RI}}\text{ }f)=f$.

###### Proof.

The first bullet is proved by structural induction on the given equality proof
$e:f\circeq g$. The other bullets are proved by structural induction on $f$.
See the associated Agda formalization for details. ∎

##  5 Extensions of the Logic

We now discuss some extensions of the sequent calculus and the focusing
strategy.

###  5.1 Additive Units

The sequent calculus in (1) can be made “fully” additive by including two
units $\top$ and $\bot$ (the latter named 0 in linear logic literature), two
new introduction rules and two new generating equations:

$\begin{array}[]{c}S\mid\Gamma\vdash\top\qquad\bot\mid\Gamma\vdash
C\end{array}$
$\small\begin{array}[]{rclll}f&\circeq\top\mathsf{R}&&(f:S\mid\Gamma\vdash\top)\\\
f&\circeq\bot\mathsf{L}&&(f:\bot\mid\Gamma\vdash C)\end{array}$

In the focused sequent calculus we add $\top\mathsf{R}$ in phase
$\vdash_{\\_}\mathsf{RI}$ and $\bot\mathsf{L}$ in phase
$\vdash_{\\_}\mathsf{LI}$, so that they can be applied as early as possible.
We include a new tag $\mathbb{T}$ for $\top$. The validity condition for lists
of tags is updated as follows: ($i$) $\mathbb{T}$ or $\mathbb{R}\in l$ or
($ii$) both $\mathbb{C}_{1}\in l$ and $\mathbb{C}_{2}\in l$.

$\begin{array}[]{c}S\mid\Gamma\vdash^{\mathbb{T}?}_{\\_}{\mathsf{RI}}\top\qquad\bot\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P\end{array}$

Categorical models of the extended sequent calculus are the distributive
monoidal categories of Section 3 with additionally a terminal and an initial
object, which moreover satisfy a _(nullary) left-distributivity_ (or
_absorption_) condition: the canonical morphism typed $0\to 0\otimes C$ has an
inverse$k:0\otimes C\to 0$. The latter is used in the interpretation of the
rule $\bot\mathsf{L}$.

###  5.2 Skew Exchange

Following [25], we consider a “skew” commutative extension of the sequent
calculus in (1) obtained by adding a rule swapping adjacent formulae in
context:

$S\mid\Gamma,B,A,\Delta\vdash CS\mid\Gamma,A,B,\Delta\vdash C$

Note that exchanging the formula in the stoup, whenever the latter is non-
empty, with a formula in context is not allowed. The new rule $\mathsf{ex}$
comes with additional generating equations for the congruence relation
$\circeq$:

$\small\begin{array}[]{rclll}\mathsf{ex}_{\\_}{B,A}(\mathsf{ex}_{\\_}{A,B}f)&\circeq&f&&(f:S\mid\Gamma,A,B,\Delta\vdash
C)\\\
\mathsf{ex}_{\\_}{A,B}(\mathsf{ex}_{\\_}{A,D}(\mathsf{ex}_{\\_}{B,D}f))&\circeq&\mathsf{ex}_{\\_}{B,D}(\mathsf{ex}_{\\_}{A,D}(\mathsf{ex}_{\\_}{A,B}f))&&(f:S\mid\Gamma,A,B,D,\Delta\vdash
C)\\\ \land\mathsf{L}_{i}\ (\mathsf{ex}_{\\_}{A,B}\
f)&\circeq&\mathsf{ex}_{\\_}{A,B}\ (\land\mathsf{L}_{i}\
f)&&(f:A^{\prime}\mid\Gamma,A,B,\Delta\vdash C)\\\ \land\mathsf{R}\
(\mathsf{ex}_{\\_}{A,B}\ f,\mathsf{ex}_{\\_}{A,B}\
g)&\circeq&\mathsf{ex}_{\\_}{A,B}\ (\land\mathsf{R}\
(f,g))&&(f:S\mid\Gamma,A,B,\Delta\vdash
A^{\prime},g:S\mid\Gamma,A,B,\Delta\vdash B^{\prime})\\\ \lor\mathsf{L}\
(\mathsf{ex}_{\\_}{A,B}\ f,\mathsf{ex}_{\\_}{A,B}\
g)&\circeq&\mathsf{ex}_{\\_}{A,B}\ (\lor\mathsf{L}\
(f,g))&&(f:A^{\prime}\mid\Gamma,A,B,\Delta\vdash
C,g:B^{\prime}\mid\Gamma,A,B,\Delta\vdash C)\\\ \lor\mathsf{R}_{i}\
(\mathsf{ex}_{\\_}{A,B}\ f)&\circeq&\mathsf{ex}_{\\_}{A,B}\
(\lor\mathsf{R}_{i}\ f)&&(f:S\mid\Gamma,A,B\vdash A^{\prime})\\\
\mathsf{ex}_{\\_}{A,B}(\mathsf{ex}_{\\_}{A^{\prime},B^{\prime}}f)&\circeq&\mathsf{ex}_{\\_}{A^{\prime},B^{\prime}}(\mathsf{ex}_{\\_}{A,B}f)&&(f:S\mid\Gamma,A,B,\Delta,A^{\prime},B^{\prime},\Lambda\vdash
C)\end{array}$

The first equation states that swapping the same two formulae twice yields the
same result as doing nothing. The second equation corresponds to the Yang-
Baxter equation. The remaining equations are permutative conversions. We left
out permutative conversions describing the relationship between $\mathsf{ex}$
and the rules $\mathsf{pass}$, $\mathsf{IL}$, $\otimes\mathsf{L}$ and
$\otimes\mathsf{R}$, which can be found in [25, Fig. 2].

The resulting sequent calculus enjoys categorical semantics in distributive
skew _symmetric_ monoidal categories, that possess a natural isomorphism
$s_{\\_}{A,B,C}:A\otimes(B\otimes C)\to A\otimes(C\otimes B)$ representing a
form of “skew symmetry” involving three objects instead of two [7].

The focused sequent calculus is extended with a new phase
$\vdash_{\\_}\mathsf{C}$ (for ‘context‘) where the exchange rule can be
applied. Rule $\otimes\mathsf{L}$ has to be modified, since we need to give
the possibility to move the formula $B$ to a different position in the
context.

$\begin{array}[]{c}S\mid\Gamma,A\raisebox{-1.5pt}[0.5pt]{\hskip
1.0pt\vdots\hskip
1.0pt}\Delta,\Lambda\vdash_{\\_}{\mathsf{C}}CS\mid\Gamma\raisebox{-1.5pt}[0.5pt]{\hskip
1.0pt\vdots\hskip 1.0pt}\Delta,A,\Lambda\vdash_{\\_}{\mathsf{C}}C\qquad
S\mid\quad\raisebox{-1.5pt}[0.5pt]{\hskip 1.0pt\vdots\hskip
1.0pt}\Gamma\vdash_{\\_}{\mathsf{C}}CS\mid\Gamma\vdash_{\\_}{\mathsf{RI}}C\qquad
A\otimes B\mid\Gamma\vdash_{\\_}{\mathsf{LI}}PA\mid
B\raisebox{-1.5pt}[0.5pt]{\hskip 1.0pt\vdots\hskip
1.0pt}\Gamma\vdash_{\\_}{\mathsf{C}}P\end{array}$

Root-first proof search now begins in the new phase $\vdash_{\\_}\mathsf{C}$,
where formulae in context are permuted. We start with a sequent
$S\mid\Gamma\raisebox{-1.5pt}[0.5pt]{\hskip 1.0pt\vdots\hskip
1.0pt}\quad\vdash_{\\_}{\mathsf{C}}C$ and end with a sequent
$S\mid\quad\raisebox{-1.5pt}[0.5pt]{\hskip 1.0pt\vdots\hskip
1.0pt}\Gamma^{\prime}\vdash_{\\_}{\mathsf{C}}C$ where $\Gamma^{\prime}$ is a
permutation of $\Gamma$. In the process, the context is divided into two parts
$\Gamma\raisebox{-1.5pt}[0.5pt]{\hskip 1.0pt\vdots\hskip 1.0pt}\Delta$, where
the formulae in $\Gamma$ are ready to be moved while those in $\Delta$ have
already been placed in their final position. Once all formulae in $\Gamma$
have been moved, we switch to phase $\vdash_{\\_}\mathsf{RI}$ with an
application of rule $\mathsf{RI}2\mathsf{C}$. Note that sequents in phase
$\vdash_{\\_}\mathsf{C}$ are not marked by list of tags, since after the
application of right non-invertible rules there is no need to further permute
formulae in context. Moreover, no new formulae can appear in context via
applications of rule $\otimes\mathsf{L}$, since the stoup is irreducible at
this point.

As already mentioned, rule $\otimes\mathsf{L}$ has been modified. Its premise
is now a sequent in phase $\vdash_{\\_}\mathsf{C}$, which allows a further
application of $\mathsf{ex}$ for the relocation of the formula $B$ to a
different position in the context.

###  5.3 Linear implication

Finally, we consider a deductive system for a skew version of Lambek calculus
with additive conjunction and disjunction. This is obtained by extending the
sequent calculus in (1) with a linear implication $\multimap$ and two
introduction rules:

$\begin{array}[]{c}A\multimap B\mid\Gamma,\Delta\vdash
C\lx@proof@logical@and-\mid\Gamma\vdash AB\mid\Delta\vdash C\qquad
S\mid\Gamma\vdash A\multimap BS\mid\Gamma,A\vdash B\end{array}$

The presence of $\multimap$ requires the extension of the congruence relation
$\circeq$ with additional generating equations: an $\eta$-conversion and more
permutative conversions.

$\small\begin{array}[]{rlll}\mathsf{ax}_{\\_}{A\multimap
B}&\circeq{\multimap}\mathsf{R}\text{ }({\multimap}\mathsf{L}\text{
}(\mathsf{pass}\text{ }\mathsf{ax}_{\\_}{A},\mathsf{ax}_{\\_}{B}))\\\
\otimes\mathsf{R}\text{ }({\multimap}\mathsf{L}\text{
}(f,g),h)&\circeq{\multimap}\mathsf{L}\text{ }(f,\otimes\mathsf{R}\text{
}(g,h))&&(f:{-}\mid\Gamma\vdash A^{\prime},g:B^{\prime}\mid\Delta\vdash
A,h:{-}\mid\Lambda\vdash B)\\\ \mathsf{pass}\text{
}({\multimap}\mathsf{R}\text{ }f)&\circeq{\multimap}\mathsf{R}\text{
}(\mathsf{pass}\text{ }f)&&(f:A^{\prime}\mid\Gamma,A\vdash B)\\\
\mathsf{IL}\text{ }({\multimap}\mathsf{R}\text{
}f)&\circeq{\multimap}\mathsf{R}\text{ }(\mathsf{IL}\text{
}f)&&(f:{-}\mid\Gamma,A\vdash B)\\\ \otimes\mathsf{L}\text{
}({\multimap}\mathsf{R}\text{ }f)&\circeq{\multimap}\mathsf{R}\text{
}(\otimes\mathsf{L}\text{ }f)&&(f:A^{\prime}\mid B^{\prime},\Gamma,A\vdash
B)\\\ {\multimap}\mathsf{L}\text{ }(f,{\multimap}\mathsf{R}\text{
}g)&\circeq{\multimap}\mathsf{R}\text{ }({\multimap}\mathsf{L}\text{
}(f,g))&&(f:{-}\mid\Gamma\vdash A^{\prime},g:B^{\prime}\mid\Delta,A\vdash
B)\\\ \land\mathsf{L}_{i}\ ({\multimap}\mathsf{R}\
f)&\circeq{\multimap}\mathsf{R}\ (\land\mathsf{L}_{i}\
f)&&(f:A^{\prime}\mid\Gamma,A\vdash B)\\\ \lor\mathsf{L}\
({\multimap}\mathsf{R}\ f,{\multimap}\mathsf{R}\
g)&\circeq{\multimap}\mathsf{R}\ (\lor\mathsf{L}\
(f,g))&&(f:A^{\prime}\mid\Gamma,A\vdash B,g:B^{\prime}\mid\Gamma,A\vdash B)\\\
\lor\mathsf{R}_{i}\ ({\multimap}\mathsf{L}\
(f,g))&\circeq{\multimap}\mathsf{L}\ (f,\lor\mathsf{R}_{i}\
g)&&(f:-\mid\Gamma\vdash A,g:B\mid\Delta\vdash A^{\prime})\end{array}$

The sequent calculus enjoys categorical semantics in skew monoidal categories
with binary products and coproducts, which moreover are endowed with a _closed
structure_ , i.e. a functor
$\multimap:\mathbb{C}^{\mathsf{op}}\times\mathbb{C}\rightarrow\mathbb{C}$
forming an adjunction ${-}\otimes B\dashv B\multimap{-}$ for all objects $B$
[19]. There is no need to require left-distributivity, since this can now be
proved using the adjunction and the universal property of coproducts.

Notice that, in non-commutative linear logic, there exist two distinct linear
implications, also called left and right residuals [14]. Our calculus includes
a single implication $\multimap$. We currently do not know whether the
inclusion of the second implication to our logic is a meaningful addition nor
whether it corresponds to some particular categorical notion.

We now discuss the extension of the focused sequent calculus. This is more
complicated than the extensions considered in Sections 5.1 and 5.2. In order
to understand the increased complexity, let us include the two new rules
${\multimap}\mathsf{R}$ and ${\multimap}\mathsf{L}$ in the “naive” focused
sequent calculus in (3). The right $\multimap$-rule is invertible, so it
belongs to phase $\vdash_{\\_}\mathsf{RI}$, while the left rule is not, so it
goes in phase $\vdash_{\\_}\mathsf{F}$.

$\begin{array}[]{c}A\multimap
B\mid\Gamma,\Delta\vdash_{\\_}\mathsf{F}P\lx@proof@logical@and-\mid\Gamma\vdash_{\\_}\mathsf{RI}AB\mid\Delta\vdash_{\\_}\mathsf{LI}P\qquad
S\mid\Gamma\vdash_{\\_}\mathsf{RI}A\multimap
BS\mid\Gamma,A\vdash_{\\_}\mathsf{RI}B\end{array}$

As we know, this calculus is too permissive, and the inclusion of the above
rules increases the non-deterministic choices in proof search even further. As
a strategy for taming non-determinism, as before we decide to prioritize left
non-invertible rules over right non-invertible ones. So we need to think of
all possible situations when a right non-invertible rule must be applied
before a left non-invertible one. The presence of $\multimap$ creates two new
possibilities: $(i)$ ${\multimap}\mathsf{L}$ splits the context differently in
different premises, or $(ii)$ left non-invertible rules manipulate formulae
that have been moved to the context by applications of
${\multimap}\mathsf{R}$. To understand these situations, let us look at two
examples.

As an example of situation $(i)$, consider the sequent
$\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I},Y\vdash_{\\_}\mathsf{F}(\mathsf{I}\land\mathsf{I})\otimes
Y$ and the following proof:

$\small\begin{array}[]{c}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I},Y\vdash_{\\_}\mathsf{F}(\mathsf{I}\land\mathsf{I})\otimes
Y\lx@proof@logical@and\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{RI}\mathsf{I}\land\mathsf{I}\lx@proof@logical@and\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{RI}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{F}\mathsf{I}\lx@proof@logical@and-\mid\mathsf{I}\vdash_{\\_}\mathsf{RI}\mathsf{I}-\mid\mathsf{I}\vdash_{\\_}\mathsf{F}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{F}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{F}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{RI}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{F}\mathsf{I}\lx@proof@logical@and-\mid\quad\vdash_{\\_}\mathsf{RI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{F}\mathsf{I}\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\mathsf{I}\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\mathsf{I}\vdash_{\\_}\mathsf{F}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{LI}\mathsf{I}-\mid\quad\vdash_{\\_}\mathsf{F}\mathsf{I}-\mid
Y\vdash_{\\_}\mathsf{RI}Y-\mid
Y\vdash_{\\_}\mathsf{F}YY\mid\quad\vdash_{\\_}\mathsf{LI}YY\mid\quad\vdash_{\\_}\mathsf{F}Y\end{array}$
(8)

Here $\otimes\mathsf{R}$ must be applied first, before
${\multimap}\mathsf{L}$. In the proofs of the two premises of
$\land\mathsf{R}$, which prove the same sequent
$\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash_{\\_}\mathsf{RI}\mathsf{I}$,
rule ${\multimap}\mathsf{L}$ splits the context in different ways: in the left
branch the unit $\mathsf{I}$ in context is sent to the left premise, while in
the right branch it goes to the right premise. If the application of the rule
${\multimap}\mathsf{L}$ would have split the context in the same way, then we
could have applied ${\multimap}\mathsf{L}$ before $\otimes\mathsf{R}$.

For $(ii)$, consider sequents ${-}\mid Y\vdash_{\\_}{\mathsf{F}}(X\multimap
X)\otimes Y$ and $X\multimap Y\mid Z\vdash_{\\_}{\mathsf{F}}(X\multimap
Y)\otimes Z$ with proofs:

${-}\mid Y\vdash_{\\_}{\mathsf{F}}(X\multimap X)\otimes
Y\lx@proof@logical@and{-}\mid\quad\vdash_{\\_}{\mathsf{RI}}X\multimap X{-}\mid
X\vdash_{\\_}{\mathsf{RI}}X{-}\mid
X\vdash_{\\_}{\mathsf{F}}XX\mid\quad\vdash_{\\_}{\mathsf{LI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}X{-}\mid
Y\vdash_{\\_}{\mathsf{RI}}Y{-}\mid
Y\vdash_{\\_}{\mathsf{F}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y$
---
$X\multimap Y\mid Z\vdash_{\\_}{\mathsf{F}}(X\multimap Y)\otimes
Z\lx@proof@logical@and X\multimap
Y\mid\quad\vdash_{\\_}{\mathsf{RI}}X\multimap YX\multimap Y\mid
X\vdash_{\\_}{\mathsf{RI}}YX\multimap Y\mid
X\vdash_{\\_}{\mathsf{F}}Y\lx@proof@logical@and{-}\mid
X\vdash_{\\_}{\mathsf{RI}}X{-}\mid
X\vdash_{\\_}{\mathsf{F}}XX\mid\quad\vdash_{\\_}{\mathsf{LI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}XY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y{-}\mid
Z\vdash_{\\_}{\mathsf{RI}}Z{-}\mid
Z\vdash_{\\_}{\mathsf{F}}ZZ\mid\quad\vdash_{\\_}{\mathsf{LI}}ZZ\mid\quad\vdash_{\\_}{\mathsf{F}}Z$
---
(9)

In the first derivation, rule $\mathsf{pass}$ in the left branch of
$\otimes\mathsf{R}$ cannot be moved to the bottom of the proof tree, since
formula $X$ is not yet in context, it becomes available only after the
application of ${\multimap}\mathsf{R}$. Analogously, in the second derivation,
rule ${\multimap}\mathsf{L}$ in the left branch of $\otimes\mathsf{R}$ cannot
be moved at the bottom, since the formula $X$ that it sends to the left
premise appears in context only after the application of
${\multimap}\mathsf{R}$.

This motivates the addition of two new tags, corresponding to the two
situations previously discussed: on top of
$\mathbb{P},\mathbb{C}_{1},\mathbb{C}_{2}$ and $\mathbb{R}$, a tag could
either be of the form $\Gamma$, for each context $\Gamma$, or of the form
$\bullet$. The validity condition for list of tags needs to be updated. A list
of tags $l$ is now valid if it is non-empty and either $(i)$ $\mathbb{R}\in
l$, $(ii)$ both $\mathbb{C}_{1}\in l$ and $\mathbb{C}_{2}\in l$, $(iii)$ there
exist contexts $\Gamma,\Gamma^{\prime}$ such that $\Gamma\in l$,
$\Gamma^{\prime}\in l$ and $\Gamma\neq\Gamma^{\prime}$, or $(iv)$ $\bullet\in
l$. Following [21], on top of tag annotations for sequents, we also require
tag annotations for formulae in context. There is only one tag $\bullet$ for
formulae. The tag on the formula $A^{\bullet}$ means that $A$ has been
previously moved to the context by an application of ${\multimap}\mathsf{R}$
in phase $\vdash^{l}_{\\_}\mathsf{RI}$.

Here are the inference rules of the focused sequent calculus with linear
implication:

$\\!\\!\\!\\!\\!\begin{array}[]{lc}\text{(right
invertible)}&\begin{tabular}[]{l}$S\mid\Gamma\vdash^{l_{\\_}1?,l_{\\_}2?}_{\\_}{\mathsf{RI}}A\land
B\lx@proof@logical@and
S\mid\Gamma\vdash^{l_{\\_}1?}_{\\_}{\mathsf{RI}}AS\mid\Gamma\vdash^{l_{\\_}2?}_{\\_}{\mathsf{RI}}B$
\quad$S\mid\Gamma\vdash^{l?}_{\\_}{\mathsf{RI}}A\multimap
BS\mid\Gamma,A^{\bullet?}\vdash^{l?}_{\\_}{\mathsf{RI}}B$
\quad$S\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{RI}}PS\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{LI}}P$\end{tabular}\\\\[10.0pt]
\text{(left
invertible)}&\begin{tabular}[]{l}$\mathsf{I}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P{-}\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$
\qquad$A\otimes B\mid\Gamma\vdash_{\\_}{\mathsf{LI}}PA\mid
B,\Gamma\vdash_{\\_}{\mathsf{LI}}P$\\\ $A\lor
B\mid\Gamma\vdash_{\\_}\mathsf{LI}P\lx@proof@logical@and
A\mid\Gamma\vdash_{\\_}\mathsf{LI}PB\mid\Gamma\vdash_{\\_}\mathsf{LI}P$
\qquad$T\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{LI}}PT\mid\Gamma\vdash^{t?}_{\\_}{\mathsf{F}}P$\end{tabular}\\\\[10.0pt]
\text{(focusing)}&\begin{tabular}[]{l}${-}\mid
A^{\bullet?},\Gamma\vdash^{t?}_{\\_}{\mathsf{F}}P\lx@proof@logical@and
A\mid\Gamma^{\circ}\vdash_{\\_}{\mathsf{LI}}P\text{if }A^{\bullet?}=A\text{
then }(t\text{ does not exist or }t=\mathbb{P})\text{ else
}t=\bullet$\end{tabular}\\\\[10.0pt] \lx@intercol\hfil
X\mid\quad\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}X\qquad{-}\mid\quad\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}\mathsf{I}\qquad
A\land
B\mid\Gamma\vdash^{\mathbb{C}_{1}?}_{\\_}{\mathsf{F}}PA\mid\Gamma^{\circ}\vdash_{\\_}{\mathsf{LI}}P\qquad
A\land
<EMAIL_ADDRESS>\lx@intercol\hfil
T\mid\Gamma,\Delta\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}A\otimes
B\lx@proof@logical@and
T\mid\Gamma^{\circ}\vdash^{l}_{\\_}{\mathsf{RI}}A{-}\mid\Delta^{\circ}\vdash_{\\_}{\mathsf{RI}}Bl\
\text{valid}\;T\mid\Gamma\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}A\lor
B\lx@proof@logical@and T\mid\Gamma^{\circ}\vdash^{l}_{\\_}{\mathsf{RI}}Al\
\text{valid}\;T\mid\Gamma\vdash^{\mathbb{R}?}_{\\_}{\mathsf{F}}A\lor
B\lx@proof@logical@and T\mid\Gamma^{\circ}\vdash^{l}_{\\_}{\mathsf{RI}}Bl\
<EMAIL_ADDRESS>\lx@intercol\hfil A\multimap
B\mid\Gamma,\Delta^{\bullet},\Lambda\vdash^{t?}_{\\_}{\mathsf{F}}P\lx@proof@logical@and-\mid\Gamma,\Delta^{\circ}\vdash_{\\_}{\mathsf{RI}}AB\mid\Lambda^{\circ}\vdash_{\\_}{\mathsf{LI}}P\text{if
}\Delta^{\bullet}\text{ is empty then }(t\text{ does not exist or
}t=\Gamma)\text{ else }t=\bullet\hfil\lx@intercol\end{array}$ (10)

Again $P$ indicates a non-negative formula, which now means that its principal
connective is neither $\land$ nor $\multimap$. The notation $\Gamma^{\bullet}$
means that all the formulae in $\Gamma$ are tagged, while $\Gamma^{\circ}$
indicates that all the tags on formulae in $\Gamma$ have been erased. We write
$A^{\bullet?}$ to denote $A$ if the formula appears in an untagged sequent and
$A^{\bullet}$ if it appears in a sequent marked with a list of tags $l$ or a
single tag $t$.

Tags of the form $t=\Gamma$ are used to record different splitting of context
in applications of ${\multimap}\mathsf{L}$, while tag $t=\bullet$ marks when
rule ${\multimap}\mathsf{L}$ sends tagged formulae to the left premise and
when rule $\mathsf{pass}$ moves a tagged formula to the stoup.

Rule ${\multimap}\mathsf{R}$ moves a formula $A$ from the succedent to the
right end of the context. If its conclusion is marked by a list of tags $l$,
then $A$ is also tagged with $\bullet$.

The side condition in rule ${\multimap}\mathsf{L}$ should be read as follows.
The tagged context $\Delta^{\bullet}$ starts with the leftmost tagged formula
in the sequent. If $\Delta^{\bullet}$ is empty, then the sequent is either
untagged (so there is no $t$) or the tag $t$ is equal to $\Gamma$. If
$\Delta^{\bullet}$ is non-empty, then $t=\bullet$. In particular,
$\Delta^{\bullet}$ contains at least one tagged formula, which must have
appeared in context from an application of ${\multimap}\mathsf{R}$. If
$\Delta^{\bullet}$ is empty and $t=\Gamma$, no new (meaning: tagged with
$\bullet$) formula is moved to the left premise. If $t=\Gamma$ then we are
performing proof search inside the premise of a right non-invertible rule and
$t$ belongs to some valid list of tags $l$. List $l$ could be valid because of
a different branch in the proof tree where ${\multimap}\mathsf{L}$ is also
applied but the context has been split differently (so its tag would be
$\Gamma^{\prime}$ for some $\Gamma\not=\Gamma^{\prime}$).

Rule $\mathsf{pass}$ has a similar side condition to ${\multimap}\mathsf{L}$.
If $A$ does not have a tag, then the sequent is also untagged or the tag $t$
is equal to $\mathbb{P}$. If $A$ has tag $\bullet$, then $t$ must also be
$\bullet$. In other words, if $t=\bullet$ then the formula that
$\mathsf{pass}$ moves to the stoup must also be tagged with $\bullet$, i.e.
must have been added to the context by an application of
${\multimap}\mathsf{R}$.

We can reconstruct the derivation in (8) within the focused sequent calculus
with tags in (10).

$\small\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{RI}}(\mathsf{I}\land\mathsf{I})\otimes
Y\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{F}}(\mathsf{I}\land\mathsf{I})\otimes
Y\lx@proof@logical@and\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash^{{[\
]},{[\mathsf{I}]}}_{\\_}{\mathsf{RI}}\mathsf{I}\land\mathsf{I}\lx@proof@logical@and\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash^{{[\
]}}_{\\_}{\mathsf{RI}}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash^{{[\
]}}_{\\_}{\mathsf{F}}\mathsf{I}\lx@proof@logical@and-\mid\quad\vdash_{\\_}{\mathsf{RI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}\mathsf{I}\mid\mathsf{I}\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\mathsf{I}\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\mathsf{I}\vdash_{\\_}{\mathsf{F}}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash^{{[\mathsf{I}]}}_{\\_}{\mathsf{RI}}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}\vdash^{{[\mathsf{I}]}}_{\\_}{\mathsf{F}}\mathsf{I}\lx@proof@logical@and-\mid\mathsf{I}\vdash_{\\_}{\mathsf{RI}}\mathsf{I}-\mid\mathsf{I}\vdash_{\\_}{\mathsf{F}}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}-\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}-\mid
Y\vdash_{\\_}{\mathsf{RI}}Y-\mid
Y\vdash_{\\_}{\mathsf{F}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y$

The proofs with tags of the derivations in (9) are analogous to the ones
described in [21].

Proving completeness of the extended focused sequent calculus is more involved
than in the absence of implication. Concretely, the complication resides in
stating and proving the analog of Proposition 4.4. First, define an operation
$\mathsf{impconj}(A)$ which produces a list of pairs of lists of formulae and
formulae as follows:

$\begin{array}[]{rll}\mathsf{impconj}(A)&=\mathsf{impconj}(A^{\prime}),\mathsf{impconj}(B^{\prime})&\text{when
}A=A^{\prime}\land B^{\prime}\\\
\mathsf{impconj}(A)&=((A^{\prime},\Gamma^{\prime}_{\\_}1),B^{\prime}_{\\_}1),\dots,((A^{\prime},\Gamma^{\prime}_{\\_}n),B^{\prime}_{\\_}n)&\text{when
}A=A^{\prime}\multimap B^{\prime}\text{ and}\\\
&&\mathsf{impconj}(B^{\prime})=([(\Gamma^{\prime}_{\\_}1,B^{\prime}_{\\_}1),\dots,(\Gamma^{\prime}_{\\_}n,B^{\prime}_{\\_}n)])\\\
\mathsf{impconj}(A)&=([\ ],A)&\text{otherwise}\end{array}$

For example, $\mathsf{impconj}(A\multimap(B\multimap(X\land(C\lor
D)\land(Y\multimap Z))))=[([A,B],X),([A,B],C\lor D),([A,B,Y],Z)]$.

The statement of Proposition 4.4 for the focused sequent calculus in (10) then
becomes:

######  Proposition 5.1.

The following rules

$\begin{array}[]{c}S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
B[S\mid\Gamma,\Gamma^{\prime}_{\\_}i\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs\quad
S\mid\Gamma\vdash_{\\_}{\mathsf{LI}}A\lor
B[S\mid\Gamma,\Gamma^{\prime\prime}_{\\_}i\vdash_{\\_}{\mathsf{LI}}Q_{\\_}i]_{\\_}{i\in[1,\dots,m]}fs\\\
S\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{LI}}A\otimes
B^{\prime}\lx@proof@logical@and[S\mid\Gamma,\Gamma^{\prime}_{\\_}i\vdash_{\\_}{\mathsf{LI}}P_{\\_}i]_{\\_}{i\in[1,\dots,n]}fs-\mid\Delta\vdash_{\\_}{\mathsf{RI}}B^{\prime}\end{array}$

are admissible, where
$\mathsf{impconj}(A)=[(\Gamma^{\prime}_{\\_}1,P_{\\_}1),\dots,(\Gamma^{\prime}_{\\_}n,P_{\\_}n)]$
and
$\mathsf{impconj}(B)=[(\Gamma^{\prime\prime}_{\\_}1,Q_{\\_}1),\dots,(\Gamma^{\prime\prime}_{\\_}m,Q_{\\_}m)]$.

##  6 Conclusion

The paper presents a sequent calculus for a semi-associative and semi-unital
logic, extending the system introduced in [24] with additive conjunction and
disjunction. Categorical models of this calculus are skew monoidal categories
with binary products and coproducts, and the tensor product preserves
coproducts on the left: $(A+B)\otimes C\cong(A\otimes C)+(B\otimes C)$.
Derivations in the sequent calculus are equated by a congruence relation
$\circeq$ and canonical representatives of each $\circeq$-equivalence class
can be computed in a separate sequent calculus of normal forms, that we dubbed
“focused” due to its phase separation similar to the one in Andreoli’s
technique [4]. It should be remarked that, differently from Andreoli’s
focusing, and also the maximally multi-focused sequent calculus for skew
monoidal closed categories by one of the authors [26], we do not insist on
keeping the focus during the synchronous phase of proof search, and we always
privilege the application of left non-invertible rules over right non-
invertible ones. In order to achieve completeness wrt. the sequent calculus,
the focused system employs a system of tag annotations providing explicit
justifications for cases where right non-invertible rules must be applied
before the left non-invertible ones.

The focused sequent calculus is a concrete presentation of the free
distributive skew monoidal category on the set of atomic formulae. Therefore
the normalization/focusing algorithm determines a procedure for solving the
coherence problem of distributive skew monoidal categories.

In the final part of the paper, we have looked at extensions of the logic with
additive units, a skew exchange rule in the style of Bourke and Lack [7], and
linear implication. This section still needs to be formalized in Agda, which
will be our forthcoming step.

This paper takes one step further in a large project aiming at modularly
analyzing proof systems with categorical models given by categories with skew
structure [27, 24, 23, 22, 25, 21]. We are interested in looking for
applications of these systems to combinatorics and linguistics, following the
initial investigation by Zeilberger [27] and Moortgat [16].

We are interested in using the techniques introduced in this paper to design a
calculus of normal forms for the classical linear logic MALL. In the latter
setting, the situation is more complicated than the skew one, since there
could be more than two formulae that can be under focus in the synchronous
phase. We expect our calculus to give an alternative presentation of the
maximally multi-focused proofs of Chaudhuri et al. [9].

#### Acknowledgements

This work was supported by the Estonian Research Council grant PSG749 and the
ESF funded Estonian IT Academy research measure (project
2014-2020.4.05.19-0001).

## References

  * [1]
  * [2] Vito Michele Abrusci (1990): _Non-commutative Intuitionistic Linear Logic_.  Mathematical Logic Quarterly 36(4), pp. 297–318, 10.1002/malq.19900360405.
  * [3] Thorsten Altenkirch, James Chapman & Tarmo Uustalu (2015): _Monads Need Not Be Endofunctors_.  Logical Methods in Computer Science 11(1):3, 10.2168/lmcs-11(1:3)2015.
  * [4] Jean-Marc Andreoli (1992): _Logic Programming with Focusing Proofs in Linear Logic_.  Journal of Logic and Computation 2(3), pp. 297–347, 10.1093/logcom/2.3.297.
  * [5] John Bourke (2017): _Skew structures in 2-category theory and homotopy theory_.  Journal of Homotopy and Related Structures 12(1), pp. 31–81, 10.1007/s40062-015-0121-z.
  * [6] John Bourke & Stephen Lack (2018): _Skew Monoidal Categories and Skew Multicategories_.  Journal of Algebra 506, pp. 237–266, 10.1016/j.jalgebra.2018.02.039.
  * [7] John Bourke & Stephen Lack (2020): _Braided Skew Monoidal Categories_.  Theory and Applications of Categories 35(2), pp. 19–63.  Available at http://www.tac.mta.ca/tac/volumes/35/2/35-02abs.html.
  * [8] Michael Buckley, Richard Garner, Stephen Lack & Ross Street (2015): _The Catalan Simplicial Set_.  Mathematical Proceedings of Cambridge Philosophical Society 158(2), pp. 211–222, 10.1017/s0305004114000498.
  * [9] Kaustuv Chaudhuri, Dale Miller & Alexis Saurin (2008): _Canonical Sequent Proofs via Multi-Focusing_.  In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri & Luke Ong, editors: Proceedings of 5th IFIP International Conference on Theoretical Computer Science, TCS 2008, International Federation of Information Processing Series 273, Springer, pp. 383–396, 10.1007/978-0-387-09680-3_26.
  * [10] Jean-Yves Girard (1987): _Linear Logic_.  Theoretical Computer Science 50, pp. 1–102, 10.1016/0304-3975(87)90045-4.
  * [11] Jean-Yves Girard (1991): _A New Constructive Logic: Classical Logic_.  Mathematical Structures in Computer Science 1(3), pp. 255–296, 10.1017/s0960129500001328.
  * [12] Stephen Lack & Ross Street (2012): _Skew Monoidales, Skew Warpings and Quantum Categories_.  Theory and Applications of Categories 26, pp. 385–402.  Available at http://www.tac.mta.ca/tac/volumes/26/15/26-15abs.html.
  * [13] Stephen Lack & Ross Street (2014): _Triangulations, Orientals, and Skew Monoidal Categories_.  Advances in Mathematics 258, pp. 351–396, 10.1016/j.aim.2014.03.003.
  * [14] Joachim Lambek (1958): _The Mathematics of Sentence Structure_.  American Mathematical Monthly 65(3), pp. 154–170, 10.2307/2310058.
  * [15] Saunders Mac Lane (1963): _Natural Associativity and Commutativity_.  Rice University Studies 49(4), pp. 28–46.  Available at http://hdl.handle.net/1911/62865.
  * [16] Michael Moortgat (2020): _The Tamari order for $D^{3}$ and derivability in semi-associative Lambek-Grishin Calculus_.  Talk at 16th Workshop on Computational Logic and Applications, CLA 2020.  Slides available at: http://cla.tcs.uj.edu.pl/history/2020/pdfs/CLAslidesMoortgat.pdf.
  * [17] Richard Moot & Christian Retoré (2012): _The Logic of Categorial Grammars - A Deductive Account of Natural Language Syntax and Semantics_.  Lecture Notes in Computer Science 6850, Springer, 10.1007/978-3-642-31555-8.
  * [18] Gabriel Scherer & Ddier Rémy (2015): _Which Simple Types Have a Unique Inhabitant?_ In: Proceedings of 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, ACM, pp. 243–255, 10.1145/2784731.2784757.
  * [19] Ross Street (2013): _Skew-Closed Categories_.  Journal of Pure and Applied Algebra 217(6), pp. 973–988, 10.1016/j.jpaa.2012.09.020.
  * [20] Kornél Szlachányi (2012): _Skew-Monoidal Categories and Bialgebroids_.  Advances in Mathematics 231(3–4), pp. 1694–1730, 10.1016/j.aim.2012.06.027.
  * [21] Tarmo Uustalu, Niccolò Veltri & Cheng-Syuan Wan (2022): _Proof Theory of Skew Non-Commutative MILL_.  In Andrzej Indrzejczak & Michal Zawidzki, editors: Proceedings of 10th International Conference on Non-classical Logics: Theory and Applications, NCL 2022, Electronic Proceedings in Theoretical Computer Science 358, Open Publishing Association, pp. 118–135, 10.4204/eptcs.358.9.
  * [22] Tarmo Uustalu, Niccoló Veltri & Noam Zeilberger (2021): _Deductive Systems and Coherence for Skew Prounital Closed Categories_.  In Claudio Sacerdoti Coen & Alwen Tiu, editors: Proceedings of 15th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Electronic Proceedings in Theoretical Computer Science 332, Open Publishing Association, pp. 35–53, 10.4204/eptcs.332.3.
  * [23] Tarmo Uustalu, Niccolò Veltri & Noam Zeilberger (2021): _Proof Theory of Partially Normal Skew Monoidal Categories_.  In David I. Spivak & Jamie Vicary, editors: Proceedings of 3rd Annual International Applied Category Theory Conference 2020, ACT 2020, Electronic Proceedings in Theoretical Computer Science 333, Open Publishing Association, pp. 230–246, 10.4204/eptcs.333.16.
  * [24] Tarmo Uustalu, Niccolò Veltri & Noam Zeilberger (2021): _The Sequent Calculus of Skew Monoidal Categories_.  In Claudio Casadio & Philip J. Scott, editors: Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, Outstanding Contributions to Logic 20, Springer, pp. 377–406, 10.1007/978-3-030-66545-611.
  * [25] Niccolò Veltri (2021): _Coherence via Focusing for Symmetric Skew Monoidal Categories_.  In Alexandra Silva, Renata Wassermann & Ruy de Queiroz, editors: Proceedings of 27th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2021, Lecture Notes in Computer Science 13028, Springer, pp. 184–200, 10.1007/978-3-030-88853-412.
  * [26] Niccolò Veltri (2023): _Maximally Multi-focused Proofs for Skew Non-Commutative MILL_.  In Helle Hvid Hansen, Andre Scedrov & Ruy J. G. B. de Queiroz, editors: Proceedings of 29th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2023, Lecture Notes in Computer Science 13923, Springer, pp. 377–393, 10.1007/978-3-031-39784-4_24.
  * [27] Noam Zeilberger (2019): _A Sequent Calculus for a Semi-Associative Law_.  Logical Methods in Computer Science 15(1):9, 10.23638/lmcs-15(1:9)2019.