# Proof Theory of Skew Non-Commutative $\mathtt{MILL}$

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

Monoidal closed categories naturally model $\mathtt{NMILL}$, non-commutative
multiplicative intuitionistic linear logic: the monoidal unit and tensor
interpret the multiplicative verum and conjunction; the internal hom
interprets linear implication. In recent years, the weaker notion of (left)
skew monoidal closed category has been proposed by Ross Street, where the
three structural laws of left and right unitality and associativity are not
required to be invertible, they are merely natural transformations with a
specific orientation. A question arises: is it possible to find a logic which
is naturally modelled by skew monoidal closed categories? We answer positively
by introducing a cut-free sequent calculus for a skew version of
$\mathtt{NMILL}$ that is a presentation of the free skew monoidal closed
category. We study the proof-theoretic semantics of the sequent calculus by
identifying a calculus of derivations in normal form, obtained from an
adaptation of Andreoli’s focusing technique to the skew setting. The resulting
focused sequent calculus peculiarly employs a system of tags for keeping track
of new formulae appearing in the antecedent and appropriately reducing non-
deterministic choices in proof search. Focusing solves the coherence problem
for skew monoidal closed categories by exhibiting an effective procedure for
deciding equality of maps in the free such category.

##  1 Introduction

It is a widely known fact from the late 80s/early 90s that symmetric monoidal
closed categories model $\mathtt{MILL}$, multiplicative intuitionistic linear
logic, whose logical connectives comprise multiplicative verum $\mathsf{I}$
and conjunction $\otimes$ and linear implication $\multimap$ [19]. Probably
lesser-known, though a quite straightforward variation of this observation
(which actually predated the inception of linear logic altogether) is the fact
that (not necessarily symmetric) monoidal biclosed categories provide a
semantics for the non-commutative variant of $\mathtt{MILL}$ (for which we use
the abbreviation $\mathtt{NMILL}$) [2], where the structural rule of exchange
is absent and there are two ordered implications $\multimap$ and  $\multimap$
. The sequent calculus of $\mathtt{NMILL}$ without verum is known as the
_Lambek calculus_ [17]. From the beginning, the Lambek calculus has been
employed in formal investigations of natural languages [16]. Lambek refers to
the implications $\multimap$ and  $\multimap$ as residuals, and monoidal
biclosed categories without unit are therefore also called residual
categories. By dropping one of the ordered implications of $\mathtt{NMILL}$,
one obtains a fragment of the logic interpretable in every monoidal closed
category.

In recent years, Ross Street introduced the new notion of (left) skew monoidal
closed categories [21]. These are a weakening of monoidal closed categories:
their structure includes a unit $\mathsf{I}$, a tensor $\otimes$, an internal
hom $\multimap$ and an adjunction relating the latter two operations, as in
usual non-skew monoidal closed categories. The difference lies in the three
structural laws of left and right unitality, $\lambda_{\\_}A:\mathsf{I}\otimes
A\to A$ and $\rho_{\\_}A:A\to A\otimes\mathsf{I}$, and associativity,
$\alpha_{\\_}{A,B,C}:(A\otimes B)\otimes C\to A\otimes(B\otimes C)$, which are
usually required to be natural isomorphisms, but in the skew variant are
merely natural transformations with the specified orientation. Street
originally proposed this weaker notion to reach better understanding of and to
fix a famous imbalance, first noticed by Eilenberg and Kelly [10], present in
the adjunction relating monoidal and closed structures [21, 24]. In the last
decade, skew monoidal closed categories, together with their non-closed/non-
monoidal variants, have been thoroughly studied, with applications ranging
from algebra and homotopy theory to programming language semantics [22, 14,
15, 3, 7, 5, 6, 23].

A question arises naturally: is it possible to characterize skew monoidal
closed categories as categorical models of (a deductive system for) a logic?
This paper provides a positive answer to this question. We introduce a cut-
free sequent calculus for a skew variant of $\mathtt{NMILL}$, which we name
$\mathtt{SkNMILL}$. Sequents are peculiarly defined as triples
$S\mid\Gamma\vdash A$, where the succedent is a single formula $A$ (as in
intuitionistic linear logic), but the antecedent is divided into two parts: an
optional formula $S$, called the _stoup_ [11], and an ordered list of formulae
$\Gamma$, the _context_. Inference rules are similar to the ones of
$\mathtt{NMILL}$ but with specific structural restrictions for accurately
capturing the structural laws of skew monoidal closed categories and nothing
more. In particular, and in analogy with $\mathtt{NMILL}$, the structural
rules of weakening, contraction and exchange are all absent. Sets of
derivations are quotiented by a congruence relation $\circeq$, carefully
crafted to serve as the sequent-calculus counterpart of the equational theory
of skew monoidal closed categories. The design of the sequent calculus draws
inspiration from, and further advance, the line of work of Uustalu, Veltri and
Zeilberger on proof systems for various categories with skew structure: skew
semigroup (a.k.a. the Tamari order) [29], skew monoidal (non-closed) [27, 26]
and its symmetric variant [28], skew prounital (non-monoidal) closed [25].

The metatheory of $\mathtt{SkNMILL}$ is developed in two different but related
directions:

  * •

We study the categorical semantics of $\mathtt{SkNMILL}$, by showing that the
cut-free sequent calculus admits an interpretation of its formulae,
derivations and equational theory $\circeq$ in any skew monoidal closed
category as soon as one fixes the intended interpretation in it of the atoms.
Moreover, the sequent calculus is the initial model in this semantics; it is a
particular presentation of the free skew monoidal closed category. This can be
shown directly or by first introducing a Hilbert-style calculus which directly
presents the free skew monoidal closed category and proving that derivations
in the two calculi are in a bijective correspondence.

  * •

We investigate the proof-theoretic semantics of $\mathtt{SkNMILL}$, by
defining a normalization strategy for sequent calculus derivations wrt. the
congruence $\circeq$, when the latter is considered as a locally confluent and
strongly normalizing reduction relation. The shape of normal forms is made
explicit in a new _focused_ sequent calculus, whose derivations act as the
target of the normalization procedure. The sequent calculus is “focused” in
the sense of Andreoli [4], as it describes a sound and complete root-first
proof search strategy for the original sequent calculus. The focused system in
this paper builds on and elaborates the previously developed normal forms for
skew monoidal categories [27] and skew prounital closed categories [25]. The
presence of both positive ($\mathsf{I}$,$\otimes$) and negative ($\multimap$)
connectives requires some extra care in the design of the proof search
strategy, reflected in the focused sequent calculus, in particular when aiming
at removing all possible undesired non-deterministic choices leading to
$\circeq$-equivalent derivations that can arise during proof search. This is
technically realized in the focused sequent calculus by peculiar employment of
a system of _tags_ for keeping track of new formulae appearing in the
antecedent. The focused sequent calculus can also be seen as an optimized
presentation of the initial model for $\mathtt{SkNMILL}$, and as such can be
used for solving the coherence problem in an effective way: deciding equality
of two maps in this model (or equality of two canonical maps in every model)
is equivalent to deciding _syntactic_ equality of the corresponding focused
derivations.

The equivalence between sequent calculus derivations, quotiented by the
equivalence relation $\circeq$, and focused derivations, that we present in
Section 4, has been formalized in the Agda proof assistant. The associated
code is available at https://github.com/niccoloveltri/code-skewmonclosed.

##  2 A Sequent Calculus for Skew Non-Commutative $\mathtt{MILL}$

We begin by introducing a sequent calculus for a skew variant of non-
commutative multiplicative intuitionistic linear logic ($\mathtt{NMILL}$),
that we call $\mathtt{SkNMILL}$.

Formulae are inductively generated by the grammar $A,B::=X\ |\ \mathsf{I}\ |\
A\otimes B\ |\ A\multimap B$, where $X$ comes from a fixed set $\mathsf{At}$
of atoms, $\mathsf{I}$ is a multiplicative verum, $\otimes$ is a
multiplicative conjunction and $\multimap$ is a linear implication.

A sequent is a triple of the form $S\mid\Gamma\vdash A$, where the succedent
$A$ is a single formula (as in $\mathtt{NMILL}$) and the antecedent is divided
in two parts: an optional formula $S$, called _stoup_ [11], and an ordered
list of formulae $\Gamma$, called _context_. The peculiar design of sequents,
involving the presence of the stoup in the antecedent, comes from previous
work on deductive systems with skew structure by Uustalu, Veltri and
Zeilberger [27, 26, 25, 28]. The metavariable $S$ always denotes a stoup,
i.e., $S$ can be a single formula or empty, in which case we write $S={-}$,
and $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 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\\\
\mathsf{I}\mid\Gamma\vdash C{-}\mid\Gamma\vdash C\qquad A\otimes
B\mid\Gamma\vdash CA\mid B,\Gamma\vdash
C\qquad{-}\mid\quad\vdash\mathsf{I}\qquad S\mid\Gamma,\Delta\vdash A\otimes
B\lx@proof@logical@and S\mid\Gamma\vdash A{-}\mid\Delta\vdash B\end{array}$
(1)

The inference rules in (1) are reminiscent of the ones in the sequent calculus
for $\mathtt{NMILL}$ [2], but there are some crucial differences.

  1. 1.

The left logical rules $\mathsf{IL}$, $\otimes\mathsf{L}$ and
${\multimap}\mathsf{L}$, read bottom-up, are only allowed to be applied on the
formula in the stoup position. In particular, there is no general way to
remove a unit $\mathsf{I}$ nor decompose a tensor $A\otimes B$ if these
formulae are located in the context and not in the stoup (we will see in (5)
that something can actually be done to deal with implications $A\multimap B$
in the context).

  2. 2.

The right tensor rule $\otimes\mathsf{R}$, read bottom-up, splits the
antecedent of the conclusion between the two premises whereby the formula in
the stoup, in case such a formula is present, has to be moved to the stoup of
the first premise. In particular, the stoup formula of the conclusion cannot
be moved to the antecedent of the second premise even if $\Gamma$ is chosen to
be empty.

  3. 3.

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

  4. 4.

The logical connectives of $\mathtt{NMILL}$ typically include two ordered
implications $\multimap$ and  $\multimap$ , which are two variants of linear
implication arising from the removal of the exchange rule from intuitionistic
linear logic. In $\mathtt{SkNMILL}$ only one of the ordered implications (the
left implication $\multimap$) is present. It is currently not clear to us
whether the inclusion of the second implication to our logic is a meaningful
addition and whether it corresponds to some particular categorical notion.

The restrictions in 1–4 are essential for precisely capturing all the features
of skew monoidal closed categories and nothing more, as we discuss in Section
3. Notice also that, similarly to the case of $\mathtt{NMILL}$, all structural
rules of weakening, contraction and exchange 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$.

Examples of valid derivations in the sequent calculus, corresponding to the
structural laws $\lambda$, $\rho$ and $\alpha$ of skew monoidal closed
categories (see Definition 3.1) are given below.

$\small\begin{array}[]{c@{\;\quad}cc}(\lambda)&(\rho)&(\alpha)\\\
\mathsf{I}\otimes A\mid\quad\vdash A\mathsf{I}\mid A\vdash A{-}\mid A\vdash
AA\mid\quad\vdash A&A\mid\quad\vdash A\otimes\mathsf{I}\lx@proof@logical@and
A\mid\quad\vdash A{-}\mid\quad\vdash\mathsf{I}&(A\otimes B)\otimes
C\mid\quad\vdash A\otimes(B\otimes C)A\otimes B\mid C\vdash A\otimes(B\otimes
C)A\mid B,C\vdash A\otimes(B\otimes C)\lx@proof@logical@and A\mid\quad\vdash
A{-}\mid B,C\vdash B\otimes CB\mid C\vdash B\otimes C\lx@proof@logical@and
B\mid\quad\vdash B{-}\mid C\vdash CC\mid\quad\vdash C\end{array}$ (2)

Examples of non-derivable sequents include the “inverses” of the conclusions
in (2), obtained by swapping the stoup formula with the succedent formula.
More precisely, the three sequents $X\mid~{}\vdash\mathsf{I}\otimes X$,
$X\otimes\mathsf{I}\mid~{}\vdash X$ and $X\otimes(Y\otimes
Z)\mid~{}\vdash(X\otimes Y)\otimes Z$ do not have any derivation. All possible
attempts of constructing a valid derivation for each of them end in failure.

$\small\begin{array}[]{ccc}(\lambda^{-1})&(\rho^{-1})&(\alpha^{-1})\\\\[6.0pt]
X\mid~{}\vdash\mathsf{I}\otimes X\lx@proof@logical@and
X\mid~{}\vdash\mathsf{I}{-}\mid~{}\vdash X&X\otimes\mathsf{I}\mid\quad\vdash
XX\mid\mathsf{I}\vdash X??&X\otimes(Y\otimes Z)\mid~{}\vdash(X\otimes
Y)\otimes ZX\mid Y\otimes Z\vdash(X\otimes Y)\otimes Z??\\\
(\text{$\otimes\mathsf{R}$ sends $X$ to 1st premise})&(\text{$\mathsf{IL}$
does not act on $\mathsf{I}$ in context})&(\text{$\otimes\mathsf{L}$ does not
act on $\otimes$ in context})\end{array}$

Analogously, the sequents $\mathsf{I}\multimap A\mid~{}\vdash A$ and
$(A\otimes B)\multimap C\mid~{}\vdash A\multimap(B\multimap C)$ are derivable,
while generally their “inverses” are not. Also, a derivation of
$A\mid~{}\vdash B$ always yields a derivation of $\mathsf{I}\mid~{}\vdash
A\multimap B$, but there are $A$, $B$ such that $\mathsf{I}\mid~{}\vdash
A\multimap B$ is derivable while $A\mid~{}\vdash B$ is not (take, e.g., $A=X$,
$B=\mathsf{I}\otimes X$).

Sets of derivations are quotiented by a congruence relation $\circeq$,
generated by the following pairs of derivations.

$\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\multimap
B}&\circeq{\multimap}\mathsf{R}\text{ }({\multimap}\mathsf{L}\text{
}(\mathsf{pass}\text{ }\mathsf{ax}_{\\_}{A},\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}\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,g:B\mid\Delta\vdash C,h:{-}\mid\Lambda\vdash
D\\\ \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\mid B,\Gamma,C\vdash D\\\
{\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\end{array}$ (3)

The first three equations above are $\eta$-conversions, completely
characterizing the $\mathsf{ax}$ rule on 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 skew monoidal closed categories, introduced in Definition 3.1. The
subsystem of equations involving only $(\mathsf{I},\otimes)$ originated in
[27] while the subsystem involving only $\multimap$ is from [25].

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

The two cut rules satisfy a large number of $\circeq$-equations, see e.g, [27,
Figures 5 and 6] for the list of such equations not involving $\multimap$. In
particular, the cut rules respect $\circeq$, in the sense that
$\mathsf{scut}(f,g)\circeq\mathsf{scut}(f^{\prime},g^{\prime})$ whenever
$f\circeq f^{\prime}$ and $g\circeq g^{\prime}$, and similarly for
$\mathsf{ccut}$.

Here are some other interesting admissible rules relevant for the metatheory
of this calculus.

  * •

The left rules for $\mathsf{I}$ and $\otimes$ are invertible up to $\circeq$,
and similarly the right rule for $\multimap$. No other rule is invertible; in
particular, the passivation rule $\mathsf{pass}$ is not.

  * •

Applications of the invertible left logical rules can be iterated, and
similarly for the invertible right ${\multimap}\mathsf{R}$ rule, resulting in
the two admissible rules

$[\\![S\mid\Gamma]\\!]_{\\_}{\otimes}\mid\Delta\vdash
CS\mid\Gamma,\Delta\vdash C\qquad S\mid\Gamma\vdash[\\![\Delta\mid
C]\\!]_{\\_}{\multimap}S\mid\Gamma,\Delta\vdash C$ (4)

The interpretation of antecedents $[\\![S\mid\Gamma]\\!]_{\\_}{\otimes}$ in
(4) is the formula obtained by substituting the separator $\mid$ and the
commas with tensors, $[\\![S\mid
A_{\\_}1,\dots,A_{\\_}n]\\!]_{\\_}{\otimes}=(\dots(([\\![S\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}\otimes
A_{\\_}1)\otimes A_{\\_}2)\dots)\otimes A_{\\_}n$, where the interpretation of
stoups is defined by
$[\\![{-}\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}=\mathsf{I}$
and
$[\\![A\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}=A$.
Dually, the formula $[\\![\Delta\mid C]\\!]_{\\_}{\multimap}$ in (4) is
obtained by substituting $\mid$ and commas with implications:
$[\\![A_{\\_}1,\dots,A_{\\_}n\mid
C]\\!]_{\\_}{\multimap}=A_{\\_}1\multimap(A_{\\_}2\multimap(\dots\multimap(A_{\\_}n\multimap
C)))$.

  * •

Another left implication rule, acting on a formula $A\multimap B$ in the
context, is derivable using cut:

$\small\\!\\!\\!\begin{tabular}[]{l}$S\mid\Delta_{\\_}0,A\multimap
B,\Gamma,\Delta_{\\_}1\vdash C\lx@proof@logical@and{-}\mid\Gamma\vdash
AfS\mid\Delta_{\\_}0,B,\Delta_{\\_}1\vdash
Cg$\end{tabular}{=}\begin{tabular}[]{l}$S\mid\Delta_{\\_}0,A\multimap
B,\Gamma,\Delta_{\\_}1\vdash C\lx@proof@logical@and{-}\mid A\multimap
B,\Gamma\vdash BA\multimap B\mid\Gamma\vdash
B\lx@proof@logical@and{-}\mid\Gamma\vdash AfB\mid~{}\vdash
BS\mid\Delta_{\\_}0,B,\Delta_{\\_}1\vdash Cg$\end{tabular}$ (5)

####  $\mathtt{SkNMILL}$ as a Logic of Resources

Similarly to other substructural logics like $\mathtt{MILL}$ and
$\mathtt{NMILL}$,$\mathtt{SkNMILL}$ can be understood as a logic of resources.
Under this perspective, formulae of the sequent calculus in (1) correspond to
resources: atomic formulae are primitive resources; the formula $A\otimes B$
is read as “resource $A$ before resource $B$”; $\mathsf{I}$ is “nothing”; the
formula $A\multimap B$ can be described as a method for turning the resource
$A$ into the resource $B$ (if $A\multimap B$ is provided before $A$). As in
other substructural systems lacking the structural rules of weakening and
contraction, all resources are one-time usable.

The antecedent of a sequent contains the resources at hand, while the
succedent contains the resource that needs to be produced. A derivation is
then a particular procedure for turning the available resources into the goal
resource. Under this interpretation, derivations are naturally read and built
from the conclusion to the premises. Resources in the antecedent are ordered,
meaning that they need to be utilized in the order they appear. If a resource
$A$ precedes another resource $B$ in the antecedent, then $A$ must be consumed
before $B$. The stoup position, when it is non-empty, contains the resource
that is immediately usable. The resources in the context can only be spent
after the resource in the stoup has been used. Time flows bottom-up in proof
trees, from conclusion to premises, and the proof of a left premise always
takes place before the proof of the right premise.

The context shares similarities with the stack (and also the queue) data
structure. If, at some moment, there is no resource immediately consumable, as
stoup is empty, then the next available resource can be promoted to this
status: the top (left-most position) of the context can be popped and moved to
the stoup by the $\mathsf{pass}$ rule. A new resource can be pushed to the
bottom (right-most position) of the context using the ${\multimap}\mathsf{R}$
rule. Using the $\otimes\mathsf{L}$ rule, the immediately usable resource
$A\otimes B$ can be decomposed into two parts $A$ and $B$; the resource $A$
becomes immediately usable (remains in the stoup) while $B$ will become usable
next (is pushed to the top of the context). The resource $\mathsf{I}$, if
immediately usable, can be disposed by the rule $\mathsf{IL}$, making it
possible to pop the next available resource from the context. The resource
$\mathsf{I}$ can always be produced free-of-charge with the rule
$\mathsf{IR}$.

In the rule ${\multimap}\mathsf{L}$, we have a resource $A\multimap B$
immediately usable and need to produce $C$. This gives us access to the
resource $B$, but only after we have produced $A$ by spending a part of the
other resources available. The context is split into two parts $\Gamma$ and
$\Delta$. The first part $\Gamma$ is used to make $A$. Once this has been
accomplished, production of $C$ can continue with $B$ immediately usable and
$\Delta$ usable thereafter.

The succedent of the rule $\otimes\mathsf{R}$ is of the form $A\otimes B$,
which implies that first $A$ and then $B$ need to be produced. This justifies
the splitting of the context into two parts again: the first part $\Gamma$,
consisting of resources that can be spent sooner, is used to produce $A$ in
the left premise, while the second part $\Delta$ is spent subsequently for
production of $B$ in the right premise. Crucially, and this is one central
“skew” aspect of $\mathtt{SkNMILL}$, if we have a resource immediately usable
in the stoup $S$, this must be spent for the construction of the first
resource we are required to produce, namely $A$; it cannot be saved for
producing $B$ even if producing $A$ needs no resources at all.

The other central “skew” aspect of $\mathtt{SkNMILL}$ is that the left rules
only act on stoup formulae. This can be understood under the resources-as-
formulae correspondence to say that we are only allowed to decompose an
available resource when it has become immediately consumable (has entered the
stoup). We are precluded from decomposing the resources in the context ahead
of their time.

##  3 Categorical Semantics via Skew Monoidal Closed Categories

Next we present a categorical semantics for the sequent calculus of
$\mathtt{SkNMILL}$.

######  Definition 3.1.

A _(left) skew monoidal closed category_ $\mathbb{C}$ is a category with a
unit object $\mathsf{I}$ and two functors
$\otimes:\mathbb{C}\times\mathbb{C}\rightarrow\mathbb{C}$ and
$\multimap:\mathbb{C}^{\mathsf{op}}\times\mathbb{C}\rightarrow\mathbb{C}$
forming an adjunction ${-}\otimes B\dashv B\multimap{-}$ for all $B$, 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
[18]:

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

The notion of skew monoidal closed category admits other equivalent
characterizations [21, 24]. Tuples of natural transformations
$(\lambda,\rho,\alpha)$ are in bijective correspondence with tuples of
(extra)natural transformations $(j,i,L)$ typed $j_{\\_}A:\mathsf{I}\to
A\multimap A$, $i_{\\_}A:\mathsf{I}\multimap A\to A$,
$L_{\\_}{A,B,C}:B\multimap C\to(A\multimap B)\multimap(A\multimap C)$.
Moreover, $\alpha$ and $L$ are interdefinable with a natural transformation
$\mathsf{p}$ typed $\mathsf{p}_{\\_}{A,B,C}:(A\otimes B)\multimap
C\to\linebreak A\multimap(B\multimap C)$, embodying an internal version of the
adjunction between $\otimes$ and $\multimap$.

######  Example 3.1 (from [24]).

This example explains how to turn every categorical model of $\mathtt{MILL}$
extended with a $\Box$-like modality of necessity (or something like the
exponential modality $!$ of linear logic) into a model of $\mathtt{SkNMILL}$.
Let $(\mathbb{C},\mathsf{I},\otimes,\multimap)$ be a (possibly symmetric)
monoidal closed category and let $(D,\varepsilon,\delta)$ be a comonad on
$\mathbb{C}$, where $\varepsilon_{\\_}A:D\,A\to A$ and $\delta_{\\_}A:D\,A\to
D\,(D\,A)$ are the counit and comultiplication of $D$. Suppose the comonad $D$
to be _lax monoidal_ , i.e., coming with a map $\mathsf{e}:\mathsf{I}\to D\,I$
and a natural transformation $\mathsf{m}$ typed
$\mathsf{m}_{\\_}{A,B}:D\,A\otimes D\,B\to D\,(A\otimes B)$ cohering suitably
with $\lambda$, $\rho$, $\alpha$, $\varepsilon$ and $\delta$. Then
$\mathbb{C}$ has also a skew monoidal closed structure
$(\mathsf{I},\otimes^{D},\;\textsuperscript{$D$}\\!\\!\multimap)$ given by
$A\otimes^{D}B=A\otimes D\,B$ and $B\;\textsuperscript{$D$}\\!\\!\multimap
C=D\,B\multimap C$. The adjunction ${-}\otimes D\,B\dashv D\,B\multimap{-}$
yields an adjunction ${-}\otimes^{D}B\dashv
B\;\textsuperscript{$D$}\\!\\!\multimap{-}$. The structural laws are

$\begin{array}[]{c}\lambda^{D}_{\\_}A\,=\,\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
18.66733pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{I}\otimes
D\,A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
23.9241pt\raise 6.49167pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.29167pt\hbox{$\scriptstyle{\mathsf{I}\otimes\varepsilon_{\\_}A}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 54.66733pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
54.66733pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{I}\otimes
A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
90.61174pt\raise 6.53055pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.33055pt\hbox{$\scriptstyle{\lambda_{\\_}A}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 117.77841pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
117.77841pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces\hskip
42.67912pt\rho^{D}_{\\_}A\,=\,\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
15.81546pt\raise 6.49167pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.29167pt\hbox{$\scriptstyle{\rho_{\\_}A}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 42.75pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
42.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A\otimes\mathsf{I}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
77.9583pt\raise 5.68333pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.1pt\hbox{$\scriptstyle{A\otimes\mathsf{e}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 105.86108pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
105.86108pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\otimes
D\,\mathsf{I}}$}}}}}}}\ignorespaces}}}}\ignorespaces\\\
\begin{array}[]{rcl}\alpha^{D}_{\\_}{A,B,C}&=&\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
41.05927pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{(A\otimes D\,B)\otimes
D\,C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
45.63486pt\raise 6.725pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.52501pt\hbox{$\scriptstyle{(A\otimes
DB)\otimes\delta_{\\_}C}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern
101.05927pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
101.05927pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{(A\otimes D\,B)\otimes
D\,(D\,C)}$}}}}}}}\ignorespaces}}}}\ignorespaces\\\ &&\hskip
42.67912pt\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
4.40236pt\raise 6.725pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.52501pt\hbox{$\scriptstyle{\alpha_{\\_}{A,DB,D(DC)}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 63.0pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
63.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\otimes(D\,B\otimes
D\,(D\,C))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
170.80661pt\raise 6.49167pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.29167pt\hbox{$\scriptstyle{A\otimes\mathsf{m}_{\\_}{B,DC}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 223.1199pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
223.1199pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\otimes D\,(B\otimes
D\,C)}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{array}\end{array}$

$(\mathbb{C},\mathsf{I},\otimes^{D},\;\textsuperscript{$D$}\\!\\!\multimap)$
is a “genuine” skew monoidal closed category, in the sense that $\lambda^{D}$,
$\rho^{D}$ and $\alpha^{D}$ are all generally non-invertible.

######  Definition 3.2.

A _(strict) skew monoidal closed functor_ $F:\mathbb{C}\rightarrow\mathbb{D}$
between skew monoidal closed categories
$(\mathbb{C},\mathsf{I},\otimes,\multimap)$ and
$(\mathbb{D},\mathsf{I}^{\prime},\otimes^{\prime},\multimap^{\prime})$ is a
functor from $\mathbb{C}$ to $\mathbb{D}$ satisfying
$F\mathsf{I}=\mathsf{I}^{\prime}$, $F(A\otimes B)=\linebreak
FA\otimes^{\prime}FB$ and $F(A\multimap B)=FA\multimap^{\prime}FB$, also
preserving the structural laws $\lambda$, $\rho$ and $\alpha$ on the nose.

The formulae, derivations and the equivalence relation $\circeq$ of the
sequent calculus for $\mathtt{SkNMILL}$ determine a skew monoidal closed
category $\mathsf{FSkMCl}(\mathsf{At}$).

######  Definition 3.3.

The skew monoidal closed category $\mathsf{FSkMCl}(\mathsf{At})$ has as
objects formulae; the operations $\mathsf{I}$, $\otimes$ and $\multimap$ 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 given by derivations in (2).

This is a good definition since all equations of a skew monoidal closed
category turn out to hold.

Skew monoidal closed categories with given interpretations of atoms into them
constitute models of the sequent calculus of $\mathtt{SkNMILL}$, in the sense
specified by the following theorem.

######  Theorem 3.1.

Let $\mathbb{D}$ be a skew monoidal closed category. Given
$F_{\\_}{\mathsf{At}}:\mathsf{At}\rightarrow|\mathbb{D}|$ providing evaluation
of atomic formulae as objects of $\mathbb{D}$, there exists a skew monoidal
closed functor $F:\mathsf{FSkMCl}(\mathsf{At})\rightarrow\mathbb{D}$.

###### Proof.

Let $(\mathbb{D},\mathsf{I}^{\prime},\otimes^{\prime},\multimap^{\prime})$ be
a skew monoidal closed category. The action on object $F_{\\_}0$ of the
functor $F$ is defined by induction on the input formula:

$F_{\\_}0X=F_{\\_}{\mathsf{At}}X\qquad
F_{\\_}0\mathsf{I}=\mathsf{I}^{\prime}\qquad F_{\\_}0(A\otimes
B)=F_{\\_}0A\otimes^{\prime}F_{\\_}0B\qquad F_{\\_}0(A\multimap
B)=F_{\\_}0A\multimap^{\prime}F_{\\_}0B$

The encoding of antecedents as formulae
$[\\![S\mid\Gamma]\\!]_{\\_}{\otimes}$, introduced immediately after (4), can
be replicated also in $\mathbb{D}$ by simply replacing $\mathsf{I}$ and
$\otimes$ with $\mathsf{I}^{\prime}$ and $\otimes^{\prime}$ in the definition,
where now $S$ is an optional object and $\Gamma$ is a list of objects of
$\mathbb{D}$. Using this encoding, it is possible to show that each rule in
(1) is derivable in $\mathbb{D}$. As an illustrative case, consider the rule
$\mathsf{pass}$. Assume given a map
$f:[\\![A\mid\Gamma]\\!]_{\\_}{\otimes^{\prime}}\to C$ in $\mathbb{D}$. Then,
assuming $\Gamma=A_{\\_}1,\dots,A_{\\_}n$, we can define the passivation of
$f$ typed $[\\![{-}\mid A,\Gamma]\\!]_{\\_}{\otimes^{\prime}}\to C$ as

$\textstyle{(\dots((\mathsf{I}^{\prime}\otimes^{\prime}A_{\\_}1)\otimes^{\prime}A_{\\_}2)\dots)\otimes^{\prime}A_{\\_}n\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\dots(\lambda^{\prime}_{\\_}{A_{\\_}1}\otimes^{\prime}A_{\\_}2)\dots)\otimes^{\prime}A_{\\_}n}$$\textstyle{(\dots(A_{\\_}1\otimes^{\prime}A_{\\_}2)\dots)\otimes^{\prime}A_{\\_}n\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{C}$

This implies the existence of a function $F_{\\_}1$, sending each derivation
$f:S\mid\Gamma\vdash A$ to a map $F_{\\_}1f:\linebreak
F_{\\_}0([\\![S\mid\Gamma]\\!]_{\\_}{\otimes})\to FA$ in $\mathbb{D}$, defined
by induction on the derivation $f$. When restricted to sequents of the form
$A\mid~{}\vdash B$, the function $F_{\\_}1$ provides the action on maps of
$F$. It is possible to show that $F$ preserves the skew monoidal closed
structure, so it is a skew monoidal closed functor. ∎

Moreover, the sequent calculus as a presentation of a skew monoidal closed
category is the _initial_ one among these models, or, equivalently,
$\mathsf{FSkMCl}(\mathsf{At})$ is the _free_ such category on the set
$\mathsf{At}$.

######  Theorem 3.2.

The skew monoidal closed functor $F$ constructed in Theorem 3.1 is the unique
one for which $F_{\\_}0X=F_{\\_}{\mathsf{At}}X$ for any atom $X$.

Alternatively, following the strategy of our previous papers [27, 26, 25, 28],
this result can be shown by going via a Hilbert-style deductive system that
directly presents the free skew monoidal closed category on $\mathsf{At}$. Its
formulae are the same of the sequent calculus, its sequents are pairs
$A\Rightarrow B$, with $A$ and $B$ single formulae. Derivations are generated
by the following rules, in which one can recognize all the structure of
Definition 3.1 (in particular $\pi$ and $\pi^{-1}$ are the adjunction data).

$\begin{array}[]{c}A\Rightarrow A\quad A\Rightarrow C\lx@proof@logical@and
A\Rightarrow BB\Rightarrow C\qquad A\otimes B\Rightarrow C\otimes
D\lx@proof@logical@and A\Rightarrow CB\Rightarrow D\qquad A\multimap
B\Rightarrow C\multimap D\lx@proof@logical@and C\Rightarrow AB\Rightarrow D\\\
\mathsf{I}\otimes A\Rightarrow A\quad A\Rightarrow
A\otimes\mathsf{I}\quad(A\otimes B)\otimes C\Rightarrow A\otimes(B\otimes
C)\qquad A\Rightarrow B\multimap CA\otimes B\Rightarrow C\quad A\otimes
B\Rightarrow CA\Rightarrow B\multimap C\end{array}$

There exists a congruence relation $\doteq$ on each set of derivations
$A\Rightarrow B$ with generators directly encoding the equations of the theory
of skew monoidal closed categories. With the Hilbert-style calculus in place,
one can show that there is a bijection between the set of derivations of the
sequent $A\mid~{}\vdash B$ modulo $\circeq$ and the set of derivations of the
sequent $A\Rightarrow B$ modulo $\doteq$.

##  4 Proof-Theoretic Semantics via Focusing

The equivalence relation $\circeq$ from (3) can also be viewed as an abstract
rewrite system, by orienting every equation from left to right. The resulting
rewrite system is locally confluent and strongly normalizing, thus confluent
with unique normal forms. Derivations in normal form thus correspond to
canonical representatives of $\circeq$-equivalence classes. These
representatives can be organized in a _focused sequent calculus_ in the sense
of [4], which describes, in a declarative fashion, a root-first proof search
strategy for the (original, unfocused) sequent calculus.

###  4.1 A First (Naïve) Focused Sequent Calculus

As a first attempt to focusing, we naïvely merge together the rules of the
focused sequent calculi of skew monoidal categories [27] and skew prounital
closed categories [25]. In the resulting calculus, sequents have one of 4
possible subscript annotations, corresponding to 4 different phases of proof
search: $\mathsf{RI}$ for ‘right invertible’, $\mathsf{LI}$ for ‘left
invertible‘, $\mathsf{P}$ for ‘passivation‘ and $\mathsf{F}$ for ‘focusing‘.
We will see soon that this focused sequent calculus is too permissive, in the
sense that two distinct derivations in the focused system can correspond to
$\circeq$-equivalent sequent calculus derivations.

$\begin{array}[]{lc}\text{(right
invertible)}&\begin{tabular}[]{l}$S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A\multimap
BS\mid\Gamma,A\vdash_{\\_}{\mathsf{RI}}B$
\qquad$S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}PS\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$\end{tabular}\\\\[9.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$
\qquad$T\mid\Gamma\vdash_{\\_}{\mathsf{LI}}PT\mid\Gamma\vdash_{\\_}{\mathsf{P}}P$\end{tabular}\\\\[9.0pt]
\text{(passivation)}&\begin{tabular}[]{l}${-}\mid
A,\Gamma\vdash_{\\_}{\mathsf{P}}PA\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$
\qquad$T\mid\Gamma\vdash_{\\_}{\mathsf{P}}PT\mid\Gamma\vdash_{\\_}{\mathsf{F}}P$\end{tabular}\\\
\text{(focusing)}&\\\ \lx@intercol\hfil\hskip
8.53581ptX\mid\quad\vdash_{\\_}{\mathsf{F}}X\quad{-}\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}\quad
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\quad
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\hfil\lx@intercol\end{array}$
(6)

In the rules above and the rest of the paper, the metavariable $P$ denotes a
_positive_ formula, i.e. $P\not=A\multimap B$, while metavariable $T$
indicates a _negative_ stoup, i.e. $T\not=\mathsf{I}$ and $T\not=A\otimes B$
($T$ can also be empty).

We explain the rules of the focused sequent calculus from the perspective of
root-first proof search. The starting phase is ‘right invertible‘
$\mathsf{RI}$.

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

We repeatedly apply the right invertible rule ${\multimap}\mathsf{R}$ with the
goal of reducing the succedent to a positive formula $P$. When the succedent
formula becomes positive, we move to phase $\mathsf{LI}$ via
$\mathsf{LI}2\mathsf{RI}$.

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

We repeatedly destruct the stoup formula via application of left invertible
rules $\otimes\mathsf{L}$ and $\mathsf{IL}$ with the goal of making it
negative. When this happens, we move to phase $\mathsf{P}$ via
$\mathsf{P}2\mathsf{LI}$.

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

We have the possibility of applying the passivation rule and move the leftmost
formula $A$ in the context to the stoup when the latter is empty. This allows
us to start decomposing $A$ using left invertible rules in phase
$\mathsf{LI}$. Otherwise, we move to phase $\mathsf{F}$ via
$\mathsf{F}2\mathsf{P}$.

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

We apply one of the four remaining rules $\mathsf{ax}$, $\mathsf{IR}$,
$\otimes\mathsf{R}$ or ${\multimap}\mathsf{L}$. The premises of
$\otimes\mathsf{R}$ are both in phase $\mathsf{RI}$ since $A$ and $B$ are
generic formulae, in particular they could be implications. The first premise
of ${\multimap}\mathsf{L}$ is in phase $\mathsf{RI}$ for the same reason while
the second premise is in $\mathsf{LI}$ because the succedent formula $P$ is
positive.

The focused calculus in (6) is sound and complete wrt. the sequent calculus in
(1) in regards to derivability, but not _equationally complete_ , i.e., there
exist $\circeq$-equivalent sequent calculus derivations which have multiple
distinct derivations using the rules in (6). In other words, the rules in (6)
are too permissive. They facilitate two forms of non-determinism in root-first
proof search that should not be there.

  1. (i)

The first premise of the $\otimes\mathsf{R}$ rule is in phase $\mathsf{RI}$,
since $A$ is potentially an implication which the invertible right rule
${\multimap}\mathsf{R}$ could act upon. Proof search for the first premise
eventually hits phase $\mathsf{P}$, when we have the possibility of applying
the $\mathsf{pass}$ rule if the stoup is empty. This implies the existence of
situations where either of the rules $\otimes\mathsf{R}$ and $\mathsf{pass}$
can be applied first, in both cases resulting in valid focused derivations. As
an example, consider the two distinct derivations of ${-}\mid
X,\Gamma,\Delta\vdash_{\\_}{\mathsf{P}}P\otimes C$ under assumptions
$f:X\mid\Gamma\vdash_{\\_}{\mathsf{LI}}P$ and
$g:{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}C$.

${-}\mid X,\Gamma,\Delta\vdash_{\\_}{\mathsf{P}}P\otimes
CX\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{LI}}P\otimes
CX\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{F}}P\otimes C\lx@proof@logical@and
X\mid\Gamma\vdash_{\\_}{\mathsf{RI}}PX\mid\Gamma\vdash_{\\_}{\mathsf{LI}}Pf{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}Cg$
${-}\mid X,\Gamma,\Delta\vdash_{\\_}{\mathsf{P}}P\otimes C{-}\mid
X,\Gamma,\Delta\vdash_{\\_}{\mathsf{F}}P\otimes C\lx@proof@logical@and{-}\mid
X,\Gamma\vdash_{\\_}{\mathsf{RI}}P{-}\mid
X,\Gamma\vdash_{\\_}{\mathsf{P}}PX\mid\Gamma\vdash_{\\_}{\mathsf{LI}}Pf{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}Cg$
---
(7)

Here and in the rest of the paper the rule $\mathsf{sw}$ above stands for a
sequence of (appropriately typed) phase switching inferences by
$\mathsf{LI}2\mathsf{RI}$, $\mathsf{P}2\mathsf{LI}$ and
$\mathsf{F}2\mathsf{P}$. The corresponding sequent calculus derivations are
equated by congruence relation $\circeq$ because of the 4th equation from (3),
i.e., the permutative conversion involving $\otimes\mathsf{R}$ and
$\mathsf{pass}$.

  2. (ii)

Rules $\otimes\mathsf{R}$ and ${\multimap}\mathsf{L}$ appear in the same phase
$\mathsf{F}$, though there are situations where both rules can be applied
first, which can lead to two distinct focused derivations. More precisely,
there are cases when $\otimes\mathsf{R}$ and ${\multimap}\mathsf{L}$ can be
interchangeably applied. As an example, consider the following two valid
derivations of $A\multimap
X\mid\Gamma,\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes D$ under the
assumption of $f:{-}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A$,
$g:X\mid\Delta\vdash_{\\_}{\mathsf{LI}}P$ and
$h:{-}\mid\Lambda\vdash_{\\_}{\mathsf{RI}}D$.

$A\multimap X\mid\Gamma,\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes
D\lx@proof@logical@and{-}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}AfX\mid\Delta,\Lambda\vdash_{\\_}{\mathsf{LI}}P\otimes
DX\mid\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes D\lx@proof@logical@and
X\mid\Delta\vdash_{\\_}{\mathsf{RI}}PX\mid\Delta\vdash_{\\_}{\mathsf{LI}}Pg{-}\mid\Lambda\vdash_{\\_}{\mathsf{RI}}Dh$
$A\multimap X\mid\Gamma,\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes
D\lx@proof@logical@and A\multimap
X\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{RI}}PA\multimap
X\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{F}}P\lx@proof@logical@and{-}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}AfX\mid\Delta\vdash_{\\_}{\mathsf{LI}}Pg{-}\mid\Lambda\vdash_{\\_}{\mathsf{RI}}Dh$
---
(8)

The corresponding sequent calculus derivations, at the same time, are
$\circeq$-equivalent because of the 7th equation from (3), the permutative
conversion for $\otimes\mathsf{R}$ and ${\multimap}\mathsf{L}$.

To get rid of type (i) undesired non-determinism, one might try an idea
similar to the one that works in the skew monoidal non-closed case [27],
namely, to prioritize $\mathsf{pass}$ over $\otimes\mathsf{R}$ by requiring
the first premise of the latter to be a sequent in phase $\mathsf{F}$. But
this does not do the right thing in the skew monoidal closed case. E.g., the
sequent ${-}\mid Y\vdash_{\\_}{\mathsf{F}}(X\multimap X)\otimes Y$ becomes
underivable while its counterpart is derivable in (1).

${-}\mid Y\vdash_{\\_}{\mathsf{F}}(X\multimap X)\otimes
Y\lx@proof@logical@and{-}\mid\quad\vdash_{\\_}{\mathsf{F}}X\multimap
X??{-}\mid Y\vdash_{\\_}{\mathsf{RI}}Y{-}\mid
Y\vdash_{\\_}{\mathsf{P}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y$

An impulsive idea for eliminating undesired non-determinism of type (ii) is to
prioritize the application of ${\multimap}\mathsf{L}$ over
$\otimes\mathsf{R}$, e.g., by forcing the application of
${\multimap}\mathsf{L}$ in phase $\mathsf{F}$ whenever the stoup formula is an
implication and restricting the application of $\otimes\mathsf{R}$ to sequents
where the stoup is empty or atomic. This too leads to an unsound calculus,
since the sequent $X\multimap Y\mid Z\vdash_{\\_}{\mathsf{F}}(X\multimap
Y)\otimes Z$, which has a derivable correspondent in (1), would not be
derivable by first applying the ${\multimap}\mathsf{L}$ rule.

$X\multimap Y\mid Z\vdash_{\\_}{\mathsf{F}}(X\multimap Y)\otimes
Z\lx@proof@logical@and{-}\mid\quad\vdash_{\\_}{\mathsf{RI}}X??Y\mid
Z\vdash_{\\_}{\mathsf{LI}}(X\multimap Y)\otimes ZY\mid
Z\vdash_{\\_}{\mathsf{F}}(X\multimap Y)\otimes Z\lx@proof@logical@and
Y\mid\quad\vdash_{\\_}{\mathsf{RI}}X\multimap YY\mid
X\vdash_{\\_}{\mathsf{RI}}Y??{-}\mid Z\vdash_{\\_}{\mathsf{RI}}Z{-}\mid
Z\vdash_{\\_}{\mathsf{P}}ZZ\mid\quad\vdash_{\\_}{\mathsf{LI}}ZZ\mid\quad\vdash_{\\_}{\mathsf{F}}Z$

Dually, prioritizing the application of $\otimes\mathsf{R}$ over
${\multimap}\mathsf{L}$ leads to similar issues, e.g., the sequent
$X\multimap(Y\otimes Z)\mid X\vdash_{\\_}\mathsf{F}Y\otimes Z$ would not be
derivable by first applying the $\otimes\mathsf{R}$ rule while its counterpart
is derivable in (1).

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

###  4.2 A Focused System with Tag Annotations

In order to eliminate undesired non-determinism of type (i) between
$\mathsf{pass}$ and $\otimes\mathsf{R}$, we need to restrict applications of
$\mathsf{pass}$ in the derivation of the first premise of an application of
$\otimes\mathsf{R}$. One way to achieve this is to force that such an
application of $\mathsf{pass}$ is allowed only if the leftmost formula of the
context is _new_ , in the sense that it was not already present in the context
before the $\otimes\mathsf{R}$ application. For example, with this restriction
in place, the application of $\mathsf{pass}$ in the 2nd derivation of (7)
would be invalid, since the formula $X$ was already present in context before
the application of $\otimes\mathsf{R}$.

Analogously, undesired non-determinism of type (ii) between
${\multimap}\mathsf{L}$ and $\otimes\mathsf{R}$ can be eliminated by
restricting applications of ${\multimap}\mathsf{L}$ after an application of
$\otimes\mathsf{R}$. This can be achieved by forcing the subsequent
application of ${\multimap}\mathsf{L}$ to split the context into two parts
$\Gamma,\Delta$ in such a way that $\Gamma$, i.e., the context of the first
premise, necessarily contains some _new_ formula occurrences that were not in
the context before the first $\otimes\mathsf{R}$ application. Under this
restriction, the application of ${\multimap}\mathsf{L}$ in the 2nd derivation
of (8) would become invalid, since all formulae in $\Gamma$ are already
present in context before the application of $\otimes\mathsf{R}$.

One way to distinguish between old and new formulae occurrences in the above
cases is to mark with a _tag_ $\bullet$ each new formula appearing in context
during the building of a focused derivation. We christen a formula occurrence
“new” whenever it is moved from the succedent to the context via an
application of the right implication rule ${\multimap}\mathsf{R}$. In order to
remember when we are building a derivation of a sequent arising as the first
premise of $\otimes\mathsf{R}$, in which the distinction between old and new
formula is relevant, we mark such sequents with a tag $\bullet$ as well. More
generally, we write $S\mid\Gamma\vdash^{x}_{\\_}{ph}C$ for a sequent that can
be untagged or tagged, i.e., the turnstile can be of the form
$\vdash_{\\_}{ph}$ or $\vdash^{\bullet}_{\\_}{ph}$, for
$ph\in\\{\mathsf{RI},\mathsf{LI},\mathsf{P},\mathsf{F}\\}$. This implies that
there are a total of eight sequent phases, corresponding to the possible
combinations of four subscript phases with the untagged/tagged state. In
tagged sequents $S\mid\Gamma\vdash_{\\_}{ph}^{\bullet}C$, the formulae in the
context $\Gamma$ can be untagged or tagged, i.e., they can be of the form $A$
or $A^{\bullet}$; to be precise, all untagged formulae in $\Gamma$ must
precede all tagged formulae (i.e., the context splits into untagged and tagged
parts and, instead of possibly tagged formulae, we could alternatively work
with contexts with two compartments). The formulae in the context of an
untagged sequent $S\mid\Gamma\vdash_{\\_}{ph}C$ must all be untagged (or,
alternatively, the tagged compartment must be empty). Given a context
$\Gamma$, we write $\Gamma^{\circ}$ for the same context where all tags have
been removed from the formulae in it.

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^{x}_{\\_}{\mathsf{RI}}A\multimap
BS\mid\Gamma,A^{x}\vdash^{x}_{\\_}{\mathsf{RI}}B$
\qquad$S\mid\Gamma\vdash^{x}_{\\_}{\mathsf{RI}}PS\mid\Gamma\vdash^{x}_{\\_}{\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$
\qquad$T\mid\Gamma\vdash^{x}_{\\_}{\mathsf{LI}}PT\mid\Gamma\vdash^{x}_{\\_}{\mathsf{P}}P$\end{tabular}\\\\[10.0pt]
\text{(passivation)}&\begin{tabular}[]{l}${-}\mid
A^{x},\Gamma\vdash^{x}_{\\_}{\mathsf{P}}PA\mid\Gamma^{\circ}\vdash_{\\_}{\mathsf{LI}}P$
\qquad$T\mid\Gamma\vdash^{x}_{\\_}{\mathsf{P}}PT\mid\Gamma\vdash^{x}_{\\_}{\mathsf{F}}P$\end{tabular}\\\\[10.0pt]
\text{(focusing)}&\begin{tabular}[]{l}$X\mid\quad\vdash^{x}_{\\_}{\mathsf{F}}X$
\qquad${-}\mid\quad\vdash^{x}_{\\_}{\mathsf{F}}\mathsf{I}$\end{tabular}\\\\[6.0pt]
\lx@intercol\hfil T\mid\Gamma,\Delta\vdash^{x}_{\\_}{\mathsf{F}}A\otimes
B\lx@proof@logical@and
T\mid\Gamma^{\circ}\vdash^{\bullet}_{\\_}{\mathsf{RI}}A{-}\mid\Delta^{\circ}\vdash_{\\_}{\mathsf{RI}}B\qquad
A\multimap
B\mid\Gamma,\Delta\vdash^{x}_{\\_}{\mathsf{F}}P\lx@proof@logical@and{-}\mid\Gamma^{\circ}\vdash_{\\_}{\mathsf{RI}}AB\mid\Delta^{\circ}\vdash_{\\_}{\mathsf{LI}}Px=\bullet\supset\bullet\in\Gamma\hfil\lx@intercol\end{array}$
(9)

Remember that $P$ is a positive formula and $T$ is a negative stoup. The side
condition in rule ${\multimap}\mathsf{L}$ reads: if $x=\bullet$, then some
formula in $\Gamma$ must be tagged. For the rule $\mathsf{pass}$ notice that,
if $x=\bullet$, it is actually forced that all formulae of $\Gamma$ are tagged
since the preceding context formula $A^{\bullet}$ is tagged. For the rules
$\otimes\mathsf{R}$ and ${\multimap}\mathsf{L}$ similarly notice that, if some
formula of $\Gamma$ is tagged, then all formulae of $\Delta$ must be tagged.

The rules in (9), when stripped of all the tags, are equivalent to the rules
in the naïve calculus (6). When building a derivation of an untagged sequent
$S\mid\Gamma\vdash_{\\_}\mathsf{RI}A$, the only possible way to enter a tagged
phase is via an application of the $\otimes\mathsf{R}$ rule, so that sequents
with turnstile marked $\vdash_{\\_}{ph}^{\bullet}$ denote the fact that we are
performing proof search for the first premise of an $\otimes\mathsf{R}$
inference (and the stoup is negative). The search for a proof of a tagged
sequent $T\mid\Gamma^{\circ}\vdash^{\bullet}_{\\_}\mathsf{RI}A$ proceeds as
follows:

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

We eagerly apply the right invertible rule ${\multimap}\mathsf{R}$ with the
goal of reducing $A$ to a positive formula $P$. All formulae that get moved to
the right end of the context are “new”, and are therefore marked with
$\bullet$. When the succedent formula becomes positive, we move to the tagged
$\mathsf{LI}$ phase via $\mathsf{LI}2\mathsf{RI}$.

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

Since $T$ is a negative stoup, we can only move to the tagged $\mathsf{P}$
phase via $\mathsf{P}2\mathsf{LI}$.

  * ($\vdash^{\bullet}_{\\_}\mathsf{P}$)

If the stoup is empty, we have the possibility of applying the $\mathsf{pass}$
rule and move the leftmost formula $A$ in the context to the stoup, but only
when this formula is marked by $\bullet$. This restriction makes it possible
to remove undesired non-determinism of type (i). We then strip the context of
all tags and jump to the untagged $\mathsf{LI}$ phase. If we do not (or
cannot) apply $\mathsf{pass}$, we move to the tagged $\mathsf{F}$ phase via
$\mathsf{F}2\mathsf{P}$.

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

The possible rules to apply (depending on the stoup and succedent formula) are
$\mathsf{ax}$, $\mathsf{IR}$, $\otimes\mathsf{R}$ or ${\multimap}\mathsf{L}$.
If we apply $\otimes\mathsf{R}$, we remove all tags from the context
$\Gamma,\Delta$ and move the first premise to the tagged $\mathsf{RI}$ phase
again. The tags are removed from the context in order to reset tracking of new
formulae. The most interesting case is ${\multimap}\mathsf{L}$, which can only
be applied if the $\Gamma$ part of the context $\Gamma,\Delta$ contains at
least one tagged formula. This side condition implements the restriction
allowing the elimination of undesired non-determinism of type (ii). All tags
are removed from $\Gamma,\Delta$ and proof search continues in the appropriate
untagged phases.

The employment of tag annotations eliminates the two types of undesired non-
determinism. For example, only one of the two derivations in (7) is valid
using the rules in (9), and similarly for (8).

$\small\begin{array}[]{cc}{-}\mid
X,\Gamma,\Delta\vdash_{\\_}{\mathsf{P}}P\otimes
CX\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{LI}}P\otimes
CX\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{F}}P\otimes C\lx@proof@logical@and
X\mid\Gamma\vdash^{\bullet}_{\\_}{\mathsf{RI}}PX\mid\Gamma\vdash^{\bullet}_{\\_}{\mathsf{LI}}Pf{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}Cg&{-}\mid
X,\Gamma,\Delta\vdash_{\\_}{\mathsf{P}}P\otimes C{-}\mid
X,\Gamma,\Delta\vdash_{\\_}{\mathsf{F}}P\otimes C\lx@proof@logical@and{-}\mid
X,\Gamma\vdash^{\bullet}_{\\_}{\mathsf{RI}}P{-}\mid
X,\Gamma\vdash^{\bullet}_{\\_}{\mathsf{P}}P??{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}Cg\\\
(\text{same derivation as in (\ref{eq:passtr})})&(\text{$\mathsf{pass}$ not
applicable since $X$ is not tagged})\\\\[10.0pt] A\multimap
X\mid\Gamma,\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes
D\lx@proof@logical@and{-}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}AfX\mid\Delta,\Lambda\vdash_{\\_}{\mathsf{LI}}P\otimes
DX\mid\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes D\lx@proof@logical@and
X\mid\Delta\vdash^{\bullet}_{\\_}{\mathsf{RI}}PX\mid\Delta\vdash^{\bullet}_{\\_}{\mathsf{LI}}Pg{-}\mid\Lambda\vdash_{\\_}{\mathsf{RI}}Dh&A\multimap
X\mid\Gamma,\Delta,\Lambda\vdash_{\\_}{\mathsf{F}}P\otimes
D\lx@proof@logical@and A\multimap
X\mid\Gamma,\Delta\vdash^{\bullet}_{\\_}{\mathsf{RI}}PA\multimap
X\mid\Gamma,\Delta\vdash^{\bullet}_{\\_}{\mathsf{F}}P??{-}\mid\Lambda\vdash_{\\_}{\mathsf{RI}}Dh\\\
(\text{same derivation as in
(\ref{eq:llefttr})})&(\text{${\multimap}\mathsf{L}$ not applicable since
$\Gamma$ is tag-free})\end{array}$

The extra restrictions on sequents and formulae that the rules in (9) impose
in comparison to those in (6) do not reduce derivability, e.g., the sequents
${-}\mid Y\vdash_{\\_}{\mathsf{F}}(X\multimap X)\otimes Y$, whose proof
requires passivation of a new formula in the derivation of the first premise
of a $\otimes\mathsf{R}$ application, $X\multimap Y\mid
Z\vdash_{\\_}{\mathsf{RI}}(X\multimap Y)\otimes Z$, whose proof requires
application of $\otimes\mathsf{R}$ before ${\multimap}\mathsf{L}$, and
$X\multimap(Y\otimes Z)\mid X\vdash_{\\_}\mathsf{F}Y\otimes Z$, which needs
${\multimap}\mathsf{L}$ invoked before $\otimes\mathsf{R}$, are all derivable.

$\footnotesize\begin{array}[]{c}\begin{tabular}[]{l}${-}\mid
Y\vdash_{\\_}{\mathsf{F}}(X\multimap X)\otimes
Y\lx@proof@logical@and{-}\vdash\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}X\multimap
X{-}\mid X^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{RI}}X{-}\mid
X^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{P}}XX\mid\quad\vdash_{\\_}{\mathsf{LI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}X{-}\mid
Y\vdash_{\\_}{\mathsf{RI}}Y{-}\mid
Y\vdash_{\\_}{\mathsf{P}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y$\end{tabular}\\\
\begin{tabular}[]{l}$X\multimap Y\mid Z\vdash_{\\_}{\mathsf{F}}(X\multimap
Y)\otimes Z\lx@proof@logical@and X\multimap
Y\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}X\multimap YX\multimap Y\mid
X^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{RI}}YX\multimap Y\mid
X^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{F}}Y\lx@proof@logical@and{-}\mid
X\vdash_{\\_}{\mathsf{RI}}X{-}\mid
X\vdash_{\\_}{\mathsf{P}}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{P}}ZZ\mid\quad\vdash_{\\_}{\mathsf{LI}}ZZ\mid\quad\vdash_{\\_}{\mathsf{F}}Z$
\quad$X\multimap(Y\otimes Z)\mid X\vdash_{\\_}{\mathsf{F}}Y\otimes
Z\lx@proof@logical@and{-}\mid X\vdash_{\\_}{\mathsf{RI}}X{-}\mid
X\vdash_{\\_}{\mathsf{P}}XX\mid\quad\vdash_{\\_}{\mathsf{LI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}XY\otimes
Z\mid\quad\vdash_{\\_}{\mathsf{LI}}Y\otimes ZY\mid
Z\vdash_{\\_}{\mathsf{LI}}Y\otimes ZY\mid Z\vdash_{\\_}{\mathsf{F}}Y\otimes
Z\lx@proof@logical@and
Y\mid\quad\vdash_{\\_}{\mathsf{RI}}^{\bullet}YY\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}Y{-}\mid
Z\vdash_{\\_}{\mathsf{RI}}Z{-}\mid
Z\vdash_{\\_}{\mathsf{P}}ZZ\mid\quad\vdash_{\\_}{\mathsf{LI}}ZZ\mid\quad\vdash_{\\_}{\mathsf{F}}Z$\end{tabular}\end{array}\normalsize$

We should point out that although the focused calculus is free of the
undesired non-determinism that the naïve attempt (6) suffered from, it is
still non-deterministic and this has to be so. In particular, the focused
calculus (9) keeps the following two types of non-determinism of the focused
calculus of [27] (see the analysis in [26]). We call these types of non-
determinism _essential_ because they reflect the fact that there are sequents
with multiple derivations in $\mathtt{SkNMILL}$ that are not
$\circeq$-equivalent.

  1. 1.

In phase $\mathsf{P}$, when the stoup is empty, there is a choice of whether
to apply $\mathsf{pass}$ or $\mathsf{F}2\mathsf{P}$ and sometimes both options
lead to a derivation. For example, the sequent $X\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{F}}X\otimes(\mathsf{I}\otimes Y)$ has two distinct
derivations in the focused system and the corresponding derivations in
$\mathtt{SkNMILL}$ are not $\circeq$-equivalent.

$\footnotesize\begin{array}[]{cc}X\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{F}}X\otimes(\mathsf{I}\otimes Y)\lx@proof@logical@and
X\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}X{-}\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{RI}}\mathsf{I}\otimes Y{-}\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{P}}\mathsf{I}\otimes Y\mathsf{I}\otimes
Y\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}\otimes Y\mathsf{I}\mid
Y\vdash_{\\_}{\mathsf{LI}}\mathsf{I}\otimes Y{-}\mid
Y\vdash_{\\_}{\mathsf{LI}}\mathsf{I}\otimes Y{-}\mid
Y\vdash_{\\_}{\mathsf{F}}\mathsf{I}\otimes
Y\lx@proof@logical@and{-}\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}\mathsf{I}{-}\mid
Y\vdash_{\\_}{\mathsf{RI}}Y{-}\mid
Y\vdash_{\\_}{\mathsf{P}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{F}Y&X\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{F}}X\otimes(\mathsf{I}\otimes Y)\lx@proof@logical@and
X\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}X{-}\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{RI}}\mathsf{I}\otimes Y{-}\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{F}}\mathsf{I}\otimes
Y\lx@proof@logical@and{-}\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}\mathsf{I}{-}\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{RI}}Y{-}\mid\mathsf{I}\otimes
Y\vdash_{\\_}{\mathsf{P}}Y\mathsf{I}\otimes
Y\mid\quad\vdash_{\\_}{\mathsf{LI}}Y\mathsf{I}\otimes\mid\quad\vdash_{\\_}{\mathsf{LI}}Y\mathsf{I}\mid
Y\vdash_{\\_}{\mathsf{LI}}{-}\mid Y\vdash_{\\_}{\mathsf{LI}}Y{-}\mid
Y\vdash_{\\_}{\mathsf{P}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y\end{array}\normalsize$

  2. 2.

In phase $\mathsf{F}$, if the succedent formula is $A\otimes B$, and the rule
$\otimes\mathsf{R}$ is to be applied, the context can be split anywhere.
Sometimes several of these splits can lead to a derivation. For example, the
sequent $X\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{F}}(X\otimes\mathsf{I})\otimes
Y$ has two distinct derivations.

$\footnotesize\begin{array}[]{cc}X\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{F}}(X\otimes\mathsf{I})\otimes
Y\lx@proof@logical@and
X\mid\mathsf{I}\vdash^{\bullet}_{\\_}{\mathsf{RI}}X\otimes\mathsf{I}X\mid\mathsf{I}\vdash_{\\_}{\mathsf{F}}^{\bullet}X\otimes\mathsf{I}\lx@proof@logical@and
X\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}X{-}\mid\mathsf{I}\vdash_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\mathsf{I}\vdash_{\\_}{\mathsf{P}}\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{P}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y&X\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{F}}(X\otimes\mathsf{I})\otimes
Y\lx@proof@logical@and
X\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}X\otimes\mathsf{I}X\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}X\otimes\mathsf{I}\lx@proof@logical@and
X\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}XX\mid\quad\vdash_{\\_}{\mathsf{F}}^{\bullet}X{-}\mid\quad\vdash_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}{-}\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{RI}}Y{-}\mid\mathsf{I},Y\vdash_{\\_}{\mathsf{P}}Y\mathsf{I}\mid
Y\vdash_{\\_}{\mathsf{LI}}Y{-}\mid
Y\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{P}}YY\mid\quad\vdash_{\\_}{\mathsf{LI}}YY\mid\quad\vdash_{\\_}{\mathsf{F}}Y\end{array}\normalsize$

The presence of $\multimap$ adds two further types of essential
nondeterminism.

  1. 3.

This type is similar to type 2. In phase $\mathsf{F}$, if the stoup formula is
$A\multimap B$, and the rule ${\multimap}\mathsf{L}$ is to be applied, the
context can be split anywhere. Again, sometimes several of these splits lead
to a derivation. For example, the sequent $\mathsf{I}\multimap(X\multimap
Y)\mid\mathsf{I},X\vdash_{\\_}{\mathsf{F}}Y$ has two derivations.

$\footnotesize\begin{array}[]{cc}\mathsf{I}\multimap(X\multimap
Y)\mid\mathsf{I},X\vdash_{\\_}{\mathsf{F}}Y\lx@proof@logical@and{-}\mid\mathsf{I}\vdash_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\mathsf{I}\vdash_{\\_}{\mathsf{P}}\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}X\multimap
Y\mid X\vdash_{\\_}{\mathsf{LI}}YX\multimap Y\mid
X\vdash_{\\_}{\mathsf{F}}Y\lx@proof@logical@and{-}\mid
X\vdash_{\\_}{\mathsf{RI}}X{-}\mid
X\vdash_{\\_}{\mathsf{P}}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&\mathsf{I}\multimap(X\multimap
Y)\mid\mathsf{I},X\vdash_{\\_}{\mathsf{F}}Y\lx@proof@logical@and{-}\mid\quad\vdash_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}X\multimap
Y\mid\mathsf{I},X\vdash_{\\_}{\mathsf{LI}}YX\multimap
Y\mid\mathsf{I},X\vdash_{\\_}{\mathsf{F}}Y\lx@proof@logical@and{-}\mid\mathsf{I},X\vdash_{\\_}{\mathsf{RI}}X{-}\mid\mathsf{I},X\vdash_{\\_}{\mathsf{P}}X\mathsf{I}\mid
X\vdash_{\\_}{\mathsf{LI}}X{-}\mid X\vdash_{\\_}{\mathsf{LI}}X{-}\mid
X\vdash_{\\_}{\mathsf{P}}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\end{array}\normalsize$

  2. 4.

Finally, in phase $\mathsf{F}$, if the succedent formula is $A\otimes B$ and
the stoup formula is $A^{\prime}\multimap B^{\prime}$, then both
$\otimes\mathsf{R}$ and ${\multimap}\mathsf{L}$ can be applied first and
sometimes both options lead to a derivation. For example, the sequent
$\mathsf{I}\multimap\mathsf{I}\mid
Z\vdash_{\\_}{\mathsf{F}}(\mathsf{I}\multimap\mathsf{I})\otimes Z$ has two
derivations.

$\footnotesize\begin{array}[]{cc}\mathsf{I}\multimap\mathsf{I}\mid
Z\vdash_{\\_}{\mathsf{F}}(\mathsf{I}\multimap\mathsf{I})\otimes
Z\lx@proof@logical@and\mathsf{I}\multimap\mathsf{I}\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}\mathsf{I}\multimap\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{RI}}\mathsf{I}\mathsf{I}\multimap\mathsf{I}\mid\mathsf{I}^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{F}}\mathsf{I}\lx@proof@logical@and{-}\mid\mathsf{I}\vdash_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\mathsf{I}\vdash_{\\_}{\mathsf{P}}\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
Z\vdash_{\\_}{\mathsf{LI}}Z{-}\mid
Z\vdash_{\\_}{\mathsf{P}}ZZ\mid\quad\vdash_{\\_}{\mathsf{LI}}ZZ\mid\quad\vdash_{\\_}{\mathsf{F}}Z&\mathsf{I}\multimap\mathsf{I}\mid
Z\vdash_{\\_}{\mathsf{F}}(\mathsf{I}\multimap\mathsf{I})\otimes
Z\lx@proof@logical@and{-}\mid\quad\vdash_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}\mathsf{I}\mid
Z\vdash_{\\_}{\mathsf{LI}}(\mathsf{I}\multimap\mathsf{I})\otimes Z{-}\mid
Z\vdash_{\\_}{\mathsf{LI}}(\mathsf{I}\multimap\mathsf{I})\otimes Z{-}\mid
Z\vdash_{\\_}{\mathsf{F}}(\mathsf{I}\multimap\mathsf{I})\otimes
Z\lx@proof@logical@and{-}\mid\quad\vdash^{\bullet}_{\\_}{\mathsf{RI}}\mathsf{I}\multimap\mathsf{I}{-}\mid\mathsf{I}^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{RI}}\mathsf{I}{-}\mid\mathsf{I}^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{P}}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}\mathsf{I}\mid\quad\vdash_{\\_}{\mathsf{LI}}\mathsf{I}{-}\mid\quad\vdash_{\\_}{\mathsf{LI}}{-}\mid\quad\vdash_{\\_}{\mathsf{F}}\mathsf{I}{-}\mid
Z\vdash_{\\_}{\mathsf{LI}}Z{-}\mid
Z\vdash_{\\_}{\mathsf{P}}ZZ\mid\quad\vdash_{\\_}{\mathsf{LI}}ZZ\mid\quad\vdash_{\\_}{\mathsf{F}}Z\end{array}\normalsize$

Note that, in the second derivation, the rule $\mathsf{pass}$ applies to the
sequent
${-}\mid\mathsf{I}^{\bullet}\vdash^{\bullet}_{\\_}{\mathsf{P}}\mathsf{I}$ only
because the context formula $\mathsf{I}^{\bullet}$ is tagged.

######  Theorem 4.1.

The focused sequent calculus is sound and complete wrt. the sequent calculus
of Section 2: there is a bijective correspondence between the set of
derivations of $S\mid\Gamma\vdash A$ quotiented by $\circeq$ and the set of
derivations of $S\mid\Gamma\vdash_{\\_}\mathsf{RI}A$.

Soundness is immediate: there exist functions
$\mathsf{emb}_{\\_}{ph}:S\mid\Gamma\vdash^{x}_{\\_}{ph}A\to S\mid\Gamma\vdash
A$, for all $ph\in\\{\mathsf{RI},\mathsf{LI},\mathsf{P},\mathsf{F}\\}$, which
simply erase all phase annotations and tags. 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\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\multimap
B\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{RI}}C\lx@proof@logical@and{-}\mid\Gamma\vdash_{\\_}{\mathsf{RI}}AB\mid\Delta\vdash_{\\_}{\mathsf{RI}}C\qquad
S\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{RI}}[\\![\Gamma^{\prime}\mid
A]\\!]_{\\_}{\multimap}\otimes B\lx@proof@logical@and
S\mid\Gamma,\Gamma^{\prime}\vdash_{\\_}{\mathsf{RI}}A{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}B\end{array}$
(10)

The interesting one is
$\otimes\mathsf{R}_{\\_}{\Gamma^{\prime}}^{\mathsf{RI}}$. The tensor right
rule $\otimes\mathsf{R}^{\mathsf{RI}}$, with premises and conclusion in phase
$\mathsf{RI}$, is an instance of the latter with empty $\Gamma^{\prime}$.
Without this generalization including the extra context $\Gamma^{\prime}$, one
quickly discovers that finding a proof of $\otimes\mathsf{R}^{\mathsf{RI}}$,
proceeding by induction on the structure of the derivation of the first
premise, is not possible when this derivation ends with an application of
${\multimap}\mathsf{R}$:

$\small\begin{tabular}[]{l}$S\mid\Gamma,\Delta\vdash_{\\_}{\mathsf{RI}}(A^{\prime}\multimap
B^{\prime})\otimes B\lx@proof@logical@and
S\mid\Gamma\vdash_{\\_}{\mathsf{RI}}A^{\prime}\multimap
B^{\prime}S\mid\Gamma,A^{\prime}\vdash_{\\_}{\mathsf{RI}}B^{\prime}f{-}\mid\Delta\vdash_{\\_}{\mathsf{RI}}Bg$\end{tabular}=\quad??$

The inductive hypothesis applied to $f$ and $g$ would produce a derivation of
the wrong sequent. The use of $\Gamma^{\prime}$ in the generalized rule
$\otimes\mathsf{R}_{\\_}{\Gamma^{\prime}}^{\mathsf{RI}}$ is there to fix
precisely this issue.

The admissibility of the rules in (10) allows the construction of a function
$\mathsf{focus}:S\mid\Gamma\vdash A\to\linebreak
S\mid\Gamma\vdash_{\\_}\mathsf{RI}A$, replacing applications of each rule in
(1) with inferences by the corresponding admissible focused rule in phase
$\mathsf{RI}$. It is possible to prove that the function $\mathsf{focus}$ maps
$\circeq$-equivalent derivations in the sequent calculus for
$\mathtt{SkNMILL}$ to syntactically identical derivations in focused sequent
calculus. One can also show that $\mathsf{focus}$ is the inverse of
$\mathsf{emb}_{\\_}\mathsf{RI}$, i.e.
$\mathsf{focus}\;(\mathsf{emb}_{\\_}\mathsf{RI}\;f)=f$ for all
$f:S\mid\Gamma\vdash_{\\_}\mathsf{RI}A$ and
$\mathsf{emb}_{\\_}\mathsf{RI}\;(\mathsf{focus}\;g)\circeq g$ for all
$g:S\mid\Gamma\vdash A$. In other words, each $\circeq$-equivalence class in
the sequent calculus corresponds uniquely to a single derivation in the
focused sequent calculus.

The focused sequent calculus solves the _coherence problem_ for skew monoidal
closed categories. As proved in Theorems 3.1, 3.2, the sequent calculus for
$\mathtt{SkNMILL}$ is a presentation of the free skew monoidal closed category
$\mathsf{FSkMCl}(\mathsf{At})$ on the set $\mathsf{At}$. The coherence problem
is the problem of deciding whether two parallel maps in
$\mathsf{FSkMCl}(\mathsf{At})$ are equal. This is equivalent to deciding
whether two sequent calculus derivations $f,g:A\mid~{}\vdash B$ are in the
same $\circeq$-equivalence class. But that in turn is the same as deciding
whether $\mathsf{focus}\;f=\mathsf{focus}\;g$ in the focused sequent calculus,
and deciding syntactic equality of focused derivations is straightforward. The
Hilbert-style calculus is a direct presentation of
$\mathsf{FSkMCl}(\mathsf{At})$, but thanks to the bijection (up to $\doteq$
resp. $\circeq$) between Hilbert-style and sequent calculus derivations, we
can also decide if two Hilbert-style derivations $f,g:A\Rightarrow B$ are in
the same $\doteq$-equivalence class.

##  5 Conclusion

The paper describes a sequent calculus for $\mathtt{SkNMILL}$, a skew variant
of non-commutative multiplicative intuitionistic linear logic. The
introduction of the logic $\mathtt{SkNMILL}$ via this sequent calculus is
motivated by the categorical notion of skew monoidal closed category, which
yields the intended categorical semantics for the logic. Sequent calculus
derivations admit unique normal forms wrt. a congruence relation $\circeq$
capturing the equational theory of skew monoidal closed categories at the
level of derivations. Normal forms can be organized in a focused sequent
calculus, where each focused derivation uniquely corresponds to (and so
represents) a $\circeq$-equivalence class in the unfocused sequent calculus.
In order to deal with all the permutative conversions of $\circeq$ and to
consequently eliminate the related sources of non-determinism in root-first
proof search, the focused sequent calculus employs a system of tags for
keeping track of the new formulae occurring in the context while building a
derivation. The focused sequent calculus solves the coherence problem for skew
monoidal closed categories: deciding if a canonical diagram commutes in every
skew monoidal closed category reduces to deciding equality of focused
derivations.

We plan to investigate alternative presentations of $\mathtt{SkNMILL}$, such
as natural deduction. Analogously to the case of the sequent calculus studied
in this paper, we expect natural deduction derivation to be strongly
normalizing wrt. an appropriately defined $\beta\\!\eta$-conversion. We are
interested in directly comparing the resulting $\beta\\!\eta$-long normal
forms with the focused derivations of Section 4.

The system of tags in focused proofs, used for taming the non-deterministic
choices arising in proof search to be able to canonically represent each
equivalence class of $\circeq$, appears to be a new idea. There exist other
techniques for drastically reducing non-determinism in proof search, such as
multi-focusing [8] and saturated focusing [20], and we wonder if our system of
tags is in any way related to these. As a general disclaimer, we should state
that we have interpreted focusing broadly as the idea of root-first proof
search defining a normal form, based on a careful discipline of application of
invertible and non-invertible rules to reduce non-determinism, but not
necessarily driven by a polarity-centric analysis. In this respect, our
approach is similar in spirit to, e.g., [9].

This paper represents the latest installment of a large project aiming at the
development of the proof theory of categories with skew structure. So far the
project, promoted and advanced by Uustalu, Veltri and Zeilberger, has
investigated proof systems for skew semigroup categories [29], (non-symmetric
and symmetric) skew monoidal categories [27, 26, 28] and skew prounital closed
categories [25]. From a purely proof-theoretic perspective, the main lesson
gained from the study of these skew systems consists in first insights into
ways of _modular_ construction of focusing calculi. This is particularly
highlighted in Uustalu et al.’s study of _partially normal_ skew monoidal
categories [26], where one or more structural laws among $\lambda$, $\rho$ and
$\alpha$ can be required to be invertible. The focused sequent calculus of
partially normal skew monoidal categories is obtained from the focused sequent
calculus of skew monoidal categories by modularly adding new rules for each
enforced normality condition. We expect similar modularity to show up in the
case of partially normal skew monoidal closed categories.

We are also planning to develop an extension of $\mathtt{SkNMILL}$ with an
exponential modality $!$. This in turns requires the study of linear
exponential comonads on skew monoidal closed categories, extending the work of
Hasegawa [12]. We would also like to consider modalities for exchange [13] and
associativity/unitality.

#### Acknowledgements

N.V. and T.U. were supported by the Estonian Research Council grants no.
PSG659, PSG749 and PRG1210, N.V. and C.-S.W. by the ESF funded Estonian IT
Academy research measure (project 2014-2020.4.05.19-0001). T.U. was supported
by the Icelandic Research Fund grant no. 196323-053. Participation of C.-S.W.
in the conference was supported by the EU COST action CA19135 (CERCIRAS).

## References

  * [1]
  * [2] V. 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] 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.
  * [8] 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.
  * [9] Roy Dyckhoff & Stéphane Lengrand (2006): _LJQ: A Strongly Focused Calculus for Intuitionistic Logic_.  In Arnold Beckmann, Ulrich Berger, Benedikt Löwe & John V. Tucker, editors: Proceedings of the 2nd Conference on Computability in Europe, CiE 2006, Lecture Notes in Computer Science 3988, Springer, pp. 173–185, 10.1007/1178034219.
  * [10] Samuel Eilenberg & G. Max Kelly (1966): _Closed Categories_.  In Samuel Eilenberg, David K. Harrison, Saunders Mac Lane & Helmut Röhrl, editors: Proceedings of the Conference on Categorical Algebra (La Jolla, 1965), Springer, pp. 421–562, 10.1007/978-3-642-99902-4_22.
  * [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] Masahito Hasegawa (2016): _Linear Exponential Comonads without Symmetry_.  In Iliano Cervesato & Maribel Fernández, editors: Proceedings of the 4th International Workshop on Linearity, LINEARITY 2016, Electronic Proceedings in Theoretical Computer Science 238, Open Publishing Association, pp. 54–63, 10.4204/etpcs.238.6.
  * [13] Jiaming Jiang, Harley Eades III & Valeria de Paiva (2018): _On the Lambek Calculus with an Exchange Modality_.  In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva & Lorenzo Tortora de Falco, editors: Proceedings of the Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA 2018, Electronic Proceedings in Theoretical Computer Science 292, Open Publishing Association, pp. 43–89, 10.4204/eptcs.292.4.
  * [14] 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.
  * [15] 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.
  * [16] Joachim Lambek (1958): _The Mathematics of Sentence Structure_.  American Mathematical Monthly 65(3), pp. 154–170, 10.2307/2310058.
  * [17] Joachim Lambek (1968): _Deductive Systems and Categories I: Syntactic Calculus and Residuated Categories_.  Mathematical Systems Theory 2(4), pp. 287–318, 10.1007/bf01703261.
  * [18] Saunders Mac Lane (1963): _Natural Associativity and Commutativity_.  Rice University Studies 49(4), pp. 28–46.  Available at http://hdl.handle.net/1911/62865.
  * [19] Paul-André Melliès (2009): _Categorical Semantics of Linear Logic_.  In Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine & Paul-André Melliès, editors: Interactive Models of Computation and Program Behavior, Panoramas et syntheses 27, Société Mathématique de France, pp. 15–215.
  * [20] Gabriel Scherer & Ddier Rémy (2015): _Which Simple Types Have a Unique Inhabitant?_ In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP ’15, ACM, pp. 243–255, 10.1145/2784731.2784757.
  * [21] Ross Street (2013): _Skew-Closed Categories_.  Journal of Pure and Applied Algebra 217(6), pp. 973–988, 10.1016/j.jpaa.2012.09.020.
  * [22] 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.
  * [23] Haruka Tomita (2021): _Realizability without Symmetry_.  In Christel Baier & Jean Goubault-Larrecq, editors: Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, Leibniz International Proceedings in Informatics 183, Dagstuhl Publishing, pp. 38:1–38:16, 10.4230/lipics.csl.2021.38.
  * [24] Tarmo Uustalu, Niccolò Veltri & Noam Zeilberger (2020): _Eilenberg-Kelly Reloaded_.  Electronic Notes in Theoretical Computer Science 352, pp. 233–256, 10.1016/j.entcs.2020.09.012.
  * [25] 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 the 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.
  * [26] Tarmo Uustalu, Niccolò Veltri & Noam Zeilberger (2021): _Proof Theory of Partially Normal Skew Monoidal Categories_.  In David I. Spivak & Jamie Vicary, editors: Proceedings of the 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.
  * [27] 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.
  * [28] Niccolò Veltri (2021): _Coherence via Focusing for Symmetric Skew Monoidal Categories_.  In Alexandra Silva, Renata Wassermann & Ruy de Queiroz, editors: Proceedings of the 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.
  * [29] 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.