# A Proof-theoretic Semantics for Intuitionistic Linear Logic

Yll Buzoku
University College London
<EMAIL_ADDRESS>0009-0006-9478-6009

###### Abstract

The approach taken in [4] is an interesting adaptation of the work presented
in [8] to the substructural setting. What is particularly interesting is how
naturally the move to the substructural setting provided a semantics for the
multiplicative fragment of intuitionistic linear logic. Whilst ultimately the
authors of the semantics for IMLL used their foundations to provide a
semantics for bunched implication logic [5], it begs the question, what of the
rest of intuitionistic linear logic? In this paper, I present a semantics for
intuitionistic linear logic, by first presenting a semantics for the
multiplicative and additive fragment after which we focus solely on
considering the modality “of-course”, thus giving a proof-theoretic semantics
for intuitionistic linear logic.

Keywords — Proof-theoretic Semantics, Base-extension Semantics, Substructural
Logic, Intuitionistic linear logic, modalities, additivity

##  1 Introduction

Providing a proof-theoretic semantics for intuitionistic linear logic is an
interesting problem, not least because, to date, we have very few concrete
results on how to express modalities within a PtS framework. Discussions in
works such as [6] give useful and interesting philosophical insights into what
might be expected of a proof-theoretic semantics for a logic with modalities
but it is clear that due to a lack of almost any such results, giving
semantics for such logics is a hard problem. The work in [3] is the first
case, as far as I am aware, where a sound and complete proof-theoretic
semantics was provided for a logic with a modality. The approach taken within
deals in terms of Kripke-like relations on bases and uses these relations to
give a categorisation of $\square\varphi$. This approach works well in the
modal logic case, but is harder to see how one may do something similar in the
substructural framework we are considering. In this paper, I give a sound and
complete semantics for intuitionistic linear logic, which of course includes
the modality “of-course”.
This paper is split broadly into two sections: The first handles the semantics
for the intuitionistic multiplicative additive fragment of linear logic, using
the results in [4] as a starting point. To give a semantics for this fragment,
it was important to generalise the notion of atomic rules to be able to handle
additivity. Doing so in the manner described in this paper is quite powerful
as it allows for very general atomic rules to be expressed in the
substructural framework. For example, it is completely natural to express
notions of “context sharing” or even, as we will show, to express the
promotion rule atomically. The second section handles the semantics of the
full logic, by showing how to use the results that we already have for the
multiplicative additive fragment with new clauses to appropriately handle the
modality. What is made abundantly clear in the semantics given for
intuitionistic linear logic is that a formula with top-level connective “of
course” behaves almost entirely differently when in the antecedent of a
sequent from when it is in the succedent. This observation, though perhaps
clear in the proof theory, is incredibly central to the semantics as presented
in this paper, and it is hoped in the final version of this paper, there will
be a detailed discussion about this asymmetry, and its manifestation in the
semantics. More interestingly, though currently not in the paper, I
additionally have a sound and complete semantics for ILL based on the notion
of a “stoup”. This will be included in due course. I mention this because it
was through studying this “stouped” semantics that I was able to create a
translation that resulted in the semantics that I present in this paper,
though this translation is not entirely trivial.

##  2 Overview of IMALL

######  Definition 1.

Formulas of IMALL are defined inductively as follows:

$\mathsf{Form}\ni\varphi,\psi::={p}\mid\varphi\otimes\psi\mid
1\mid\varphi\multimap\psi\mid\varphi\with\psi\mid\varphi\oplus\psi\mid 0$

The following definition of derivability for the multiplicative additive
fragment of intuitionistic linear logic can be found in papers such as [1],
[2], [7].

######  Definition 2.

The derivability relation $\vdash_{\mathrm{ILL}}$ is defined inductively as
follows:

Ax $\varphi\vdash_{\mathrm{IMALL}}\varphi$

$\Gamma,\varphi\vdash_{\mathrm{IMALL}}\psi$ $\multimap$-I
$\Gamma\vdash_{\mathrm{IMALL}}\varphi\multimap\psi$

$\Gamma\vdash_{\mathrm{IMALL}}\varphi$ $\Delta\vdash_{\mathrm{IMALL}}\psi$
$\otimes$-I $\Gamma,\Delta\vdash_{\mathrm{IMALL}}\varphi\otimes\psi$

$1$-I $\vdash_{\mathrm{IMALL}}1$

$\Gamma^{\gamma}\vdash_{\mathrm{IMALL}}\varphi$
$\Gamma^{\gamma}\vdash_{\mathrm{IMALL}}\psi$ $\with$-I
$\Gamma\vdash_{\mathrm{IMALL}}\varphi\with\psi$

$\Gamma\vdash_{\mathrm{IMALL}}\varphi_{i}$ $\oplus$-$\text{I}_{i}$
$\Gamma\vdash_{\mathrm{IMALL}}\varphi_{0}\oplus\varphi_{1}$

No $0$ intro rule

$\Gamma\vdash_{\mathrm{IMALL}}\varphi\multimap\psi$
$\Delta\vdash_{\mathrm{IMALL}}\varphi$ $\multimap$-E
$\Gamma,\Delta\vdash_{\mathrm{IMALL}}\psi$

$\Gamma\vdash_{\mathrm{IMALL}}\varphi\otimes\psi$
$\Delta,\varphi,\psi\vdash_{\mathrm{IMALL}}\chi$ $\otimes$-E
$\Gamma,\Delta\vdash_{\mathrm{IMALL}}\chi$

$\Gamma\vdash_{\mathrm{IMALL}}\varphi$ $\Delta\vdash_{\mathrm{IMALL}}1$ $1$-E
$\Gamma,\Delta\vdash_{\mathrm{IMALL}}\varphi$

$\Gamma\vdash_{\mathrm{IMALL}}\varphi_{0}\with\varphi_{1}$
$\with$-$\text{E}_{i}$ $\Gamma\vdash_{\mathrm{IMALL}}\varphi_{i}$

$\Gamma\vdash_{\mathrm{IMALL}}\varphi\oplus\psi$
$\Delta^{\gamma},\varphi\vdash_{\mathrm{IMALL}}\chi$
$\Delta^{\gamma},\psi\vdash_{\mathrm{IMALL}}\chi$ $\oplus$-E
$\Gamma,\Delta\vdash_{\mathrm{IMALL}}\chi$

$\Gamma\vdash_{\mathrm{IMALL}}0$ $0$-E $\Gamma\vdash_{\mathrm{IMALL}}\varphi$

Note that when hypotheses of a rule are marked with a superscript, such as in
the rule ($\with$-I), this is taken to mean that all all instances of this
hypotheses are the same, i.e. in the case of ($\with$-I), both $\Delta$ are
actually the _same_ multiset $\Delta$.

Before we move on, we define the notion of a sequent in intuitionistic
multiplicative additive linear logic.

######  Definition 3 (Sequent).

A sequent is a pair $\langle\Theta,\varphi\rangle$, where $\Theta$ is a
multiset of IMALL formulas and $\varphi$ is a single IMALL formula.

######  Example 4.

An example sequent is $\langle\\{\varphi,\varphi\multimap\psi\\},\psi\rangle$.

##  3 Base-extension Semantics for IMALL

###  3.1 Atomic Systems

We begin by setting up some notation. We start by fixing a countably infinite
set of propositional atoms $\mathrm{At}$. Unless otherwise stated, lower case
latin letters are used to denote propositional atoms and upper case latin
letters are used to denote finite _multisets_ of propositional atoms. The
empty multiset is denoted $\varnothing$. The sum of two multisets ${P}$ and
${Q}$ is denoted ${P}\cup{Q}$ or in the more abbreviated form ${P},{Q}$. As
before, lower case greek letters are used to denote formulas and upper case
greek letters are used to denote finite _multisets_ thereof. Finally,
throughout this work, the term atomic multiset is taken to mean multiset of
propositional atoms.

######  Definition 5 (Atomic rules).

Atomic rules take the following form:

$\\{({P}_{1_{1}}\Rightarrow{q}_{1_{1}}),\dots,({P}_{1_{l_{1}}}\Rightarrow{q}_{1_{l_{1}}})\\},\dots,\\{({P}_{n_{1}}\Rightarrow{q}_{n_{1}}),\dots,({P}_{n_{l_{n}}}\Rightarrow{q}_{n_{l_{n}}})\\}\Rightarrow{r}$

where

  * •

Each $P_{i}$ is an atomic multiset, called a set of premisses.

  * •

Each $q_{i}$ and $r$ is an atomic proposition.

  * •

Each $(P_{i}\Rightarrow q_{i})$ is a pair $(P_{i},q_{i})$ called an atomic
sequent.

  * •

Each set
$\\{({P}_{i_{1}}\Rightarrow{q}_{i_{1}}),\dots,({P}_{i_{l_{i}}}\Rightarrow{q}_{i_{l_{i}}})\\}$
is called an additive atomic box.

The rule may be read as saying: _Given derivations of $q_{i_{j}}$ from
$P_{i_{j}}$ relative to some multisets $C_{i}$ one infers $r$ relative to all
$C_{i}$, discharging from the derivations in question, the premiss atomic
multisets $P_{i_{j}}$._ The rule may additionally be written as follows to
save space:

$\\{({P}_{1_{i}}\Rightarrow{q}_{1_{i}})\\}^{l_{1}}_{i=1},\dots,\\{({P}_{n_{i}}\Rightarrow{q}_{n_{i}})\\}^{l_{n}}_{i=1}\Rightarrow{r}$

${r}\leavevmode\hbox to94.57pt{\vbox
to75.54pt{\pgfpicture\makeatletter\hbox{\hskip
46.97185pt\lower-61.10994pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.7,0.7}\pgfsys@color@rgb@fill{1}{0.7}{0.7}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.7,0.7}\pgfsys@color@rgb@fill{1}{0.7}{0.7}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{38.67914pt}{14.22638pt}\pgfsys@lineto{-38.67914pt}{14.22638pt}\pgfsys@curveto{-40.8883pt}{14.22638pt}{-42.67914pt}{12.43555pt}{-42.67914pt}{10.22638pt}\pgfsys@lineto{-42.67914pt}{-10.22638pt}\pgfsys@curveto{-42.67914pt}{-12.43555pt}{-40.8883pt}{-14.22638pt}{-38.67914pt}{-14.22638pt}\pgfsys@lineto{38.67914pt}{-14.22638pt}\pgfsys@curveto{40.8883pt}{-14.22638pt}{42.67914pt}{-12.43555pt}{42.67914pt}{-10.22638pt}\pgfsys@lineto{42.67914pt}{10.22638pt}\pgfsys@curveto{42.67914pt}{12.43555pt}{40.8883pt}{14.22638pt}{38.67914pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{-42.67914pt}{-14.22638pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.79811pt}{-2.26299pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${C_{1}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-43.97214pt}{-39.08759pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${q}_{1_{1}}[{P}_{1_{1}}]$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.375pt}{-56.31024pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\ldots}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.30539pt}{-38.68039pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${q}_{1_{l_{1}}}[{P}_{1_{l_{1}}}]$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\leavevmode\hbox
to12.75pt{\vbox to14.1pt{\pgfpicture\makeatletter\hbox{\hskip
6.37471pt\lower-7.0497pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.375pt}{-2.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\ldots}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\leavevmode\hbox
to95.81pt{\vbox to75.54pt{\pgfpicture\makeatletter\hbox{\hskip
47.47702pt\lower-61.10994pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.7,0.7}\pgfsys@color@rgb@fill{1}{0.7}{0.7}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.7,0.7}\pgfsys@color@rgb@fill{1}{0.7}{0.7}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{38.67914pt}{14.22638pt}\pgfsys@lineto{-38.67914pt}{14.22638pt}\pgfsys@curveto{-40.8883pt}{14.22638pt}{-42.67914pt}{12.43555pt}{-42.67914pt}{10.22638pt}\pgfsys@lineto{-42.67914pt}{-10.22638pt}\pgfsys@curveto{-42.67914pt}{-12.43555pt}{-40.8883pt}{-14.22638pt}{-38.67914pt}{-14.22638pt}\pgfsys@lineto{38.67914pt}{-14.22638pt}\pgfsys@curveto{40.8883pt}{-14.22638pt}{42.67914pt}{-12.43555pt}{42.67914pt}{-10.22638pt}\pgfsys@lineto{42.67914pt}{10.22638pt}\pgfsys@curveto{42.67914pt}{12.43555pt}{40.8883pt}{14.22638pt}{38.67914pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{-42.67914pt}{-14.22638pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.0507pt}{-2.53249pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${C_{n}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-44.47731pt}{-39.23859pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${q}_{n_{1}}[{P}_{n_{1}}]$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.375pt}{-56.31024pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\ldots}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.56926pt}{-39.07309pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${q}_{n_{l_{n}}}[{P}_{n_{l_{n}}}]$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ Figure 1: A generic
atomic rule

The length of each additive atomic box will always be written as $l_{i}$ where
$i$ denotes the additive atomic box in question. If each additive atomic box
contains only one element, then the rule may be said to be multiplicative.
Else, it may be said to be additive.

######  Definition 6 (Base).

A _base_ is a set of atomic rules.

######  Definition 7 (Derivability in a base).

The relation of derivability in a base $\mathscr{B}$, denoted as
$\vdash_{\\!\\!\mathscr{B}}$, is a relation indexed by the base $\mathscr{B}$
between an atomic multiset and an individual atomic proposition, defined
inductively according to the following two clauses:

(Ref)

${p}\vdash_{\\!\\!\mathscr{B}}{p}$.

(App)

Given that
$(\\{({P}_{1_{i}}\Rightarrow{q}_{1_{i}})\\}^{l_{1}}_{i=1},\dots,\\{({P}_{n_{i}}\Rightarrow{q}_{n_{i}})\\}^{l_{n}}_{i=1}\Rightarrow{r})\in\mathscr{B}$
and atomic multisets ${C}_{i}$ such that the following hold:

${C}_{i},{P}_{i_{j}}\vdash_{\\!\\!\mathscr{B}}{q}_{i_{j}}\text{ for all
}i=1,\dots,n\text{ and }j=1,\dots,l_{i}$

Then ${C}_{1},\dots,{C}_{n}\vdash_{\\!\\!\mathscr{B}}r$.

######  Proposition 8 (Monotonicity of $\vdash_{\\!\\!\mathscr{B}}$).

If ${P}\vdash_{\\!\\!\mathscr{B}}{p}$ then for all
$\mathscr{C}\supseteq\mathscr{B}$ we also have that
${P}\vdash_{\\!\\!\mathscr{C}}{p}$.

This follows immediately by noting that if there is a rule in $\mathscr{B}$
allowing a derivation of ${p}$ from ${P}$ then that rule will also be in
$\mathscr{C}$.

######  Lemma 9 (Cut admissibility for $\vdash_{\\!\\!\mathscr{B}}$).

The following are equivalent for arbitrary atomic multisets ${P},{S}$, atom
${q}$, and base $\mathscr{B}$, where we assume
${P}=\\{{p}_{1},\dots,{p}_{n}\\}$:

  1. 1.

${P},{S}\vdash_{\\!\\!\mathscr{B}}{q}$.

  2. 2.

For every $\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${T_{1}},\dots
T_{m}$ where
${T}_{1}\vdash_{\\!\\!\mathscr{C}}{p}_{1},\dots,{T}_{n}\vdash_{\\!\\!\mathscr{C}}{p}_{m}$,
then ${T}_{1},\dots,{T}_{m},{S}\vdash_{\\!\\!\mathscr{C}}{q}$.

###### Proof.

We begin by proving that (2) implies (1). For this, we begin by taking
$\mathscr{C}=\mathscr{B}$ and ${T}_{i}$ to be $\\{{p}_{i}\\}$ for each
$i=1,\dots,n$. Since
${p}_{1}\vdash_{\\!\\!\mathscr{B}}{p}_{1},\dots,{p}_{n}\vdash_{\\!\\!\mathscr{B}}{p}_{n}$
all hold by ((Ref)), it thus follows from (2) that
${p}_{1},\dots,{p}_{n},{S}\vdash_{\\!\\!\mathscr{B}}{q}$ which is nothing more
than ${P},{S}\vdash_{\\!\\!\mathscr{B}}{q}$.
To now show (1) implies (2), we need to consider how
${P},{S}\vdash_{\\!\\!\mathscr{B}}{q}$ is derived; that is, we proceed by
induction, considering the cases when the derivation holds due to ((Ref)), our
base case, and ((App)) separately.

  * -

${P},{S}\vdash_{\\!\\!\mathscr{B}}{q}$ holds by ((Ref)). This gives us that
${P},{S}=\\{{q}\\}$, giving ${q}\vdash_{\\!\\!\mathscr{B}}{q}$. There are thus
two cases to consider, depending on which of ${P}$ and ${S}$ is $\\{{q}\\}$.

    * Case 1:

${P}=\\{{q}\\}$ and ${S}=\varnothing$. In this case, the statement of (2)
becomes, for every $\mathscr{C}\supseteq\mathscr{B}$ and atomic multiset ${T}$
where ${T}\vdash_{\\!\\!\mathscr{C}}{q}$, then
${T}\vdash_{\\!\\!\mathscr{C}}{q}$. This holds trivially.

    * Case 2:

${P}=\varnothing$ and ${S}=\\{{q}\\}$. In this case, the statement of (2)
becomes, for every $\mathscr{C}\supseteq\mathscr{B}$,
${S}\vdash_{\\!\\!\mathscr{C}}{q}$. This holds by hypothesis from (1).

We are now left to show that (1) implies (2) according to ((App)). We show
this by induction on ${P}$.

  * -

${P},{S}\vdash_{\\!\\!\mathscr{B}}{q}$ holds by ((App)).
Let that ${P}={P}_{1},\dots,{P}_{n}$ and that ${S}={S}_{1},\dots,{S}_{n}$.
Note that some of the $S_{i}$ may be empty. Suppose further that ((App))
applies by:

$\displaystyle(\\{({Q}_{1_{i}}\Rightarrow{r}_{1_{i}})\\}^{l_{1}}_{i=1},\dots,\\{({Q}_{n_{i}}\Rightarrow{r}_{n_{i}})\\}^{l_{n}}_{i=1}\Rightarrow{q})\in\mathscr{B}$
(1)
$\displaystyle{P}_{i},{S}_{i},{Q}_{(\sum_{j=1}^{i}l_{j}+a)}\vdash_{\\!\\!\mathscr{B}}{r}_{(\sum_{j=1}^{i}l_{j}+a)}\text{
for $a=1,\dots,l_{i}$ and $i=1,\dots,n$}$ (2)

The hypothesis gives that we have multisets ${T}_{1},\dots,{T}_{n}$ such that
${T}_{1}\vdash_{\\!\\!\mathscr{C}}{p}_{1},\dots,{T}_{n}\vdash_{\\!\\!\mathscr{C}}{p}_{n}$
hold. Now we assume that each
${P}_{i}=\\{{p}_{i_{1}},\dots,{p}_{i_{j_{i}}}\\}$ and that
$T_{i}=T_{i_{1}},\dots,T_{i_{j_{i}}}$ for $i=1,\dots,n$ and apply the
induction hypothesis to each formula in (2) giving:

$\displaystyle{T}_{i_{1}},\dots,{T}_{i_{j_{i}}},{S}_{i},{Q}_{(\sum_{j=1}^{i}l_{j}+a)}\vdash_{\\!\\!\mathscr{C}}{r}_{(\sum_{j=1}^{i}l_{j}+a)}\text{
for $a=1,\dots,l_{i}$ and $i=1,\dots,n$}$ (3)

Since the atomic rule (1) is in $\mathscr{B}\subseteq\mathscr{C}$ then by
((App)) we get that

$\displaystyle{T}_{1_{1}},\dots,{T}_{1_{l_{1}}},{S}_{1},\dots,{T}_{n_{1}},\dots,{T}_{n_{l_{n}}},{S}_{n}\vdash_{\\!\\!\mathscr{C}}{q}$

Which by rearranging the multisets gives

$\displaystyle{T}_{1},\dots,{T}_{m},{S}_{1},\dots,{S}_{m}\vdash_{\\!\\!\mathscr{C}}{q}$

which is nothing more than

$\displaystyle{T}_{1},\dots,{T}_{m},S\vdash_{\\!\\!\mathscr{C}}{q}$

as desired, completing the induction.

∎

We now define our key semantical relation, that of support in a base.

######  Definition 10 (Support).

The relation of support, denoted as $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}$,
is a relation indexed by a base $\mathscr{B}$ and an atomic multiset ${P}$,
defined inductively as follows:

(At)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{p}$ iff
${L}\vdash_{\\!\\!\mathscr{B}}{p}$.

($\otimes$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi\otimes\psi$ iff for every base
$\mathscr{C}\supseteq\mathscr{B}$, atomic multiset ${K}$, and atom ${p}$, if
$\varphi\fatcomma\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}p$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!L,K}{p}$.

($1$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}1$ iff for every base
$\mathscr{C}\supseteq\mathscr{B}$, atomic multiset ${S}$, and atom ${p}$, if
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$, then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{P},{S}}{p}$.

($\multimap$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\varphi\multimap\psi$ iff
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\psi$.

($\with$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\varphi\with\psi$ iff
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\psi$.

($\oplus$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\varphi\oplus\psi$ iff for every
$\mathscr{C}\supseteq\mathscr{B}$, atom ${p}$ and atomic multiset ${S}$ such
that $\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$ and
$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$ hold, then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{P},{S}}{p}$.

($0$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}0$ iff
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}{p}$, for all atomic ${p}$.

()

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\Gamma\fatcomma\Delta$ iff there are
atomic multisets ${U}$ and ${V}$ such that $P=U\fatcomma V$ and that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{U}}\Gamma$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{V}}\Delta$.

(Inf)

For $\Theta$ being a nonempty multiset,
$\Theta\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\varphi$ iff for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${K}$ and atoms ${p}$ if
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}\Theta$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L}\fatcomma{K}}\varphi$.

We read $\Gamma\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\varphi$ as saying
$\mathscr{B}$ supports an inference from $\Gamma$ to $\varphi$ in some context
${P}$. The notion of support is key to our semantical notion of validity.

######  Definition 11 (Validity).

A sequent $\langle\Gamma,\varphi\rangle$ is said to be valid if
$\Gamma\Vdash_{\\!\\!\varnothing}^{\\!\\!\varnothing}\varphi$. This is denoted
as $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$.

This notion of validity might seem odd at first, as one might want to say that
a sequent $\langle\Gamma,\varphi\rangle$ is valid if and only if for _all_
bases $\mathscr{B}$ that
$\Gamma\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}\varphi$ holds, however,
in light of the fact that support is monotonic with respect to bases, this is
equivalent to saying that our sequent is supported in the smallest base which
is included in every base; namely, the empty base. We now formally state this
monotonicity property.

######  Proposition 12 (Monotonicity of
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}$).

If $\Gamma\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\phi$ then for all
$\mathscr{C}\supseteq\mathscr{B}$, we have that
$\Gamma\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{P}}\phi$ holds.

The proof follows immediately from Lemma 8 and the inductive clauses of
Definition 10. Note however, that the support relation is monotone _only_ with
respect to the base, not with respect to the context. Were it so, it would
correspond to having a notion of weakening and contraction in the context.

We can now prove the main result of this section which describes the interplay
between our atomic derivability relation and our support relation on
propositional atoms.

######  Lemma 13 (Soundness and completeness for atomic systems).

${P},{S}\vdash_{\\!\\!\mathscr{B}}{q}$ iff
${P}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S}}{q}$.

###### Proof.

If ${P}=\varnothing$, then the result holds immediately by ((At)). So consider
${P}=\\{{p}_{1},\dots,{p}_{n}\\}$. Proceeding from left to right, we begin by
immediately applying Lemma 9 to the hypothesis which gives us that for all
$\mathscr{C}\supseteq\mathscr{B}$ and atomic multisets ${T}_{i}$ such that
${T}_{i}\vdash_{\\!\\!\mathscr{C}}{p}_{i}$ for $i=1,\dots,n$, that we have
${T}_{1},\dots,{T}_{n},{S}\vdash_{\\!\\!\mathscr{C}}{q}$. By ((At)), this
means that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{T}_{1},\dots,{T}_{n},{S}}{q}$.
Thus by ((Inf)) we conclude that
${P}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S}}{q}$, since again by ((At))
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{T}_{i}}{p}_{i}$ for $i=1,\dots,n$.
Finally, because ((Inf)), ((At)) and Lemma 9 are bi-implications, that
therefore completes the proof. ∎

##  4 Soundness

######  Theorem 14 (Soundness).

If $\Gamma\vdash_{\mathrm{IMALL}}\varphi$, then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$.

###### Proof.

By the inductive definition of $\vdash_{\mathrm{IMALL}}$, it suffices to prove
the following:

(Ax)

$\varphi\Vdash_{\\!\\!}^{\\!\\!}\varphi$

($\multimap$I)

If $\Gamma,\varphi\Vdash_{\\!\\!}^{\\!\\!}\psi$, then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\multimap\psi$.

($\multimap$E)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\multimap\psi$ and
$\Delta\Vdash_{\\!\\!}^{\\!\\!}\varphi$, then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\psi$.

($\otimes$I)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ and
$\Delta\Vdash_{\\!\\!}^{\\!\\!}\psi$, then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\varphi\otimes\psi$.

($\otimes$E)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\otimes\psi$ and
$\Delta,\varphi,\psi\Vdash_{\\!\\!}^{\\!\\!}\chi$, then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\chi$.

($1$I)

$\Vdash_{\\!\\!}^{\\!\\!}1$

($1$E)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}1$ and
$\Delta\Vdash_{\\!\\!}^{\\!\\!}\varphi$ then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\varphi$.

($\with$I)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ and
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\psi$ then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\with\psi$.

($\with$E)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\with\psi$ then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ and
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\psi$.

($\oplus$I)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ or
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\psi$ then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\oplus\psi$.

($\oplus$E)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\oplus\psi$ and
$\Delta,\varphi\Vdash_{\\!\\!}^{\\!\\!}\chi$ and
$\Delta,\psi\Vdash_{\\!\\!}^{\\!\\!}\chi$ then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\chi$.

($0$E)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}0$ then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\chi$.

We now proceed through the cases. In some cases, the proofs are supported by
the use of what we dub “elimination rule lemmas”; these lemmas are included in
Appendix A:

  * -

The following cases are proven in [4]: ((Ax)), (($\multimap$I)),
(($\multimap$E)), (($\otimes$I)), (($\otimes$E)), (($1$I)), (($1$E))
Note that for the case of (($\otimes$E)), the lemma used in the proof needs to
be extended to include the cases where $\chi$ contains an additive connective.
This is done in lemma 32. Similarly, in the case of (($1$E)), the lemma used
in the proof needs to be similarly extended. This is done in lemma 33.

  * -

(($\with$I)). We assume $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ and
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\psi$. Fix $\mathscr{B}$ and ${L}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\Gamma$. Thus, by ((Inf)), we have that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\psi$. Thus by (($\with$)) we have
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\varphi\with\psi$, and thus by ((Inf)) we
conclude $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\with\psi$.

  * -

(($\with$E)). We assume $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\with\psi$. Fix
$\mathscr{B}$ and ${L}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\Gamma$, we then have by ((Inf)) that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi\with\psi$. By (($\with$)) we
thus get that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\psi$, which by ((Inf)) gives
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ and
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\psi$ as desired.

  * -

(($\oplus$I)). We assume $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ or
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\psi$ holds. Fix $\mathscr{B}$ and ${L}$ such
that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\Gamma$ holds. Thus, by ((Inf)) we
have that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi$ or
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\psi$ hold. Thus by (($\oplus$)), we
have that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi\oplus\psi$ holds.
Thus by ((Inf)) we conclude $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\oplus\psi$,
as desired.

  * -

(($\oplus$E)). We suppose $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi\oplus\psi$
and that both $\Delta,\varphi\Vdash_{\\!\\!}^{\\!\\!}\chi$ and
$\Delta,\psi\Vdash_{\\!\\!}^{\\!\\!}\chi$ hold and want to show that
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\chi$. By ((Inf)), this is equivalent to
showing that for all $\mathscr{B}$ and ${P}={Q},{R}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\Gamma,\Delta$ (where
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{Q}}\Gamma$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{R}}\Delta$) that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\chi$.

Fix $\mathscr{B}$ and ${Q}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{Q}}\Gamma$. Thus, by ((Inf)), we have that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{Q}}\varphi\oplus\psi$.

Moreover, we have by monotonicity that
$\Delta,\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!}\chi$. Applying ((Inf))
gives that for all $\mathscr{C}\supseteq\mathscr{B}$ and atomic multisets
${M}={R},{S}$ such that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}\Delta,\varphi$
(where $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{R}}\Delta$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S}}\varphi$) that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}\chi$. Rewriting this as
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{R},{S}}\chi$, by ((Inf)), we conclude that
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{R}}\chi$. A similar argument gives
also that $\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{R}}\chi$. Thus by induction
on the structure of $\chi$ and Lemma 31 we conclude that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{Q},{R}}\chi$ or more simply,
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{P}}\chi$ as desired.

  * -

(($0$E)). We suppose $\Gamma\Vdash_{\\!\\!}^{\\!\\!}0$. We fix some base
$\mathscr{B}$ and atomic multiset ${L}$ such that we conclude by ((Inf)) that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}0$. Spelling out the definition of
(($0$)) gives that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{p}$ for all atomic
${p}$. Thus by induction on the structure of any formula $\chi$ we get that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\chi$, and thus by ((Inf)) that
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\chi$.

This complete the proof of all items. ∎

##  5 Completeness

######  Theorem 15 (Completeness).

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$, then
$\Gamma\vdash_{\mathrm{IMALL}}\varphi$.

The goal of this section is to prove that the semantics are complete with
respect to IMALL. The proof presented is very similar to the proof of
completeness in [4] for IMLL and [8] for IPL and consequently, the cases for
IMLL are again noted but not included. The strategy goes as follows:

  1. 1.

Define two functions which allow us to uniquely map formulas to atoms and
vice-versa. Finding such atoms is always possible as our set of atoms is
countable.

  2. 2.

Show that any valid judgement remains valid when flattened using the
previously defined functions.

  3. 3.

Construct a base whose rules simulate the natural deduction rules of IMALL.

  4. 4.

Show that every derivation in this simulation base is equivalent to the
corresponding derivation in IMALL.

  5. 5.

Show we can go from a valid judgement to a derivation in IMALL.

For this section we will assume that we are working on the sequent
$\langle\Gamma,\varphi\rangle$ and that $\Xi$ is the set of all subformulas in
$\Gamma\cup\\{\varphi\\}$. We also define an extended set of atoms
$\widetilde{\mathrm{At}}=\mathrm{At}\cup\\{0,1\\}$.

######  Definition 16 (Flattening and naturalising functions).

We define a class of functions called flattening functions ${(\cdot)}^{\flat}$
as:

${\alpha}^{\flat}=\begin{cases*}\alpha&when
$\alpha\in\widetilde{\mathrm{At}}$,\\\ {p}&for ${p}\notin\Xi$ and for all
$\beta\in\Xi$ such that $\beta\neq\alpha$ then
${\beta}^{\flat}\neq{\alpha}^{\flat}$\end{cases*}$

Each flattening function ${(\cdot)}^{\flat}$ has an inverse,
${(\cdot)}^{\natural}$, called the naturalising function and is defined as:

${{p}}^{\natural}=\begin{cases*}{p}&when ${p}\in\widetilde{\mathrm{At}}$,\\\
{({\alpha}^{\flat})}^{\natural}=\alpha&otherwise.\end{cases*}$

Such functions distribute over elements of multisets i.e. if
$\Gamma=\\{\gamma_{1},\dots,\gamma_{n}\\}$ then
${\Gamma}^{\flat}=\\{{\gamma_{1}}^{\flat},\dots,{\gamma_{n}}^{\flat}\\}$ and
${\Gamma}^{\natural}=\\{{\gamma_{1}}^{\natural},\dots,{\gamma_{n}}^{\natural}\\}$.

One might wish to question the existence of such flattening functions. Indeed,
their existence follows immediately from the injectivity of
${(\cdot)}^{\flat}$ as one may pick any atom in $\mathrm{At}$ to assign to a
formula, so long as that atom has not been already assigned a formula or is
not already an atom in $\Xi$. Since $\mathrm{At}$ is countable, we always have
enough atoms with which to do this assignment. The existence of a
corresponding ${(\cdot)}^{\natural}$ for any given ${(\cdot)}^{\flat}$ is
immediate. For the rest of this work, we assume a generic such
${(\cdot)}^{\flat}$ as the particulars of the assignments are irrelevent to
our treatment.
We now with to construct a base $\mathscr{N}$ using such a flattening
function, in a similar fashion to that found in [8] to simulate the rules of
natural deduction for IMALL.

######  Definition 17 (Simulation Base $\mathscr{N}$).

Given a flattening function ${(\cdot)}^{\flat}$, we define the base
$\mathscr{N}$ to contain the following rules, where $\alpha$ and $\beta$ are
universally quantified over all elements of $\Xi$ and ${p}$ is universally
quantified over all elements of $\mathrm{At}$:

  1. 1.

$\\{({\alpha}^{\flat}\Rightarrow{\beta}^{\flat})\\}\Rightarrow{(\alpha\multimap\beta)}^{\flat}$

  2. 2.

$\\{(\Rightarrow{(\alpha\multimap\beta)}^{\flat})\\},\\{(\Rightarrow{\alpha}^{\flat})\\}\Rightarrow{\beta}^{\flat}$

  3. 3.

$\\{(\Rightarrow{\alpha}^{\flat})\\},\\{(\Rightarrow{\beta}^{\flat})\\}\Rightarrow{(\alpha\otimes\beta)}^{\flat}$

  4. 4.

$\\{(\Rightarrow{(\alpha\otimes\beta)}^{\flat})\\},\\{({\alpha}^{\flat},{\beta}^{\flat}\Rightarrow{p})\\}\Rightarrow{p}$

  5. 5.

$\\{(\Rightarrow{(\alpha\otimes\beta)}^{\flat})\\},\\{({\alpha}^{\flat},{\beta}^{\flat}\Rightarrow
1)\\}\Rightarrow 1$

  6. 6.

$\Rightarrow 1$

  1. 7.

$\\{(\Rightarrow{\alpha}^{\flat}),(\Rightarrow{\beta}^{\flat})\\}\Rightarrow{(\alpha\with\beta)}^{\flat}$

  2. 8.

$\\{(\Rightarrow{(\alpha\with\beta)}^{\flat})\\}\Rightarrow{\alpha}^{\flat}$

  3. 9.

$\\{(\Rightarrow{(\alpha\with\beta)}^{\flat})\\}\Rightarrow{\beta}^{\flat}$

  4. 10.

$\\{(\Rightarrow{\alpha}^{\flat})\\}\Rightarrow{(\alpha\oplus\beta)}^{\flat}$

  5. 11.

$\\{(\Rightarrow{\beta}^{\flat})\\}\Rightarrow{(\alpha\oplus\beta)}^{\flat}$

  6. 12.

$\\{(\Rightarrow{(\alpha\oplus\beta)}^{\flat})\\},\\{({\alpha}^{\flat}\Rightarrow{p}),({\beta}^{\flat}\Rightarrow{p})\\}\Rightarrow
p$

  7. 13.

$\\{(\Rightarrow{0}^{\flat})\\}\Rightarrow{p}$

Note that by defining a base $\mathscr{N}$, we must fix a particular
flattening function ${(\cdot)}^{\flat}$ which gives a corresponding inverse
${(\cdot)}^{\natural}$. Where $\mathscr{N}$ is considered in the following
section, this will be implicit.
We are now ready to prove the key lemmas that will give us the tools with
which to prove completeness. We begin by making the following observations
about ${(\cdot)}^{\flat}$ in relation to (($\with$)) and (($\oplus$)). This
extends similar observations made in [4] about (($\otimes$)) and
(($\multimap$)).

######  Proposition 18.

The following hold for arbitrary bases $\mathscr{B}\supseteq\mathscr{N}$ and
atomic multiset ${U}$, for arbitrary $\alpha$ and $\beta$ in $\Xi$:

  1. 1.

${U}\vdash_{\\!\\!\mathscr{B}}{(\alpha\with\beta)}^{\flat}$ iff
${U}\vdash_{\\!\\!\mathscr{B}}{\alpha}^{\flat}\text{ and
}{U}\vdash_{\\!\\!\mathscr{B}}{\beta}^{\flat}$

  2. 2.

${U}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}$ iff for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${K}$ and atomic ${p}$,
such that ${K},{\alpha}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$ and
${K},{\beta}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$ then,
${U},{K}\vdash_{\\!\\!\mathscr{C}}{p}$

###### Proof.

Let us fix arbitrary base $\mathscr{B}\supseteq\mathscr{N}$ and atomic
multiset ${S}$.

  1. 1.

Showing both sides separately:

     * •

Left to right: We assume that
${L}\vdash_{\\!\\!\mathscr{B}}{(\alpha\with\beta)}^{\flat}$ and want to show
that both ${L}\vdash_{\\!\\!\mathscr{B}}{\alpha}^{\flat}$ and
${L}\vdash_{\\!\\!\mathscr{B}}{\beta}^{\flat}$ hold. From the rules
$\\{(\Rightarrow{(\alpha\with\beta)}^{\flat})\\}\Rightarrow{\alpha}^{\flat}$
and
$\\{(\Rightarrow{(\alpha\with\beta)}^{\flat})\\}\Rightarrow{\beta}^{\flat}$
and ((App)) we are able to derive the desired result.

     * •

Right to left: Assuming that ${L}\vdash_{\\!\\!\mathscr{B}}{\alpha}^{\flat}$
and ${L}\vdash_{\\!\\!\mathscr{B}}{\beta}^{\flat}$ holds we want to show that
${L}\vdash_{\\!\\!\mathscr{B}}{(\alpha\with\beta)}^{\flat}$. From the atomic
rule
$\\{((\Rightarrow{\alpha}^{\flat}),(\Rightarrow{\beta}^{\flat}))\\}\Rightarrow{(\alpha\with\beta)}^{\flat}$
and ((App)), we are able to derive our conclusion.

  2. 2.

Once again, showing both sides separately:

     * •

Left to right: We have
${U}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}$ and want to show
that for all $\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${K}$ and
atomic ${p}$, such that ${K},{\alpha}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$
and ${K},{\beta}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$ then,
${U},{K}\vdash_{\\!\\!\mathscr{C}}{p}$. Since
$\mathscr{B}\subseteq\mathscr{C}$ then we have that
${U}\vdash_{\\!\\!\mathscr{C}}{(\alpha\oplus\beta)}^{\flat}$ holds. Then
considering what is given as follows allows us to use ((App)) to derive our
result:

       1. (a)

${U},{\varnothing}\vdash_{\\!\\!\mathscr{C}}{(\alpha\oplus\beta)}^{\flat}$

       2. (b)

${K},{\alpha}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$

       3. (c)

${K},{\beta}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$

Thus by the atomic rule
$\\{(\Rightarrow{(\alpha\oplus\beta)}^{\flat})\\},\\{({\alpha}^{\flat}\Rightarrow{p}),({\beta}^{\flat}\Rightarrow{p})\\}\Rightarrow
p$, since relations (b) and (c) have the same context ${K}$ then we conclude
that ${U},{K}\vdash_{\\!\\!\mathscr{C}}{p}$ as desired.

     * •

Right to left: Given that for all $\mathscr{C}\supseteq\mathscr{B}$, atomic
multisets ${K}$ and atomic ${p}$, such that
${K},{\alpha}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$ and
${K},{\beta}^{\flat}\vdash_{\\!\\!\mathscr{C}}{p}$ then,
${U},{K}\vdash_{\\!\\!\mathscr{C}}{p}$ then we want to show that
${U}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}$. In particular
our hypotheses hold in the case where $\mathscr{C}=\mathscr{B}$ and
${p}={(\alpha\oplus\beta)}^{\flat}$ and ${K}=\varnothing$. Thus our hypothesis
gives us that:

$\displaystyle\text{If
}{\alpha}^{\flat}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}\text{
and
}{\beta}^{\flat}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}\text{
then }{U}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}$

We show the case for the first relation as the second follows similarly. To
apply ((App)) with the rule
$\\{(\Rightarrow{\alpha}^{\flat})\\}\Rightarrow{(\alpha\oplus\beta)}^{\flat}$
we need to show that we can derive ${\alpha}^{\flat}$ from some context ${C}$.
Since by ((Ref)) we have that
${\alpha}^{\flat}\vdash_{\\!\\!\mathscr{B}}{\alpha}^{\flat}$ then we simply
put ${C}={\alpha}^{\flat}$ giving us the correct precondition to use the rule,
namely ${\alpha}^{\flat},\varnothing\vdash_{\\!\\!B}{\alpha}^{\flat}$. Thus we
get by ((App)) that
${\alpha}^{\flat}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}$.
Thus we conclude that
${U}\vdash_{\\!\\!\mathscr{B}}{(\alpha\oplus\beta)}^{\flat}$ as desired.

This completes the proof for both statements. ∎

######  Lemma 19.

For every $\xi\in\Xi$, $\mathscr{B}\supseteq\mathscr{N}$ and atomic multiset
${L}$, we have that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{\xi}^{\flat}$ iff
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\xi$.

###### Proof.

We begin by fixing an arbitrary $\mathscr{B}\supseteq\mathscr{N}$, atomic
multiset ${L}$ and prove by induction on the structure of $\xi$. The cases
where the topmost connective of $\xi$ is (($\otimes$)) and (($\multimap$)) and
where $\xi$ is atomic and (($1$)) are considered in [4]. So we consider the
cases where the topmost connective of $\xi$ is (($\with$)), (($\oplus$)) and
where $\xi$ is (($0$)). We take these three cases in turn:

  * •

$\xi$ is of the form $\alpha\with\beta$. Then, since $\alpha$ and $\beta$ are
both in $\Xi$, we have the following:

$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{(\alpha\with\beta)}^{\flat}$
$\displaystyle\text{ iff
}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{\alpha}^{\flat}\text{ and
}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{\beta}^{\flat}$ (Prop. 18 and Lemma
13) $\displaystyle\text{ iff
}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\alpha\text{ and
}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\beta$ (IH) $\displaystyle\text{ iff
}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\alpha\with\beta$

  * •

$\xi$ is of the form $\alpha\oplus\beta$. Then again, Then, since $\alpha$ and
$\beta$ are both in $\Xi$, we have the following:

$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}{(\alpha\oplus\beta)}^{\flat}$
$\displaystyle\text{ iff for every
}\mathscr{C}\supseteq\mathscr{B},{K},{p},\text{ if
}{\alpha}^{\flat}\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}{p}\text{ and
}{\beta}^{\flat}\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}{p},\text{ then
}\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K}}{p}$ (Prop. 18 and Lemma 13)
$\displaystyle\text{ iff for every
}\mathscr{C}\supseteq\mathscr{B},{K},{p},\text{ if
}\alpha\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}{p}\text{ and
}\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}{p},\text{ then
}\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K}}{p}$ (IH) $\displaystyle\text{ iff
}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\alpha\otimes\beta.$ (($\otimes$))

  * •

Finally, $\xi$ is of the form $0$. Then by definition ${0}^{\flat}=0$.

This concludes our induction on $\xi$ and thus our proof of Lemma 19. ∎

######  Lemma 20.

For every atomic multiset ${P}$ and atom ${q}$, if
${P}\vdash_{\\!\\!\mathscr{N}}{q}$ then
${{P}}^{\natural}\vdash_{\mathrm{IMALL}}{{q}}^{\natural}$.

###### Proof.

We begin by noting that by the definition of $\mathscr{N}$ it suffices to show
the following:

  * •

${{p}}^{\natural}\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$.

  * •

If
$(\\{({P_{1_{i}}}\Rightarrow{p_{1_{i}}})\\}^{l_{1}}_{i=1},\dots,\\{({P_{n_{i}}}\Rightarrow{p_{n_{i}}})\\}^{l_{n}}_{i=1}\Rightarrow{r})\in\mathscr{N}$
and
${{C}_{i}}^{\natural},{{P}_{i_{j}}}^{\natural}\vdash_{\mathrm{IMALL}}{p}_{i_{j}}$
for $j=1,\dots,l_{i}$ and $i=1,\dots,n$ then
${C}_{1},\dots,{C}_{n}\vdash_{\mathrm{IMALL}}{r}$.

The first point holds true by the (Ax) rule of our natural deduction system.
The second point requires analysis of the rules in $\mathscr{N}$. Luckily, we
know them all, and thus all that is left to show is that for each rule and
given sufficient premiss, that we can conclude as expected. For rules (1) to
(6), we again cite [4] as those cases are considered there. Thus we only
consider rules (7) to (13) below:

  1. 7.

Suppose
$\\{(\Rightarrow{\alpha}^{\flat}),(\Rightarrow{\beta}^{\flat})\\}\Rightarrow{(\alpha\with\beta)}^{\flat}$
is in $\mathscr{N}$. Then we want to show that given
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({\alpha}^{\flat})}^{\natural}$ and
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({\beta}^{\flat})}^{\natural}$, we
conclude that ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\with\beta$. By
the definition of ${(\cdot)}^{\natural}$, our hypothesis is eqivalent to
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha$ and
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\beta$ which by ($\with$-I), gives
that ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\with\beta$.

  2. 8.

Suppose
$\\{(\Rightarrow{(\alpha\with\beta)}^{\flat})\\}\Rightarrow{\alpha}^{\flat}$
is in $\mathscr{N}$. Then we want to show that given
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({(\alpha\with\beta)}^{\flat})}^{\natural}$
we can conclude ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha$. By the
definition of ${(\cdot)}^{\natural}$, our hypothesis is eqivalent to
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\with\beta$. Thus by
($\with$-E), we conclude crucially that
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha$.

  3. 9.

Suppose
$\\{(\Rightarrow{(\alpha\with\beta)}^{\flat})\\}\Rightarrow{\beta}^{\flat}$ is
in $\mathscr{N}$. Then we want to show that given
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({(\alpha\with\beta)}^{\flat})}^{\natural}$
we can conclude ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\beta$. By the
definition of ${(\cdot)}^{\natural}$, our hypothesis is eqivalent to
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\with\beta$. Thus by
($\with$-E), we conclude crucially that
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\beta$.

  4. 10.

Suppose
$\\{(\Rightarrow{\alpha}^{\flat})\\}\Rightarrow{(\alpha\oplus\beta)}^{\flat}$
is in $\mathscr{N}$. Then we want to show that given
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({\alpha}^{\flat})}^{\natural}$ that
we can prove ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\oplus\beta$. By
the definition of ${(\cdot)}^{\natural}$, our hypothesis is eqivalent to
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha$. Thus, by ($\oplus$-I) we
conclude that ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\oplus\beta$.

  5. 11.

Suppose
$\\{(\Rightarrow{\beta}^{\flat})\\}\Rightarrow{(\alpha\oplus\beta)}^{\flat}$
is in $\mathscr{N}$. Then we want to show that given
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({\beta}^{\flat})}^{\natural}$ that
we can prove ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\oplus\beta$. By
the definition of ${(\cdot)}^{\natural}$, our hypothesis is eqivalent to
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\beta$. Thus, by ($\oplus$-I), we
conclude that ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\oplus\beta$.

  6. 12.

Suppose
$\\{(\Rightarrow{(\alpha\oplus\beta)}^{\flat})\\},\\{({\alpha}^{\flat}\Rightarrow{p}),({\beta}^{\flat}\Rightarrow{p})\\}\Rightarrow
p$ is in $\mathscr{N}$. Then we want to show that given:

     * •

${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({(\alpha\oplus\beta)}^{\flat})}^{\natural}$

     * •

${{K}}^{\natural},{({\alpha}^{\flat})}^{\natural}\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$

     * •

${{K}}^{\natural},{({\beta}^{\flat})}^{\natural}\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$.

we can prove that
${{C}}^{\natural},{{K}}^{\natural}\vdash_{\mathrm{IMALL}}{p}^{\natural}$.
By the definition of ${(\cdot)}^{\natural}$, our hypothesis is eqivalent to

     * •

${{C}}^{\natural}\vdash_{\mathrm{IMALL}}\alpha\oplus\beta$

     * •

${{K}}^{\natural},\alpha\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$

     * •

${{K}}^{\natural},\beta\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$.

Thus, by ($\oplus$-E), we conclude that
${{C}}^{\natural},{{K}}^{\natural}\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$.

  7. 13.

Suppose $\\{(\Rightarrow{0}^{\flat})\\}\Rightarrow{p}$ is in $\mathscr{N}$.
Then we want to show that given
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{({0}^{\flat})}^{\natural}$ we can
conclude ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$ for all
atomic ${p}$. By the definition of ${(\cdot)}^{\natural}$, our hypothesis is
eqivalent to ${{C}}^{\natural}\vdash_{\mathrm{IMALL}}0$. Thus by ($0$-E) and
our atomic rule, we can conclude that
${{C}}^{\natural}\vdash_{\mathrm{IMALL}}{{p}}^{\natural}$.

This completes the case analysis for establising Lemma 20. ∎

We can now prove the statement of completeness, namely that if
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$, then
$\Gamma\vdash_{\mathrm{IMALL}}\varphi$. This part of the proof is the same as
in [4], but we include it for completeness.

###### Proof of Theorem 15.

Given that $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$, we begin by fixing some
arbitrary base $\mathscr{B}\supseteq\mathscr{N}$ with atomic multiset ${C}$
such that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{C}}{\Gamma}^{\flat}$ (which give
us the hypothesis for using ((Inf))). Since Lemma 19 is bidirectional, we have
that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{C}}\Gamma$ and thus we get that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{C}}\varphi$. Therefore, it must hold that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{C}}{\varphi}^{\flat}$ from which we get
${\Gamma}^{\flat}\Vdash_{\\!\\!\mathscr{N}}^{\\!\\!}{\varphi}^{\flat}$ by
((Inf)). By Lemma 13, we get from
${\Gamma}^{\flat}\Vdash_{\\!\\!\mathscr{N}}^{\\!\\!}{\varphi}^{\flat}$ that
${\Gamma}^{\flat}\vdash_{\\!\\!\mathscr{N}}{\varphi}^{\flat}$ holds. Thus, by
Lemma 20, we have that
${\Gamma}^{\flat}\vdash_{\mathrm{IMALL}}{\varphi}^{\flat}$. Finally, by the
definitions of ${(\cdot)}^{\flat}$ and ${(\cdot)}^{\natural}$, we get can
unflatten this equation giving
${({\Gamma}^{\flat})}^{\natural}\vdash_{\mathrm{IMALL}}{({\varphi}^{\flat})}^{\natural}$
which is nothing more than $\Gamma\vdash_{\mathrm{IMALL}}\varphi$ as desired.
∎

##  6 Extension to ILL

If we wish to extend our semantics for IMALL to a semantics for Intuitionistic
Linear Logic we must begin by extending our notion of derivability in IMALL to
include rules for the exponential of ILL. We could use the system given in
[7], which introduces a single introduction and elimination rule for
$\mathop{!}$ as this would have fewer cases to consider and is equivalent to
the system we will consider herein. However, we instead opt for a more
explicit system, such as that given in [2], opting to change the form of the
dereliction rule, from the simple form as is presented in the paper, to a form
closer to a generalised elimination rule, noting that the author themselves
makes note of the fact that both systems are equivalent, and makes their in
their work choice for simplicity. We also choose to use this system for
conceptual simplicity and ease of understanding. To recap:

######  Definition 21.

Formulas of ILL are defined inductively as follows:

$\mathsf{Form}\ni\varphi,\psi::={p}\mid\varphi\otimes\psi\mid
1\mid\varphi\multimap\psi\mid\varphi\with\psi\mid\varphi\oplus\psi\mid
0\mid\mathop{!}\varphi$

Our notion of derivability in ILL, based on the natural deduction system in
[2], is defined as follows:

######  Definition 22.

The derivability relation $\vdash_{\mathrm{ILL}}$ is defined inductively as
for $\vdash_{\mathrm{IMALL}}$ with following additional four rules:

$\Gamma_{1}\vdash_{\mathrm{ILL}}\mathop{!}\psi_{1}$ $\ldots$
$\Gamma_{n}\vdash_{\mathrm{ILL}}\mathop{!}\psi_{n}$
$\mathop{!}\psi_{1},\ldots,\mathop{!}\psi_{n}\vdash_{\mathrm{ILL}}\varphi$
$\mathop{!}$-Promotion
$\Gamma_{1},\ldots,\Gamma_{n}\vdash_{\mathrm{ILL}}\mathop{!}\varphi$

$\Gamma\vdash_{\mathrm{ILL}}\mathop{!}\varphi$
$\Delta,\varphi\vdash_{\mathrm{ILL}}\psi$ $\mathop{!}$-Dereliction
$\Gamma,\Delta\vdash_{\mathrm{ILL}}\psi$

$\Gamma\vdash_{\mathrm{ILL}}\mathop{!}\varphi$
$\Delta\vdash_{\mathrm{ILL}}\psi$ $\mathop{!}$-Weakening
$\Gamma,\Delta\vdash_{\mathrm{ILL}}\psi$

$\Gamma\vdash_{\mathrm{ILL}}\mathop{!}\varphi$
$\Delta,\mathop{!}\varphi,\mathop{!}\varphi\vdash_{\mathrm{ILL}}\psi$
$\mathop{!}$-Contraction $\Gamma,\Delta\vdash_{\mathrm{ILL}}\psi$

We also have the following definition for a sequent in ILL.

######  Definition 23 (Sequent).

A sequent is a pair $\langle\Theta,\varphi\rangle$, where $\Theta$ is a
multiset of ILL formulas and $\varphi$ is a single ILL formula.

We give the following definition of support over a base.

######  Definition 24.

The relation of support is defined inductively as in Definition 10, extended
as follows:

($\mathop{!}$)

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\mathop{!}\varphi$ iff for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${K}$, atoms ${p}$, if for
all $\mathscr{D}\supseteq\mathscr{C}$ such that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!\varnothing}\varphi$ then
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K}}{p}$, then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K}}{p}$.

(Inf)

Suppose $\Gamma$ is non-empty. Then,
$\Gamma\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi$ iff for all
$\mathscr{C}\supseteq\mathscr{B}$ and atomic multisets ${K}$, if
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}\Gamma$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K}}\varphi$.

(iInf)

Suppose $\mathop{!}\Gamma$ is non-empty. Then
$\mathop{!}\Gamma\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\varphi$ iff for all
$\mathscr{C}\supseteq\mathscr{B}$, if
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!\varnothing}\Gamma$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!L}\varphi$.

A couple of points about these semantical clauses:

  * •

We note immediately, that by ((iInf)), our clause for (($\mathop{!}$)) can be
simplified as follows:

$\small\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\mathop{!}\varphi\text{ iff for
all bases }\mathscr{C}\supseteq\mathscr{B}\text{, atomic multisets }K\text{,
and atoms }{p}\text{, if
}\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!K}p\text{ then
}\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!K}p.$

We will make use of this form of the definition herein.

  * •

For any support judgement,
$\Gamma\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\varphi$, there is precisely one
rule of inference that can be directly used. If $\Gamma$ contains any formulas
whose top-level connective is not (($\mathop{!}$)) one must use ((Inf)). Else,
one must use ((iInf)). Thus, there is never any ambiguity as to what the
definition of a sequent is, as every sequent falls into one of these two
categories.

  * •

Our support relation is still monotone with respect to bases, as in the case
for IMALL.

Subsequently, our notion of validity has not changed. A sequent
$\langle\Gamma,\varphi\rangle$ is valid if and only if
$\Gamma\Vdash_{\\!\\!\varnothing}^{\\!\\!\varnothing}\varphi$ holds. Recall,
we abbreviate this as $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$.

###  6.1 Soundness

Proving the soundness of our semantics for ILL, for the most part, is exactly
the same as in the case for IMALL. However, we now have to consider the
following further two things:

  * •

For the elimination rule lemmas (Lemmas 31, 32, 33), the case where
$\chi=\mathop{!}\alpha$. We do not provide these proofs as they are entirely
similar to other cases in the aforementioned lemmas.

  * •

That the semantics is sound with respect to the four rules governing the
behaviour of (($\mathop{!}$)). We prove these below as they require some new
techniques.

To prove soundness, we will need the following lemmas:

######  Lemma 25.

Given $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}\varphi$ and for all
$\mathscr{X}\supseteq\mathscr{B}$ if
$\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!L}\psi$ then
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!L}\psi$.

###### Proof.

Lemma 12 tells us that if
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}\varphi$ then for all
$\mathscr{X}\supseteq\mathscr{B}$, we have that
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\varnothing}\varphi$ holds.
By ((iInf)), our second hypothesis says for all bases
$\mathscr{Y}\supseteq\mathscr{X}$, if
$\Vdash_{\\!\\!\mathscr{Y}}^{\\!\\!\varnothing}\varphi$ then
$\Vdash_{\\!\\!\mathscr{Y}}^{\\!\\!L}\psi$. By proposition 12, we thus have
that $\Vdash_{\\!\\!\mathscr{Y}}^{\\!\\!\varnothing}\varphi$. Therefore, we
have that $\Vdash_{\\!\\!\mathscr{Y}}^{\\!\\!L}\psi$. Since this holds in all
extensions over the base $\mathscr{X}$, then we have in particular that
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!L}\psi$, as desired. ∎

######  Corollary 26.

Given $\mathop{!}\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$ then
$\mathop{!}\Gamma\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$.

###### Proof.

We start by considering all bases $\mathscr{B}$ where $\mathop{!}\Gamma$ is
supported. Thus, our statement becomes, under this quantifier, given
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}\varphi$ then
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}\mathop{!}\varphi$. This is
equivalent to saying given
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}\varphi$ and that for all bases
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets $K$ and atoms $p$ such
that $\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!K}{p}$, we want to
show that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!K}{p}$ holds. This immediately
follows by monotonicity (proposition 12) and lemma 25. ∎

######  Lemma 27.

Given $\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\psi$ then
$\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\psi$.

###### Proof.

This follows immediately by ((Inf)) and ((iInf)). ∎

We now give some lemmas related to $1$ that are useful in proving the
following soundness results.

######  Lemma 28.

Given $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\mathop{!}\varphi$ then
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}1$.

###### Proof.

To prove this, it is equivalent to prove that given for all
$\mathscr{X}\supseteq\mathscr{B}$, atomic multisets $K$ and atoms ${p}$, such
that $\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!K}{p}$ implies
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!L,K}{p}$ and for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets $M$ and atoms ${p}$, such
that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!M}{p}$, that we show
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!L,M}{p}$. Expanding
$\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!K}{p}$ gives us that for
all $\mathscr{Y}\supseteq\mathscr{X}$ if
$\Vdash_{\\!\\!\mathscr{Y}}^{\\!\\!\varnothing}\varphi$ then
$\Vdash_{\\!\\!\mathscr{Y}}^{\\!\\!M}{p}$. We see that, in particular at
$\mathscr{Y}=\mathscr{X}=\mathscr{C}$ and when $M=K$ this implication holds
true since we are given that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!M}{p}$ by
hypothesis. Thus, we obtain that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!L,M}{p}$,
as desired. ∎

It is obvious by expanding the definition of $1$ that
$\Vdash_{\\!\\!\varnothing}^{\\!\\!\varnothing}1$ is valid. As a consequence,
by lemma 33, it is the case that for any $\varphi$, we have that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\varphi\Rightarrow
1\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\varphi$, since we can always cut with
$\Vdash_{\\!\\!}^{\\!\\!}1$. Furthermore, we have that if
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}1$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}1$ hold, then
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L,K}1$ also holds, again by cut. These
minor technical results will be useful in what follows.

######  Proposition 29 (Soundness for ILL).

If $\Gamma\vdash_{\mathrm{ILL}}\varphi$ then
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\varphi$.

###### Proof.

By the inductive definition of $\vdash_{\mathrm{ILL}}$, it suffices to prove
the following:

($\mathop{!}$-Promotion)

If
$\Gamma_{1}\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\psi_{1}$,…,$\Gamma_{n}\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\psi_{n}$
and
$\mathop{!}\psi_{1},\dots,\mathop{!}\psi_{n}\Vdash_{\\!\\!}^{\\!\\!}\varphi$
then $\Gamma_{1},\dots,\Gamma_{n}\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$.
By lemma 26, we have that the second hypothesis gives that
$\mathop{!}\psi_{1},\dots,\mathop{!}\psi_{n}\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$.
By lemma 33, we know this implies
$\mathop{!}\psi_{1},\dots,\mathop{!}\psi_{n},1\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$.
Thus, by ((Inf)), we have for all $\mathscr{X}$ and multisets $L$ such that
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!L}\mathop{!}\psi_{1},\dots,\mathop{!}\psi_{n},1$
that $\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!L}\mathop{!}\varphi$. By taking base
extensions such that in a base $\mathscr{B}$, and for all multisets
$K_{1},\dots K_{n}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K_{i}}\Gamma_{i}$, we have that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K_{i}}\mathop{!}\psi_{i}$. Since we know
that $\Vdash_{\\!\\!\varnothing}^{\\!\\!\varnothing}1$, then by monotonicity,
we have that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\varnothing}1$. Thus, in
particular we have the case when $\mathscr{X}=\mathscr{B}$ and
$L=K_{1},\dots,K_{n}$. In this case we have
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K_{1},\dots,K_{n}}\mathop{!}\varphi$, which
is equivalent to
$\Gamma_{1},\dots,\Gamma_{n}\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$, as
desired.

($\mathop{!}$-Dereliction)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$, and
$\Delta,\varphi\Vdash_{\\!\\!}^{\\!\\!}\psi$ then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\psi$ holds. It suffices, by lemma 27,
to show that given $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\mathop{!}\varphi$ and
$\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$ that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L,K}\psi$ holds. The second hypothesis
implies $\mathop{!}\varphi\fatcomma
1\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$. From here, by ((Inf)), we obtain
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L,K}\psi$, as desired.

($\mathop{!}$-Weakening)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$ and
$\Delta\Vdash_{\\!\\!}^{\\!\\!}\psi$ then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\psi$. It suffices to show, given
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\mathop{!}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$ that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L,K}\psi$. By lemma 28, we have that the
first hypothesis implies $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}1$. Similarly,
the second hypothesis implies $1\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$.
Thus, by cutting on $1$ we obtain the desired result.

($\mathop{!}$-Contraction)

If $\Gamma\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$ and
$\Delta,\mathop{!}\varphi,\mathop{!}\varphi\Vdash_{\\!\\!}^{\\!\\!}\psi$ then
$\Gamma,\Delta\Vdash_{\\!\\!}^{\\!\\!}\psi$. It suffices to show that given
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\mathop{!}\varphi$ and
$\mathop{!}\varphi\fatcomma\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$
we can obtain $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L,K}\psi$. By ((iInf)), we
observe that the second hypothesis is equivalent to
$\mathop{!}\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$ which implies
$\mathop{!}\varphi\fatcomma 1\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!K}\psi$. Since
we know that $\Vdash_{\\!\\!}^{\\!\\!}1$, we can therefore cut on
$\mathop{!}\varphi\fatcomma 1$, giving us
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L,K}\psi$, as desired.

∎

###  6.2 Completeness

When we build our simulation base $\mathscr{N}$, we now add the following
rules, where $\alpha$ and $\beta_{i}$ are quantified over all elements of
$\Xi$ and $p$ is universally quantified over all elements of $\mathrm{At}$:

(Promotion)

For all $n\geq 0$,
$\\{(\Rightarrow{\mathop{!}\beta_{1}}^{\flat})\\},\ldots,\\{(\Rightarrow{\mathop{!}\beta_{n}}^{\flat})\\},({\mathop{!}\beta_{1}}^{\flat},\ldots,{\mathop{!}\beta_{n}}^{\flat}\Rightarrow\alpha)\Rightarrow{\mathop{!}\alpha}^{\flat}$.

(Dereliction)

$\\{(\Rightarrow{\mathop{!}\alpha}^{\flat})\\},\\{({\alpha}^{\flat}\Rightarrow{p})\\}\Rightarrow{p}$

(Weakening)

$\\{(\Rightarrow{\mathop{!}\alpha}^{\flat})\\},\\{(\Rightarrow{p})\\}\Rightarrow{p}$

(Contraction)

$\\{(\Rightarrow{\mathop{!}\alpha}^{\flat})\\},\\{({\mathop{!}\alpha}^{\flat},{\mathop{!}\alpha}^{\flat}\Rightarrow{p})\\}\Rightarrow{p}$

In the ((Promotion)) rule, the atomic sequent without an additive box is
intended to be read as a derivation for which there is no context multiset.
Thus, there must be a derivation of $\alpha$ directly from the hypothesis in
the rule. It is also _very_ important to note that the number of such
hypotheses can be $0$, and that we add a separate rule for each
$i\in\\{0,\dots,n\\}$.

######  Proposition 30.

This proposition is an extension of proposition 18.
The following holds for arbitrary bases $\mathscr{B}\supseteq\mathscr{N}$ and
atomic multiset ${L}$, for arbitrary $\alpha$ in $\Xi$:

  * •

${L}\vdash_{\\!\\!\mathscr{B}}{\mathop{!}\alpha}^{\flat}$ iff for every base
$\mathscr{C}\supseteq\mathscr{B}$, atomic multiset ${K}$, and atom ${p}$, if
for every base $\mathscr{D}\supseteq\mathscr{C}$ such that
$\vdash_{\\!\\!\mathscr{D}}{\alpha}^{\flat}$ implies
${K}\vdash_{\\!\\!\mathscr{D}}{p}$ then
${L},{K}\vdash_{\\!\\!\mathscr{C}}{p}$.

###### Proof.

We go left to right first. We have two cases to consider:

  * Case 1:

$\vdash_{\\!\\!\mathscr{D}}{\alpha}^{\flat}$ holds. In this case, by lemma 9,
we obtain ${\alpha}^{\flat},{K}\vdash_{\\!\\!\mathscr{C}}{p}$. Then, by the
((Dereliction)) rule, we obtain ${L},{K}\vdash_{\\!\\!\mathscr{C}}{p}$.

  * Case 2:

$\vdash_{\\!\\!\mathscr{D}}{\alpha}^{\flat}$ doesn’t hold. In this case, we
immediately obtain ${L},{K}\vdash_{\\!\\!\mathscr{C}}{p}$ by the ((Weakening))
rule.

Going right to left, we observe that the ((Promotion)) rule holds for
arbitrary many $\Gamma_{i}\vdash_{\mathrm{ILL}}\mathop{!}\psi_{i}$. In
particular, we consider the case when there are no such $i$. In that case, we
degenerate into the case where the inference,
$\vdash_{\\!\\!\mathscr{B}}{\alpha}^{\flat}$ implies
$\vdash_{\\!\\!\mathscr{B}}\mathop{!}{\alpha}^{\flat}$ is valid. Thus, by
restricting our attention to ${p}={\mathop{!}\alpha}^{\flat}$ and
${K}=\varnothing$ and when the base $\mathscr{C}=\mathscr{D}$, our hypotheses
now give us that $\vdash_{\\!\\!\mathscr{C}}{\alpha}^{\flat}$ and
$\vdash_{\\!\\!\mathscr{C}}{\mathop{!}\alpha}^{\flat}$ together imply
${L}\vdash_{\\!\\!\mathscr{C}}{\mathop{!}\alpha}^{\flat}$, which in particular
holds when $\mathscr{B}=\mathscr{C}$, thus leading to our desired conclusion.
∎

As mentioned, proposition 30 extends proposition 18, thus allowing us to
conlcude that lemma 19 still holds, i.e. for all
$\mathscr{B}\supseteq\mathscr{N}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}\mathop{!}\varphi$ iff
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!L}{\mathop{!}\varphi}^{\flat}$ as desired.

Lemma 20 also holds when $\mathscr{N}$ is extended to include the natural
deduction rules governing (($\mathop{!}$)). Thus, crucially,
$\Gamma\Vdash_{\\!\\!}^{\\!\\!}\mathop{!}\varphi$ implies
$\Gamma\vdash_{\mathrm{ILL}}\mathop{!}\varphi$, i.e. our completeness result
extends to include (($\mathop{!}$)).

## Acknowledgements

I would like to thank Timo Eckhardt, Alex Gheorghiu, Tao Gu, Victor
Nascimento, Elaine Pimentel and David Pym for our many discussions on PtS for
ILL, for all your suggestions and help with writing this manuscript. I am
grateful to you all!

## References

  * [1] Benton, N., G. Bierman, V. de Paiva and M. Hyland, _A term calculus for intuitionistic linear logic_ , in: M. Bezem and J. F. Groote, editors, _Typed Lambda Calculi and Applications_ (1993), pp. 75–90.
  * [2] Bierman, G., _On intuitionistic linear logic_ , Technical Report UCAM-CL-TR-346, University of Cambridge, Computer Laboratory (1994).
URL https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-346.pdf

  * [3] Eckhardt, T. and D. J. Pym, _Base-extension semantics for modal logic_ (2024).
  * [4] Gheorghiu, A. V., T. Gu and D. J. Pym, _Proof-theoretic semantics for intuitionistic multiplicative linear logic_ , in: R. Ramanayake and J. Urban, editors, _Automated Reasoning with Analytic Tableaux and Related Methods_ (2023), pp. 367–385.
  * [5] Gu, T., A. V. Gheorghiu and D. J. Pym, _Proof-theoretic semantics for the logic of bunched implications_ (2023).
  * [6] Kürbis, N., _Proof-theoretic semantics, a problem with negation and prospects for modality_ , Journal of Philosophical Logic 44 (2015), pp. 713–727.
  * [7] Negri, S., _A normalizing system of natural deduction for intuitionistic linear logic_ , ARCHIVE FOR MATHEMATICAL LOGIC 41 (2002), pp. 789–810.
  * [8] Sandqvist, T., _Base-extension semantics for intuitionistic sentential logic_ , Log. J. IGPL 23 (2015), pp. 719–731.
URL https://api.semanticscholar.org/CorpusID:7310523

##  Appendix A Technical lemmas used in the proof of soundness

This appendix contains the technical lemmas necessary to complete the cases
for proving soundness of the semantics for IMALL.

######  Lemma 31.

If  1. $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi\oplus\psi$,  2.
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\chi$,  3.
$\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\chi$,  then  4.
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\chi$.

###### Proof.

We proceed by induction on the structure of $\chi$.

  * -

$\chi={p}$, for atomic ${p}$. Conditions (2) and (3) give sufficient
conditions to conclude from (1) and (($\oplus$)) that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}{p}$.

  * -

$\chi=\alpha\with\beta$. By (1) we have that for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${K}$ and atomic ${p}$
such that $\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}{p}$ and that
$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K}}{p}$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K}}{p}$. We use this as the base case
of our inductive argument. From (2) by (($\with$)) we get
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\alpha$ and
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\beta$. Similarly, from (3), we
get $\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\alpha$ and
$\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\beta$. Thus, applying the
inductive hypothesis on the structures of $\alpha$ and $\beta$ gives that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\alpha$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\beta$. Thus, by (($\with$)), we
conclude $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\alpha\with\beta$.

  * -

$\chi=\alpha\oplus\beta$. Unfolding (4) says that we need to show that, for
all $\mathscr{C}\supseteq\mathscr{B}$, atomic ${p}$ and atomic multisets ${M}$
such that $\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}{p}$ and
$\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}{p}$ implies
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{M}}{p}$. To show this it suffices
we show the following:

    * –

$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L}}\varphi\oplus\psi$. This holds by
monotonicity of (1).

    * –

$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{N}}{p}$. Consider some
$\mathscr{D}\supseteq\mathscr{C}$ and atomic multiset ${H}$ such that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{H}}\varphi$. Then by ((Inf)) and (2) we
have that $\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{H}}\alpha\oplus\beta$. Thus,
by (($\oplus$)) we have for all $\mathscr{E}\supseteq\mathscr{D}$ and
arbitrary ${N}$ that $\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{K},{H},{N}}{p}$. In
particular, this holds for the case when $\mathscr{E}=\mathscr{D}$ and so we
have that $\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{H},{N}}{p}$.

    * –

$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{N}}{p}$. The proof is similar to
the previous case.

From the first point, we get that for all $\mathscr{D}\supseteq\mathscr{C}$
atomic ${p}$ and atomic multisets ${Q}$ that
$\varphi\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{Q}}{p}$ and
$\psi\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{Q}}{p}$ imply that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{L},{Q}}{p}$. Importantly, we can consider
the case when $\mathscr{C}=\mathscr{D}$ and set ${Q}={K},{N}$ since ${Q}$ and
${N}$ are arbitrary and thus conclude that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{M}}{p}$, appropriately renaming
${N}$ to ${M}$.

  * -

$\chi=0$. It suffices to conclude this case from the following three facts:

    * –

$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}\varphi\oplus\psi$. This is just (1).

    * –

$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}{p}$ for all atomic ${p}$. This
is just (($0$)) and (2).

    * –

$\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}{p}$ for all atomic ${p}$. Same as
before.

From the first point, we have that for all $\mathscr{C}\supseteq\mathscr{B}$,
atomic ${p}$ and arbitrary ${M}$ such that
$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}0$ and
$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}0$ imply
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}0$. Setting $\mathscr{C}=\mathscr{B}$
and ${M}={K}$ since ${M}$ is universally quantified, we can conclude that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}0$.

  * -

$\chi=\alpha\multimap\beta$. Unfolding (4) says that we want to show that for
all $\mathscr{C}\supseteq\mathscr{B}$ and atomic multisets ${H}$ such that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{H}}\alpha$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{H}}\beta$. To show this, we need
to show the following three facts:

    * –

$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L}}\varphi\oplus\psi$. This immediately
follows by monotonicity and (1).

    * –

$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{H}}\beta$. To show this, we
suppose we have an atomic multiset ${I}$ such that for all
$\mathscr{D}\supseteq\mathscr{C}$ we have
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{I}}\varphi$. By (2), we conclude that
$\alpha\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{I}}\beta$. By hypothesis, we
have that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{H}}\alpha$ and since
$\mathscr{C}\subseteq\mathscr{D}$ then we can use ((Inf)) to conclude that
$\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{K},{I},{H}}\beta$ for all
$\mathscr{E}\supseteq\mathscr{D}$. In particular, this holds for when
$\mathscr{E}=\mathscr{D}$ and thus
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{I},{H}}\beta$ from which we conclude
$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{H}}\beta$.

    * –

$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{H}}\beta$. This holds similarly to
the above case.

By the inductive hypothesis on the structure of $\beta$, using the first point
as the base case, we obtain that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{H}}\beta$ as desired.

  * -

$\chi=\alpha\otimes\beta$. Unfolding (4) gives that we want to show that for
all $\mathscr{C}\supseteq\mathscr{B}$, atomic mulitsets ${S}$, atoms ${p}$
such that $\alpha,\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$ then we can
conclude $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$. To do this, we
need to show three things:

    * –

$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L}}\varphi\oplus\psi$. This follows by
monotonicity from (1).

    * –

$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{S}}{p}$. To show this, suppose
we have that for all $\mathscr{D}\supseteq\mathscr{C}$ and atomic multisets
${M}$ such that $\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{M}}\varphi$. The we have
by (2) that $\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{M}}\alpha\otimes\beta$.
Thus by the definition of (($\otimes$)) we have that for all
$\mathscr{E}\supseteq\mathscr{D}$, atomic multisets ${N}$ and atomic ${p}$
then $\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{K},{M},{S}}{p}$. In particular, this
holds when $\mathscr{E}=\mathscr{D}$ and when ${N}={S}$, so we get
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{M},{S}}{p}$, and thus, we conclude
that $\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{S}}{p}$.

    * –

$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{S}}{p}$. Follows similarly to the
previous case.

Thus, from the first point, we have that for all
$\mathscr{D}\supseteq\mathscr{C}$, atomic multisets ${H}$ and atoms ${p}$, if
$\varphi\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{H}}{p}$ and
$\psi\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{H}}{p}$ then
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{L},{H}}{p}$. Thus, by setting
$\mathscr{D}=\mathscr{C}$ and setting ${H}={K},{S}$, we get that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$ as desired.

  * -

$\chi=1$. Again, unfolding (4) gives that we want to show that for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${S}$ and atoms ${p}$,
such that $\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}p$ implies
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$. To do this we need to
show three things:

    * –

$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L}}\varphi\oplus\psi$. This follows from
(1) by monotonicity.

    * –

$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{S}}{p}$. Suppose that we have
that for all $\mathscr{D}\supseteq\mathscr{C}$ and atomic multisets ${M}$ that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{M}}\varphi$. Then by (2) we get that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{K},{M}}1$ which gives by (($1$)) that for
all $\mathscr{E}\supseteq\mathscr{D}$, atomic multisets ${S}$ and atomic ${p}$
that $\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{K},{M},{S}}{p}$. In particular, this
holds for $\mathscr{E}=\mathscr{D}$ and thus we conclude that
$\varphi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{S}}{p}$.

    * –

$\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{K},{S}}{p}$. Follows similarly to the
previous case.

Thus we conclude from these three points that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$

This concludes the lemma. ∎

_Note_ : The following two lemmas are extensions of those presented in [4] for
IMLL and as such, the proofs will only contain the cases needed to handle the
additional connectives of IMALL. The cases with the other connectives are
found [4].

######  Lemma 32.

If  1. $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S}}\varphi\otimes\psi$,  2.
$\varphi,\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{T}}\chi$,  then  3.
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}\chi$.

###### Proof.

We proceed by proving by induction on the structure of $\chi$.

  * -

$\chi=\alpha\with\beta$. From (3) and (($\with$)), we see we need to show that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}\alpha$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}\beta$.

We use (1) as the base case of our inductive argument. From (2) we have that
$\varphi,\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{T}}\alpha\with\beta$ which by
(($\with$)) gives $\varphi,\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{T}}\alpha$
and $\varphi,\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{T}}\beta$. Thus, we apply
the inductive hypothesis on the structures of $\alpha$ and $\beta$ which gives
us that $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}\alpha$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}\beta$ which by (($\with$)) gives
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}\alpha\with\beta$, as desired.

  * -

$\chi=\alpha\oplus\beta$. Spelling out (3) gives that we want to show that for
all $\mathscr{C}\supseteq\mathscr{B}$ atomic multisets ${M}$ and atoms ${p}$
such that $\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}{p}$ and
$\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{M}}{p}$ implies that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S},{T},{M}}{p}$. To do that it suffces to
show the following two things:

    * –

$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}\varphi\otimes\psi$. This holds by
monotonicity from (1).

    * –

$\varphi,\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{T},{M}}p$. To show this we
suppose that we have for all $\mathscr{D}\supseteq\mathscr{C}$ and atomic
multisets ${N}$ that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{N}}\\{\varphi,\psi\\}$. Thus by (2) we get
that $\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{T},{N}}\alpha\oplus\beta$. Spelling
out the definition of (($\oplus$)) gives that we have that for all
$\mathscr{E}\supseteq\mathscr{D}$, atomic multisets ${M}$ and atoms ${p}$ such
that $\alpha\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{M}}p$ and
$\beta\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{M}}p$ implies
$\Vdash_{\\!\\!\mathscr{E}}^{\\!\\!{T},{N},{M}}p$ and in particular when
$\mathscr{E}=\mathscr{D}$ that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{T},{N},{M}}p$. Thus we conclude that
$\varphi,\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{T},{M}}p$, as desired.

To finish the argument, we unfold
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}\varphi\otimes\psi$ according to
(($\otimes$)) which gives that for all $\mathscr{D}\supseteq\mathscr{C}$,
atomic multisets ${V}$ and atoms $p$ such that
$\varphi,\psi\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{V}}{p}$ implies that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{S},{V}}{p}$. In particular this holds when
$\mathscr{D}=\mathscr{C}$ and ${V}={T},{M}$. Thus we conclude that
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S},{T},{M}}{p}$, as desired.

  * -

$\chi=0$. Unfolding (3) gives that we want to show that for all atomic ${p}$
we have $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}{p}$. To show this we start
by unpacking (2) gives that we have that for all atomic ${p}$ that
$\varphi,\psi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{T}}{p}$. Further unpacking (1)
according to (($\otimes$)) and (($0$)) gives that for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${V}$ and atoms ${p}$, if
$\varphi,\psi\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{V}}{p}$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{V}}{p}$. In particular, this holds when
${V}={T}$ and $\mathscr{C}=\mathscr{B}$, which gives our condition from the
unpacked form of (2). Thus we conclude that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{S},{T}}{p}$ for all ${p}$ as desired.

This completes all the additional cases of the proof by induction. ∎

######  Lemma 33.

If  1. $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L}}1$,  2.
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\chi$,  then  3.
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\chi$.

###### Proof.

$\chi=\alpha\with\beta$. We use (1) as the base case of our inductive
argument. From (2) we have that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\alpha\with\beta$ which by (($\with$))
gives $\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\alpha$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}\beta$. Thus, we apply the inductive
hypothesis on the structures of $\alpha$ and $\beta$ which gives us that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\alpha$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\beta$ which by (($\with$)) gives
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}\alpha\with\beta$, as desired.

$\chi=\alpha\oplus\beta$. Unfolding (3) gives that for all
$\mathscr{C}\supseteq\mathscr{B}$, atomic multisets ${S}$ and atoms ${p}$ if
$\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$ and
$\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}$ then
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$. Thus given such an
$\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$ and
$\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}$ we want to show
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$. To show this, we do the
following:

  * -

$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L}}1$. This follows by monotonicity.

  * -

$\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{S}}{p}$. Starting from
$\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{S}}{p}$, by ((Inf)) we have that for
all $\mathscr{D}\supseteq\mathscr{C}$ and atomic multisets ${N}$ such that
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{N}}\alpha$ implies
$\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{L},{S},{N}}{p}$. By the previous fact, we
thus have $\Vdash_{\\!\\!\mathscr{D}}^{\\!\\!{L},{S}}{p}$ which by ((Inf))
gives $\alpha\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{S}}{p}$ as desired.

  * -

$\beta\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{S}}{p}$. The proof of this case
is identical to the previous case.

We thus have sufficient grounds to use (2) to conclude
$\Vdash_{\\!\\!\mathscr{C}}^{\\!\\!{L},{K},{S}}{p}$ as desired.

$\chi=0$. Unfolding (2) gives us that for all atoms ${p}$ we have
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{K}}{p}$. Using (1) we get that this
implies that for all ${p}$ that
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}{p}$. Thus we conclude
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!{L},{K}}0$, as desired. ∎