example $\blacksquare$ proof $\square$

11institutetext: University College London, London WC1E 6BT, UK
22institutetext: Institute of Philosophy, University of London, London WC1H
0AR, UK
22email<EMAIL_ADDRESS>
# Proof-theoretic Semantics for the
Logic of Bunched Implications

Tao Gu 11 Alexander V. Gheorghiu 11 David J. Pym 1122

###### Abstract

Typically, substructural logics are used in applications because of their
resource interpretations, and these interpretations often refer to the
celebrated number-of-uses reading of their implications. However, despite its
prominence, this reading is not at all reflected in the truth-functional
semantics of these logics. It is a proof-theoretic interpretation of the
logic. Hence, one desires a _proof-theoretic semantics_ of such logics in
which this reading is naturally expressed. This paper delivers such a
semantics for the logic of Bunched Implications (BI), generalizing earlier
work on IMLL, which is well-known as a logic of resources with numerous
applications to verification and modelling. Specifically, it delivers a base-
extension semantics (B-eS) for BI in which resources are _bunches_ of atoms
that get passed from antecedent to consequent in precisely the expected way.

###### Keywords:

Logic Semantics Proof Theory Proof-theoretic Semantics Substructural Logic
Bunched Implications

##  1 Introduction

In model-theoretic semantics (M-tS), logical consequence is defined in terms
of truth in models; that is, abstract mathematical structures in which
propositions are interpreted and their truth is judged. As Schroeder-Heister
[46] explains, in the standard reading given by Tarski [49, 50], a
propositional formula $\varphi$ follows (model-theoretically) from a context
$\mathrm{\Gamma}$ iff every model of $\mathrm{\Gamma}$ is a model of
$\varphi$:

$\begin{array}[]{r@{\quad}c@{\quad}l}\mbox{$\mathrm{\Gamma}\models\varphi$}&\mbox{iff}&\mbox{for
all models $\mathcal{M}$, if $\mathcal{M}\models\psi$ for all
$\psi\in\mathrm{\Gamma}$, then $\mathcal{M}\models\varphi$}\end{array}$

Therefore, consequence is understood as the _transmission of truth_.
Importantly, from this perspective, _meaning_ and _validity_ are characterized
in terms of _truth_.

Proof-theoretic semantics (P-tS) is an alternative approach to meaning and
validity in which they are characterized in terms of _proofs_ — understood as
objects denoting collections of acceptable inferences from accepted premisses.
This is subtle. Crucially, P-tS is not about providing a proof system for the
logic, but about explicating the meaning _in terms of_ proof systems. Indeed,
as Schroeder-Heister [46] observes, since no formal system is fixed (only
notions of inference) the relationship between semantics and provability
remains the same as it has always been — in particular, soundness and
completeness are desirable features of formal systems. Essentially, what
differs is that _proof_ in P-tS plays the part of _truth_ in M-tS. The
semantic paradigm supporting P-tS is _inferentialism_ — the view that meaning
(or validity) arises from rules of inference (see Brandom [4]).

Current work in Pt-S largely follows two different approaches. The first is
proof-theoretic validity (P-tV), following Dummett [10] and Prawitz [33, 34] —
see, for example, Schroeder-Heister [45]. It aims to define what makes a proof
valid, and is closely related to, though not coincident with, BHK semantics —
see Schroeder-Heister [46]. The second is _base-extension semantics_ (B-eS),
as developed in, for example, Makinson, Piecha, Sandqvist, and Schroeder-
heister [26, 31, 40, 41, 42, 30]. It aims to give a semantics to the logical
constants in terms of proof and provability in arbitrary systems called
_bases_. We elaborate on this presently. There are deep connections between
B-eS and definite formulae, proof-search, logic programming, and negation-as-
failure — see, for example, work by Hallnäs and Schroeder-Heister [20, 21],
and Gheorghiu and Pym [15, 16].

A _base_ is a set of _atomic rules_. An _atomic rule_ is natural deduction
rule (in the sense of Gentzen [48]) over atomic propositions (not closed under
substitution); for example, following Sandqvist [44], from the propositions
‘Tammy is a fox’ and ‘Tammy is female’ one may infer ‘Tammy is a vixen,’

$\text{Tammy is a vixen}\lx@proof@logical@and\text{Tammy is a fox}\text{Tammy
is female}$

This is the standard approach to atomic rules, which will be generalized in
this paper to accommodate certain technical issues explained below; in
particular, we move from a natural deduction presentation to a sequent
calculus presentation. In B-eS, the validity of atoms and the meaning of the
logical connectives is then inductively defined relative to these bases — see,
for example, Figure 1 for IPL, Figure 2 for intuitionistic multiplicative
linear logic (IMLL), and Figure 4 for the logic of Bunched Implications (BI),
which are all explained below. The choice of the form of atomic rules has
profound repercussions; for example, limiting the atomic rules to simple
production rules in the B-eS for IPL collapses it to classical propositional
logic (CPL), or (conversely) generalizing atomic rules include discharged
hypotheses and making a subtle choice about the treatment of disjunction (cf.
the incompleteness results by Piecha and Schroeder-Heister [29, 28, 32]) in
the semantics of CPL delivers a semantics for IPL — see Sandqvist [40, 41,
43]. This understanding of B-eS is the form of P-tS used in this paper; see
Goldfarb [19] and Stafford and Nascimento [47] for alternative approaches that
are related to Kripke semantics.

Why study the B-eS of substructural logics? One motivation is to be able to
understand and account for _resources_ in formal systems, semantically.
Consider the celebrated ‘resource interpretation’ of IMLL via the number-of-
uses reading in which a proof of a formula $\varphi\multimap\psi$ determines a
function that _uses_ its arguments exactly once. This reading is entirely
proof-theoretic and is _not_ at all expressed in the truth-functional
semantics of the logic — see Girard [18], Allwein and Dunn [2], and Coumans et
al. [7]. Meanwhile, this reading of resource is quite clearly seen in the B-eS
for IMLL by Gheorghiu et al. [13]. This illustrates the value of studying B-eS
for substructural logics in informatics as far as their use as logics of
resources according to the typical number-of-uses reading. Of course, there
are other applications of substructural logics to formal systems, but they all
tend to be close to the proof-theoretic accounts of the logic for which P-tS
is ideally suited.

This paper delivers a B-eS for the _logic of Bunched Implications_ (BI) [27].
The logic is, perhaps, best-known for its role as the logical basis for the
program logic known as _Separation Logic_ [22, 39, 37] and its many
derivatives. This application of BI is entirely based on its reading as a
logic of resource — see, for example, Pym [35]. Thus, on one hand we have P-tS
as a semantics paradigm in which a certain common notion of resource is
handled explicitly and naturally, on the other we have BI as a logic whose
resource interpretation has formidable applications to foundational computer
and systems science. This paper brings these two worlds together. However,
resource-sensitive semantics is not the only reason to study BI. Another use
of the logic is as the basis for van Benthem-Hennessy-Milner-type logics
associated with process algebras that provide a foundation for simulation
modelling tools — see, for example, Anderson and Pym [3]. Kuorikoski and
Reijula [23] have recently used P-tS in the context of simulation modelling —
briefly, execution of a program (akin to a proof in a formal system) is
understood as one of its possible interpretations — giving another reason to
study the B-eS for BI in particular. In this paper, we illustrate the value of
the B-eS of BI by application to yet another domain: rule-based access control
— see Section 3.2

One way to regard BI is as the free combination of IPL — with connectives
$\land,\lor,\to,\top,\bot$ — and IMLL — with connectives
$\mathrel{\ast},\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast},\top^{\ast}$. Both
of these logics already have B-eS — see Sandqvist [42] and Gheorghiu et al.
[13] — which suggests that the semantics for BI should be a ‘free combination’
of those semantics. The same is true of BI’s model-theoretic semantics, but
the subject proves quite subtle — see, for example, work by Docherty,
Galmiche, Gheorghiu, Méry, Pym [9, 11, 17]. The issues arise out of the
complex structure involved in BI. As a consequence of having two implications,
contexts in BI are not the typical _flat_ data structures typically used in
logic (e.g., lists or multisets), but instead are layered structures called
_bunches_ , a term that derives from the relevance logic literature — see, for
example, Read [38]. Therefore the technical challenges for providing a B-eS
for BI amount to understanding how to handle the bunch structure, and how that
manifests in the resource reading of the logic and semantics. The technical
details are contained within the body of the paper. The remainder of this
section provides intuitions as to how these ideas are developed.

Our starting point is the B-eS for IPL by Sandqvist [42]. Fix a set of atoms
$\mathbb{A}$. A base $\mathscr{B}$ is a set of atomic rules as described above
and provability in a base ($\vdash_{\\!\\!\mathscr{B}})$ is defined as in
Figure 1 — that is, inductively, by ref and app. This provides the base case
of the _support_ relation defined in Figure 1 that provides the semantics —
here, $\and{p},\and{p}_{1},\ldots,\and{p}_{n},\and{c}\in\mathbb{A}$,
$\and{P}_{1},\dots\and{P}_{n},\ldots\subseteq\mathbb{A}$ (finite), and
$\varphi,\psi,\ldots$ denote IPL-formulae, and $\mathrm{\Gamma}$ denotes a set
of IPL-formulae. Observe it differs from the standard Kripke semantics for IPL
[24] in the treatment of disjunction ($\lor$) and absurdity ($\bot$); indeed,
this choice is critical as Piecha and Schroeder-Heister [29, 28, 32] have
shown that a meta-level ‘or’ for disjunction results in incompleteness.

$\begin{array}[]{l@{\qquad}c@{\quad}l@{\quad}r}\Vdash_{\\!\\!\mathscr{B}}\and{p}&\mbox{iff}&\vdash_{\\!\\!\mathscr{B}}\and{p}&\mbox{(At)}\\\\[2.84526pt]
\Vdash_{\\!\\!\mathscr{B}}\varphi\to\psi&\mbox{iff}&\varphi\Vdash_{\\!\\!\mathscr{B}}\psi&(\to)\\\\[2.84526pt]
\Vdash_{\\!\\!\mathscr{B}}\varphi\land\psi&\mbox{iff}&\mbox{$\Vdash_{\\!\\!\mathscr{B}}\varphi$
and $\Vdash_{\\!\\!\mathscr{B}}\psi$}&(\land)\\\\[2.84526pt]
\Vdash_{\\!\\!\mathscr{B}}\varphi\lor\psi&\mbox{iff}&\mbox{$\forall\mathscr{C}\supseteq\mathscr{B}$
and $\forall\and{p}\in\mathbb{A}$, if
$\varphi\Vdash_{\\!\\!\mathscr{C}}\and{p}$ and
$\psi\Vdash_{\\!\\!\mathscr{C}}\and{p}$, then
$\Vdash_{\\!\\!\mathscr{C}}\and{p}$}&(\lor)\\\\[2.84526pt]
\Vdash_{\\!\\!\mathscr{B}}\bot&\mbox{iff}&\Vdash_{\\!\\!\mathscr{B}}\and{p}\text{
for any }\and{p}\in\mathbb{A}&(\bot)\\\\[2.84526pt]
\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}\varphi&\mbox{iff}&\mbox{$\forall\mathscr{C}\supseteq\mathscr{B}$,
if $\Vdash_{\\!\\!\mathscr{C}}\psi$ for any $\psi\in\mathrm{\Gamma}$, then
$\Vdash_{\\!\\!\mathscr{C}}\varphi$ }&\mbox{(Inf)}\end{array}\vspace{-2mm}$

$\raisebox{-10.00002pt}{
$\and{c}\lx@proof<EMAIL_ADDRESS>}\quad\begin{array}[]{r@{\quad}l}\mbox{\hypertarget{ipl-
ref}{{ref}}:}&\mbox{$\and{P},\and{p}\vdash_{\mathscr{B}}\and{p}$}\\\
\mbox{\hypertarget{ipl-app}{{app}}:}&\mbox{If
$\and{P},\and{P}_{i}\vdash_{\\!\\!\mathscr{B}}\and{p}_{i}$ for $i=1\ldots n$,
then $\and{P}\vdash_{\\!\\!\mathscr{B}}\and{c}$}\end{array}$

Figure 1: Base-extension Semantics for IPL

Recently, a B-eS for IMLL [13] has been given in the style of the B-eS for IPL
given above. This is summarized in Figure 2 in which
$\and{P}_{1},\ldots,\and{P}_{n},\and{U},\and{V}$ are _multisets_ of atoms,
$\mathrm{\Gamma},\mathrm{\Delta}$ are _multisets_ of formulae, and denotes
multiset union. There are a few features to note about this semantics. First,
observe that provability in a base ($\vdash_{\\!\\!\mathscr{B}}$) has been
made substructural as the base case (Ref) is restricted to only have the
conclusion as a context, and the inductive step (App) combines the contexts
delivering each premiss of an atomic rule for the context delivering the
conclusion of that rule. Second, observe that the support judgement
$\Vdash_{\\!\\!}^{\\!\\!}$ is parametrized on a multiset of atoms, which can
usefully be thought of as ‘resources’. Doing this manifests the number-of-uses
resource reading of IMLL restricted to atoms. The role of resource
parametrization can be seen particularly clearly in the (Inf) clause: the
resources required for the sequent $\mathrm{\Gamma}\triangleright\varphi$ are
combined with those required for $\mathrm{\Gamma}$ in order to deliver those
required for $\varphi$. Third, the treatment of the support of a combination
of contexts $\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$ follows
the naïve Kripke-style interpretation of multiplicative conjunction,
corresponding to an introduction rule in natural deduction, but the support of
the tensor product $\otimes$ follows the form of a natural deduction
elimination rule. Fourth, observe that everywhere there are restrictions to
the atomic case (e.g., the $\otimes$-clause takes the form of the
$\otimes$-elimination rule _restricted_ to atomic conclusion), which are
required to ensure the connection to provability in a base. Overall, we
observe that aside from expected modifications on the set-up for IPL, there
are two key technical developments required in this work: first, the use of
resources to capture substructurality; second, a delicate treatment of the
relationship between the multiplicative context-building operation and the
corresponding multiplicative conjunction.

$\begin{array}[]{l@{\quad}c@{\quad}l@{\qquad}r}\mbox{$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\and{P}}\and{p}$}&\mbox{iff}&\mbox{$\and{P}\vdash_{\\!\\!\mathscr{B}}\and{p}$}&\mbox{(At)}\\\\[2.84526pt]
\mbox{$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\and{P}}\varphi\multimap\psi$}&\mbox{iff}&\mbox{$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\and{P}}\psi$}&\mbox{($\multimap$)}\\\\[2.84526pt]
\mbox{$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\and{P}}\varphi\otimes\psi$}&\mbox{iff}&\mbox{$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}$, $\forall\and{p}\in\mathbb{A}$, if
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\and{U}}\and{p}$,
then
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\and{P}\mathrel{\fatcomma}\and{U}}\and{p}$}&\mbox{($\otimes$)}\\\\[2.84526pt]
\mbox{$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\and{P}}\top^{\ast}$}&\mbox{iff}&\mbox{$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}$, $\forall\and{p}\in\mathbb{A}$, if
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\;\and{U}}\and{p}$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\;\and{P}\;\\!\mathrel{\fatcomma}\\!\;\and{U}}\and{p}$}&\mbox{($\top^{\ast}$)}\\\\[2.84526pt]
\mbox{$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!P}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$}&\mbox{iff}&\mbox{$\exists\and{U},\and{V}$
s.t. $\and{P}=(\and{U}\\!\mathrel{\fatcomma}\\!\and{V})$,
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!\and{U}}\mathrm{\Gamma}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!V}\mathrm{\Delta}$}&\mbox{(\,\,$\\!\mathrel{\fatcomma}\\!$\,\,)}\\\\[2.84526pt]
\mbox{$\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}^{\\!\\!P}\varphi$}&\mbox{iff}&\mbox{$\forall\mathscr{X}\supseteq\mathscr{B}$
and $\forall\and{U}$, if
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\and{U}}\mathrm{\Gamma}$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\\!\\!\;\and{P}\;\\!\mathrel{\fatcomma}\\!\;\and{U}}\varphi$}&\mbox{\hypertarget{imll-
inf}{(Inf)}}\end{array}$

$\raisebox{-10.00002pt}{
$\and{c}\lx@proof<EMAIL_ADDRESS>}\quad\begin{array}[]{r@{\quad}l}\mbox{\hypertarget{imll-
ref}{{ref}}:}&\and{p}\vdash_{\\!\\!\mathscr{B}}\and{p}\\\
\mbox{\hypertarget{imll-app}{{app}}:}&\mbox{If
$\and{S}_{i}\\!\mathrel{\fatcomma}\\!\and{P}_{i}\vdash_{\\!\\!\mathscr{B}}\and{p}_{i}$
for $i=1\ldots n$, then
$\and{S}_{1}\\!\mathrel{\fatcomma}\\!\dots\\!\mathrel{\fatcomma}\\!\and{S}_{n}\vdash_{\\!\\!\mathscr{B}}\and{c}$}\end{array}$

Figure 2: Base-extension Semantics for IMLL

In this paper, we deliver the B-eS for BI by generalizing the set-up for IMLL
from multisets to bunches, mixing multiplicative structure and additive
structure. There are a number of technical challenges that arise when doing
this. First, we diverge from the traditional literature on atomic systems in
P-tS — see, for example, Piecha and Schroeder-Heister [30, 31] — as natural
deduction in the sense of Gentzen [48] appears insufficiently expressive to
make all the requisite distinctions with regards to multiplicative and
additive structures in bunches. Second, in order to recover the appropriate
amount of structurality in the clauses of the logical constants we introduce a
_bunch-extension_ relation. Third, we introduce formally a notion of
_contextual bunch_ (i.e., a bunch with a hole) in order to handle substitution
in bunches of parameterizing resources in the support relation. The importance
of this structure can be seen from the (Inf) clause that we shall need for BI
(see Figure 4),

$\begin{array}[]{l@{\quad}c@{\quad}l@{\qquad}r}\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\varphi&\mbox{iff}&\mbox{$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}\in\mathbb{B}(\mathbb{A})$, if
$\Vdash_{\\!\\!\mathscr{X}}^{\and{U}}\mathrm{\Gamma}$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\and{R(U)}}\varphi$}&\mbox{(Inf)}\end{array}$

That is, the contextual bunch $\and{R}(\cdot)$ manages the construction of the
bunch of atomic resources in a way that matches the structure of the required
judgement.

In Section 2, we define BI and give the background meta-theory required for
this paper. In Section 3, give the B-eS for IPL. In Section 4 and Section 5,
we prove soundness and completeness, respectively. The paper concludes in
Section 6 with a summary of results and a discussion of future work.

Henceforth, we fix a denumerable set of atomic propositions $\mathbb{A}$, and
the following conventions: $\and{p},\and{q},\dots$ denote atoms;
$\and{P},\and{Q},\dots$ denote bunches of atoms; $\varphi,\psi,\theta,\dots$
denote formulae; $\mathrm{\Gamma},\mathrm{\Delta},\dots$ denote bunches of
formulae.

##  2 The Logic of Bunched Implications

In this section, we define BI and give the technical background required for
the development of this paper. First, we define its syntax and consequence
relation in Section 2.1. Second, we give the meta-theory required to
understand the use of _bunches_ in this paper in Section 2.2.

###  2.1 Syntax and Consequence

In this section, we present the syntax of BI and define the consequence
relation in terms of a natural deduction system in sequent calculus form. It
follows standard presentations (cf. O’Hearn and Pym [27]) except that it also
introduces _contextual bunches_ , which are used throughout this paper but are
not part of the standard background of BI.

######  Definition 1 (Formulae)

The set of formulae $\mathbb{F}$ (over $\mathbb{A}$) is defined by the
following grammar:

$\varphi::=\and{p}\in\mathbb{A}\mid\top\mid\bot\mid\top^{\ast}\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\varphi\to\varphi\mid\varphi\mathrel{\ast}\varphi\mid\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\varphi$

######  Definition 2 (Bunches)

Let $\mathbb{X}$ be a set of syntactic structures. The set of bunches over
$\mathbb{X}$ is denoted $\mathbb{B}(\mathbb{X})$ and is defined by the
following grammar:

$\mathrm{\Gamma}::=x\in\mathbb{X}\mid\varnothing_{\\!+}\mid\varnothing_{\\!\times}\mid\mathrm{\Gamma}\fatsemi\mathrm{\Gamma}\mid\mathrm{\Gamma}\fatcomma\mathrm{\Gamma}$

The is the additive constructor, and the $\varnothing_{\\!+}$ is the additive
unit; the is the multiplicative constructor, and the $\varnothing_{\\!\times}$
is the multiplicative unit.

If a bunch $\mathrm{\Delta}$ is a sub-tree of a bunch $\mathrm{\Gamma}$, then
$\mathrm{\Delta}$ is a _sub-bunch_ of $\mathrm{\Gamma}$. Importantly, sub-
bunches are sensitive to occurrence — for example, in the bunch
$\mathrm{\Delta}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$, each occurence of
$\mathrm{\Delta}$ is a different sub-bunch. We may write
$\mathrm{\Gamma}(\mathrm{\Delta})$ to express that $\mathrm{\Delta}$ is a sub-
bunch of $\mathrm{\Gamma}$. This notation is traditional for BI [27], but
requires sensitive handling. To avoid confusion, we never write
$\mathrm{\Gamma}$ and later $\mathrm{\Gamma}(\mathrm{\Delta})$ to denote the
same bunch, but rather maintain one presentation. The substitution of
$\mathrm{\Delta}$ for $\mathrm{\Delta}^{\prime}$ in $\mathrm{\Gamma}$ is
denoted
$\mathrm{\Gamma}(\mathrm{\Delta})[\mathrm{\Delta}\mapsto\mathrm{\Delta}^{\prime}]$.
To emphasize: this is not a universal substitution, but a substitution of the
particular occurrence of $\mathrm{\Delta}$ meant in writing
$\mathrm{\Gamma}(\mathrm{\Delta})$. The bunch
$\mathrm{\Gamma}(\mathrm{\Delta})[\mathrm{\Delta}\mapsto\mathrm{\Delta}^{\prime}]$
may be denoted $\mathrm{\Gamma}(\mathrm{\Delta}^{\prime})$ when no confusion
arises.

Substitution in bunches is an essential part of expressing of BI. It plays the
part of concatenation of lists and union of sets and multisets in the
presentations of other logics — see, for example, van Dalen [8]. Indeed, so
integral are substitutions that it is instructive to have a notion of
_contextual bunch_ that allows us to handle them smoothly.

######  Definition 3 (Contextual Bunch)

A _contextual bunch_ (over $\mathbb{X}$) is a function
$b:\mathbb{B}(\mathbb{X})\to\mathbb{B}(\mathbb{X})$ such that there is
$\mathrm{\Gamma}(\mathrm{\Delta})\in\mathbb{B}(\mathbb{X})$ and
$b(\mathrm{\Sigma})=\mathrm{\Gamma}(\mathrm{\Sigma})$ for any
$\mathrm{\Sigma}\in\mathbb{B}(\mathbb{X})$. The set of all contextual bunches
(over $\mathbb{X}$) is $\dot{\mathbb{B}}(\mathbb{X})$.

Importantly, the identity on $\mathbb{B}(\mathbb{X})$ is a contextual bunch,
it is denoted $(\cdot)$. We think of a contextual bunch as a _bunch with a
hole_ — cf. _nests with a hole_ in work by Brünner [6]. That is,
$\dot{\mathbb{B}}(\mathbb{X})$ can be identified as the subset of
$\mathbb{B}(\mathbb{X}\cup\\{\circ\\})$, where $\circ\not\in\mathbb{X}$, in
which bunches contain a single occurrence of $\circ$. Specifically, if
$b(x)=\mathrm{\Gamma}(x)$, then identify $b$ with
$\mathrm{\Gamma}(\circ)\in\mathbb{B}(\mathbb{X}\cup\\{\circ\\})$. We write
$\mathrm{\Gamma}(\cdot)$ for the contextual bunch identified with
$\mathrm{\Gamma}(\circ)$.

###### Example 1

The contextual bunch
$b:x\mapsto\varphi_{1}\\!\mathrel{\fatsemi}\\!((\varphi_{2}\\!\mathrel{\fatsemi}\\!\varnothing_{\\!\times}\\!\mathrel{\fatsemi}\\!(\varphi_{3}\\!\mathrel{\fatcomma}\\!\varphi_{4}))\\!\mathrel{\fatcomma}\\!(\varphi_{5}\\!\mathrel{\fatsemi}\\!(x)))$
is identified with $\mathrm{\Gamma}(\cdot)$, where
$\mathrm{\Gamma}(\circ):=\varphi_{1}\\!\mathrel{\fatsemi}\\!((\varphi_{2}\\!\mathrel{\fatsemi}\\!\varnothing_{\\!\times}\\!\mathrel{\fatsemi}\\!(\varphi_{3}\\!\mathrel{\fatcomma}\\!\varphi_{4}))\\!\mathrel{\fatcomma}\\!(\varphi_{5}\\!\mathrel{\fatsemi}\\!\circ))$.

In BI, bunches are the data structures over which collections of formulae are
taken. Each of the context-former is meant as a multiset constructor, with the
usual properties of commutativity and associativity, but they do not
distribute over each other. That is, bunches are intended to be read _modulo
coherent equivalence_ in the same way that lists for the contexts of classical
logic sequents are understood modulo permutation.

######  Definition 4 (Coherent Equivalence)

Two bunches
$\mathrm{\Gamma},\mathrm{\Gamma}^{\prime}\in\mathbb{B}(\mathbb{X})$ are
_coherently equivalent_ when $\mathrm{\Gamma}\equiv\mathrm{\Gamma}^{\prime}$,
where $\equiv$ is the least relation satisfying:

  * •

commutative monoid equations for with unit $\varnothing_{\\!+}$

  * •

commutative monoid equations for with unit $\varnothing_{\\!\times}$

  * •

coherence; that is, if $\mathrm{\Delta}\equiv\mathrm{\Delta}^{\prime}$ then
$\mathrm{\Gamma}(\mathrm{\Delta})\equiv\mathrm{\Gamma}(\mathrm{\Delta}^{\prime})$.

Further discussion about bunches as data structures is given in Section 2.2
and Section 3. Presently, we continue defining BI.

######  Definition 5 (Sequent)

A _sequent_ is a pair $\mathrm{\Gamma}\triangleright\varphi$ in which
$\mathrm{\Gamma}\in\mathbb{B}(\mathbb{F})$ is a bunch of formulae and
$\varphi$ is a formula.

That a sequent $\mathrm{\Gamma}\triangleright\varphi$ is a consequence of BI
is denoted $\mathrm{\Gamma}\vdash_{\\!\\!}\varphi$. In this paper, we
characterize BI by its natural deduction system $\mathsf{NBI}$. We assume
general familiarity with sequent calculus presentation of proof systems — see,
for example, Troelstra and Schwichtenberg [51].

######  Definition 6 (Natural Deduction System $\mathsf{NBI}$)

System $\mathsf{NBI}$ comprises the rules of Figure 3, in which
$\varphi,\psi,\chi\in\mathbb{F}$,
$\mathrm{\Gamma},\mathrm{\Delta},\mathrm{\Delta}^{\prime}\in\mathbb{B}(\mathbb{F})$,
and e has the side-condition $\mathrm{\Gamma}\equiv\mathrm{\Gamma}^{\prime}$
and $i\in\\{1,2\\}$ in ∨I.

$\begin{array}[]{c}\varphi\triangleright\varphi\quad\mathrm{\Gamma}\triangleright\varphi\mathrm{\Gamma}^{\prime}\triangleright\varphi\quad\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})\triangleright\varphi\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\varphi\quad\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\varphi\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta})\triangleright\varphi\\\\[6.45831pt]
\varnothing_{\\!\times}\triangleright\top^{\ast}\quad\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\chi\lx@proof@logical@and\mathrm{\Gamma}(\varnothing_{\\!\times})\triangleright\chi\mathrm{\Delta}\triangleright\top^{\ast}\quad\mathrm{\Gamma}\triangleright\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi\triangleright\psi\\\\[6.45831pt]
\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\triangleright\psi\lx@proof@logical@and\mathrm{\Gamma}\triangleright\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi\mathrm{\Delta}\triangleright\varphi\quad\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\triangleright\varphi\mathrel{\ast}\psi\lx@proof@logical@and\mathrm{\Gamma}\triangleright\varphi\mathrm{\Delta}\triangleright\psi\quad\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\chi\lx@proof@logical@and\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\triangleright\chi\mathrm{\Delta}\triangleright\varphi\mathrel{\ast}\psi\\\\[6.45831pt]
\varnothing_{\\!+}\triangleright\top\quad\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\chi\lx@proof@logical@and\mathrm{\Gamma}(\varnothing_{\\!+})\triangleright\chi\mathrm{\Delta}\triangleright\top\quad\mathrm{\Gamma}\triangleright\varphi\to\psi\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\varphi\triangleright\psi\\\\[6.45831pt]
\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}\triangleright\psi\lx@proof@logical@and\mathrm{\Gamma}\triangleright\varphi\to\psi\mathrm{\Delta}\triangleright\varphi\quad\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}\triangleright\varphi\land\psi\lx@proof@logical@and\mathrm{\Gamma}\triangleright\varphi\mathrm{\Delta}\triangleright\psi\quad\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\chi\lx@proof@logical@and\mathrm{\Gamma}(\varphi\\!\mathrel{\fatsemi}\\!\psi)\triangleright\chi\mathrm{\Delta}\triangleright\varphi\land\psi\\\\[6.45831pt]
\mathrm{\Gamma}\triangleright\varphi_{1}\lor\varphi_{2}\mathrm{\Gamma}\triangleright\varphi_{i}\quad\mathrm{\Gamma}(\mathrm{\Delta})\triangleright\chi\lx@proof@logical@and\mathrm{\Gamma}(\varphi)\triangleright\chi\mathrm{\Gamma}(\psi)\triangleright\chi\mathrm{\Delta}\triangleright\varphi\lor\psi\quad\mathrm{\Gamma}\triangleright\varphi\mathrm{\Gamma}\triangleright\bot\end{array}$

Figure 3: Natural Deduction System $\mathsf{NBI}$

Let $\vdash_{\\!\\!\mathsf{NBI}}$ denote provability in $\mathsf{NBI}$. When
we say that $\mathsf{NBI}$ characterizes BI, we mean the following:
$\mathrm{\Gamma}\vdash_{\\!\\!}\varphi\mbox{ iff
}\mathrm{\Gamma}\vdash_{\\!\\!\mathsf{NBI}}\varphi$. Of course, BI admits
$\mathsf{cut}$:

######  Lemma 1 (Brotherston [5])

If $\mathrm{\Gamma}(\chi)\vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\vdash_{\\!\\!}\chi$, then
$\mathrm{\Gamma}(\mathrm{\Delta})\vdash_{\\!\\!}\varphi$.

###  2.2 Bunches Modulo Coherent Equivalence

As stated in Section 2, bunches as data structures are really the syntax trees
in Definition 2 modulo coherent equivalence (Definition 4). Gheorghiu and
Marin [14] gave a formal description of
$\mathbb{B}(\mathbb{X})/\scriptsize{\equiv}$ as _nested multisets of two
kinds_ that delivers this view. While the formalism is intuitive, it
ultimately requires more metatheory and background work than it is itself
useful. Therefore, in this paper, we forego a formal treatment, and instead
illustrate the main idea. We will move smoothly between bunches and bunches
modulo coherent equivalence when no confusion arises. Regarding bunches in
this way allows us to perform structural analysis (e.g., inductions) and not
repeat trivial case-distinctions arising from associativity and commutative of
the context-formers.

Intuitively, a bunch modulo coherent equivalence is structure of the form
$\mathrm{\Sigma}_{1}\star\cdots\star\mathrm{\Sigma}_{k}$, where
$\star\in\\{\mathrel{\fatsemi},\mathrel{\fatcomma}\\}$ and
$\mathrm{\Sigma}_{i}$ for $i=1,\dots,k$ is either an element of $\mathbb{X}$,
the unit for the complementary context-former, or a structure of the same form
but with the complementary context-former. Essentially, bunches modulo
coherent equivalence are trees satisfying the following:

  * •

the internal nodes are either or

  * •

the leaves are either $x\in\mathbb{X}$, $\varnothing_{\\!+}$, or
$\varnothing_{\\!\times}$

  * •

for a node , all the non-leaf children are

  * •

for a node , all its non-leaf children are

  * •

no child of a -node is labelled with $\varnothing_{\\!+}$

  * •

no child of a -node is labelled with $\varnothing_{\\!\times}$.

In other words, - and -nodes appear alternately, and units are removed if they
can be. This produces a layered effect of alternating additive and
multiplicative combinations of data.

Henceforth, we do not distinguish bunches and bunches modulo coherent
equivalence unless necessary. In the remainder of this section, we provide
some simple background that illustrate this quotients reading of bunches and
which will be useful later.

######  Definition 7 (Nest Depth)

Let $\mathrm{\Gamma}\in\mathbb{B}(\mathbb{X})$ be a bunch, $\mathrm{\Delta}$
be a sub-bunch of $\mathrm{\Gamma}$. The nest depth of $\mathrm{\Delta}$ in
$\mathrm{\Gamma}$ — denoted
$\mathrm{nestDepth}{(\mathrm{\Gamma})}(\mathrm{\Delta})$ — is defined as
follows:

  * •

if $\mathrm{\Gamma}=\mathrm{\Delta}$, then
$\mathrm{nestDepth}{(\mathrm{\Gamma})}(\mathrm{\Delta}):=0$

  * •

if $\mathrm{\Gamma}$ is
$\mathrm{\Sigma}_{1}\star\cdots\star\mathrm{\Sigma}_{k}$ and $\mathrm{\Delta}$
is a sub-bunch of $\mathrm{\Sigma}_{i}$, then
$\mathrm{nestDepth}{(\mathrm{\Gamma})}(\mathrm{\Delta}):=\mathrm{nestDepth}{(\mathrm{\Sigma}_{i})}(\mathrm{\Delta})+1$.

In other words, it is zero if $\mathrm{\Delta}$ is $\mathrm{\Gamma}$ itself
and otherwise one more than the number of context-former alternations between
the principal context-former of $\mathrm{\Delta}$ and the principal context-
former of $\mathrm{\Gamma}$.

######  Definition 8 (Hole Depth)

Let $b\in\dot{\mathbb{B}}(\mathbb{X})$ be a contextual bunch. Identify $b$
with the element $\mathrm{\Gamma}(\circ)$ in
$\mathbb{B}(\mathbb{X}\cup\\{\circ\\})$. The _hole depth_ of $b$ — denoted
$\mathrm{holeDepth}{(b)}{}$ — is
$\mathrm{nestDepth}{(\mathrm{\Gamma}(\circ))}(\circ)$.

###### Example 2

Let $\mathrm{\Gamma}(\cdot)$ be as in Example 1, then
$\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}{}=3$.

##  3 Base-extension Semantics for BI

This section defines the B-eS for BI. First, in Section 3.1, we define
derivability in a base, departing somewhat from existing treatments of atomic
systems in P-tS. Second, in Section 3.2, we define the _support_ judgement
that makes the semantics. Third, a toy example of the application to rule-
based access control is presented in Section 3.3. Proofs of claims may be
found in Appendix 0.A.

###  3.1 Derivability in a Base

The definition of a B-eS begins by with defining systems of rules called
_bases_ and the corresponding notion of _derivability in a base_. This forms
the base case of the semantics. Traditionally, bases are presented as natural
deduction rules in the sense of Gentzen [48] — see, for example, Peicha and
Schroeder-Heister [30, 31]. This becomes difficult in the case of BI as one
requires more careful context-management to accommodate bunching. For this
reason, we depart from the standard presentation of bases and atomic rules in
P-tS, and present them in a more general sequent calculus form.

######  Definition 9 (Sequent of Atoms)

A _sequent of atoms_ is a pair $\and{P}\triangleright\and{p}$ in which
$\and{P}\in\mathbb{B}(\mathbb{A})$ and $\and{p}\in\mathbb{A}$.

######  Definition 10 (Atomic Rule)

An _atomic rule_ is a rule-figure with a set of sequents of atoms above, and a
sequent of atoms below,

$\and{P}\triangleright\and{p}\lx@proof@logical@and\and{P}_{1}\triangleright\and{p}_{1}\ldots\and{P}_{n}\triangleright\and{p}_{n}$

In an atomic rule, the sequents above are called the _premisses_ and the
sequent below is called the _conclusion_. An atomic rule with an empty set of
premisses is called an atomic axiom.

Importantly, atomic rules are taken _per se_ and not closed under
substitution. We may write
$(\and{P}_{1}\triangleright\and{p}_{1},\dots,\and{P}_{n}\triangleright\and{p}_{n})\Rightarrow(\and{P}\triangleright\and{p})$
to denote the atomic rule in Definition 10 — note, axioms are the cases when
the left-hand side is empty.

A collection of atomic rules determines a _base_. Intuitively, a base is a
system of inference that is logic _free_ and thus suitable to ground the
semantics of the logical constants.

######  Definition 11 (Base)

A base is a set of atomic rules with at least one axiom.

We write $\mathscr{B},\mathscr{C},\dots$ to denote bases, and $\varnothing$ to
denote the empty base (i.e., the base with no rules). We say $\mathscr{C}$ is
an _extension_ of $\mathscr{B}$ if $\mathscr{C}$ is a superset of
$\mathscr{B}$, denoted $\mathscr{C}\supseteq\mathscr{B}$.

###### Example 3

The following is an example of an atomic rule, in which
$\and{p},\and{q},\and{r},\and{s}\in\mathbb{A}$:

$\and{p}\fatsemi\and{q}\triangleright\and{r}\lx@proof@logical@and\and{p}\triangleright\and{s}\and{s}\fatsemi\and{q}\triangleright\and{r}$

It may be expressed inline as follows:
$((\and{p}\triangleright\and{s}),(\and{s}\fatsemi\and{q}\triangleright\and{r}))\Rightarrow(\and{p}\fatsemi\and{q}\triangleright\and{r})$.
The set consisting of just this atomic rule is a base $\mathscr{B}$.

Let $\mathscr{C}$ be the set of all atomic rules of taking the same form as
$\and{p}$,$\and{q}$,$\and{r}$, and $\and{s}$ range — that is,

$\mathscr{C}:=\left\\{\raisebox{-5.0pt}{
$\and{x}\fatsemi\and{y}\triangleright\and{z}\lx@proof@logical@and\and{x}\triangleright\and{w}\and{w}\fatsemi\and{y}\triangleright\and{z}$
}\mid\and{x},\and{y},\and{z},\and{w}\in\mathbb{A}\right\\}$

Observe, $\mathscr{C}\supseteq\mathscr{B}$ and $\mathscr{B}\neq\mathscr{C}$.

Intuitively, $\Rightarrow(\and{P}\triangleright\and{p})$ means that the
sequent of atoms $(\and{P}\triangleright\and{p})$ may be concluded whenever,
while
$(\and{P}_{1}\triangleright\and{p}_{1},\dots,\and{P}_{n}\triangleright\and{p}_{n})\Rightarrow(\and{P}\triangleright\and{p})$
means that one may derive $\and{P}\triangleright\and{p}$ if one has derived
$(\and{P}_{i}\triangleright\and{p}_{i})$ for $i=1,...,n$. However, we regard
the context-formers as _meta-logical_ so that it is essential that
derivability in a base respects _coherent equivalence_ (see Definition 4).
Similarly, the additive context-former must admit weakening and contractions
because that is what it means as a data constructor in BI. Hence, we arrive at
the following definition of derivability in a base, which is in the sequent
calculus format (cf. the natural deduction format used for IPL [42] and IMLL
[13]):

######  Definition 12 (Derivability in a Base)

Let $\mathscr{B}$ be a base. Derivability in $\mathscr{B}$ — denoted
$\vdash_{\\!\\!\mathscr{B}}$ — is the smallest relation satisfying the
following:

  * •

taut. If $\and{p}\in\mathbb{A}$, then
$\and{p}\vdash_{\\!\\!\mathscr{B}}\and{p}$

  * •

initial. If $\Rightarrow(\and{P}\triangleright\and{p})\in\mathscr{B}$, then
$\and{P}\vdash_{\\!\\!\mathscr{B}}\and{p}$

  * •

rule. If
$(\and{P}_{1}\triangleright\and{p}_{1},\ldots,\and{P}_{n}\triangleright\and{p}_{n})\Rightarrow(\and{P}\triangleright\and{p})\in\mathscr{B}$
and
$\and{P}_{1}\vdash_{\\!\\!\mathscr{B}}\and{p}_{1},\dots,\and{P}_{n}\vdash_{\\!\\!\mathscr{B}}\and{p}_{n}$,
then $\and{P}\vdash_{\\!\\!\mathscr{B}}\and{p}$

  * •

weak. If $\and{P}(\and{Q})\vdash_{\\!\\!\mathscr{B}}\and{p}$, then
$\and{P}(\and{Q}\fatsemi\and{Q}^{\prime})\vdash_{\\!\\!\mathscr{B}}\and{p}$
for any $\and{Q}^{\prime}\in\mathbb{B}(\mathbb{A})$

  * •

cont. If $\and{P}(\and{Q}\fatsemi\and{Q})\vdash_{\\!\\!\mathscr{B}}\and{p}$,
then $\and{P}(\and{Q})\vdash_{\\!\\!\mathscr{B}}\and{p}$

  * •

exch. Let $\and{Q},\and{Q}^{\prime}\in\mathbb{B}(\mathbb{A})$ be such that
$\and{Q}\equiv\and{Q}^{\prime}$. If
$\and{P}(\and{Q})\vdash_{\\!\\!\mathscr{B}}\and{p}$, then
$\and{P}(\and{Q}^{\prime})\vdash_{\\!\\!\mathscr{B}}\and{p}$.

  * •

cut. If $\and{T}\vdash_{\\!\\!\mathscr{B}}\and{q}$ and
$\and{S}(\and{q})\vdash_{\\!\\!\mathscr{B}}\and{p}$, then
$\and{S}(\and{T})\vdash_{\\!\\!\mathscr{B}}\and{p}$.

######  Example 4 (Example 3 cont’d)

The expressive power of $\mathscr{B}$ and $\mathscr{C}$ is the same as
$\varnothing$ because of cut — that is,
$\and{P}\vdash_{\\!\\!\mathscr{B}}\and{p}$ iff
$\and{P}\vdash_{\\!\\!\mathscr{C}}\and{p}$ iff
$\and{P}\vdash_{\\!\\!\varnothing}\and{p}$.

As Example 4 illustrates, it is possible to define a base that satisfies some
of weak, cont, exch, cut using just initial and rule. Indeed, in Section 5, we
construct a base $\mathscr{N}$ that satisfies all of them, but the property
must be persistent with respect to base-extension. The work of this paper goes
through without modification if one were to fix such a class of bases and
define the semantics, and prove soundness and completeness, relative to that
class, but it requires wanton repetition of infinitely many structural rules
in each base. Things are clearer if one regards the context-formers as meta-
logical, analogous to the treatment in other logics.

To conclude this section, we state an obvious but important fact about
derivability in a base:

######  Proposition 1 ()

If $\and{T}\vdash_{\\!\\!\mathscr{B}}\and{p}$ and
$\mathscr{C}\supseteq\mathscr{B}$, then
$\and{T}\vdash_{\\!\\!\mathscr{C}}\and{p}$.

###  3.2 Support in a Base

Derivability in base forms the ground for the B-eS of BI. That is, it gives
the semantics of the non-logical parts of BI — namely, the atoms. The
semantics of the logical constants is expressed in terms of a support
judgement that unfold according the clauses, analogous to the satisfaction
relation used in model-theoretic semantics. This section is about defining the
support judgement.

Intuitively, support (in a base) for BI combines the notion of support (in a
base) for IPL [42] and for IMLL [13]. However, the use of bunches as data-
structures renders it more complex than in either of the preceding work. As in
the B-eS for IMLL, to handle substructurality, support carries a collection of
atoms thought of as _resources_. In BI, that collection is a _bunch_. Hence,
it is necessary to accommodate the particular idiosyncrasies of this data
structure. To this end, we use _bunch-extensions_ , which appear elsewhere in
the semantics and proof theory of BI, but without uniform treatment — see, for
example, Gheorghiu et al. [12], where it is in-advisably called _weak
coherence_.

######  Definition 13 (Bunch-extension)

The _bunch-extension_ relation $\succeq$ is the least relation satisfying:

  * –

if
$\mathrm{\Gamma}\equiv\mathrm{\Gamma}^{\prime}[\mathrm{\Delta}\mapsto\mathrm{\Delta}\fatsemi\mathrm{\Delta}^{\prime}]$,
then $\mathrm{\Gamma}\succeq\mathrm{\Gamma}^{\prime}$

  * –

if $\mathrm{\Gamma}\succeq\mathrm{\Gamma}^{\prime}$ and
$\mathrm{\Gamma}^{\prime}\succeq\mathrm{\Gamma}^{\prime\prime}$, then
$\mathrm{\Gamma}\succeq\mathrm{\Gamma}^{\prime\prime}$.

###### Example 5

Observe
$((\and{p}\mathrel{\fatcomma}\and{q})\mathrel{\fatsemi}\and{u})\\!\mathrel{\fatcomma}\\!\and{r}\succeq(\and{p}\mathrel{\fatcomma}\and{q})\\!\mathrel{\fatcomma}\\!\and{r}$,
since
$((\and{p}\mathrel{\fatcomma}\and{q})\mathrel{\fatsemi}\and{u})\\!\mathrel{\fatcomma}\\!\and{r}\equiv((\and{p}\mathrel{\fatcomma}\and{q})\\!\mathrel{\fatcomma}\\!\and{r})[(\and{p}\mathrel{\fatcomma}\and{q})\mapsto(\and{p}\mathrel{\fatcomma}\and{q})\mathrel{\fatsemi}\and{u}]$.
Moreover,
$(\and{p}\mathrel{\fatcomma}\and{q})\\!\mathrel{\fatcomma}\\!\and{r}\succeq\and{p}\mathrel{\fatcomma}(\and{q}\\!\mathrel{\fatcomma}\\!\and{r})$,
since
$(\and{p}\mathrel{\fatcomma}\and{q})\\!\mathrel{\fatcomma}\\!\and{r}\equiv\and{p}\mathrel{\fatcomma}(\and{q}\\!\mathrel{\fatcomma}\\!\and{r})$.
Hence,
$((\and{p}\mathrel{\fatcomma}\and{q})\mathrel{\fatsemi}\and{u})\\!\mathrel{\fatcomma}\\!\and{r}\succeq\and{p}\mathrel{\fatcomma}(\and{q}\\!\mathrel{\fatcomma}\\!\and{r})$.

######  Proposition 2 ()

If $\and{T}\preceq\and{S}$, then $\and{P(T)}\preceq\and{P(S)}$.

Having defined derivability in a base, and base- and bunch-extensions, it is
possible to give the semantics.

######  Definition 14 (Support in a Base)

Supports in the base $\mathscr{B}$ relative to either a contextual bunch or
bunch of atoms $\and{P}$ is the smallest relation
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}$ defined by the clauses of Figure 4 in
which $\and{p}\in\mathbb{A}$, $\varphi,\psi\in\mathbb{F}$,
$\and{S}\in\mathbb{B}(\mathbb{A})$,
$\and{R}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$ and
$\mathrm{\Gamma},\mathrm{\Delta}\in\mathbb{B}(\mathbb{F})$.

It is easy to see that Figure 4 is an inductive definition on a structure of
formulas that prioritizes the conjunctions and disjunction (i.e.,
$\mathrel{\ast}$, $\land$, and $\lor$) over the implications
($\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$ and $\to$); this follows similar
treatments in the B-eS of IPL [43] and IMLL [13]. The concept of bunch-
extension is used in (() ‣ 4) and (() ‣ 4). As explained in Section 1, the
purpose of the bunches of atoms indexing the support relation is to express
the susbtructurality of the logical constants and delivers a resource
interpretation of the logic. This is made clear in application of BI via the
B-eS to access control in Section 3.3.

$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\and{p}\quad$ iff
$\displaystyle\and{S}\vdash_{\\!\\!\mathscr{B}}\and{p}$ (At)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\land\psi\quad$ iff
$\displaystyle\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{
if
}\varphi\\!\mathrel{\fatsemi}\\!\psi\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p},\text{
then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(S)}}\and{p}$ ($\land$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{\ast}\psi\quad$
iff
$\displaystyle\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{
if
}\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p},\text{
then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(S)}}\and{p}$ ($\mathrel{\ast}$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\lor\psi\quad$ iff
$\displaystyle\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},$
$\displaystyle\text{if
}\varphi\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p}\text{ and
}\psi\Vdash_{\\!\\!\mathscr{X}}^{\and{U(\cdot)}}\and{p},\text{ then
}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(S)}}\and{p}$ ($\lor$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\to\psi\quad$ iff
$\displaystyle\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{S}\mathrel{\fatsemi}(\cdot)}\psi$
($\to$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi\quad$
iff
$\displaystyle\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{S}\mathrel{\fatcomma}(\cdot)}\psi$
($\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\bot\quad$ iff
$\displaystyle\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\Vdash_{\\!\\!\mathscr{B}}^{\and{U(S)}}\and{p}$
($\bot$) $\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\top\quad$ iff
$\displaystyle\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U(\cdot)}\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{
if }\Vdash_{\\!\\!\mathscr{X}}^{\and{U(\varnothing_{\\!+})}}\and{p},\text{
then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(S)}}\and{p}$ ($\top$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\top^{\ast}\quad$ iff
$\displaystyle\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U(\cdot)}\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{
if
}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(\varnothing_{\\!\times})}}\and{p},\text{
then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(S)}}\and{p}$ ($\top^{\ast}$)
$\displaystyle\mathrm{\Gamma}$
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{R(\cdot)}}\psi\quad$ iff
$\displaystyle\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}\in\mathbb{B}(\mathbb{A}),\text{
if }\Vdash_{\\!\\!\mathscr{X}}^{\and{U}}\mathrm{\Gamma},\text{ then
}\Vdash_{\\!\\!\mathscr{X}}^{\and{R(U)}}\psi$ (Inf)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!\times}\hskip
25.00003pt$ iff $\displaystyle\and{S}\succeq\varnothing_{\\!\times}$
($\varnothing_{\\!\times}$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!+}\quad$
always ($\varnothing_{\\!+}$)
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\fatcomma\mathrm{\Delta}\quad$
iff
$\displaystyle\exists\and{Q_{1}},\and{Q_{2}}\in\mathbb{B}(\mathbb{A})\text{
such that
}\and{S}\succeq\and{Q_{1}}\\!\mathrel{\fatcomma}\\!\and{Q_{2}},\Vdash_{\\!\\!\mathscr{B}}^{\and{Q_{1}}}\mathrm{\Gamma},\Vdash_{\\!\\!\mathscr{B}}^{\and{Q_{2}}}\mathrm{\Delta}$
()
$\displaystyle\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}\quad$
iff
$\displaystyle\exists\and{Q_{1}},\and{Q_{2}}\in\mathbb{B}(\mathbb{A})\text{
such that
}\and{S}\succeq\and{Q_{1}},\and{S}\succeq\and{Q_{2}},\Vdash_{\\!\\!\mathscr{B}}^{\and{Q_{1}}}\mathrm{\Gamma},\Vdash_{\\!\\!\mathscr{B}}^{\and{Q_{2}}}\mathrm{\Delta}$
()

Figure 4: Support for BI

######  Definition 15 (Validity)

A sequent $\mathrm{\Gamma}\triangleright\varphi$ is _valid_ iff
$\mathrm{\Gamma}\Vdash\varphi$, where

$\mathrm{\Gamma}\Vdash\varphi\qquad\mbox{iff}\qquad\mbox{for any base
$\mathscr{B}$,}\quad\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}^{(\cdot)}\varphi$

###### Example 6

It is instructive to see that
$\Vdash_{\\!\\!\varnothing}^{((\and{p}\mathrel{\fatcomma}\and{q})\mathrel{\fatsemi}\and{u})\mathrel{\fatcomma}\and{r}}\and{p}\\!\mathrel{\fatcomma}\\!(\and{q}\mathrel{\ast}\and{r})$
obtains. From Example 5,
$((\and{p}\\!\mathrel{\fatcomma}\\!\and{q})\\!\mathrel{\fatsemi}\\!\and{u})\\!\mathrel{\fatcomma}\\!\and{r}\succeq\and{p}\\!\mathrel{\fatcomma}\\!(\and{q}\\!\mathrel{\fatcomma}\\!\and{r})$.
Hence, by (() ‣ 4), it suffices to show the following: (1)
$\Vdash_{\\!\\!\varnothing}^{\and{p}}\and{p}$, and (2)
$\Vdash_{\\!\\!\varnothing}^{\and{q}\mathrel{\fatcomma}\and{r}}\and{q}\mathrel{\ast}\and{r}$.
That (1) obtains is immediate by (At) and taut in Definition 12. By
($\mathrel{\ast}$ ‣ 4), claim $(2)$ is equivalent to the following:

$\forall\mathscr{X}\supseteq\varnothing,\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{s}\in\mathbb{A},\text{
if
}\and{q}\\!\mathrel{\fatcomma}\\!\and{r}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{s},\text{
then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\and{q}\mathrel{\fatcomma}\and{r})}\and{s}$
($\dagger$)

Analogous to (1), we have $\Vdash_{\\!\\!\mathscr{X}}^{\and{q}}\and{q}$ and
$\Vdash_{\\!\\!\mathscr{X}}^{\and{r}}\and{r}$ for any $\mathscr{X}$.
Therefore, by (() ‣ 4),
$\Vdash_{\\!\\!\mathscr{X}}^{\and{q}\mathrel{\fatcomma}\and{r}}\and{q}\\!\mathrel{\fatcomma}\\!\and{r}$.
The result follows by (Inf) on the antecedent of ($\dagger$ ‣ 6). We see in
this example why $\preceq$ must apply to sub-bunches and not merely at the
top-level.

The main result of this paper is to show that consequence for BI is the same
as validity in the B-eS — that is,
$\mathrm{\Gamma}\vdash_{\\!\\!}\varphi\mbox{ iff
}\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$. This is captured in Theorem 4.1
(Soundness) and Theorem 5.1 (Completeness), which are stated and proved in
Section 4 and Section 5, respectively.

To conclude this section, it is instructive to observe that the following
expected properties do indeed hold for the semantics:

######  Lemma 2 (Monotonicity)

If $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\varphi$ and
$\mathscr{C}\supseteq\mathscr{B}$ and $\and{S}\succeq\and{T}$, then
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}}\varphi$.

It is easy to see that monotonicity (Lemma 2) extends to bunches. Moreover, as
a corollary: $\mathrm{\Gamma}\Vdash\varphi$ iff
$\mathrm{\Gamma}\Vdash_{\\!\\!\varnothing}^{(\cdot)}\varphi$.

######  Lemma 3 (Identity)

For any base $\mathscr{B}$ and $\and{P}\in\mathbb{B}(\mathbb{A})$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\and{P}$ obtains.

The following lemmas show that the structurality of bunches in BI is
adequately captured in the support judgement:

######  Lemma 4 ()

For any base $\mathscr{B}$,
$\and{S},\and{S}^{\prime}\in\mathbb{B}(\mathbb{A})$,
$\and{P}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\varphi\in\mathbb{F}$,

(4) if $\Vdash_{\\!\\!\mathscr{B}}^{\and{P}(\and{S})}\varphi$, then
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}(\and{S}\mathrel{\fatsemi}\and{S}^{\prime})}\varphi$
(4) if
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}(\and{S}\mathrel{\fatsemi}\and{S})}\varphi$,
then $\Vdash_{\\!\\!\mathscr{B}}^{\and{P}(\and{S})}\varphi$.

######  Lemma 5 ()

For any base $\mathscr{B}$, $\and{S}\in\mathbb{B}(\mathbb{A})$,
$\mathrm{\Delta},\mathrm{\Delta}^{\prime}\in\mathbb{B}(\mathbb{F})$,
$\mathrm{\Gamma}(\cdot)\in\dot{\mathbb{B}}(\mathbb{F})$,

(5) if
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$,
then $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$
(5) if $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$,
then
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta})$.

######  Lemma 6 (Compositionality)

If $\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{S}(\cdot)}\psi$ and
$\psi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\cdot)}\chi$, then
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\and{S}(\cdot))}\chi$.

This final result implies that this semantics is _categorical_ in the sense
that the B-eS of IPL by Sandqvist [42] is categorical — see Pym et al. [36].
Briefly, objects are bunches of formulae (i.e., $\mathbb{B}(\mathbb{F})$) and
morphisms $\mathrm{\Gamma}\to\mathrm{\Delta}$ are pairs
$\langle\mathscr{B},\and{S}(\cdot)\rangle$ such that
$\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}^{\and{S}(\cdot)}\mathrm{\Delta}$.
In this set-up, Lemma 2 and Lemma 6 enable composition to be defined as
follows:

$\mathrm{\Gamma}\xrightarrow{\langle\mathscr{B},\and{S}(\cdot)\rangle}\mathrm{\Delta}\xrightarrow{\langle\mathscr{B}^{\prime},\and{T}(\cdot)\rangle}\mathrm{\Sigma}=\mathrm{\Gamma}\xrightarrow{\langle\mathscr{B}\cup\mathscr{B}^{\prime},\and{T(S(\cdot))}\rangle}\mathrm{\Sigma}$

This can be viewed as an enrichment of the traditional category-theoretic
treatment of IPL in which Heyting algebras are regarded in terms of posets —
see, for example, Lambek and Scott [25].

###  3.3 Example: Rule-based Access Control

In this section, we introduce a toy example to demonstrate the application of
the B-eS given in this paper to access control, which is central to security
in computer systems — see, for example, Abadi [1].

Suppose you subscribe to the movie streaming service _BunchedFlix_. There are
three films on the platform: $\and{a}$, $\and{b}$, and $\and{c}$. Users can
become members or purchase tokens that are consumed to access the films. More
specifically:

  * –

to watch $\and{a}$, a user must either be a member or pay three tokens

  * –

to watch $\and{b}$, a user must be a member

  * –

to watch $\and{c}$, a user must be a member and still pay two tokens.

These access-control conditions for _BunchedFlix_ can readily be modelled
using the B-eS for BI.

Let
$\and{p}^{k}:=\and{p}\\!\mathrel{\fatcomma}\\!\ldots\\!\mathrel{\fatcomma}\\!\and{p}$
with $k$-copies. The following base captures the access control conditions
above:

$\mathscr{A}:=\left\\{\and{m}\triangleright\and{a}\right\\}\cup\left\\{\and{p}^{k}\triangleright\and{a}\mid
k\geq
3\right\\}\cup\left\\{\and{m}\triangleright\and{b}\right\\}\cup\left\\{\and{m}\fatsemi\and{p}^{k}\triangleright\and{c}\mid
k\geq 2\right\\}$

Here $\and{m}$ denotes membership, and $\and{p}$ denotes a token. Consider an
arbitrary user: let $\and{u}$ denote her membership status — that is,
$\and{u}:=\and{m}$ if she is a member of _BunchedFlix_ , and
$\and{u}:=\varnothing_{\\!+}$ otherwise. Suppose that she has $k$ tokens on
her account. To check that she has the right to watch the film
$\and{x}\in\\{\and{a},\and{b},\and{c}\\}$ on _BunchedFlix_ is modelled by the
support judgement
$\and{u}\Vdash_{\\!\\!\mathscr{A}}^{\and{p}^{k}\mathrel{\fatsemi}(\cdot)}\and{x}$.

For example, let Alice be one such user, and suppose she has $4$ tokens. It is
easy to see that Alice has the right to watch all three films $\and{a}$,
$\and{b}$, and $\and{c}$ if she is a member, and otherwise only film
$\and{a}$.

Suppose Alice is indeed member of _BunchedFlix_. Can she watch both film $a$
and film $\and{c}$? In one sense, yes; in another sense, no. As stated above,
she may indeed watch either film. However, having watched one of them she may
_not_ watch the other as she will have insufficient tokens. The first reading
corresponds to the judgement
$\and{u}\Vdash_{\\!\\!\mathscr{A}}^{\and{p}^{4}\mathrel{\fatsemi}(\cdot)}\and{a}\land\and{c}$,
which obtains, and the second to
$\and{u}\Vdash_{\\!\\!\mathscr{A}}^{\and{p}^{4}\mathrel{\fatsemi}(\cdot)}\and{a}\mathrel{\ast}\and{c}$,
which does not obtain. This illustrates the resource-sensitivity of the
semantics and how it is handled by the additive and multiplicative parts of
the logic.

Observe that not much of the possible structures in the B-eS of BI are
required to make this example work, despite its making some subtle
distinctions about access (i.e., what it means to access both films $\and{a}$
and $\and{c}$). For example, all the rules of $\mathscr{A}$ are axioms, while
the general set-up of the B-eS indeed allows rules with premisses.

##  4 Soundness

######  Theorem 4.1 (Soundness)

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

The proof proceeds by the typical method of induction on derivations
witnessing $\vdash_{\\!\\!\mathsf{NBI}}$. There are nineteen cases to
consider, corresponding to the rules in $\mathsf{NBI}$ (Figure 3). We
illustrate $\mathsf{\mathrel{\ast}}_{\mathsf{I}}$, and
$\mathsf{\mathrel{\ast}}_{\mathsf{E}}$ here, the rest being similar. The
complete proof is contained in Appendix 0.B.

####  $\mathrel{\ast}$-Introduction $(\mathsf{\mathrel{\ast}}_{\mathsf{I}})$.

We require to show the following:

$\text{if }\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\text{ and
}\mathrm{\Delta}\Vdash_{\\!\\!}\psi,\text{ then
}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\mathrel{\ast}\psi$
($\otimes I$)

###### Proof

Assume $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$. By (Inf) on the consequent of ($\otimes
I$), we require to show
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{\ast}\psi$ for an
arbitrary base $\mathscr{B}$ and $\and{S}\in\mathbb{B}(\mathbb{A})$ satisfying
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$.
By ($\mathrel{\ast}$ ‣ 4), the desired conclusion is equivalent to the
following:

$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and
$\forall\and{p}\in\mathbb{A}$, if
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p}$,
then $\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\and{S})}\and{p}$.

Therefore, fix $\mathscr{C}\supseteq\mathscr{B}$,
$\and{Q}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{q}\in\mathbb{A}$
such that
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}(\cdot)}\and{q}$.
We require to show $\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}(\and{S})}\and{q}$. By
(() ‣ 4), from
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$,
infer there exist $\and{T}_{1},\and{T}_{2}\in\mathbb{B}(\mathbb{A})$ such that
$\and{S}\succeq(\and{T}_{1}\\!\mathrel{\fatcomma}\\!\and{T}_{2})$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\mathrm{\Gamma}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\mathrm{\Delta}$. Therefore, by (Inf)
on $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$, infer
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\psi$. Hence, by (() ‣ 4), obtain
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}}\varphi\\!\mathrel{\fatcomma}\\!\psi$.
The desired result follows by (Inf) on
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}(\cdot)}\and{q}$.

####  $\mathrel{\ast}$-Elimination $(\mathsf{\mathrel{\ast}}_{\mathsf{E}})$.

We require to show the following:

$\text{if
}\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\Vdash_{\\!\\!}\chi\text{
and }\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\mathrel{\ast}\psi,\text{ then
}\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\chi.$ ($\mathrel{\ast}E$)

###### Proof

This follows immediately by Lemma 7, which is a generalization of the claim
amenable to proof by induction, by taking $\and{R}(\cdot):=(\cdot)$ and
$\mathscr{B}:=\varnothing$.

######  Lemma 7 (General $\mathrel{\ast}$E)

If
$\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\\!\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\\!\\!\chi$
and
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}\varphi\\!\mathrel{\ast}\\!\psi$,
then
$\mathrm{\Gamma}(\mathrm{\Delta})\\!\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\\!\\!\chi$.

###### Proof

Label the statements
$\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\chi$,
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}\varphi\mathrel{\ast}\psi$, and
$\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\chi$
by (1), (2), and (3), respectively. We proceed by induction on the size of
$\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}$.

  * •

Base case. $\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}=0$. It must be that
$\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)=\varphi\\!\mathrel{\fatcomma}\\!\psi$,
and the statement follows immediately from Lemma 8.

  * •

Inductive step. $\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}=d+1$ for some
$d\geq 0$. It must be that
$\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\equiv\mathrm{\Sigma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\star\mathrm{\Theta}$,
where $\mathrm{holeDepth}{(\mathrm{\Sigma}(\cdot))}=d-1$ and
$\star\in\\{\mathrel{\fatcomma},\mathrel{\fatsemi}\\}$. We verify the case for
, the case for being similar.

By (Inf), to show
$\mathrm{\Sigma}(\mathrm{\Delta})\\!\mathrel{\fatsemi}\\!\mathrm{\Theta}\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\chi$,
we require to show that for arbitrary $\mathscr{C}\supseteq\mathscr{B}$ and
$\and{P}\in\mathbb{B}(\mathbb{A})$ such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}}\mathrm{\Sigma}(\mathrm{\Delta})\\!\mathrel{\fatsemi}\\!\mathrm{\Theta}$,
we may infer $\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\and{P})}\chi$. By
definition,
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}}\mathrm{\Sigma}(\mathrm{\Delta})\\!\mathrel{\fatsemi}\\!\mathrm{\Theta}$
says there exist $\and{P}_{1}$ and $\and{P}_{2}$ satisfying
$\and{P}_{1}\preceq\and{P}$ and $\and{P}_{2}\preceq\and{P}$, such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}_{1}}\mathrm{\Sigma}(\mathrm{\Delta})$ and
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}_{2}}\mathrm{\Theta}$.

Now, (7) says that
$\mathrm{\Sigma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\\!\mathrel{\fatsemi}\\!\mathrm{\Theta}\Vdash_{\\!\\!\mathscr{B}}^{\and{R}(\cdot)}\chi$;
that is, for arbitrary $\mathscr{X}\supseteq\mathscr{B}$,
$\and{U}\in\mathbb{B}(\mathbb{A})$, if there exist $\and{V}_{1}\preceq\and{U}$
and $\and{V}_{2}\preceq\and{U}$ such that
$\Vdash_{\\!\\!\mathscr{X}}^{\and{V}_{1}}\mathrm{\Sigma}(\varphi\\!\mathrel{\fatsemi}\\!\psi)$
and $\Vdash_{\\!\\!\mathscr{X}}^{\and{V}_{2}}\mathrm{\Theta}$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\and{R}(\and{U})}\chi$. Given
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}_{2}}\mathrm{\Theta}$, this implies: for
arbitrary $\mathscr{X}\supseteq\mathscr{C}$ and
$\and{U}\in\mathbb{B}(\mathbb{A})$, if $\and{U}\succeq\and{P}_{2}$ and there
exists $\and{V}$ such that $\and{V}\preceq\and{U}$ and
$\Vdash_{\\!\\!\mathscr{X}}^{\and{V}}\mathrm{\Sigma}(\varphi\\!\mathrel{\fatsemi}\\!\psi)$,
then $\Vdash_{\\!\\!\mathscr{X}}^{\and{R}(\and{U})}\chi$. By the definition of
$\preceq$, this implies:

$\forall\mathscr{X}\supseteq\mathscr{C},\forall\and{V}\in\mathbb{B}(\mathbb{A}),\text{
if
}\Vdash_{\\!\\!\mathscr{X}}^{\and{V}}\mathrm{\Sigma}(\varphi\\!\mathrel{\fatsemi}\\!\psi),\text{
then
}\Vdash_{\\!\\!\mathscr{X}}^{\and{R}(\and{V}\mathrel{\fatsemi}\and{P}_{2})}\chi$

This is exactly
$\Vdash_{\\!\\!\mathscr{C}}^{\and{R}((\cdot)\mathrel{\fatsemi}\and{P}_{2})}\chi$.
Apply the IH to this and
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{C}}\varphi\mathrel{\ast}\psi$ to obtain
$\mathrm{\Sigma}(\mathrm{\Delta})\Vdash_{\\!\\!\mathscr{C}}^{\and{R}((\cdot)\mathrel{\fatsemi}\and{P}_{2})}\chi$.
By $\Vdash_{\\!\\!\mathscr{C}}^{\and{P}_{1}}\mathrm{\Sigma}(\mathrm{\Delta})$,
infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\and{P}_{1}\mathrel{\fatsemi}\and{P}_{2})}\chi$.
Note that $\and{P}_{1}\preceq\and{P}$ and $\and{P}_{2}\preceq\and{P}$ implies
$\and{P}_{1}\mathrel{\fatsemi}\and{P}_{2}\preceq\and{P}\mathrel{\fatsemi}\and{P}$.
Therefore, by monotonicity (i.e., Lemma 2), we have
$\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\and{P}\mathrel{\fatsemi}\and{P})}\chi$.
By Lemma 4, infer $\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\and{P})}\chi$.

This completes the induction.

######  Lemma 8 (Basic $\mathrel{\ast}$E)

If
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\cdot)}\chi$
and
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}^{\and{S}(\cdot)}\varphi\mathrel{\ast}\psi$,
then
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\and{S}(\cdot))}\chi$.

###### Proof

Label the
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\cdot)}\chi$,
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}^{\and{S}(\cdot)}\varphi\mathrel{\ast}\psi$,
and $\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\and{S}(\cdot))}\chi$
by (1), (2), and (3), respectively. We proceed by induction on the structure
of $\chi$. For space reasons, we focus on one representative case in the
inductive step. The complete proof can be found in Appendix 0.B.

  * •

Base case. $\chi$ is an atom, say $\and{p}$. Then the statment follows
immediately from the semantics of $\mathrel{\ast}$ (see Definition 14,
($\mathrel{\ast}$ ‣ 4)).

  * •

Inductive step. We makes a case-analysis over the principal connective of
$\chi$. Here we show one of the most complex cases: $\chi=\sigma\lor\tau$. The
other cases are similar.

By (Inf) on the consequent of (8), it suffices to fix some
$\mathscr{C}\supseteq\mathscr{B}$ and $\and{Q}\in\mathbb{B}(\mathbb{A})$ such
that $\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}}\mathrm{\Delta}$, and prove that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}(\and{S}(\and{Q}))}\sigma\lor\tau$. To
this end, fix some arbitrary $\mathscr{D}\supseteq\mathscr{C}$,
$\and{P}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{q}\in\mathbb{A}$
such that $\sigma\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\cdot)}\and{q}$ and
$\tau\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\cdot)}\and{q}$, and the goal is to
prove
$\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\and{T}(\and{S}(\and{Q})))}\and{q}$. By
(8), we have
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}(\and{Q})}\varphi\mathrel{\ast}\psi$. By
(Inf) and ($\lor$ ‣ 4), assumption (8) can be rendered as follows:

$\begin{split}&\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}\in\mathbb{B}(\mathbb{A}),\text{
if
}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}}\varphi\\!\mathrel{\fatcomma}\\!\psi,\text{
then:}\\\
\forall\mathscr{Y}\supseteq\mathscr{X},&\forall\and{V}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{
if }\sigma\Vdash_{\\!\\!\mathscr{Y}}^{\and{V}(\cdot)}\and{p}\text{ and
}\tau\Vdash_{\\!\\!\mathscr{Y}}^{\and{V}(\cdot)}\and{p},\text{
then}\Vdash_{\\!\\!\mathscr{Y}}^{\and{V}(\and{T}(\and{U}))}\and{p}\end{split}$

Given $\sigma\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\cdot)}\and{q}$,
$\tau\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\cdot)}\and{q}$, this implies:

$\forall\mathscr{Y}\supseteq\mathscr{D},\forall\and{U}\in\mathbb{B}(\mathbb{A}),\text{
if
}\Vdash_{\\!\\!\mathscr{Y}}^{\and{U}}\varphi\\!\mathrel{\fatcomma}\\!\psi,\text{
then}\Vdash_{\\!\\!\mathscr{Y}}^{\and{P}(\and{T}(\and{U}))}\and{q}$

In other words,
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\and{T}(\and{\cdot}))}\and{q}$.
Apply the IH to
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\and{T}(\and{\cdot}))}\and{q}$
and $\Vdash_{\\!\\!\mathscr{D}}^{\and{S}(\and{Q})}\varphi\mathrel{\ast}\psi$
to obtain
$\Vdash_{\\!\\!\mathscr{D}}^{\and{P}(\and{T}(\and{Q}(\and{S})))}\and{q}$.

This completes the induction.

##  5 Completeness

######  Theorem 5.1 (Completeness)

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

We follow the strategy used by Sandqvist [42] for IPL and by the authors for
IMLL [13], suitably modified for BI. We require to show that
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ implies that there is an
$\mathsf{NBI}$-proof witnessing $\mathrm{\Gamma}\vdash_{\\!\\!}{}\varphi$. To
this end, we associate to each sub-formula $\rho$ of
$\mathrm{\Gamma}\cup\\{\varphi\\}$ a unique atom $\and{r}$, and construct a
base $\mathscr{N}$ such that $\and{r}$ behaves in $\mathscr{N}$ as $\rho$
behaves in $\mathsf{NBI}$. Moreover, formulae and their atomizations are
semantically equivalent in any extension of $\mathscr{N}$ so that support in
$\mathscr{N}$ characterizes both validity and provability — that is
$\varphi^{\flat}\Vdash_{\\!\\!\mathscr{N}}^{(\cdot)}\varphi$ and
$\varphi\Vdash_{\\!\\!\mathscr{N}}^{(\cdot)}\varphi^{\flat}$. When
$\rho\in\mathbb{A}$, we take $\and{r}:=\rho$, but for complex $\rho$ we choose
$r$ to be alien to $\mathrm{\Gamma}\cup\\{\varphi\\}$.

We proceed with a formal treatment. Let $\mathrm{\Xi}$ be the set of all sub-
formulae of $\mathrm{\Gamma}$ and $\varphi$. Let
${(\cdot)}^{\flat}\colon\mathrm{\Xi}\to\mathbb{A}$ be an injection that acts
as an identity on $\mathrm{\Xi}\cap\mathbb{A}$ (i.e.,
${\and{p}}^{\flat}=\and{p}$ for $\and{p}\in\mathrm{\Xi}\cap\mathbb{A}$). Let
${(\cdot)}^{\natural}$ be the left-inverse of ${(\cdot)}^{\flat}$ — that is,

${\and{p}}^{\natural}:=\begin{cases}\chi&\mbox{if $\and{p}={\chi}^{\flat}$}\\\
\and{p}&\mbox{otherwise}\end{cases}$

Both extend to bunches pointwise with identity on units; that is,

$\begin{array}[]{c@{\qquad}c}\mathrm{\Delta}^{\flat}:=\begin{cases}{\varphi}^{\flat}&\mbox{if
}\mathrm{\Delta}=\varphi\in\mathbb{F}\\\ \varnothing_{\\!+}&\mbox{if
}\mathrm{\Delta}=\varnothing_{\\!+}\\\ \varnothing_{\\!\times}&\mbox{if
}\mathrm{\Delta}=\varnothing_{\\!\times}\\\
{\mathrm{\Delta}}^{\flat}_{1}\fatsemi{\mathrm{\Delta}}^{\flat}_{2}&\mbox{if
}\mathrm{\Delta}=\mathrm{\Delta}_{1}\fatsemi\mathrm{\Delta}_{2}\\\
{\mathrm{\Delta}}^{\flat}_{1}\fatcomma{\mathrm{\Delta}}^{\flat}_{2}&\mbox{if
}\mathrm{\Delta}=\mathrm{\Delta}_{1}\fatcomma\mathrm{\Delta}_{2}\end{cases}&{\and{P}}^{\natural}:=\begin{cases}{\and{p}}^{\natural}&\mbox{if
}\and{P}=\and{p}\in\mathbb{A}\\\ \varnothing_{\\!+}&\mbox{if
}\and{P}=\varnothing_{\\!+}\\\ \varnothing_{\\!\times}&\mbox{if
}\and{P}=\varnothing_{\\!\times}\\\
{\and{P}}^{\natural}_{1}\fatsemi{\and{P}}^{\natural}_{2}&\mbox{if
}\and{P}=\and{P}_{1}\fatsemi\and{P}_{2}\\\
{\and{P}}^{\natural}_{1}\fatcomma{\and{P}}^{\natural}_{2}&\mbox{if
}\and{P}=\and{P}_{1}\fatcomma\and{P}_{2}\end{cases}\end{array}$

$\begin{array}[]{c}{\sigma}^{\flat}\triangleright{\sigma}^{\flat}\quad{\mathrm{\Delta}}^{\flat}\triangleright{\sigma}^{\flat}{\mathrm{\Delta}^{\prime}}^{\flat}\triangleright{\sigma}^{\flat}\quad{\mathrm{\Delta}(\mathrm{\Lambda}\\!\mathrel{\fatsemi}\\!\mathrm{\Lambda}^{\prime})}^{\flat}\triangleright{\sigma}^{\flat}{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright{\sigma}^{\flat}\quad{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright{\sigma}^{\flat}{\mathrm{\Delta}(\mathrm{\Lambda}\\!\mathrel{\fatsemi}\\!\mathrm{\Lambda})}^{\flat}\triangleright{\sigma}^{\flat}\\\\[6.45831pt]
\varnothing_{\\!\times}\triangleright{\top^{\ast}}^{\flat}\quad{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright\and{p}\lx@proof@logical@and{\mathrm{\Delta}(\varnothing_{\\!\times})}^{\flat}\triangleright\and{p}{\mathrm{\Lambda}}^{\flat}\triangleright{\top^{\ast}}^{\flat}\quad{\mathrm{\Delta}}^{\flat}\triangleright{(\sigma\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\tau)}^{\flat}{\mathrm{\Delta}}^{\flat}\\!\mathrel{\fatcomma}\\!{\sigma}^{\flat}\triangleright{\tau}^{\flat}\\\\[6.45831pt]
{\mathrm{\Delta}}^{\flat}\\!\mathrel{\fatcomma}\\!{\mathrm{\Lambda}}^{\flat}\triangleright{\tau}^{\flat}\lx@proof@logical@and{\mathrm{\Delta}}^{\flat}\triangleright{(\sigma\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\tau)}^{\flat}{\mathrm{\Lambda}}^{\flat}\triangleright{\sigma}^{\flat}\quad{\mathrm{\Delta}}^{\flat}\\!\mathrel{\fatcomma}\\!{\mathrm{\Lambda}}^{\flat}\triangleright{(\sigma\mathrel{\ast}\tau)}^{\flat}\lx@proof@logical@and{\mathrm{\Delta}}^{\flat}\triangleright{\sigma}^{\flat}{\mathrm{\Lambda}}^{\flat}\triangleright{\tau}^{\flat}\quad{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright\and{p}\lx@proof@logical@and{\mathrm{\Delta}(\sigma\\!\mathrel{\fatcomma}\\!\tau)}^{\flat}\triangleright{\and{p}}^{\flat}{\mathrm{\Lambda}}^{\flat}\triangleright{(\sigma\mathrel{\ast}\tau)}^{\flat}\\\\[6.45831pt]
\varnothing_{\\!+}\triangleright{\top}^{\flat}\quad{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright\and{p}\lx@proof@logical@and{\mathrm{\Delta}(\varnothing_{\\!+})}^{\flat}\triangleright\and{p}{\mathrm{\Lambda}}^{\flat}\triangleright{\top}^{\flat}\quad{\mathrm{\Delta}}^{\flat}\triangleright{(\sigma\to\tau)}^{\flat}{(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\sigma)}^{\flat}\triangleright{\tau}^{\flat}\\\\[6.45831pt]
{\mathrm{\Delta}}^{\flat}\\!\mathrel{\fatsemi}\\!{\mathrm{\Lambda}}^{\flat}\triangleright{\tau}^{\flat}\lx@proof@logical@and{\mathrm{\Delta}}^{\flat}\triangleright{(\sigma\to\tau)}^{\flat}{\mathrm{\Lambda}}^{\flat}\triangleright{\sigma}^{\flat}\quad{\mathrm{\Delta}}^{\flat}\\!\mathrel{\fatsemi}\\!{\mathrm{\Lambda}}^{\flat}\triangleright{(\sigma\land\tau)}^{\flat}\lx@proof@logical@and{\mathrm{\Delta}}^{\flat}\triangleright{\sigma}^{\flat}{\mathrm{\Lambda}}^{\flat}\triangleright{\tau}^{\flat}\quad{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright\and{p}\lx@proof@logical@and{\mathrm{\Delta}(\sigma\\!\mathrel{\fatsemi}\\!\tau)}^{\flat}\triangleright\and{p}{\mathrm{\Lambda}}^{\flat}\triangleright{(\sigma\land\tau)}^{\flat}\\\\[6.45831pt]
{\mathrm{\Delta}}^{\flat}\triangleright{(\sigma_{1}\lor\sigma_{2})}^{\flat}{\mathrm{\Delta}}^{\flat}\triangleright{\sigma}^{\flat}_{i}\quad{\mathrm{\Delta}(\mathrm{\Lambda})}^{\flat}\triangleright\and{p}\lx@proof@logical@and{\mathrm{\Delta}(\sigma)}^{\flat}\triangleright\and{p}{\mathrm{\Delta}(\tau)}^{\flat}\triangleright\and{p}{\mathrm{\Lambda}}^{\flat}\triangleright{(\sigma\lor\tau)}^{\flat}\quad{\mathrm{\Delta}}^{\flat}\triangleright\and{p}{\mathrm{\Delta}}^{\flat}\triangleright{\bot}^{\flat}\end{array}$

Figure 5: The Natural Base $\mathscr{N}$

We construct a base $\mathscr{N}$ such that ${\sigma}^{\flat}$ behaves in
$\mathscr{N}$ as $\sigma$ behaves in $\mathsf{NBI}$. The base $\mathscr{N}$
contains all instances of the rules of Figure 5, which merits comparison with
Figure 3, for all $\and{p}\in\mathbb{A}$,
$\sigma,\sigma_{1},\sigma_{2},\tau\in\mathrm{\Xi}$, and
$\mathrm{\Delta},\mathrm{\Delta}^{\prime},\mathrm{\Lambda},\mathrm{\Lambda}^{\prime}\in\mathbb{B}{(\mathrm{\Xi})}$
such that $\mathrm{\Delta}\equiv\mathrm{\Delta}^{\prime}$. Note, we need not
include 5, 5, 5, and 5 because of taut, exch, weak, and cont, respectively.
Theorem 5.1 (Completeness) follows from the following three properties:

(AtComp)

Let $\and{S}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, $\and{p}\in\mathbb{A}$,
and $\mathscr{B}$ be a base:
$\and{P}\Vdash_{\\!\\!\mathscr{B}}^{\and{S(\cdot)}}\and{p}\text{ iff
}\and{S(P)}\vdash_{\\!\\!\mathscr{B}}\and{p}.$

(Flat)

For any sub-formula $\xi\in\mathrm{\Xi}$ and
$\mathscr{N}^{\prime}\supseteq\mathscr{N}$:
$\Vdash_{\\!\\!\mathscr{N}^{\prime}}^{\and{S}}\xi^{\flat}\text{ iff
}\Vdash_{\\!\\!\mathscr{N}^{\prime}}^{\and{S}}\xi$.

(Nat)

Let $S\in\mathbb{B}(\mathbb{A})$ and $\and{p}\in\mathbb{A}$: if
$\and{S}\vdash_{\\!\\!\mathscr{N}}\and{p}\text{, then
}\and{S}^{\natural}\vdash_{\\!\\!\mathsf{NBI}}\and{p}^{\natural}$.

The first claim (i.e., 5) follows from cut in the definition of derivability
in a base (Definition 12) and is the base case of completeness. It is proved
by induction on support according to the structure of $\and{P}$.

The second claim (i.e., 5) formalizes the idea that every formula $\xi$
appearing in $\mathrm{\Gamma}\cup\\{\varphi\\}$ behaves the same as
${\xi}^{\flat}$ in any base extending $\mathscr{N}$. Consequently,
${\mathrm{\Gamma}}^{\flat}\Vdash_{\\!\\!\mathscr{N}}{\varphi}^{\flat}$ iff
$\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{N}}\varphi$. Of course, it is immediate
to see that it applies to sequents,

$\mathrm{\Gamma}^{\flat}\Vdash_{\\!\\!\mathscr{N}^{\prime}}\varphi^{\flat}\qquad\text{
iff }\qquad\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{N}^{\prime}}\varphi$

It is proved by showing through a case analysis that
$\Vdash_{\\!\\!\mathscr{N}}^{\and{T}}\xi^{\flat}$ respects the clauses of
$\Vdash_{\\!\\!}$ (see Figure 4) according to the structure of $\xi$.

The third claim (i.e., 5) intuitively says that $\mathscr{N}$ is a faithful
atomic encoding of $\mathsf{NBI}$, witnessed by ${(\cdot)}^{\natural}$. This
together with (5) guarantee that every $\xi\in\mathrm{\Xi}$ behaves in
$\mathscr{N}$ as ${\xi}^{\flat}$ in $\mathscr{N}$, thus as
${\left({\xi}^{\flat}\right)}^{\natural}=\xi$ in $\mathsf{NBI}$. It is proved
by induction on derivability in a base.

######  Proof (Completeness — Theorem 5.1)

Assume $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and let $\mathscr{N}$ be the
bespoke base for $\mathrm{\Gamma}\triangleright\varphi$. By (5),
$\mathrm{\Gamma}^{\flat}\Vdash_{\\!\\!\mathscr{N}}^{\varnothing}\varphi^{\flat}$.
Therefore, by (5),
${\mathrm{\Gamma}}^{\flat}\vdash_{\\!\\!\mathscr{N}}{\varphi}^{\flat}$.
Finally, by (5),
${\left({\mathrm{\Gamma}}^{\flat}\right)}^{\natural}\vdash_{\\!\\!\mathsf{NBI}}{\left({\varphi}^{\flat}\right)}^{\natural}$
— that is, $\mathrm{\Gamma}\vdash_{\\!\\!\mathsf{NBI}}\varphi$.

The proofs of the lemmas — that is, (5), (5), and (5) — are included in
Appendix 0.C.

##  6 Conclusion

This paper delivers a B-eS for BI. While BI may be regarded as the free
combination of IPL and IMLL, both of which have been given B-eS before (see
Sandqvist [43] and Gheorghiu et al. [13]), several technical challenges
remain. Foremost is that BI uses a more complex data-structure for contexts
than either of the other logics: bunches. Handling bunches with the
appropriate structural behaviour is the major challenge in giving a B-eS for
BI relative to the earlier work. These details are contained above.
Nevertheless, there is faithful embedding from IMLL and IPL into BI that is
reflected in the relationship between their B-eS and the one for BI in this
paper.

A reason for studying the B-eS of substructural logics in the systems-oriented
sciences is that it clearly and naturally supports the celebrated number-of-
uses reading of the implications. This reading is rarely, if at all, reflected
in the truth-functional semantics of these logics. In this paper, we
illustrate the use of the B-eS for BI by a toy example in the setting of
_access control_. This is a promising area for the use of B-eS as it is
dynamic in the sense that ‘access’ is about actions as opposed to states and
this dynamics corresponds to the passing of resources through implications on
the number-of-uses reading. Other ‘dynamic’ settings for which the B-eS of
substructural logics may be appropriate include modelling automata, modelling
Petri nets, simulation modelling, etc.. On the last, Kuorikoski and Reijula
[23] have recently shown P-tS (in general) to be a suitable paradigm of
meaning. Developing these applications remains future work.

## Acknowledgements

We are grateful to Yll Buzoku, Diana Costa, Sonia Marin, and Elaine Pimentel
for many useful discussions on the P-tS for substructural logics, to Eike
Ritter and Edmund Robinson for discussions on the category-theoretic
formulation of B-eS, and to Tim Button for discussion of P-tS’s philosophical
context.

## References

  * [1] Abadi, M.: Logic in Access Control. In: Logic in Computer Science — LICS. pp. 228–233. IEEE (2003)
  * [2] Allwein, G., Dunn, J.M.: Kripke Models for Linear Logic. The Journal of Symbolic Logic 58(2), 514–545 (1993)
  * [3] Anderson, G., Pym, D.J.: A Calculus and Logic of Bunched Resources and Processes. Theoretical Computer Science 614, 63–96 (2016). https://doi.org/https://doi.org/10.1016/j.tcs.2015.11.035
  * [4] Brandom, R.: Articulating Reasons: An Introduction to Inferentialism. Harvard University Press (2000)
  * [5] Brotherston, J.: Bunched Logics Displayed. Studio Logica 100(6), 1223–1254 (2012). https://doi.org/10.1007/s11225-012-9449-0
  * [6] Brünnler, K.: Deep Sequent Systems for Modal Logic. Archive for Mathematical Logic 48(6), 551–577 (Jul 2009). https://doi.org/10.1007/s00153-009-0137-3
  * [7] Coumans, D., Gehrke, M., van Rooijen, L.: Relational semantics for full linear logic. Journal of Applied Logic 12(1), 50–66 (2014). https://doi.org/10.1016/j.jal.2013.07.005
  * [8] van Dalen, D.: Logic and Structure. Universitext, Springer, 5 edn. (2013). https://doi.org/10.1007/978-1-4471-4558-5
  * [9] Docherty, S.: Bunched Logics: A Uniform Approach. Ph.D. thesis, University College London (2019)
  * [10] Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press (1991)
  * [11] Galmiche, D., Méry, D., Pym, D.: The Semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science 15(6), 1033–1088 (Dec 2005). https://doi.org/10.1017/S0960129505004858, https://doi.org/10.1017/S0960129505004858
  * [12] Gheorghiu, A.V., Docherty, S., Pym, D.J.: Reductive Logic, Coalgebra, and Proof-search: A Perspective from Resource Semantics. In: Palmigiano, A., Sadrzadeh, M. (eds.) Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Outstanding Contributions to Logic Series, Springer (2021). https://doi.org/10.1007/978-3-031-24117-8_23
  * [13] Gheorghiu, A.V., Gu, T., Pym, D.J.: Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (2023), accepted at TABLEAUX 2023
  * [14] Gheorghiu, A.V., Marin, S.: Focused Proof-search in the Logic of Bunched Implications. In: Kiefer, S., Tasson, C. (eds.) Foundations of Software Science and Computation Structures - FOSSACS 24. Lecture Notes in Computer Science, vol. 12650, pp. 247–267. Springer (2021). https://doi.org/10.1007/978-3-030-71995-1_13
  * [15] Gheorghiu, A.V., Pym, D.J.: Definite Formulae, Negation-as-Failure, and the Base-extension Semantics for Intuitionistic Propositional Logic. https://arxiv.org/abs/2210.05336 (2022), accepted — Bulletin of the Section of Logic
  * [16] Gheorghiu, A.V., Pym, D.J.: From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic. https://arxiv.org/pdf/2210.05344 (2022), submitted
  * [17] Gheorghiu, A.V., Pym, D.J.: Semantical Analysis of the Logic of Bunched Implications. Studia Logica (2023). https://doi.org/10.1007/s11225-022-10028-z
  * [18] Girard, J.Y.: Linear Logic: its Syntax and Semantics. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, p. 1–42. London Mathematical Society Lecture Note Series, Cambridge University Press (1995). https://doi.org/10.1017/CBO9780511629150.002
  * [19] Goldfarb, W.: On Dummett’s “Proof-theoretic Justifications of Logical Laws”. In: Advances in Proof-theoretic Semantics, pp. 195–210. Springer (2016). https://doi.org/10.1007/978-3-319-22686-6_13
  * [20] Hallnäs, L., Schroeder-Heister, P.: A Proof-theoretic Approach to Logic Programming: I. Clauses as Rules. Journal of Logic and Computation 1(2), 261–283 (1990). https://doi.org/10.1093/logcom/1.2.261
  * [21] Hallnäs, L., Schroeder-Heister, P.: A Proof-theoretic Approach to Logic Programming: II. Programs as Definitions. Journal of Logic and Computation 1(5), 635–660 (1991). https://doi.org/10.1093/logcom/1.5.635
  * [22] Ishtiaq, S.S., O’Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: Symposium on Principles of Programming Languages — POPL. pp. 14–26. Association for Computing Machinery (ACM) (2001). https://doi.org/10.1145/360204.375719
  * [23] Jaakko Kuorikoski, S.R.: Making It Count: An Inferentialist Account of Computer Simulation. https://osf.io/preprints/socarxiv/v9bmr (2022). https://doi.org/10.31235/osf.io/v9bmr, accessed January 2023
  * [24] Kripke, S.A.: Semantical Analysis of Intuitionistic Logic I. In: Studies in Logic and the Foundations of Mathematics, vol. 40, pp. 92–130. Elsevier (1965). https://doi.org/10.1016/S0049-237X(08)71685-9
  * [25] Lambek, J., Scott, P.J.: Introduction to Higher-order Categorical Logic, vol. 7. Cambridge University Press (1988), https://dl.acm.org/doi/10.5555/53626
  * [26] Makinson, D.: On an Inferential Semantics for Classical Logic. Logic Journal of IGPL 22(1), 147–154 (2014). https://doi.org/10.1093/jigpal/jzt038
  * [27] O’Hearn, P.W., Pym, D.J.: The Logic of Bunched Implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999). https://doi.org/10.2307/421090
  * [28] Piecha, T.: Completeness in Proof-theoretic Semantics. In: Advances in Proof-theoretic Semantics, pp. 231–251. Springer (2016). https://doi.org/10.1007/978-3-319-22686-6_15
  * [29] Piecha, T., de Campos Sanz, W., Schroeder-Heister, P.: Failure of Completeness in Proof-theoretic Semantics. Journal of Philosophical Logic 44(3), 321–335 (2015). https://doi.org/10.1007/s10992-014-9322-x
  * [30] Piecha, T., Schroeder-Heister, P.: Atomic Systems in Proof-Theoretic Semantics: Two Approaches. In: Ángel Nepomuceno Fernández, Martins, O.P., Redmond, J. (eds.) Epistemology, Knowledge and the Impact of Interaction. Springer Verlag (2016). https://doi.org/10.1007/978-3-319-26506-3_2
  * [31] Piecha, T., Schroeder-Heister, P.: The Definitional View of Atomic Systems in Proof-theoretic Semantics. In: The Logica Yearbook 2016, pp. 185–200. College Publications London (2017). https://doi.org/10.15496/publikation-70829
  * [32] Piecha, T., Schroeder-Heister, P.: Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-theoretic Semantics. Studia Logica 107(1), 233–246 (2019). https://doi.org/10.1007/s11225-018-9823-7
  * [33] Prawitz, D.: Ideas and Results in Proof Theory. In: Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 235–307. Elsevier (1971). https://doi.org/10.1016/S0049-237X(08)70849-8
  * [34] Prawitz, D.: Natural Deduction: A Proof-theoretical Study. Courier Dover Publications (2006 [1965]). https://doi.org/10.2307/2271676
  * [35] Pym, D.J.: Resource Semantics: Logic as a Modelling Technology. ACM SIGLOG News 6(2), 5–41 (2019). https://doi.org/10.1145/3326938.3326940
  * [36] Pym, D.J., Ritter, E., Robinson, E.: Proof-theoretic Semantics in Sheaves (Extended Abstract). In: Proceedings of the Eleventh Scandinavian Logic Symposium — SLSS 11 (2022)
  * [37] Pym, D.J., Spring, J.M., O’Hearn, P.: Why Separation Logic Works. Philosophy & Technology 32, 483–516 (2019). https://doi.org/10.1007/s13347-018-0312-8
  * [38] Read, S.: Relevant Logic. Basil Blackwell (1988). https://doi.org/10.2307/2219818
  * [39] Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Logic in Computer Science — LICS. pp. 55–74. Springer (2002). https://doi.org/10.1109/LICS.2002.1029817
  * [40] Sandqvist, T.: An Inferentialist Interpretation of Classical Logic. Ph.D. thesis, Uppsala University (2005)
  * [41] Sandqvist, T.: Classical Logic without Bivalence. Analysis 69(2), 211–218 (2009)
  * [42] Sandqvist, T.: Base-extension Semantics for Intuitionistic Sentential Logic. Logic Journal of the IGPL 23(5), 719–731 (2015). https://doi.org/10.1093/jigpal/jzv021
  * [43] Sandqvist, T.: Hypothesis-discharging Rules in Atomic Bases. In: Dag Prawitz on Proofs and Meaning, pp. 313–328. Springer (2015). https://doi.org/10.1007/978-3-319-11041-7_14
  * [44] Sandqvist, T.: Atomic Bases and the Validity of Peirce’s Law. https://sites.google.com/view/wdl-ucl2022/schedule#h.ttn75i73elfw (2022), World Logic Day — University College London (Accessed June 2023)
  * [45] Schroeder-Heister, P.: Validity Concepts in Proof-theoretic Semantics. Synthese 148(3), 525–571 (2006). https://doi.org/10.1007/s11229-004- 6296-1
  * [46] Schroeder-Heister, P.: Proof-Theoretic versus Model-Theoretic Consequence. In: Pelis, M. (ed.) The Logica Yearbook 2007. Filosofia (2008). https://doi.org/95b360ffe9ad174fd305539813800ea23fec33de
  * [47] Stafford, W., Nascimento, V.: Following All the Rules: Intuitionistic Completeness for Generalized Proof-Theoretic Validity. Analysis (forthcoming). https://doi.org/10.1093/analys/anac100
  * [48] Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland Publishing Company (1969). https://doi.org/10.2307/2272429
  * [49] Tarski, A.: O pojȩciu wynikania logicznego. Przegla̧d Filozoficzny 39 (1936)
  * [50] Tarski, A.: On the concept of following logically. History and Philosophy of Logic 23(3), 155–196 (2002). https://doi.org/10.1080/0144534021000036683
  * [51] Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press (2000). https://doi.org/10.1017/CBO9781139168717

##  Appendix 0.A Omitted Proofs from Section 3

See 2

###### Proof

It is easy to see that $\mathrm{\Gamma}\succeq\mathrm{\Gamma}^{\prime}$ iff
$\mathrm{\Gamma}\equiv\mathrm{\Gamma}^{\prime}\sigma_{1}...\sigma_{n}$, where
$\sigma_{i}$ is a substitution of the form
$[\mathrm{\Delta}\mapsto\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime}]$.
We proceed by induction on $\mathrm{holeDepth}{(\and{P}(\cdot))}$.

  * •

Base Case. $\mathrm{holeDepth}{(\and{P}(\cdot))}=0$. By Definition 8,
$\and{P}(\cdot)=(\cdot)$. Hence, the antecedent of the claim is identical to
the consequent.

  * •

Inductive Step. $\mathrm{holeDepth}{(\and{P}(\cdot))}=d+1$ for some $d>0$. By
Definition 8, $\and{P}(\cdot)=\and{P}^{\prime}(\cdot)\star\and{Q}$, where
$\mathrm{holeDepth}{(\and{P}^{\prime}(\cdot))}=d$,
$\and{Q}\in\mathbb{B}(\mathbb{A})$, and
$\star\in\\{\mathrel{\fatsemi},\mathrel{\fatcomma}\\}$. By the induction
hypothesis (IH), $\and{P}^{\prime}(\and{T})\preceq\and{P}^{\prime}(\and{S})$.
Let $\tau_{1},...,\tau_{k}$ witness the extension. Since
$\and{P}(\and{S})\equiv\and{P}^{\prime}(\and{S})\star\and{Q}\equiv\and{P}^{\prime}(\and{T})\tau_{1}...\tau_{k}\star\and{Q}\equiv(\and{P}^{\prime}(\and{T})\star\and{Q})\tau_{1}....\tau_{k}\equiv\and{P}(\and{T})\tau_{1}...\tau_{k}$,
we have $\and{P(\and{S})}\succeq\and{P(\and{T})}$.

This completes the induction.

Lemma 2 (Monotonicity) is the combination of Proposition 1, Lemma 9 and Lemma
10:

See 1

###### Proof

Follows by induction on the derivation of
$\and{T}\vdash_{\\!\\!\mathscr{B}}\and{p}$ since all the rules of
$\mathscr{B}$ are contained in $\mathscr{C}$.

###### Lemma 9

If $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\varphi$ and
$\mathscr{C}\supseteq\mathscr{B}$, then
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\varphi$.

###### Proof

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

  * -

Base Case. This follows from Proposition 1.

  * -

Inductive Step. If there is no base-extension in the relevant clause for
$\varphi$, then the result follows from applying the induction hypothesis (IH)
to the judgements in the definiens. For example, consider the case where
$\varphi$ is $\bot$: by ($\bot$ ‣ 4), from
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\varphi$ infer that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\and{p}$ for every
$\and{p\in\mathbb{A}}$; hence, by the IH,
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\and{p}$ for every
$\and{p\in\mathbb{A}}$; whence, by ($\bot$ ‣ 4),
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\bot$, as required.

If base-extension is used in the relevant clause for $\varphi$, the result
holds immediately since $\mathscr{X}\supseteq\mathscr{C}$ implies
$\mathscr{X}\supseteq\mathscr{B}$. For example, consider the case where
$\varphi$ is $\psi_{1}\mathrel{\ast}\psi_{2}$. By ($\mathrel{\ast}$ ‣ 4),

$\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{F}),\forall\and{p}\in\mathbb{A},\text{
if
}\psi_{1}\\!\mathrel{\fatcomma}\\!\psi_{2}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p},\text{
then }\Vdash_{\\!\\!\mathscr{X}}^{\and{U(T)}}\and{p}$

Hence, since $\mathscr{C}\supseteq\mathscr{B}$,

$\forall\mathscr{X}\supseteq\mathscr{C},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{F}),\forall\and{p}\in\mathbb{A},\text{
if
}\psi_{1}\\!\mathrel{\fatcomma}\\!\psi_{2}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p},\text{
then }\Vdash_{\\!\\!\mathscr{X}}^{\and{U(T)}}\and{p}$

By ($\mathrel{\ast}$ ‣ 4),
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\psi_{1}\mathrel{\ast}\psi_{2}$, as
required.

This completes the induction.

###### Lemma 10

If $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\varphi$ and $\and{S}\succeq\and{T}$,
then $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$.

###### Proof

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

  * •

$\varphi=\and{p}\in\mathbb{A}$. By (At),
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\and{p}$ iff
$\and{T}\vdash_{\\!\\!\mathscr{B}}\and{p}$. By, weak in Definition 12, since
$\and{S}\succeq\and{T}$, it follows that $\and{S}\vdash_{\\!\\!\mathscr{B}}p$.

  * •

$\varphi=\varphi_{1}\land\varphi_{2}$. By ($\land$ ‣ 4) it suffices to show
the following:

$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{F})$,
$\forall\and{p}\in\mathbb{A}$, if
$\varphi_{1}\\!\mathrel{\fatsemi}\\!\varphi_{2}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p}$,
then $\Vdash_{\\!\\!\mathscr{X}}^{\and{U(S)}}\and{p}$

Therefore, let $\mathscr{C}\supseteq\mathscr{B}$, $\and{P}(\cdot)$, and
$\and{q}$ be arbitrary such that
$\varphi_{1}\\!\mathrel{\fatsemi}\\!\varphi_{2}\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\cdot)}\and{q}$.
We require to show that $\Vdash_{\\!\\!\mathscr{C}}^{\and{P(S)}}\and{q}$.

By ($\land$ ‣ 4), from the assumption
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\varphi_{1}\land\varphi_{2}$, infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(T)}}\and{q}$. By Proposition 2, from
$\and{S}\succeq\and{T}$, infer $\and{P(S)}\succeq\and{P(T)}$. By the induction
hypothesis (IH), from $\Vdash_{\\!\\!\mathscr{C}}^{\and{P(T)}}\and{q}$ and
$\and{P(S)}\succeq\and{P(T)}$, infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(S)}}\and{q}$.

  * •

$\varphi=\top$. By ($\top$ ‣ 4) it suffices to show the following:

$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{F})$,
$\forall\and{p}\in\mathbb{A}$, if
$\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\varnothing_{\\!+})}\and{p}$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\and{U(T)}}\and{p}$

Therefore, let $\mathscr{C}\supseteq\mathscr{B}$, $\and{P}(\cdot)$, and
$\and{q}$ be arbitrary such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\varnothing_{\\!+})}\and{q}$. We require
to show $\Vdash_{\\!\\!\mathscr{C}}^{\and{P(S)}}\and{q}$ holds.

By ($\top$ ‣ 4), from the assumption,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\top$, infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(T)}}\and{q}$. By Proposition 2, from
$\and{S}\succeq\and{T}$, infer $\and{P(S)}\succeq\and{P(T)}$. By the IH, from
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(T)}}\and{q}$ and
$\and{P(S)}\succeq\and{P(T)}$, infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(S)}}\and{q}$.

  * •

$\varphi=\varphi_{1}\to\varphi_{2}$. By ($\to$ ‣ 4) it suffices to show
$\varphi_{1}\Vdash_{\\!\\!\mathscr{B}}^{\and{S}\mathrel{\fatsemi}(\cdot)}\varphi_{2}$.
By (Inf), this is equivalent to the following:

$\forall\mathscr{X}\supseteq\mathscr{B}$,
$\forall\and{U}\in\mathbb{B}(\mathbb{F})$, if
$\Vdash_{\\!\\!\mathscr{X}}^{\and{U}}\varphi_{1}$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\and{S}\mathrel{\fatsemi}\and{U}}\varphi_{2}$.

Therefore, let $\mathscr{C}\supseteq\mathscr{B}$, $\and{P}$ be arbitrary such
that $\Vdash_{\\!\\!\mathscr{C}}^{\and{P}}\varphi_{1}$. We require to show
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatsemi}\and{P}}\varphi_{2}$.

By ($\to$ ‣ 4) and $\eqref{cl:BI-BeS-supp:inf}$, from the assumption
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\varphi_{1}\to\varphi_{2}$, infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}\mathrel{\fatsemi}\and{P}}\varphi_{2}$. By
Proposition 2, from $\and{S}\succeq\and{T}$, infer
$\and{S}\mathrel{\fatsemi}\and{P}\succeq\and{T}\mathrel{\fatsemi}\and{P}$. By
the IH, from
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}\mathrel{\fatsemi}\and{P}}\varphi_{2}$ and
$\and{S}\mathrel{\fatsemi}\and{P}\succeq\and{T}\mathrel{\fatsemi}\and{P}$,
infer
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatsemi}\and{P}}\varphi_{2}$.

  * •

$\varphi=\varphi_{1}\mathrel{\ast}\varphi_{2}$. _Mutatis mutandis_ on the
$\land$-case.

  * •

$\varphi=\top^{\ast}$. _Mutatis mutandis_ on the $\top$-case.

  * •

$\varphi=\varphi_{1}\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\varphi_{2}$._Mutatis
mutandis_ on the $\to$-case.

  * •

$\varphi=\varphi_{1}\lor\varphi_{2}$. _Mutatis mutandis_ on the $\land$-case.

  * •

$\varphi=\bot$. By ($\bot$ ‣ 4) on the assumption
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\bot$, infer
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\and{p}$ holds for all
$\and{p}\in\mathbb{A}$. By the IH,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\and{p}$ for all $\and{p}\in\mathbb{A}$.
Hence, by ($\bot$ ‣ 4), $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\bot$.

This completes the induction.

That Lemma 2 may be generalized to bunches is witnessed by the following
generalizations of the above lemmas:

###### Lemma 11

If $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\mathrm{\Gamma}$ and
$\mathscr{C}\supseteq\mathscr{B}$, then
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\mathrm{\Gamma}$.

###### Proof

We proceed by induction on the structure of $\mathrm{\Gamma}$.

  * •

$\mathrm{\Gamma}=\varphi\in\mathbb{F}$. This is Lemma 9.

  * •

$\mathrm{\Gamma}=\varnothing_{\\!+}$. This follows immediately by
($\varnothing_{\\!+}$ ‣ 4).

  * •

$\mathrm{\Gamma}=\varnothing_{\\!\times}$. By ($\varnothing_{\\!\times}$ ‣ 4),
$\and{T}\succeq\varnothing_{\\!\times}$. Hence, by ($\varnothing_{\\!\times}$
‣ 4), $\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\varnothing_{\\!\times}$.

  * •

$\mathrm{\Gamma}=\mathrm{\Gamma}_{1}\\!\mathrel{\fatsemi}\\!\mathrm{\Gamma}_{2}$.
By (() ‣ 4), there are $\and{Q}_{1}$ and $\and{Q}_{2}$ such that
$\and{T}\succeq\and{Q}_{1}$, $\and{T}\succeq\and{Q}_{1}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Gamma}_{1}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Gamma}_{2}$. By the
induction hypothesis (IH),
$\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}_{1}}\mathrm{\Gamma}_{1}$ and
$\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}_{2}}\mathrm{\Gamma}_{2}$. Whence, by (()
‣ 4),
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\mathrm{\Gamma}_{1}\\!\mathrel{\fatsemi}\\!\mathrm{\Gamma}_{2}$.

  * •

$\mathrm{\Gamma}=\mathrm{\Gamma}_{1}\\!\mathrel{\fatcomma}\\!\mathrm{\Gamma}_{2}$.
By (() ‣ 4), there are $\and{Q}_{1}$ and $\and{Q}_{2}$ such that
$\and{T}\succeq(\and{Q}_{1}\\!\mathrel{\fatcomma}\\!\and{Q}_{2})$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Gamma}_{1}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Gamma}_{2}$. By the IH,
$\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}_{1}}\mathrm{\Gamma}_{1}$ and
$\Vdash_{\\!\\!\mathscr{C}}^{\and{Q}_{2}}\mathrm{\Gamma}_{2}$. Whence, by (()
‣ 4),
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\mathrm{\Gamma}_{1}\\!\mathrel{\fatcomma}\\!\mathrm{\Gamma}_{2}$.

This completes the induction.

###### Lemma 12

If $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}}\mathrm{\Gamma}$ and
$\and{S}\succeq\and{T}$, then
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$.

###### Proof

We proceed by case-analysis on the structure of $\mathrm{\Gamma}$.

  * •

$\mathrm{\Gamma}=\varphi\in\mathbb{F}$. This is Lemma 10.

  * •

$\mathrm{\Gamma}=\varnothing_{\\!+}$. This follows immediately by
($\varnothing_{\\!+}$ ‣ 4).

  * •

$\mathrm{\Gamma}=\varnothing_{\\!\times}$. By ($\varnothing_{\\!\times}$ ‣ 4),
$\and{T}\succeq\varnothing_{\\!\times}$. Hence,
$\and{S}\succeq\varnothing_{\\!\times}$. Whence, ($\varnothing_{\\!\times}$ ‣
4), $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!\times}$.

  * •

$\mathrm{\Gamma}=\mathrm{\Gamma}_{1}\\!\mathrel{\fatsemi}\\!\mathrm{\Gamma}_{2}$.
By (() ‣ 4), there are $\and{Q}_{1}$ and $\and{Q}_{2}$ such that
$\and{T}\succeq\and{Q}_{1}$, $\and{T}\succeq\and{Q}_{1}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Gamma}_{1}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Gamma}_{2}$. From
$\and{S}\succeq\and{T}$, infer $\and{S}\succeq\and{Q}_{1}$ and
$\and{S}\succeq\and{Q}_{2}$. Hence, by (() ‣ 4),
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}_{1}\\!\mathrel{\fatsemi}\\!\mathrm{\Gamma}_{2}$.

  * •

$\mathrm{\Gamma}=\mathrm{\Gamma}_{1}\\!\mathrel{\fatcomma}\\!\mathrm{\Gamma}_{2}$.
By (() ‣ 4), there are $\and{Q}_{1}$ and $\and{Q}_{2}$ such that
$\and{T}\succeq(\and{Q}_{1}\\!\mathrel{\fatcomma}\\!\and{Q}_{2})$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Gamma}_{1}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Gamma}_{2}$. From
$\and{S}\succeq\and{T}$, infer
$\and{S}\succeq(\and{Q}_{1}\\!\mathrel{\fatcomma}\\!\and{Q}_{2})$. Hence, by
(() ‣ 4),
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}_{1}\\!\mathrel{\fatcomma}\\!\mathrm{\Gamma}_{2}$.

This completes the induction.

###### Lemma 13

$\mathrm{\Gamma}\Vdash\varphi$ iff
$\mathrm{\Gamma}\Vdash_{\\!\\!\varnothing}^{(\cdot)}\varphi$

###### Proof

The ‘if’ direction is follows from Lemma 2. The ‘only if’ direction is
immediate by Definition 15.

See 3

###### Proof

We proceed by induction on the structure of $\and{P}$.

  * -

$\and{P}$ is in $\mathbb{A}$. That is, $\and{P}$ is some atom $\and{p}$. By
(At), this is equivalent to $\and{p}\vdash_{\\!\\!\mathscr{B}}\and{p}$, which
obtains by taut in Definition 12.

  * -

$\and{P}$ is $\varnothing_{\\!+}$. This is immediate by ($\varnothing_{\\!+}$
‣ 4).

  * -

$\and{P}$ is $\varnothing_{\\!\times}$. This is immediate by
($\varnothing_{\\!\times}$ ‣ 4) as
$\varnothing_{\\!\times}\succeq\varnothing_{\\!\times}$.

  * -

$\and{P}$ is $\and{P}_{1}\\!\mathrel{\fatsemi}\\!\and{P}_{2}$. By the
induction hypothesis (IH), both $\Vdash_{\\!\\!\and{P}_{1}}^{\and{P}_{1}}$ and
$\Vdash_{\\!\\!\and{P}_{2}}^{\and{P}_{2}}$ obtain. Since
$\and{P}_{1}\\!\mathrel{\fatsemi}\\!\and{P}_{2}\succeq\and{P}_{1}$ and
$\and{P}_{1}\\!\mathrel{\fatsemi}\\!\and{P}_{2}\succeq\and{P}_{2}$, the result
follows by (() ‣ 4).

  * -

$\and{P}$ is $\and{P}_{1}\\!\mathrel{\fatcomma}\\!\and{P}_{2}$. By the IH,
both $\Vdash_{\\!\\!\and{P}_{1}}^{\and{P}_{1}}$ and
$\Vdash_{\\!\\!\and{P}_{2}}^{\and{P}_{2}}$ obtain. Since
$\and{P}_{1}\\!\mathrel{\fatcomma}\\!\and{P}_{2}\succeq\and{P}_{1}\\!\mathrel{\fatcomma}\\!\and{P}_{2}$,
the result follows by (() ‣ 4).

This completes the induction.

See 4

###### Proof

Since
$\and{P}(\and{S})\preceq\and{P}(\and{S}\\!\mathrel{\fatsemi}\\!\and{S}^{\prime})$,
claim 4 follows from Lemma 2. It remains to show claim 4. We proceed by
induction on $\varphi$.

  * •

Base Case. This follows immediately by cont in Definition 12.

  * •

Inductive Step. We demonstrate the case for
$\varphi=\varphi_{1}\lor\varphi_{2}$ and $\varphi=\varphi_{1}\to\varphi_{2}$,
the others being similar.

    * –

Assume
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}(\and{S}\mathrel{\fatsemi}\and{S})}\varphi_{1}\lor\varphi_{2}$.
By ($\lor$ ‣ 4), the consequent of 4 is equivalent to the following:

$\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{if
}\varphi_{1}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p}\text{ and
}\varphi_{2}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p},\text{
then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U(P(S))}}\and{p}$

Let $\and{V}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$ and
$\mathscr{C}\supseteq\mathscr{B}$ and $\and{q}\in\mathbb{A}$ be arbitrary such
that $\varphi_{1}\Vdash_{\\!\\!\mathscr{C}}^{\and{V}(\cdot)}\and{q}$ and
$\varphi_{2}\Vdash_{\\!\\!\mathscr{C}}^{\and{V}(\cdot)}\and{q}$. We require to
show $\Vdash_{\\!\\!\mathscr{C}}^{\and{V(P(S))}}\and{q}$. By ($\lor$ ‣ 4) on
the assumption, we have
$\Vdash_{\\!\\!\mathscr{C}}^{\and{V(P(S\mathrel{\fatsemi}S))}}\and{q}$. The
result follows immediately by cont in Definition 12.

    * –

Assume
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}(\and{S}\mathrel{\fatsemi}\and{S})}\varphi_{1}\to\varphi_{2}$.
By ($\to$ ‣ 4) and (Inf), the consequent of 4 is equivalent to the following:

$\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},$
if $\Vdash_{\\!\\!\mathscr{X}}^{\and{U}}\varphi$, then
$\Vdash_{\\!\\!\mathscr{X}}^{\and{P(S)}\mathrel{\fatsemi}\and{U}}\psi$

Let $\and{V}\in\dot{\mathbb{B}}(\mathbb{A})$ and
$\mathscr{C}\supseteq\mathscr{B}$ be arbitrary such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{V}}\varphi_{1}$. We require to show
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(S)}\mathrel{\fatsemi}\and{V}}\varphi_{2}$.
By ($\to$ ‣ 4) on the assumption, we have
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P(S\mathrel{\fatsemi}S)}\mathrel{\fatsemi}\and{V}}\varphi_{2}$.
The result follows from the induction hypothesis (IH).

This completes the case analysis. Observe that in the $\lor$-case we did not
require the IH.

This completes the induction.

See 5

###### Proof

We prove claim 5, the other being similar. We proceed by induction on
$\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}$ — if
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$,
then $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$.

  * •

Base Case. $\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}=0$. By Definition 8,
$\mathrm{\Gamma}(\cdot)=(\cdot)$, so the statement becomes: if
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime}$,
then $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Delta}$. By (() ‣ 4), from
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime}$,
infer $\exists\and{Q}_{1},\and{Q}_{2}\in\mathbb{B}(\mathbb{A})$ such that
$\and{S}\succeq\and{Q}_{1}$, $\and{S}\succeq\and{Q}_{2}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Delta}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Delta}^{\prime}$. Hence, by
monotonicity (Lemma 2), infer
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Delta}$ — that is,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$.

  * •

Inductive Step. Suppose $\mathrm{holeDepth}{(\mathrm{\Gamma}(\cdot))}=d+1$ for
some $d\in\mathbb{N}$. Therefore (by Definition 8),
$\mathrm{\Gamma}(\mathrm{\Delta})\equiv\mathrm{\Sigma}(\mathrm{\Delta})\star\mathrm{\Theta}$,
where $\mathrm{holeDepth}{(\mathrm{\Sigma}(\cdot))}=d$, and $\star$ is either
or . We consider the two cases of $\star$ separately:

    * –

$\star=\,\,\mathrel{\fatsemi}$. By (() ‣ 4), from
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Sigma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})\\!\mathrel{\fatsemi}\\!\mathrm{\Theta}$,
infer $\exists\and{Q}_{1},\and{Q}_{1}\in\mathbb{B}(\mathbb{A})$ such that
$\and{S}\succeq\and{Q}_{1}$, $\and{S}\succeq\and{Q}_{2}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Sigma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$,
and $\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Theta}$. By the
induction hypothesis (IH),
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Sigma}(\mathrm{\Delta})$.
Hence, by (() ‣ 4), infer
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Sigma}(\mathrm{\Delta})\\!\mathrel{\fatsemi}\\!\mathrm{\Theta}$
— that is,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$.

    * –

$\star=\,\,\mathrel{\fatcomma}$. By (() ‣ 4), from
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Sigma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})\\!\mathrel{\fatcomma}\\!\mathrm{\Theta}$,
infer $\exists\and{Q}_{1},\and{Q}_{2}\in\mathbb{B}(\mathbb{A})$ such that
$\and{S}\succeq(\and{Q}_{1}\\!\mathrel{\fatcomma}\\!\and{Q}_{2})$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Sigma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$,
and $\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Theta}$. By the IH, from
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{1}}\mathrm{\Sigma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$,
infer
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}_{2}}\mathrm{\Sigma}(\mathrm{\Delta})$.
Hence, by (() ‣ 4), infer
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Sigma}(\mathrm{\Delta})\\!\mathrel{\fatcomma}\\!\mathrm{\Theta}$
— that is,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$.

This completes the case analysis.

This completes the induction.

See 6

###### Proof

It suffices to fix some $\mathscr{C}\supseteq\mathscr{B}$ and
$\and{P}\in\mathbb{B}(\mathbb{A})$ such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}}\varphi$, and prove
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}(\and{S}(\and{P}))}\chi$.
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}}\varphi$ and
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{S}(\cdot)}\psi$ imply
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}(\and{P})}\psi$; together with
$\psi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\cdot)}\chi$, it follows that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}(\and{S}(\and{P}))}\chi$.

It is obvious that the very same line of proof works for the supporting
relation between bunches, namely:
$\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}^{\and{S}(\cdot)}\mathrm{\Delta}$
and
$\mathrm{\Delta}\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\cdot)}\mathrm{\Sigma}$
imply
$\mathrm{\Gamma}\Vdash_{\\!\\!\mathscr{B}}^{\and{T}(\and{S}(\cdot))}\mathrm{\Sigma}$.

##  Appendix 0.B Proof of Soundness

We present the proof for soundness first, and leave the lemmas (and their
proofs) used in this proof till afterwards. See 4.1

###### Proof

Given the inductive definition of $\vdash_{\\!\\!\mathsf{NBI}}$ (see Figure
3), it suffices to prove the following statements:

Ax

$\varphi\Vdash_{\\!\\!}\varphi$.

E

If $\mathrm{\Gamma}^{\prime}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Gamma}\equiv\mathrm{\Gamma}^{\prime}$, then
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$.

W

If $\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$, then
$\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})\Vdash_{\\!\\!}\varphi$.

C

If
$\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$,
then $\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$

$\top^{\ast}$I

$\varnothing_{\\!\times}\Vdash_{\\!\\!}\top^{\ast}$.

$\top^{\ast}$E

If $\mathrm{\Gamma}(\varnothing_{\\!\times})\Vdash_{\\!\\!}\chi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\top^{\ast}$, then
$\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\chi$.

$\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$I

If $\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi\Vdash_{\\!\\!}\psi$, then
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$.

$\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$E

If
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$
and $\mathrm{\Delta}\Vdash_{\\!\\!}\varphi$, then
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\psi$.

$\mathrel{\ast}$I

If $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$, then
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\mathrel{\ast}\psi$.

$\mathrel{\ast}$E

If $\mathrm{\Gamma}(\varphi\\!\mathrel{\fatcomma}\\!\psi)\Vdash_{\\!\\!}\chi$
and $\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\mathrel{\ast}\psi$, then
$\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\chi$.

$\top$I

$\varnothing_{\\!+}\Vdash_{\\!\\!}\top$.

$\top$E

If $\mathrm{\Gamma}(\varnothing_{\\!+})\Vdash_{\\!\\!}\chi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\top$, then
$\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\chi$.

$\to$I

If $\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\varphi\Vdash_{\\!\\!}\psi$ then
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\to\psi$.

$\to$E

If $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\to\psi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\varphi$, then
$\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\psi$.

$\land$I

If $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$, then
$\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\land\psi$.

$\land$E

If $\mathrm{\Gamma}(\varphi\\!\mathrel{\fatsemi}\\!\psi)\Vdash_{\\!\\!}\chi$
and $\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\land\psi$, then
$\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\chi$.

$\lor$I

If $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi_{i}$, then
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi_{1}\lor\varphi_{2}$, for $i=1,2$.

$\lor$E

If $\mathrm{\Gamma}(\varphi)\Vdash_{\\!\\!}\chi$,
$\mathrm{\Gamma}(\psi)\Vdash_{\\!\\!}\chi$, and
$\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\lor\psi$, then
$\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\chi$.

$\bot$E

If $\mathrm{\Gamma}\Vdash_{\\!\\!}\bot$, then
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$.

Now we verify each of them. Note that some cases require subinduction, which
we move to separate lemmas listed after the current proof.

  1. Ax

This holds _a fortiori_ : according to (Inf) and Definition 14,
$\varphi\Vdash_{\\!\\!}\varphi$ says that for arbitrary base $\mathscr{X}$ and
$\and{S}\in\mathbb{B}(\mathbb{A})$, if
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$, then
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$.

  2. E.

It suffices to show that whenever
$\mathrm{\Gamma}\equiv\mathrm{\Gamma}^{\prime}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$ iff
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}^{\prime}$. Note that
$\equiv$ is the reflexive transitive closure obtained by applying
associativity and unitality laws, so it suffices to show that the supporting
relation is invariant under application of associativity and unitality.
Associativity is obvious, and we only check unitality. In particular, we
verify the multiplicative case, namely
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varnothing_{\\!\times}$
iff $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$. By definition,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varnothing_{\\!\times}$
iff there exist $\and{Q}$ and $\and{R}$ satisfying
$\and{S}\succeq\and{Q}\\!\mathrel{\fatcomma}\\!\and{R}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\mathrm{\Gamma}$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{R}}\varnothing_{\\!\times}$. This means
$\and{R}\succeq\varnothing_{\\!\times}$, thus
$\and{S}\succeq\and{Q}\\!\mathrel{\fatcomma}\\!\and{R}\succeq\and{Q}\\!\mathrel{\fatcomma}\\!\varnothing_{\\!\times}\equiv\and{Q}$.
Therefore
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varnothing_{\\!\times}$
iff there exists $\and{Q}\preceq\and{S}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$, namely
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$.

  3. W.

We assume that $\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$, and
show that
$\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})\Vdash_{\\!\\!}\varphi$
holds for an arbitrary $\mathrm{\Delta}^{\prime}\in\mathbb{B}(\mathbb{F})$. So
let us fix some $\mathscr{B}$ and $\and{S}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$,
and show that $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$. According to
Lemma 5,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}^{\prime})$
implies
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$. This
together with $\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$
conclude that $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$.

  4. C.

We assume
$\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$,
and show that $\mathrm{\Gamma}(\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$. So we
fix some $\mathscr{B}$ and $\and{S}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$, and
show that $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$. By Lemma 5,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta})$ implies
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta})$.
This together with
$\mathrm{\Gamma}(\mathrm{\Delta}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta})\Vdash_{\\!\\!}\varphi$
implies $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi$.

  5. $\top^{\ast}$I.

It suffices to fix some $\mathscr{B}$ and $\and{S}$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!\times}$, and then show
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\top^{\ast}$. By Definition 14,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!\times}$ if and only if
$\and{S}\succeq\varnothing_{\\!\times}$; in other words,
$\and{S}\equiv\varnothing_{\\!\times}\\!\mathrel{\fatsemi}\\!\and{T}$ for some
$\and{T}\in\mathbb{B}(\mathbb{A})$. To show
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\top^{\ast}$, we fix some
$\mathscr{C}\supseteq\mathscr{B}$,
$\and{P}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{q}\in\mathbb{A}$,
such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\varnothing_{\\!\times})}\and{q}$, and
show that $\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\and{S})}\and{q}$. Since
$\and{S}\equiv\varnothing_{\\!\times}\\!\mathrel{\fatsemi}\\!\and{T}$, it
follows that $\and{S}\succeq\varnothing_{\\!\times}$, so
$\and{P}(\and{S})\succeq\and{P}(\varnothing_{\\!\times})$ (Proposition 2). By
monotonicity (Lemma 2),
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\varnothing_{\\!\times})}\and{q}$ then
implies $\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\and{S})}\and{q}$.

  6. $\top^{\ast}$E.

This follows as a special case of Lemma 14.1. In particular, one takes there
$\and{R}(\cdot)$ to be $(\cdot)$, and $\mathscr{B}$ to be the empty base
$\varnothing$.

  7. $\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$I.

We assume
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi\Vdash_{\\!\\!}\psi$, and show
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$.
Towards this, we further assume some $\mathscr{B}$ and $\and{S}$ satisfying
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$, and show
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$.
By ($\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$ ‣ 4), this amounts to showing
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{S}\mathrel{\fatcomma}(\cdot)}\psi$.
So we in addition fix some arbitrary base $\mathscr{C}\supseteq\mathscr{B}$
and atomic bunch $\and{T}$ such that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\varphi$, and then verify that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatcomma}\and{T}}\psi$. Since
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$ and
$\mathscr{C}\supseteq\mathscr{B}$, we have
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}}\mathrm{\Gamma}$; so
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatcomma}\and{T}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi$.
Together with
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi\Vdash_{\\!\\!}\psi$, it
follows that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatcomma}\and{T}}\psi$.

  8. $\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}$E.

We assume
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$
and $\mathrm{\Delta}\Vdash_{\\!\\!}\varphi$, and prove
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\psi$.
For this, we fix some arbitrary $\mathscr{B}$ and atomic bunch $\and{S}$ such
that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$,
and show $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\psi$. By definition,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$
means that there exist $\and{T}_{1},\and{T}_{2}\in\mathbb{B}(\mathbb{A})$ such
that $\and{T}_{1}\\!\mathrel{\fatcomma}\\!\and{T}_{2}\preceq\and{S}$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\mathrm{\Gamma}$, and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\mathrm{\Delta}$. Now
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$
and $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\mathrm{\Gamma}$ imply that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\varphi\mathrel{-\mkern-12.0mu-\mkern-12.0mu\ast}\psi$;
that is,
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}\mathrel{\fatcomma}(\cdot)}\psi$.
$\mathrm{\Delta}\Vdash_{\\!\\!}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\mathrm{\Delta}$ imply
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\varphi$. Then
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}\mathrel{\fatcomma}(\cdot)}\psi$
together with $\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\varphi$ imply
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}\mathrel{\fatcomma}\and{T}_{2}}\psi$,
thus $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\psi$ by Lemma 2.

  9. $\mathrel{\ast}$I.

Suppose $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$, we prove that
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\mathrel{\ast}\psi$.
So we fix arbitrary base $\mathscr{B}$ and $\and{S}\in\mathbb{B}(\mathbb{A})$
such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\mathrm{\Delta}$,
and show that $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{\ast}\psi$.
By ($\mathrel{\ast}$ ‣ 4), there exist
$\and{T}_{1},\and{T}_{2}\in\mathbb{B}(\mathbb{A})$ satisfying
$(\and{T}_{1}\\!\mathrel{\fatcomma}\\!\and{T}_{2})\preceq\and{S}$, such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\mathrm{\Gamma}$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\mathrm{\Delta}$. The goal
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{\ast}\psi$ means that for
arbitrary $\mathscr{X}\supseteq\mathscr{B}$,
$\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{p}\in\mathbb{A}$,
if
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{U}(\cdot)}\and{p}$,
then $\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\and{S})}\and{p}$. So we fix some
$\mathscr{C}\supseteq\mathscr{B}$,
$\and{P}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{q}\in\mathbb{A}$
such that
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\cdot)}\and{q}$,
and show that $\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\and{S})}\and{q}$. Since
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\varphi$, it follows that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}}\varphi$; since
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\mathrm{\Delta}$, it follows that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{2}}\psi$. So
$\Vdash_{\\!\\!\mathscr{B}}^{\and{T}_{1}\mathrel{\fatcomma}\and{T}_{2}}\varphi\\!\mathrel{\fatcomma}\\!\psi$;
together with $\and{T}_{1}\\!\mathrel{\fatcomma}\\!\and{T}_{2}\preceq\and{S}$,
it follows that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\mathrel{\ast}\psi$ by Lemma 2.
Together with
$\varphi\\!\mathrel{\fatcomma}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\cdot)}\and{q}$
and $\mathscr{C}\supseteq\mathscr{B}$, we conclude that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}}\and{q}$.

  10. $\mathrel{\ast}$E.

This follows as a special case of Lemma 14.2, where one takes $\mathscr{B}$
and $R(\cdot)$ to be the empty base $\varnothing$ and the empty context
$(\cdot)$, respectively.

  11. $\top$I.

It suffices to fix some base $\mathscr{B}$ and
$\and{S}\in\mathbb{B}(\mathbb{A})$ satisfying
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!+}$, and the goal is to
show $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\top$. To this end, we further fix
some arbitrary $\mathscr{C}\supseteq\mathscr{B}$ and
$\and{P}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$ satisfying
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\varnothing_{\\!+})}\and{q}$, and prove
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\and{S})}\and{q}$. Since
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varnothing_{\\!+}$ says
$\and{S}\succeq\varnothing_{\\!+}$, by Lemma 2,
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\varnothing_{\\!+})}\and{q}$ implies
$\Vdash_{\\!\\!\mathscr{C}}^{\and{P}(\and{S})}\and{q}$.

  12. $\top^{\ast}$E.

This follows immediately from Lemma 14.3.

  13. $\to$I.

Fix some base $\mathscr{B}$ and $\and{S}\in\mathbb{B}(\mathbb{A})$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$, and the goal is to
prove $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\to\psi$. By ($\to$ ‣ 4),
this amounts to showing
$\varphi\Vdash_{\\!\\!\mathscr{B}}^{\and{S}\mathrel{\fatsemi}(\cdot)}\psi$. So
we further fix some $\mathscr{C}\supseteq\mathscr{B}$ and
$\and{T}\in\mathbb{B}(\mathbb{A})$ satisfying
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\varphi$, and prove
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatsemi}\and{T}}\psi$. By (() ‣
4), $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$ and
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}}\varphi$ imply
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatcomma}\and{T}}\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi$.
Together with
$\mathrm{\Gamma}\\!\mathrel{\fatcomma}\\!\varphi\Vdash_{\\!\\!}\psi$, it
follows that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{S}\mathrel{\fatcomma}\and{T}}\psi$.

  14. $\to$E.

Given the assumptions, we assume some arbitrary base $\mathscr{B}$ and
$\and{S}\in\mathbb{B}(\mathbb{A})$ such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}$,
and prove that $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\psi$. By (() ‣ 4), there
exist $\and{P},\and{Q}\in\mathbb{B}(\mathbb{A})$ satisfying
$\and{P}\preceq\and{S}$ and $\and{Q}\preceq\and{S}$, such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\mathrm{\Gamma}$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\mathrm{\Delta}$.
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi\to\psi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\mathrm{\Gamma}$ imply
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\varphi\to\psi$, namely
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}\mathrel{\fatsemi}(\cdot)}\psi$.
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\mathrm{\Delta}$ imply
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\psi$. Then, by (Inf), it follows that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}\mathrel{\fatsemi}\and{Q}}\psi$. Since
$\and{S}\succeq\and{P}\mathrel{\fatsemi}\and{Q}$, it follows that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\psi$, by Lemma 2.

  15. $\land$I.

Suppose $\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$, and we show that
$\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}\Vdash_{\\!\\!}\varphi\land\psi$.
So, we fix some arbitrary $\mathscr{B}$ and $\and{S}$ satisfying that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}$,
and show $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\land\psi$. Applied to
(() ‣ 4),
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}\\!\mathrel{\fatsemi}\\!\mathrm{\Delta}$,
there exist $\and{P},\and{Q}\in\mathbb{B}(\mathbb{A})$ satisfying
$\and{P}\preceq\and{S}$ and $\and{Q}\preceq\and{S}$, such that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\mathrm{\Gamma}$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\mathrm{\Delta}$.
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\mathrm{\Gamma}$ imply
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\varphi$.
$\mathrm{\Delta}\Vdash_{\\!\\!}\psi$ and
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\mathrm{\Delta}$ imply
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\psi$. In order to show
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\land\psi$, we fix some
$\mathscr{C}\supseteq\mathscr{B}$,
$\and{R}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{q}\in\mathbb{A}$
such that
$\varphi\\!\mathrel{\fatsemi}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\cdot)}\and{q}$,
and prove $\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\and{S})}\and{q}$. Since
$\Vdash_{\\!\\!\mathscr{B}}^{\and{P}}\varphi$,
$\Vdash_{\\!\\!\mathscr{B}}^{\and{Q}}\psi$, $\and{P}\preceq\and{S}$, and
$\and{Q}\preceq\and{S}$, it follows by (() ‣ 4) that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi\\!\mathrel{\fatsemi}\\!\psi$.
This together with
$\varphi\\!\mathrel{\fatsemi}\\!\psi\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\cdot)}\and{q}$
imply $\Vdash_{\\!\\!\mathscr{C}}^{\and{R}(\and{S})}\and{q}$.

  16. $\land$E.

This follows as a special case of Lemma 14.4.

  17. $\lor$I.

Without loss of generality, assume that
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi_{1}$ and show that
$\mathrm{\Gamma}\Vdash_{\\!\\!}\varphi_{1}\lor\varphi_{2}$. So let us assume
some arbitrary base $\mathscr{B}$ and $\and{S}\in\mathbb{B}(\mathbb{A})$ such
that $\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$, and show that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\varphi_{1}\lor\varphi_{2}$. Under
($\lor$ ‣ 4), this amounts to showing that:

$\forall\mathscr{X}\supseteq\mathscr{B},\forall\and{U}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A}),\forall\and{p}\in\mathbb{A},\text{
if }\varphi_{i}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\cdot)}\and{p}\text{ for
}i=1,2,\text{ then}\Vdash_{\\!\\!\mathscr{X}}^{\and{U}(\and{S})}\and{p}$

So, we fix some arbitrary $\mathscr{C}\supseteq\mathscr{B}$,
$\and{T}(\cdot)\in\dot{\mathbb{B}}(\mathbb{A})$, and $\and{q}\in\mathbb{A}$
such that $\varphi_{i}\Vdash_{\\!\\!\mathscr{C}}^{\and{T}(\cdot)}\and{q}$ for
$i=1,2$, and then prove that
$\Vdash_{\\!\\!\mathscr{C}}^{\and{T}(\and{S})}\and{q}$. Note that
$\Vdash_{\\!\\!\mathscr{B}}^{\and{S}}\mathrm{\Gamma}$ and