The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist’s B-eS for IPL, deferring an analysis of proof-theoretic validity (in the sense of Dummett and Prawitz) to another occasion. Essential to BI’s formulation in proof-theoretic terms is the concept of a ‘bunch’ of hypotheses, a notion familiar from relevance logic. Bunches amount to trees whose internal vertices are labelled with either the IMLL or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the ‘resource interpretation’ of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the ‘number-of-uses’ interpretation of propositions in linear logic. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling.
1 Introduction
In model-theoretic semantics (M-tS), logical consequence is defined in terms of truth in models, which are abstract mathematical structures in which propositions are interpreted and their truth is judged. In the standard reading given by Tarski [48,49], a propositional formula $\phi$ follows from a context $\Gamma$ iff every model of $\Gamma$ is a model of $\phi$: $\Gamma \models \phi$ iff for all models M, if $M \models \psi$ for all $\psi \in \Gamma$, then $M \models \phi$. Therefore, consequence is understood as the transmission of truth. 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 meaning and validity are characterized in terms of proofs instead. By ‘proofs’ we mean objects denoting collections of acceptable inferences from accepted premisses. This is subtle. Essentially, what differs in P-tS is that proof plays the part of truth in M-tS.
Crucially, P-tS is not about providing a proof system for the logic, but about explicating meaning in terms of ‘proof ’. Indeed, as Schroeder-Heister [44] observes, since no formal system is fixed (only notions of inference) the relationship between semantics and provability for the logic in question remains the same as it has always been. In particular, soundness and completeness with respect to a P-tS are desirable features of formal systems.
We defer to Schroeder-Heister [43–45] for discussion of the motivation and philosophy for P-tS. The paradigm of meaning supporting P-tS is inferentialism; that is, the view that meaning (or validity) arises from rules of inference (see Brandom [5]). This stands in contrast to, for example, denotationalism as the paradigm of meaning underpinning M-tS. Current work in P-tS largely follows two different approaches. We call the first proof-theoretic validity (P-tV): it aims to define what makes an object purporting to be a ‘proof’ valid. Major approaches in P-tV follow ideas by Dummett [10] and Prawitz [31,32]—see, for example, Schroeder-Heister [43]. It is closely related to—though not identical to—BHK semantics—see Schroeder-Heister [44].
We call the second approach to P-tS base-extension semantics (B-eS): it aims to give a semantics to the logical constants through defining the validity of formulae in terms of consequence/inference in arbitrary pre-logical systems called bases. Major ideas in B-eS relevant to this paper follow Makinson, Piecha, Sandqvist, and Schroeder-Heister, and Stafford [24,27,28,38– 40,46]. In Section 2, we explain the B-eS for intuitionistic propositional logic (IPL) by Sandqvist [40] and explain how it motivates the work in this paper.
The nomenclature outlined here is taken from the historical development of the respective areas, but is not intended to divide the techniques of P-tS. In particular, both P-tV and B-eS concern validity—the former of proofs, and the latter in terms of proofs—and both may use ‘bases’ and ‘baseextensions’ in so doing.
This paper delivers a P-tS for the logic of bunched implications (BI) [6,12,25]. The logic is, perhaps, best-known for its role as the logical basis for the program logic known as Separation Logic [20,34,37] and its many derivatives. Formally, as explained in [20], Separation Logic amounts to a specific theory of BI that is concerned with memory locations. This application of BI is essentially based on its reading as a logic of resource—see, for example, Pym [33]. In this paper, we concentrate on the technical development of P-tS for BI.
Why study the B-eS of BI? One motivation is to be able to understand and account for resources in formal systems, semantically. Consider the celebrated ‘resource interpretation’ of linear logic (LL) [19] via the number-ofuses reading in which a proof of a formula $\phi \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 [19], Allwein and Dunn [2], and Coumans et al. [8]. Meanwhile, this reading of resource is quite clearly seen in the B-eS for IMLL by Gheorghiu et al. [18]. 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.
Thus, on the one hand we have P-tS as a semantic 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 informatics and systems science. This paper brings these two worlds together and is further explored by the present authors in [14]. Providing a resource-sensitive B-eS 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 [21] have recently used P-tS in the context of simulation modelling—briefly, execution of a model (or 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 4.2.
More fundamentally, BI is a logic that integrates ‘additive’ (here, intuitionistic) and ‘multiplicative’ structure and is closely related to the class of relevance logics—note, for relevance logics the additive and multiplicative structures are often given opposite notation to what is used in BI. Hence, studying the P-tS for BI expands the field into the wider space of logical systems across philosophy, mathematics, and informatics. In Section 2, we illustrate how B-eS for IPL and for IMLL, and discuss the challenges in handling BI.
In Section 3, we introduce BI in detail, providing its definition at the level of detail that is required to set up its B-eS. and including its sequential natural deduction system, NBI. In Section 4, we set up BI’s Be-S and give, in Section 4.4, a toy example of how the semantics can be used to model a resource-sensitive systems example (about access control), where we also briefly discuss the developments of this idea that have been presented in [14]. In Sections 5 and 6, we establish the soundness and completeness, respectively, of BI’s sequential natural deduction system, NBI. Finally, in Section 7, we summarize our contribution and briefly discuss some directions for further work.
2 Background: Base-extension Semantics
A base is a set of atomic rules. An atomic rule is a natural deduction rule (in the sense of Gentzen [47]) over atomic propositions (not closed under substitution). For example, following Sandqvist [42], from the propositions ‘Tammy is a fox’ and ‘Tammy is female’ one may infer ‘Tammy is a vixen’, $$\dfrac{\text{Tammy is a fox} \qquad \text{Tammy is female}}{\text{Tammy is a vixen}}$$ 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. We defer to Piecha and Schroeder-Heister [27,28] for various interpretations of atomic systems.
In B-eS, the validity of atoms and the meaning of the logical connectives is inductively defined relative to bases—see, for example, Figure 1 for intuitionistic propositional logic (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 yields incompleteness, or (conversely) generalizing atomic rules to include discharged hypotheses in the semantics of CPL delivers a semantics for IPL—see Sandqvist [38,39,41]. This understanding of B-eS is the form of P-tS used in this paper.
BI can be understood as the free combination of IPL—with connectives $\land, \lor, \to, \top, \bot$—and IMLL—with connectives $\ast$, $\wand$, $\top^{*}$ (the unit of $\ast$). Both of these logics already have B-eS—see Sandqvist [40] and Gheorghiu et al. [18]—which suggests that the semantics for BI should be a ‘free combination’ of those semantics.
In the case of BI’s model-theoretic semantics, this topic turns out to be quite delicate—see, for example, work by Docherty, Galmiche, Gheorghiu, M´ery, Pym [9,11,16]. The issues in BI’s M-tS arise from the complex structures involved in BI. In particular, as a consequence of having two implications, contexts in BI are not the typical flat data structures 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 [36].
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 [40]. Fix a (denumerable) set of atoms A. A base B is a set of atomic rules as described above and provability in a base ($\vdash_{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, $p, p_1, ..., p_n, c \in A$, $P_1, ... P_n, ... \subseteq A$ (finite), and $\phi, \psi, ...$ denote IPL-formulae, and $\Gamma$ denotes a set of IPL-formulae.
Observes that this B-eS differs from the standard Kripke semantics for IPL [22] in the treatment of disjunction $(\lor)$ and absurdity $(\bot).$ Indeed, this choice is critical as Piecha and Schroeder-Heister [26,29,30] have shown that a meta-level ‘or’ for disjunction results in incompleteness. Recently, the present authors have given a B-eS for IMLL [18] in the style of the B-eS for IPL given above. This is summarized in Figure 2 in which Pi, Si, U, V are multisets of atoms for i =1 $...n,\Gamma, \Delta$ are multisets of IMLL formulae, and , denotes multiset union. There are a few features to note about this semantics. First, observe that provability in a base ($\vdash_{\mathcal{B}}$) has been made substructural as the base case (ref) is restricted to have only 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 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 $\Gamma \rhd \phi$ are combined with those required for $\Gamma$ in order to deliver those required for $\phi$.
Third, the treatment of the support of a combination of contexts $\Gamma$, $\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 conclusions), 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. 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 [27,28]—as natural deduction in the sense of Gentzen [47] 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 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): $$\Gamma \forces_{B}^{R(\cdot)} \phi \quad\text{iff}\quad \forall X \supseteq B,\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{X}^{U} \Gamma,\ \text{then } \forces_{X}^{R(U)} \phi \tag{Inf}$$ That is, the contextual bunch $R(\cdot)$ manages the construction of the bunch of atomic resources in a way that matches the structure of the required judgement.
3 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 3.1. Second, we give the meta-theory required to understand the use of bunches in this paper in Section 3.2. We defer motivations for BI to Pym and O’Hearn [25] to concentrate on the technical question of its P-tS in this paper. Notations and Conventions. Henceforth, we fix a denumerable set of atomic propositions A, and the following conventions: p, q,... denote atoms; P, Q,... denote bunches (defined below) of atoms; $\phi, \psi, \theta,$. . . denote formulae; $\Gamma, \Delta,...$ denote bunches of formulae. We also use A , B, C ,... to denote bases (defined below).
3.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. We follow standard presentations (cf. O’Hearn and Pym [25]) except that it also introduces contextual bunches, which are used throughout this paper but are not part of the standard background of BI.
The set of formulae F (over A) is defined by the following grammar: $$\phi ::= p \in A \mid \top \mid \bot \mid \top^{*} \mid \phi \land \phi \mid \phi \lor \phi \mid \phi \to \phi \mid \phi \ast \phi \mid \phi \wand \phi$$
Let X be a set of syntactic structures. The set of bunches over X is denoted $\mathcal{B}(X)$ and is defined by the following grammar: $$\Gamma ::= x \in X \mid \emptyplus \mid \emptytimes \mid \Gamma \mathbin{;} \Gamma \mid \Gamma \mathbin{,} \Gamma$$ The $;$ is the additive context-former, and the $\emptyplus$ is the additive unit; the $,$ is the multiplicative context-former, and the $\emptytimes$ is the multiplicative unit. In the bunch $\Gamma_1 ;\Gamma_2$(resp. $\Gamma_1 ,\Gamma_2),$ we call ; (resp. ,) the principal contextformer. If a bunch $\Delta$ is a sub-tree of a bunch $\Gamma,$ then $\Delta$ is a sub-bunch of $\Gamma.$ Importantly, sub-bunches are sensitive to occurrence—for example, in the bunch $\Delta$, $\Delta,$ each occurrence of $\Delta$ is a different sub-bunch. We may write $\Gamma(\Delta)$ to express that $\Delta$ is a sub-bunch of $\Gamma.$ This notation is traditional for BI [25], but requires sensitive handling. To avoid confusion, we never write $\Gamma$ and later $\Gamma(\Delta)$ to denote the same bunch, but rather maintain one presentation. The substitution of $\Delta$ for $\Delta$ in $\Gamma$ is denoted $\Gamma(\Delta)[\Delta \to \Delta$]. To emphasize: this is not a universal substitution, but a substitution of the particular occurrence of $\Delta$ meant in writing $\Gamma(\Delta).$ The bunch $\Gamma(\Delta)[\Delta \to \Delta$] may be denoted $\Gamma(\Delta$) when no confusion arises.
Consider the bunches $\Gamma(q)$:= $\emptyset\times$,(p; q). We have by direct substitution $\Gamma(\emptyset+)= \emptyset\times ,(p;\emptyset+).$ Substitution in bunches is an essential part of expressing 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 [51]. Indeed, so integral are substitutions that it is instructive to have a notion of contextual bunch that allows us to handle substitutions smoothly.
A contextual bunch (over X) is a function $b : \mathcal{B}(X) \to \mathcal{B}(X)$ for which there is $\Gamma(\Delta) \in \mathcal{B}(X)$ such that $b(\Sigma) = \Gamma(\Sigma)$ for any $\Sigma \in \mathcal{B}(X)$. The set of all contextual bunches (over X) is $\dot{\mathcal{B}}(X)$.
Importantly, the identity on $\mathcal{B}(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 [7]. That is, $\dot{\mathcal{B}}(X)$ can be identified as the subset of $\mathcal{B}(X \cup \{\circ\})$, where $\circ \in X$, in which bunches contain a single occurrence of $\circ$. Specifically, if $b(x) = \Gamma(x)$, then identify $b$ with $\Gamma(\circ) \in \mathcal{B}(X \cup \{\circ\})$. We write $\Gamma(\cdot)$ for the contextual bunch identified with $\Gamma(\circ)$.
The contextual bunch b : x $\to \phi_1 ;((\phi_2 ;\emptyset\times ;(\phi_3 ,\phi_4)),(\phi_5$; (x))) is identified with $\Gamma(\cdot),$ where $\Gamma(\circ )$:= $\phi_1 ;((\phi_2 ;\emptyset\times ;(\phi_3 ,\phi_4)),(\phi_5$;◦)). In BI, bunches serve as the data structures over which collections of formulae are organized. Each of the two context-formers (i.e., ; and ,) is intended behave as a multiset constructor, possessing the usual properties of commutativity and associativity. For example, a bunch $\Delta,\Delta$(resp. $\Delta;\Delta$) is meant to represent the same data as the bunch $\Delta$, $\Delta$(resp. $\Delta$; $\Delta).$ For clarity, we explicitly define the equivalence relation that captures this intended meaning, called coherent equivalence. This is similar to how lists for the contexts of classical logic sequents may be understood ‘up to permutation’ to render multisets. Importantly, in BI, the two context-formers do not distribute over each other.
Two bunches $\Gamma, \Gamma \in$ B(X) are coherently equivalent when $\Gamma \equiv \Gamma$, where $\equiv$ is the least relation satisfying:
– commutative monoid equations for $;$ with unit $\emptyplus$—that is, for arbitrary $\Gamma_1, \Gamma_2, \Gamma_3 \in \mathcal{B}(X)$, $$(\Gamma_1 \mathbin{;} \Gamma_2) \mathbin{;} \Gamma_3 \equiv \Gamma_1 \mathbin{;} (\Gamma_2 \mathbin{;} \Gamma_3) \qquad \Gamma_1 \mathbin{;} \Gamma_2 \equiv \Gamma_2 \mathbin{;} \Gamma_1 \qquad \Gamma_1 \mathbin{;} \emptyplus \equiv \Gamma_1$$
– commutative monoid equations for $,$ with unit $\emptytimes$—that is, for arbitrary $\Gamma_1, \Gamma_2, \Gamma_3 \in \mathcal{B}(X)$, $$(\Gamma_1 \mathbin{,} \Gamma_2) \mathbin{,} \Gamma_3 \equiv \Gamma_1 \mathbin{,} (\Gamma_2 \mathbin{,} \Gamma_3) \qquad \Gamma_1 \mathbin{,} \Gamma_2 \equiv \Gamma_2 \mathbin{,} \Gamma_1 \qquad \Gamma_1 \mathbin{,} \emptytimes \equiv \Gamma_1$$
– coherence; that is, if $\Delta \equiv \Delta'$ then $\Gamma(\Delta) \equiv \Gamma(\Delta')$.
Recall the bunch $\Gamma(q) := \emptytimes \mathbin{,} (p \mathbin{;} q)$ from Example 3.3. Observe, $\Gamma(\emptyplus) \equiv p$ by the unitality of $\emptyplus$ and $\emptytimes$ with respect to $;$ and $,$, respectively. Further discussion about bunches as data structures is given in Sections 3.2 and 4. Presently, we continue defining BI.
A sequent is a pair $\Gamma \rhd \phi$ in which $\Gamma \in \mathcal{B}(F)$ is a bunch of formulae and $\phi$ is a formula.
That a sequent $\Gamma \rhd \phi$ is a consequence of BI is denoted $\Gamma \vdash \phi$. There are several ways to define $\vdash$, for example semantical. In this paper, we shall concentrate on its natural deduction system NBI. We assume general familiarity with sequent calculus presentation of proof systems—see, for example, Troelstra and Schwichtenberg [50].
System NBI comprises the rules of Figure 3, in which $\phi, \psi, \chi \in F$, $\Gamma, \Delta, \Delta' \in \mathcal{B}(F)$, and e has the side-condition $\Gamma \equiv \Gamma'$ and $i \in \{1, 2\}$ in $\lor I$. Let $\vdash_{\mathrm{NBI}}$ denote provability in NBI. When we say that NBI characterizes BI, we mean the following: $\Gamma \vdash \phi$ iff $\Gamma \vdash_{\mathrm{NBI}} \phi$. Of course, BI admits cut:
If $\Gamma(\chi) \vdash \phi$ and $\Delta \vdash \chi,$ then $\Gamma(\Delta) \vdash \phi.$
3.2 Bunches Modulo Coherent Equivalence
As stated in Section 3, bunches as data structures are really the syntax trees in Definition 3.2 modulo coherent equivalence (Definition 3.6). Gheorghiu
and Marin [15] gave a formal description of $B(X)/\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 is useful for the purpose of the current paper. Therefore, here 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. Essentially, bunches modulo coherent equivalence are trees satisfying the following:
– the internal nodes are either $;$ or $,$
– the leaves are either $x \in X$, $\emptyplus$, or $\emptytimes$
– 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 $\emptyplus$
– no child of a $,$-node is labelled with $\emptytimes$.
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.
Intuitively, we may identify bunches as being additive or multiplicative according to whether their principal context-former is an additive or multiplicative context-former or unit, respectively. This is not quite a partition as bunches consisting of just a formula are considered both to be additive and multiplicative. An additive (resp. multiplicative) bunch that is not a formula may then be expressed $\Sigma_1$; $\cdots$; $\Sigma_k$ (resp. $\Sigma_1$, $\cdots$, $\Sigma_k$), where $\Sigma_i$ for i = 1,...,k is a multiplicative (resp. additive) bunch.
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.
Let $\Gamma \in$ B(X) be a bunch, $\Delta$ be a subbunch of $\Gamma.$ The nest depth of $\Delta$ in $\Gamma$—denoted $nestDepth(\Gamma)(\Delta)$—is defined as follows:
– if $\Gamma$= $\Delta,$ then $nestDepth(\Gamma)(\Delta)$:= 0
– if $\Gamma$ is of the form $\Sigma_1 \cdots \Sigma_k,$ where $\circ \in \{;, {,}\},$ and $\Delta$ is a sub-bunch of $\Sigma_i,$ then $nestDepth(\Gamma)(\Delta)$:= $nestDepth(\Sigma_i)(\Delta)$ + 1. In other words, $nestDepth(\Gamma)(\Delta)$= 0 if $\Delta$ is $\Gamma$ itself, and otherwise one more than the number of context-former alternations between the principal context-former of $\Delta$ and the principal context-former of $\Gamma.$
Let $b \in \dot{\mathcal{B}}(X)$ be a contextual bunch. Identify $b$ with the element $\Gamma(\circ)$ in $\mathcal{B}(X \cup \{\circ\})$. The hole depth of $b$—denoted $\mathrm{holeDepth}(b)$—is $\mathrm{nestDepth}(\Gamma(\circ))(\circ)$.
Let $\Gamma(\cdot)$ be as in Example 3.5; that is, $\Gamma(\circ) = \phi_1 \mathbin{;} ((\phi_2 \mathbin{;} \emptytimes \mathbin{;} (\phi_3 \mathbin{,} \phi_4)), (\phi_5 \mathbin{;} \circ))$. Then $holeDepth(\Gamma(\cdot))$ can be calculated as follows: $$\begin{aligned} holeDepth(\Gamma(\cdot)) &= nestDepth(\Gamma(\circ))(\circ) \\ &= nestDepth\big((\phi_2 \mathbin{;} \emptytimes \mathbin{;} (\phi_3 \mathbin{,} \phi_4)), (\phi_5 \mathbin{;} \circ)\big)(\circ) + 1 \\ &= nestDepth(\phi_5 \mathbin{;} \circ)(\circ) + 2 = nestDepth(\circ)(\circ) + 3 = 3 \end{aligned}$$ This is exactly the number of the alternations of context-formers starting from $\circ$ to the principal context-former in $\Gamma(\circ)$.
4 Base-extension Semantics for BI
This section defines the B-eS for BI. We defer elaboration and motivation for the sequence of steps and the final form of the semantics to earlier work on IMLL [18] and other discussions [13]. This enables us to concentrate on the technical questions of proving soundness and completeness. First, in Section 4.1, we define derivability in a base, departing somewhat from existing treatments of atomic systems in P-tS. Second, in Section 4.2, we define the support judgement that makes the semantics. Third, some preliminary results that show that support has the expected behaviour with respect to structurality and monotonicity in Section 4.3. Fourth, a toy example of the application to rule-based access control is presented in Section 4.4.
4.1 Derivability in a Base
The definition of a B-eS begins 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 in the style of natural deduction rules in the sense of Gentzen [47]—see, for example, Peicha and Schroeder-Heister [27,28]. This is difficult in the case of BI as more careful context-management is required in order 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.
A sequent of atoms is a pair $P \rhd p$ in which $P \in \mathcal{B}(A)$ and $p \in A$.
An atomic rule is a rule-figure with a (finite) set of sequents of atoms above, and a sequent of atoms below, $$\dfrac{P_1 \rhd p_1 \quad \dots \quad P_n \rhd p_n}{P \rhd p}$$ 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; that is, for a given rule, we do not consider ‘instances’ of it, rather it applies only to those atoms explicit in it. We may write $(P_1 \rhd p_1, ..., P_n \rhd p_n) \Rightarrow (P \rhd p)$ to denote the atomic rule in Definition 4.2—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.
A base is a set of atomic rules. We write $\mathcal{B}, \mathcal{C}, ...$ to denote bases, and $\emptyset$ to denote the empty base (i.e., the base with no rules). We say $\mathcal{C}$ is an extension of $\mathcal{B}$ if $\mathcal{C}$ is a superset of $\mathcal{B}$; hence it is denoted as $\mathcal{C} \supseteq \mathcal{B}$.
The following is an example of an atomic rule, in which $p, q, r, s \in A$: $$\dfrac{p \rhd s \qquad s \mathbin{;} q \rhd r}{p \mathbin{;} q \rhd r}$$ It may be expressed inline as follows: $((p \rhd s), (s \mathbin{;} q \rhd r)) \Rightarrow (p \mathbin{;} q \rhd r)$. The set consisting of just this atomic rule is a base $\mathcal{B}$. Let $\mathcal{C}$ be the set of all atomic rules taking the same form as the above while $p, q, r$, and $s$ range over A—that is, $$\mathcal{C} := \left\{ \dfrac{x \rhd w \qquad w \mathbin{;} y \rhd z}{x \mathbin{;} y \rhd z} \;\middle|\; x, y, z, w \in A \right\}$$
Observe, $\mathcal{C} \supseteq \mathcal{B}$ and $\mathcal{B} \neq \mathcal{C}$. Intuitively, $\Rightarrow (P \rhd p)$ means that the sequent of atoms $(P \rhd p)$ may be concluded whenever, while $(P_1 \rhd p_1, ..., P_n \rhd p_n) \Rightarrow (P \rhd p)$ means that one may derive $P \rhd p$ if one has derived $(P_i \rhd 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 3.6). 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 [40] and IMLL [18]):
Let $\mathcal{B}$ be a base. Derivability in $\mathcal{B}$—denoted $\vdash_{\mathcal{B}}$—is the smallest relation satisfying the following:
– taut. If $p \in A$, then $p \vdash_{\mathcal{B}} p$
– initial. If $\Rightarrow (P \rhd p) \in \mathcal{B}$, then $P \vdash_{\mathcal{B}} p$
– rule. If $(P_1 \rhd p_1, ..., P_n \rhd p_n) \Rightarrow (P \rhd p) \in \mathcal{B}$ and $P_1 \vdash_{\mathcal{B}} p_1, ..., P_n \vdash_{\mathcal{B}} p_n$, then $P \vdash_{\mathcal{B}} p$
– weak. If $P(Q) \vdash_{\mathcal{B}} p$, then $P(Q \mathbin{;} Q') \vdash_{\mathcal{B}} p$ for any $Q' \in \mathcal{B}(A)$
– cont. If $P(Q \mathbin{;} Q) \vdash_{\mathcal{B}} p$, then $P(Q) \vdash_{\mathcal{B}} p$
– exch. If $P(Q) \vdash_{\mathcal{B}} p$ and $Q \equiv Q'$, then $P(Q') \vdash_{\mathcal{B}} p$.
– cut. If $T \vdash_{\mathcal{B}} q$ and $S(q) \vdash_{\mathcal{B}} p$, then $S(T) \vdash_{\mathcal{B}} p$.
The expressive power of $\mathcal{B}$ and $\mathcal{C}$ is the same as $\emptyset$ because of cut.—that is, $P \vdash_{\mathcal{B}} p$ iff $P \vdash_{\mathcal{C}} p$ iff $P \vdash_{\emptyset} p$. As Example 4.6 illustrates, it is possible for a base to satisfy some of weak., cont., exch., cut. using just initial. and rule.. Indeed, in Section 6, we construct a base N that satisfies all of them. However, we require these properties to hold of arbitrary bases, and that may not be the case. For this reason, we include properties as closure conditions on derivability in a base. Another possibility is to restrict the notion of base to be exactly those sets of atomic rules that satisfies these conditions, but this option requires wanton repetition of infinitely many structural rules in each base. To conclude this section, we state an obvious but important fact about derivability in a base:
If $T \vdash_{\mathcal{B}} p$ and $\mathcal{C} \supseteq \mathcal{B}$, then $T \vdash_{\mathcal{C}} p$.
Follows by induction on the derivation of $T \vdash_{\mathcal{B}} p$ since all the rules of $\mathcal{B}$ are contained in $\mathcal{C}$.
□4.2 Support in a Base
Derivability in a base is the starting point 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 unfolds 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 [40] and for IMLL [18]. However, the use of bunches as datastructures renders it more complex than in either of the preceding works. 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. [17], where it is in-advisably called weak coherence. It is also closely related to the ‘is a pruning of’ relation used in relevance logic [36], but fixed with the specific structural rules of BI.
The bunch-extension relation $\succeq$ is the least relation satisfying:
– if $\Gamma \equiv \Gamma'[\Delta \mapsto (\Delta \mathbin{;} \Delta')]$, then $\Gamma \succeq \Gamma'$
– if $\Gamma \succeq \Gamma'$ and $\Gamma' \succeq \Gamma''$, then $\Gamma \succeq \Gamma''$.
Observe $((p \mathbin{,} q) \mathbin{;} u) \mathbin{,} r \succeq (p \mathbin{,} q) \mathbin{,} r$, since $((p \mathbin{,} q) \mathbin{;} u) \mathbin{,} r \equiv ((p \mathbin{,} q) \mathbin{,} r)[(p \mathbin{,} q) \mapsto ((p \mathbin{,} q) \mathbin{;} u)]$. Moreover, $(p \mathbin{,} q) \mathbin{,} r \succeq p \mathbin{,} (q \mathbin{,} r)$, since $(p \mathbin{,} q) \mathbin{,} r \equiv p \mathbin{,} (q \mathbin{,} r)$. Hence, $((p \mathbin{,} q) \mathbin{;} u) \mathbin{,} r \succeq p \mathbin{,} (q \mathbin{,} r)$.
If $T \succeq S$, then $P(T) \succeq P(S)$.
It is easy to see that $\Gamma \succeq \Gamma'$ iff $\Gamma \equiv \Gamma' \cdot \Sigma_1 \cdots \Sigma_n$, where $\Sigma_i$ is a substitution of the form $[\Delta \mapsto \Delta \mathbin{;} \Delta']$. We proceed by induction on $holeDepth(P(\cdot))$.
– base case. $holeDepth(P(\cdot)) = 0$. By Definition 3.12, $P(\cdot) = (\cdot)$. Hence, the antecedent of the claim is identical to the consequent.
– inductive step. $holeDepth(P(\cdot)) = d + 1$ for some $d > 0$. By Definition 3.12, $P(\cdot) = P'(\cdot) \circ Q$, where $holeDepth(P'(\cdot)) = d$, $Q \in \mathcal{B}(A)$, and $\circ \in \{;, {,}\}$. By the induction hypothesis (IH), $P'(T) \succeq P'(S)$. Let $\tau_1, ..., \tau_k$ witness the extension. Since $P(S) \equiv P'(S) \circ Q \equiv P'(T)\tau_1\cdots\tau_k \circ Q \equiv (P'(T) \circ Q)\tau_1\cdots\tau_k \equiv P(T)\tau_1\cdots\tau_k$, we have $P(S) \preceq P(T)$.
This completes the induction. Having defined derivability in a base, and base- and bunch-extension, it is possible to give the semantics.
□Supports in a base $\mathcal{B}$ relative to either a contextual bunch or bunch of atoms P is the relation $\forces_{\mathcal{B}}^{P}$ defined by the clauses of Figure 4 in which $p \in A$, $\phi, \psi \in F$, $S \in \mathcal{B}(A)$, $R(\cdot) \in \dot{\mathcal{B}}(A)$ and $\Gamma, \Delta \in \mathcal{B}(F)$. It is easy to see that Figure 4 is an inductive definition on a structure of formulas that prioritizes the binary signs over the units, and the units over atoms; this follows similar treatments in the B-eS of IPL [41] and IMLL [18]. That is, there is a measure $\mu$ on formulae as follows: $$\mu(\phi) := \begin{cases} 0 & \text{if } \phi \in A \\ 1 & \text{if } \phi \in \{\top, \top^{*}, \bot\} \\ \mu(\phi_1) + \mu(\phi_2) + 1 & \text{if } \phi = \phi_1 \circ \phi_2 \text{ where } \circ \in \{\land, \ast, \lor, \to, \wand\} \end{cases}$$
It may be extended to bunches as follows: $$\mu(\Gamma) := \begin{cases} \mu(\phi) & \text{if } \Gamma = \phi \in F \\ 1 & \text{if } \Gamma \in \{\emptyplus, \emptytimes\} \\ \mu(\Gamma_1) + \mu(\Gamma_2) & \text{if } \Gamma = \Gamma_1 \circ \Gamma_2 \text{ where } \circ \in \{;, {,}\} \end{cases}$$ In each clauses of Figure 4, the sum of this measure of the formulas flanking the support relation in the definiendum exceeds the corresponding number for any occurrence in the definiens. Thus Definition 4.11 is inductive with respect to this measure.
The bunch-extension relation is used in (;) and (,). 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 4.4. We note the use of a base-extension in (Inf). The idea originates with Prawitz’s [31] treatment of open derivation in his account of proof-theoretic validity. Intuitively, support does not only render analytic connection between hypotheses $\Gamma$ and conclusion $\phi,$ but rather constructively grounded connections where the available data is encoded in the base and available resources. This warrants the reading that if one were to accept the inferences in the base and resources sufficient to yield all the formulae in $\Gamma,$ then, whatever else you may accept, one is committed to accepting $\phi$ too.
The general pattern for the clauses of the connectives is to follow their elimination rules. Precisely why this is the correct approach is something of an open problem within the literature on P-tS—see, for example, Gheorghiu et al. [13]. What one can say is that the clauses essentially represent what it means to use the defined signs; for example, to use disjunction is to form a case distinction, and that is exactly what is encapsulated by its clause.
A sequent $\Gamma \rhd \phi$ is valid iff $\Gamma \forces \phi$, where $$\Gamma \forces \phi \quad\text{iff}\quad \text{for any base } \mathcal{B},\ \Gamma \forces_{\mathcal{B}}^{(\cdot)} \phi$$
It is instructive to see how $\forces_{\emptyset}^{((p,q);u),r} p \mathbin{,} (q \ast r)$ obtains. From Example 4.9, $((p,q) \mathbin{;} u) \mathbin{,} r \succeq p \mathbin{,} (q \mathbin{,} r)$. Hence, by $(,)$, it suffices to show the following: (1) $\forces_{\emptyset}^{p} p$, and (2) $\forces_{\emptyset}^{q,r} q \ast r$. That (1) obtains is immediate by (At) and taut. in Definition 4.5. By $(\ast)$, claim (2) is equivalent to the following: $$\forall X \supseteq \emptyset,\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall s \in A,\ \text{if } q,r \forces_{X}^{U(\cdot)} s,\ \text{then } \forces_{X}^{U(q,r)} s \tag{$\dagger$}$$ It is clear that we have $\forces_{X}^{q} q$ and $\forces_{X}^{r} r$ for any X. Therefore, by $(,)$, $\forces_{X}^{q,r} q,r$. Hence, the result follows by (Inf) on the antecedent of $(\dagger)$ by choosing $q \mathbin{,} r$ for the resources. We see in this example why $\succeq$ 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, $\Gamma \vdash \phi$ iff $\Gamma \phi.$ This is captured in Theorems 5.1 (Soundness) and 6.1 (Completeness), which are stated and proved in Sections 5 and 6, respectively.
4.3 Preliminary Results
Before proceeding to soundness and completeness, it is instructive to observe that some properties about support.
If $\forces_{\mathcal{B}}^{T} \phi$ and $\mathcal{C} \supseteq \mathcal{B}$ and $S \succeq T$, then $\forces_{\mathcal{C}}^{S} \phi$. This follows as the combination of Proposition 4.7 (above), Lemmas 4.15, and 4.16:
If $\forces_{\mathcal{B}}^{T} \phi$ and $\mathcal{C} \supseteq \mathcal{B}$, then $\forces_{\mathcal{C}}^{T} \phi$.
We proceed by induction on the structure of $\phi.$– base case. This follows from Proposition 4.7.
– inductive step. If there is no base-extension in the relevant clause for $\phi$, then the result follows from applying the induction hypothesis (IH) to the judgements in the definiens. For example, consider the case where $\phi$ is $\bot$: by $(\bot)$, from $\forces_{\mathcal{B}}^{T} \phi$ infer that $\forces_{\mathcal{B}}^{T} p$ for every $p \in A$; hence, by the IH, $\forces_{\mathcal{C}}^{T} p$ for every $p \in A$; whence, by $(\bot)$, $\forces_{\mathcal{C}}^{T} \bot$, as required. If base-extension is used in the relevant clause for $\phi$, the result holds immediately since $X \supseteq \mathcal{C}$ implies $X \supseteq \mathcal{B}$. For example, consider the case where $\phi$ is $\psi_1 \ast \psi_2$. By $(\ast)$, $$\forall X \supseteq \mathcal{B},\ \forall U(\cdot) \in \dot{\mathcal{B}}(F),\ \forall p \in A,\ \text{if } \psi_1, \psi_2 \forces_{X}^{U(\cdot)} p,\ \text{then } \forces_{X}^{U(T)} p$$ Hence, since $\mathcal{C} \supseteq \mathcal{B}$, $$\forall X \supseteq \mathcal{C},\ \forall U(\cdot) \in \dot{\mathcal{B}}(F),\ \forall p \in A,\ \text{if } \psi_1, \psi_2 \forces_{X}^{U(\cdot)} p,\ \text{then } \forces_{X}^{U(T)} p$$ By $(\ast)$, $\forces_{\mathcal{C}}^{T} \psi_1 \ast \psi_2$, as required. For clarity, we also show the case where $\phi$ is $\psi_1 \wand \psi_2$. Assume $\forces_{\mathcal{B}}^{T} \phi \wand \psi$ and some $\mathcal{C} \supseteq \mathcal{B}$. We want to show $\forces_{\mathcal{C}}^{T} \phi \wand \psi$. Therefore, fix some arbitrary $D \supseteq \mathcal{C}$ and U such that $\forces_{D}^{U} \phi$. The goal is to show $\forces_{D}^{T,U} \psi$. This follows immediately from $D \supseteq \mathcal{C} \supseteq \mathcal{B}$ and $\phi \forces_{\mathcal{B}}^{T} \psi$. This completes the induction.
□If $\forces_{\mathcal{B}}^{T} \phi$ and $S \succeq T$, then $\forces_{\mathcal{B}}^{S} \phi$.
We proceed by induction on the structure of $\phi$.
– $\phi = p \in A$. By (At), $\forces_{\mathcal{B}}^{T} p$ iff $T \vdash_{\mathcal{B}} p$. By weak. from Definition 4.5, since $S \succeq T$, it follows that $S \vdash_{\mathcal{B}} p$.
– $\phi = \phi_1 \land \phi_2$. By $(\land)$ it suffices to show the following: $$\forall X \supseteq \mathcal{B},\ \forall U(\cdot) \in \dot{\mathcal{B}}(\mathcal{F}),\ \forall p \in A,\ \text{if } \phi_1 \mathbin{;} \phi_2 \forces_{X}^{U(\cdot)} p,\ \text{then } \forces_{X}^{U(S)} p$$ Therefore, let $\mathcal{C} \supseteq \mathcal{B}$, $P(\cdot)$, and q be arbitrary such that $\phi_1 \mathbin{;} \phi_2 \forces_{\mathcal{C}}^{P(\cdot)} q$. We require to show that $\forces_{\mathcal{C}}^{P(S)} q$. By $(\land)$, from the assumption $\forces_{\mathcal{B}}^{T} \phi_1 \land \phi_2$, infer $\forces_{\mathcal{C}}^{P(T)} q$. By Proposition 4.10, from $S \succeq T$, infer $P(S) \succeq P(T)$. By the induction hypothesis (IH), from $\forces_{\mathcal{C}}^{P(T)} q$ and $P(S) \succeq P(T)$, infer $\forces_{\mathcal{C}}^{P(S)} q$.
– $\phi = \top$. By $(\top)$ it suffices to show the following: $$\forall X \supseteq \mathcal{B},\ \forall U(\cdot) \in \dot{\mathcal{B}}(F),\ \forall p \in A,\ \text{if } \forces_{X}^{U(\emptyplus)} p,\ \text{then } \forces_{X}^{U(T)} p$$ Therefore, let $\mathcal{C} \supseteq \mathcal{B}$, $P(\cdot)$, and q be arbitrary such that $\forces_{\mathcal{C}}^{P(\emptyplus)} q$. We require to show $\forces_{\mathcal{C}}^{P(S)} q$ holds. By $(\top)$, from the assumption $\forces_{\mathcal{B}}^{T} \top$, infer $\forces_{\mathcal{C}}^{P(T)} q$. By Proposition 4.10, from $S \succeq T$, infer $P(S) \succeq P(T)$. By the IH, from $\forces_{\mathcal{C}}^{P(T)} q$ and $P(S) \succeq P(T)$, infer $\forces_{\mathcal{C}}^{P(S)} q$.
– $\phi = \phi_1 \to \phi_2$. By $(\to)$ it suffices to show $\phi_1 \forces_{\mathcal{B}}^{S \mathbin{;} (\cdot)} \phi_2$. By (Inf), this is equivalent to the following: $$\forall X \supseteq \mathcal{B},\ \forall U \in \mathcal{B}(F),\ \text{if } \forces_{X}^{U} \phi_1,\ \text{then } \forces_{X}^{S \mathbin{;} U} \phi_2$$ Therefore, let $\mathcal{C} \supseteq \mathcal{B}$, P be arbitrary such that $\forces_{\mathcal{C}}^{P} \phi_1$. We require to show $\forces_{\mathcal{C}}^{S \mathbin{;} P} \phi_2$. By $(\to)$ and (Inf), from the assumption $\forces_{\mathcal{B}}^{T} \phi_1 \to \phi_2$, infer $\forces_{\mathcal{C}}^{T \mathbin{;} P} \phi_2$. By Proposition 4.10, from $S \succeq T$, infer $S \mathbin{;} P \succeq T \mathbin{;} P$. By the IH, from $\forces_{\mathcal{C}}^{T \mathbin{;} P} \phi_2$ and $S \mathbin{;} P \succeq T \mathbin{;} P$, infer $\forces_{\mathcal{C}}^{S \mathbin{;} P} \phi_2$.
– $\phi = \phi_1 \ast \phi_2$. Mutatis mutandis on the $\land$-case.
– $\phi = \top^{*}$. Mutatis mutandis on the $\top$-case.
– $\phi = \phi_1 \wand \phi_2$. Mutatis mutandis on the $\to$-case.
– $\phi = \phi_1 \lor \phi_2$. Mutatis mutandis on the $\land$-case.
– $\phi = \bot$. By $(\bot)$ on the assumption $\forces_{\mathcal{B}}^{T} \bot$, infer $\forces_{\mathcal{B}}^{T} p$ holds for all $p \in A$. By either the IH or the atomic case, $\forces_{\mathcal{B}}^{S} p$ for all $p \in A$. Hence, by $(\bot)$, $\forces_{\mathcal{B}}^{S} \bot$. This completes the induction. It is easy to see that monotonicity (Proposition 4.14) extends to bunches:
If $\forces_{\mathcal{B}}^{T} \Gamma$ and $\mathcal{C} \supseteq \mathcal{B}$, then $\forces_{\mathcal{C}}^{T} \Gamma$.
We proceed by induction on the structure of $\Gamma$.
– $\Gamma = \phi \in F$. This is Lemma 4.15.
– $\Gamma = \emptyplus$. This follows immediately by $(\emptyplus)$.
– $\Gamma = \emptytimes$. By $(\emptytimes)$, $T \succeq \emptytimes$. Hence, by $(\emptytimes)$, $\forces_{\mathcal{C}}^{T} \emptytimes$.
– $\Gamma = \Gamma_1 \mathbin{;} \Gamma_2$. By $(;)$, there are $Q_1$ and $Q_2$ such that $T \succeq Q_1$, $T \succeq Q_2$, $\forces_{\mathcal{B}}^{Q_1} \Gamma_1$, and $\forces_{\mathcal{B}}^{Q_2} \Gamma_2$. By the induction hypothesis (IH), $\forces_{\mathcal{C}}^{Q_1} \Gamma_1$ and $\forces_{\mathcal{C}}^{Q_2} \Gamma_2$. Whence, by $(;)$, $\forces_{\mathcal{C}}^{T} \Gamma_1 \mathbin{;} \Gamma_2$.
– $\Gamma = \Gamma_1 \mathbin{,} \Gamma_2$. By $(,)$, there are $Q_1$ and $Q_2$ such that $T \succeq (Q_1, Q_2)$, $\forces_{\mathcal{B}}^{Q_1} \Gamma_1$, and $\forces_{\mathcal{B}}^{Q_2} \Gamma_2$. By the IH, $\forces_{\mathcal{C}}^{Q_1} \Gamma_1$ and $\forces_{\mathcal{C}}^{Q_2} \Gamma_2$. Whence, by $(,)$, $\forces_{\mathcal{C}}^{T} \Gamma_1 \mathbin{,} \Gamma_2$. This completes the induction.
□If $\forces_{\mathcal{B}}^{T} \Gamma$ and $S \succeq T$, then $\forces_{\mathcal{B}}^{S} \Gamma$.
We proceed by case-analysis on the structure of $\Gamma$.
– $\Gamma = \phi \in F$. This is Lemma 4.16.
– $\Gamma = \emptyplus$. This follows immediately by $(\emptyplus)$.
– $\Gamma = \emptytimes$. By $(\emptytimes)$, $T \succeq \emptytimes$. Hence, $S \succeq \emptytimes$. Whence, $(\emptytimes)$, $\forces_{\mathcal{B}}^{S} \emptytimes$.
– $\Gamma = \Gamma_1 \mathbin{;} \Gamma_2$. By $(;)$, there are $Q_1$ and $Q_2$ such that $T \succeq Q_1$, $T \succeq Q_2$, $\forces_{\mathcal{B}}^{Q_1} \Gamma_1$, and $\forces_{\mathcal{B}}^{Q_2} \Gamma_2$. From $S \succeq T$, infer $S \succeq Q_1$ and $S \succeq Q_2$. Hence, by $(;)$, $\forces_{\mathcal{B}}^{S} \Gamma_1 \mathbin{;} \Gamma_2$.
– $\Gamma = \Gamma_1 \mathbin{,} \Gamma_2$. By $(,)$, there are $Q_1$ and $Q_2$ such that $T \succeq (Q_1, Q_2)$, $\forces_{\mathcal{B}}^{Q_1} \Gamma_1$, and $\forces_{\mathcal{B}}^{Q_2} \Gamma_2$. From $S \succeq T$, infer $S \succeq (Q_1, Q_2)$. Hence, by $(,)$, $\forces_{\mathcal{B}}^{S} \Gamma_1 \mathbin{,} \Gamma_2$. This completes the induction. As a corollary of monotonicity, validity corresponds to support in the empty base with respect to no resources.
□The ‘if’ direction is follows from Proposition 4.14. The ‘only if’ direction is immediate by Definition 4.12. We now proceed to showing that support respects the intended structural behaviour of bunches—that is, weakening, contraction, and coherent equivalence, as well as the correspondence between bunched resources and the support of bunches.
□For any base $\mathcal{B}$ and $P \in \mathcal{B}(A)$, $\forces_{\mathcal{B}}^{P} P$ obtains.
We proceed by induction on the structure of P.
– P is in $A$. That is, P is some atom p. By (At), this is equivalent to $p \vdash_{\mathcal{B}} p$, which obtains by taut. in Definition 4.5.
– P is $\emptyplus$. This is immediate by $(\emptyplus)$.
– P is $\emptytimes$. This is immediate by $(\emptytimes)$ as $\emptytimes \succeq \emptytimes$.
– P is $P_1 \mathbin{;} P_2$. By the induction hypothesis (IH), both $\forces_{\mathcal{B}}^{P_1} P_1$ and $\forces_{\mathcal{B}}^{P_2} P_2$ obtain. Since $P_1 \mathbin{;} P_2 \succeq P_1$ and $P_1 \mathbin{;} P_2 \succeq P_2$, the result follows by $(;)$.
– P is $P_1 \mathbin{,} P_2$. By the IH, both $\forces_{\mathcal{B}}^{P_1} P_1$ and $\forces_{\mathcal{B}}^{P_2} P_2$ obtain. Since $P_1 \mathbin{,} P_2 \succeq P_1 \mathbin{,} P_2$, the result follows by $(,)$. This completes the induction.
□For any base $\mathcal{B}$, $S, S' \in \mathcal{B}(A)$, $P(\cdot) \in \dot{\mathcal{B}}(A)$, and $\phi \in F$, (i) if $\forces_{\mathcal{B}}^{P(S)} \phi$, then $\forces_{\mathcal{B}}^{P(S \mathbin{;} S')} \phi$; (ii) if $\forces_{\mathcal{B}}^{P(S \mathbin{;} S')} \phi$, then $\forces_{\mathcal{B}}^{P(S)} \phi$.
Since $P(S) \preceq P(S \mathbin{;} S')$, claim (i) follows from Proposition 4.14. It remains to show claim (ii). We proceed by induction on $\phi$.
– base case. This follows immediately by cont. in Definition 4.5.
– inductive step. We demonstrate the case for $\phi = \phi_1 \lor \phi_2$ and $\phi = \phi_1 \to \phi_2$, the others being similar.
– Assume $\forces_{\mathcal{B}}^{P(S \mathbin{;} S')} \phi_1 \lor \phi_2$. By $(\lor)$, the consequent of (ii) is equivalent to the following: $$\forall X \supseteq \mathcal{B},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \text{if } \phi_1 \forces_{X}^{U(\cdot)} p \text{ and } \phi_2 \forces_{X}^{U(\cdot)} p,\ \text{then } \forces_{X}^{U(P(S))} p$$ Let $V(\cdot) \in \dot{\mathcal{B}}(A)$ and $\mathcal{C} \supseteq \mathcal{B}$ and $q \in A$ be arbitrary such that $\phi_1 \forces_{\mathcal{C}}^{V(\cdot)} q$ and $\phi_2 \forces_{\mathcal{C}}^{V(\cdot)} q$. We require to show $\forces_{\mathcal{C}}^{V(P(S))} q$. By $(\lor)$ on the assumption, we have $\forces_{\mathcal{C}}^{V(P(S \mathbin{;} S'))} q$. The result follows immediately by cont. in Definition 4.5.
– Assume $\forces_{\mathcal{B}}^{P(S \mathbin{;} S')} \phi_1 \to \phi_2$. By $(\to)$ and (Inf), the consequent of (ii) is equivalent to the following: $$\forall X \supseteq \mathcal{B},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \text{if } \forces_{X}^{U} \phi_1,\ \text{then } \forces_{X}^{P(S) \mathbin{;} U} \phi_2$$ Let $V \in \mathcal{B}(A)$ and $\mathcal{C} \supseteq \mathcal{B}$ be arbitrary such that $\forces_{\mathcal{C}}^{V} \phi_1$. We require to show $\forces_{\mathcal{C}}^{P(S) \mathbin{;} V} \phi_2$. By $(\to)$ on the assumption, we have $\forces_{\mathcal{C}}^{P(S \mathbin{;} S') \mathbin{;} V} \phi_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.
□For any base $\mathcal{B}$, $S \in \mathcal{B}(A)$, $\Delta, \Delta' \in \mathcal{B}(F)$, $\Gamma(\cdot) \in \dot{\mathcal{B}}(F)$, (i) if $\forces_{\mathcal{B}}^{S} \Gamma(\Delta \mathbin{;} \Delta')$, then $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$; (ii) if $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$, then $\forces_{\mathcal{B}}^{S} \Gamma(\Delta \mathbin{;} \Delta')$.
We prove claim (i), the other being similar. We proceed by induction on $holeDepth(\Gamma(\cdot))$—if $\forces_{\mathcal{B}}^{S} \Gamma(\Delta \mathbin{;} \Delta')$, then $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$.
– base case. $holeDepth(\Gamma(\cdot)) = 0$. By Definition 3.12, $\Gamma(\cdot) = (\cdot)$, so the statement becomes: if $\forces_{\mathcal{B}}^{S} \Delta \mathbin{;} \Delta'$, then $\forces_{\mathcal{B}}^{S} \Delta$. By $(;)$, from $\forces_{\mathcal{B}}^{S} \Delta \mathbin{;} \Delta'$, infer $\exists Q_1, Q_2 \in \mathcal{B}(A)$ such that $S \succeq Q_1$, $S \succeq Q_2$, $\forces_{\mathcal{B}}^{Q_1} \Delta$, and $\forces_{\mathcal{B}}^{Q_2} \Delta'$. Hence, by monotonicity (Proposition 4.14), infer $\forces_{\mathcal{B}}^{S} \Delta$—that is, $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$.
– inductive step. Suppose $holeDepth(\Gamma(\cdot)) = d+1$ for some $d \in \mathbb{N}$. Therefore (by Definition 3.12), $\Gamma(\Delta) \equiv \Sigma(\Delta) \circ \Theta$, where $holeDepth(\Sigma(\cdot)) = d$, and $\circ$ is either $;$ or $,$. We consider the two cases of $\circ$ separately:
– $\circ = {;}$. By $(;)$, from $\forces_{\mathcal{B}}^{S} \Sigma(\Delta \mathbin{;} \Delta') \mathbin{;} \Theta$, infer $\exists Q_1, Q_2 \in \mathcal{B}(A)$ such that $S \succeq Q_1$, $S \succeq Q_2$, $\forces_{\mathcal{B}}^{Q_1} \Sigma(\Delta \mathbin{;} \Delta')$, and $\forces_{\mathcal{B}}^{Q_2} \Theta$. By the induction hypothesis (IH), $\forces_{\mathcal{B}}^{Q_1} \Sigma(\Delta)$. Hence, by $(;)$, infer $\forces_{\mathcal{B}}^{S} \Sigma(\Delta) \mathbin{;} \Theta$—that is, $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$.
– $\circ = {,}$. By $(,)$, from $\forces_{\mathcal{B}}^{S} \Sigma(\Delta \mathbin{;} \Delta') \mathbin{,} \Theta$, infer $\exists Q_1, Q_2 \in \mathcal{B}(A)$ such that $S \succeq (Q_1, Q_2)$, $\forces_{\mathcal{B}}^{Q_1} \Sigma(\Delta \mathbin{;} \Delta')$, and $\forces_{\mathcal{B}}^{Q_2} \Theta$. By the IH, from $\forces_{\mathcal{B}}^{Q_1} \Sigma(\Delta \mathbin{;} \Delta')$, infer $\forces_{\mathcal{B}}^{Q_1} \Sigma(\Delta)$. Hence, by $(,)$, infer $\forces_{\mathcal{B}}^{S} \Sigma(\Delta) \mathbin{,} \Theta$—that is, $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$. This completes the case analysis. This completes the induction.
□If $\phi \forces_{\mathcal{B}}^{S(\cdot)} \psi$ and $\psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, then $\phi \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$.
It suffices to fix some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \phi$, and prove $\forces_{\mathcal{C}}^{T(S(P))} \chi$. $\forces_{\mathcal{C}}^{P} \phi$ and $\phi \forces_{\mathcal{B}}^{S(\cdot)} \psi$ imply $\forces_{\mathcal{C}}^{S(P)} \psi$; together with $\psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, it follows that $\forces_{\mathcal{C}}^{T(S(P))} \chi$.
□This final result implies that this semantics is categorical in the sense that the B-eS of IPL by Sandqvist [40] is categorical—see Pym et al. [35]. Briefly, objects are bunches of formulae (i.e., $\mathcal{B}(F)$) and morphisms $\Gamma \to \Delta$ are pairs $\langle \mathcal{B}, S(\cdot)\rangle$ such that $\Gamma \forces_{\mathcal{B}}^{S(\cdot)} \Delta$. In this set-up, Proposition 4.14 and Proposition 4.23 enable composition to be defined as follows: $$\langle \mathcal{B}, S(\cdot)\rangle \circ \langle \mathcal{B}', T(\cdot)\rangle = \langle \mathcal{B} \cup \mathcal{B}', T(S(\cdot))\rangle$$ 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 [23].
4.4 Example: Rule-based Access Control Policies
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]—and in other systems contexts, such as the passage of people from ground-side to air-side in airports—see for example, Gheorghiu et al. [14].
Access control policies specify declaratively the conditions under which agents are intended to be able to access resources in a system. They are then implemented by operational authentication and authorization technologies. This is the context of this example in which we consider the access control policy of a movie streaming service, BunchedFlix. BunchedFlix has three films on its platform: a, b, and c. Users can become members or purchase tokens that are consumed to access the films. More specifically: – to watch a, a user must either be a member or pay three tokens – to watch b, a user must be a member – to watch 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 p denote a token; we may write $p^k := p \mathbin{,} ... \mathbin{,} p$, with k-copies, to denote k-tokens. Let m denotes membership. The following base captures the access control conditions above: $$\mathcal{A} := \{m \rhd a\} \cup \{p^k \rhd a \mid k \geq 3\} \cup \{m \rhd b\} \cup \{m \mathbin{;} p^k \rhd c \mid k \geq 2\}$$ Consider an arbitrary user, Alice: let u denote her membership status—that is, $u := m$ if Alice is a member of BunchedFlix, and $u := \emptyplus$ otherwise.
Suppose that she has k tokens on her account. To check that she has the right to watch the film $x \in \{a, b, c\}$ on BunchedFlix is modelled by the support judgement $u \forces_{\mathcal{A}}^{p^k \mathbin{;} (\cdot)} x$. Suppose Alice is indeed member of BunchedFlix and she has 4 tokens. Can she watch both film a and film c? In one sense, yes: she may watch either film. In another sense, no: she may not go through the transaction with both films in her basket at once. The first reading corresponds to the judgement $u \forces_{\mathcal{A}}^{p^4 \mathbin{;} (\cdot)} a \land c$, which indeed obtains. The second to $u \forces_{\mathcal{A}}^{p^4 \mathbin{;} (\cdot)} a \ast c$, which does not. To see this, it suffices to show that $u \forces_{\mathcal{A}}^{p^4 \mathbin{;} (\cdot)} a \land c$ fails. That is, we require an atom r, a base $\mathcal{B} \supseteq \mathcal{A}$, and a contextual bunch $U(\cdot)$ such that $a \mathbin{,} c \forces_{\mathcal{B}}^{U(\cdot)} r$ but not $\forces_{\mathcal{B}}^{U(p^4 \mathbin{;} u)} r$. Choose r to be alien to the discussion, let $\mathcal{B} = \mathcal{A} \cup \{a \mathbin{,} c \rhd r\}$, and $U(\cdot) = (\cdot)$.
Of course, being a member, Alice could watch a first and then watch c, but these are two separate transactions. Passing this information on to the BunchedFlix sales team, they may feel that this indicate a flaw in the system, and fix it in an update.
The problem here arises from the fact that membership m is treated as a single resource. If in the next update, the sales team wanted Alice to be able to complete the purchase in a single transaction, we may introduce a $!$ modality, such $!m$ represents an arbitrary amount of membership-resources. Then purchasing both transactions could be modelled as $!u \forces_{\mathcal{A}}^{p^4 \mathbin{;} (\cdot)} a \ast c$. We defer the introduction of such modalities for modelling purposes to future work.
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 delicate distinctions about access (i.e., what it means to access both films a and c). For example, all the rules of A are axioms, while the general set-up of the B-eS indeed allows rules with premisses. Indeed, it is evident that simpler logics can easily represent this example. Our purpose here is to give a simple example of how BI’s B-eS works.
It should be clear that this basic example suggests many generalizations and variations. In particular, in [14], the present authors have shown how BI’s B-eS gives rise to an ‘inferentialist resource semantics’ in which both BI’s sharing/separation interpretation and linear logic’s ‘number-of-uses’ reading of propositions as resources can be understood uniformly. It is also shown in [14] how such an inferentialist resource semantics might provide a basis for an inferentialist account of reasoning about distributed systems (cf. [4]).
5 Soundness
If $\Gamma \vdash \phi$, then $\Gamma \forces \phi$. The proof proceeds by the typical method of showing that validity respects the inductive definition of logical consequence as determined by provability; for example, the $\ast$ E-rule in NBI means we expect validity to satisfy the following: $$\text{If } \Gamma(\phi, \psi) \forces \chi \text{ and } \Delta \forces \phi \ast \psi,\ \text{then } \Gamma(\Delta) \forces \chi$$ In some cases, this requires knowing that support locally (i.e., with arbitrary base and resources) respect the corresponding rule; for example, for any base $\mathcal{B}$ and $R(\cdot) \in \dot{\mathcal{B}}(A)$, $$\text{If } \Gamma(\phi, \psi) \forces_{\mathcal{B}}^{R(\cdot)} \chi \text{ and } \forces_{\mathcal{B}}^{\Delta} \phi \ast \psi,\ \text{then } \Gamma(\Delta) \forces_{\mathcal{B}}^{R(\cdot)} \chi$$ These propositions are collected in Lemma 5.2, whose base case has been extracted as Lemma 5.3 for readability.
Given the inductive definition of $\vdash_{\mathrm{NBI}}$ (see Figure 3), it suffices to prove the following statements:
- Ax. $\phi \forces \phi$.
- E. If $\Gamma' \forces \phi$ and $\Gamma \equiv \Gamma'$, then $\Gamma \forces \phi$.
- W. If $\Gamma(\Delta) \forces \phi$, then $\Gamma(\Delta \mathbin{;} \Delta') \forces \phi$.
- C. If $\Gamma(\Delta \mathbin{;} \Delta) \forces \phi$, then $\Gamma(\Delta) \forces \phi$.
- $\top^{*}$ I. $\emptytimes \forces \top^{*}$.
- $\top^{*}$ E. If $\Gamma(\emptytimes) \forces \chi$ and $\Delta \forces \top^{*}$, then $\Gamma(\Delta) \forces \chi$.
- $\wand$ I. If $\Gamma, \phi \forces \psi$, then $\Gamma \forces \phi \wand \psi$.
- $\wand$ E. If $\Gamma \forces \phi \wand \psi$ and $\Delta \forces \phi$, then $\Gamma, \Delta \forces \psi$.
- $\ast$ I. If $\Gamma \forces \phi$ and $\Delta \forces \psi$, then $\Gamma, \Delta \forces \phi \ast \psi$.
- $\ast$ E. If $\Gamma(\phi, \psi) \forces \chi$ and $\Delta \forces \phi \ast \psi$, then $\Gamma(\Delta) \forces \chi$.
- $\top$ I. $\emptyplus \forces \top$.
- $\top$ E. If $\Gamma(\emptyplus) \forces \chi$ and $\Delta \forces \top$, then $\Gamma(\Delta) \forces \chi$.
- $\to$ I. If $\Gamma \mathbin{;} \phi \forces \psi$ then $\Gamma \forces \phi \to \psi$.
- $\to$ E. If $\Gamma \forces \phi \to \psi$ and $\Delta \forces \phi$, then $\Gamma \mathbin{;} \Delta \forces \psi$.
- $\land$ I. If $\Gamma \forces \phi$ and $\Delta \forces \psi$, then $\Gamma \mathbin{;} \Delta \forces \phi \land \psi$.
- $\land$ E. If $\Gamma(\phi \mathbin{;} \psi) \forces \chi$ and $\Delta \forces \phi \land \psi$, then $\Gamma(\Delta) \forces \chi$.
- $\lor$ I. If $\Gamma \forces \phi_i$, then $\Gamma \forces \phi_1 \lor \phi_2$, for $i = 1, 2$.
- $\lor$ E. If $\Gamma(\phi) \forces \chi$, $\Gamma(\psi) \forces \chi$, and $\Delta \forces \phi \lor \psi$, then $\Gamma(\Delta) \forces \chi$.
- $\bot$ E. If $\Gamma \forces \bot$, then $\Gamma \forces \phi$.
We consider each proposition separately. Note that some cases require subinduction, which we move to separate lemmas listed after the current proof. Ax. This holds a fortiori: according to (Inf) and Definition 4.11, $\phi \forces \phi$ says that for arbitrary base $\mathcal{X}$ and $S \in \mathcal{B}(A)$, if $\forces_{\mathcal{X}}^{S} \phi$, then $\forces_{\mathcal{X}}^{S} \phi$. E. It suffices to show that whenever $\Gamma \equiv \Gamma'$, $\forces_{\mathcal{B}}^{S} \Gamma$ iff $\forces_{\mathcal{B}}^{S} \Gamma'$. 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 trivial, so restrict attention to unitality. In particular, we verify the multiplicative case, namely $\forces_{\mathcal{B}}^{S} \Gamma \mathbin{,} \emptytimes$ iff $\forces_{\mathcal{B}}^{S} \Gamma$. By definition, $\forces_{\mathcal{B}}^{S} \Gamma \mathbin{,} \emptytimes$ iff there exist Q and R satisfying $S \succeq Q, R$ such that $\forces_{\mathcal{B}}^{Q} \Gamma$ and $\forces_{\mathcal{B}}^{R} \emptytimes$. This means $R \succeq \emptytimes$, thus $S \succeq Q, R \succeq Q, \emptytimes \equiv Q$. Therefore $\forces_{\mathcal{B}}^{S} \Gamma \mathbin{,} \emptytimes$ iff there exists $Q \preceq S$ such that $\forces_{\mathcal{B}}^{S} \Gamma$, namely $\forces_{\mathcal{B}}^{S} \Gamma$. W. We assume that $\Gamma(\Delta) \forces \phi$, and show that $\Gamma(\Delta \mathbin{;} \Delta') \forces \phi$ holds for an arbitrary $\Delta' \in \mathcal{B}(F)$. So let us fix some $\mathcal{B}$ and S such that $\forces_{\mathcal{B}}^{S} \Gamma(\Delta \mathbin{;} \Delta')$, and show that $\forces_{\mathcal{B}}^{S} \phi$. According to Lemma 4.22, $\forces_{\mathcal{B}}^{S} \Gamma(\Delta \mathbin{;} \Delta')$ implies $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$. This together with $\Gamma(\Delta) \forces \phi$ conclude that $\forces_{\mathcal{B}}^{S} \phi$. C. We assume $\Gamma(\Delta \mathbin{;} \Delta) \forces \phi$, and show that $\Gamma(\Delta) \forces \phi$. So we fix some $\mathcal{B}$ and S such that $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$, and show that $\forces_{\mathcal{B}}^{S} \phi$. By Lemma 4.22, $\forces_{\mathcal{B}}^{S} \Gamma(\Delta)$ implies $\forces_{\mathcal{B}}^{S} \Gamma(\Delta \mathbin{;} \Delta)$. This together with $\Gamma(\Delta \mathbin{;} \Delta) \forces \phi$ implies $\forces_{\mathcal{B}}^{S} \phi$. $\top^{*}$ I. It suffices to fix some $\mathcal{B}$ and S such that $\forces_{\mathcal{B}}^{S} \emptytimes$, and then show $\forces_{\mathcal{B}}^{S} \top^{*}$. By Definition 4.11, $\forces_{\mathcal{B}}^{S} \emptytimes$ if and only if $S \succeq \emptytimes$. To show $\forces_{\mathcal{B}}^{S} \top^{*}$, we fix some $\mathcal{C} \supseteq \mathcal{B}$, $P(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$, such that $\forces_{\mathcal{C}}^{P(\emptytimes)} q$, and show that $\forces_{\mathcal{C}}^{P(S)} q$. Since $S \succeq \emptytimes$, we have $P(S) \succeq P(\emptytimes)$ (Proposition 4.10). By monotonicity (Proposition 4.14), $\forces_{\mathcal{C}}^{P(\emptytimes)} q$ then implies $\forces_{\mathcal{C}}^{P(S)} q$. $\top^{*}$ E. This follows as a special case of Lemma 5.2.1. In particular, one takes there $R(\cdot)$ to be $(\cdot)$, and $\mathcal{B}$ to be the empty base $\emptyset$. $\wand$ I. We assume $\Gamma, \phi \forces \psi$, and show $\Gamma \forces \phi \wand \psi$. Towards this, we further assume some $\mathcal{B}$ and S satisfying $\forces_{\mathcal{B}}^{S} \Gamma$, and show $\forces_{\mathcal{B}}^{S} \phi \wand \psi$. By $(\wand)$, this amounts to showing $\phi \forces_{\mathcal{B}}^{S, (\cdot)} \psi$. So we in addition fix some arbitrary base $\mathcal{C} \supseteq \mathcal{B}$ and atomic bunch T such that $\forces_{\mathcal{C}}^{T} \phi$, and then verify that $\forces_{\mathcal{C}}^{S, T} \psi$. Since $\forces_{\mathcal{B}}^{S} \Gamma$ and $\mathcal{C} \supseteq \mathcal{B}$, we have $\forces_{\mathcal{C}}^{S} \Gamma$; so $\forces_{\mathcal{C}}^{S, T} \Gamma, \phi$. Together with $\Gamma, \phi \forces \psi$, it follows that $\forces_{\mathcal{C}}^{S, T} \psi$. $\wand$ E. We assume $\Gamma \forces \phi \wand \psi$ and $\Delta \forces \phi$, and prove $\Gamma, \Delta \forces \psi$. For this, we fix some arbitrary $\mathcal{B}$ and atomic bunch S such that $\forces_{\mathcal{B}}^{S} \Gamma, \Delta$, and show $\forces_{\mathcal{B}}^{S} \psi$. By definition, $\forces_{\mathcal{B}}^{S} \Gamma, \Delta$ means that there exist $T_1, T_2 \in \mathcal{B}(A)$ such that $T_1, T_2 \succeq S$, $\forces_{\mathcal{B}}^{T_1} \Gamma$, and $\forces_{\mathcal{B}}^{T_2} \Delta$. Now $\Gamma \forces \phi \wand \psi$ and $\forces_{\mathcal{B}}^{T_1} \Gamma$ imply that $\forces_{\mathcal{B}}^{T_1} \phi \wand \psi$; that is, $\phi \forces_{\mathcal{B}}^{T_1, (\cdot)} \psi$. $\Delta \forces \phi$ and $\forces_{\mathcal{B}}^{T_2} \Delta$ imply $\forces_{\mathcal{B}}^{T_2} \phi$. Then $\phi \forces_{\mathcal{B}}^{T_1, (\cdot)} \psi$ together with $\forces_{\mathcal{B}}^{T_2} \phi$ imply $\forces_{\mathcal{B}}^{T_1, T_2} \psi$, thus $\forces_{\mathcal{B}}^{S} \psi$ by Proposition 4.14. $\ast$ I. Suppose $\Gamma \forces \phi$ and $\Delta \forces \psi$, we prove that $\Gamma, \Delta \forces \phi \ast \psi$. So we fix arbitrary base $\mathcal{B}$ and $S \in \mathcal{B}(A)$ such that $\forces_{\mathcal{B}}^{S} \Gamma, \Delta$, and show that $\forces_{\mathcal{B}}^{S} \phi \ast \psi$. By $(,)$, there exist $T_1, T_2 \in \mathcal{B}(A)$ satisfying $(T_1, T_2) \succeq S$, such that $\forces_{\mathcal{B}}^{T_1} \Gamma$ and $\forces_{\mathcal{B}}^{T_2} \Delta$. The goal $\forces_{\mathcal{B}}^{S} \phi \ast \psi$ means that for arbitrary $X \supseteq \mathcal{B}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, and $p \in A$, if $\phi, \psi \forces_{X}^{U(\cdot)} p$, then $\forces_{X}^{U(S)} p$. So we fix some $\mathcal{C} \supseteq \mathcal{B}$, $P(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\phi, \psi \forces_{\mathcal{C}}^{P(\cdot)} q$, and show that $\forces_{\mathcal{C}}^{P(S)} q$. Since $\Gamma \forces \phi$ and $\forces_{\mathcal{B}}^{T_1} \Gamma$, it follows that $\forces_{\mathcal{B}}^{T_1} \phi$; since $\Delta \forces \psi$ and $\forces_{\mathcal{B}}^{T_2} \Delta$, it follows that $\forces_{\mathcal{B}}^{T_2} \psi$. So $\forces_{\mathcal{B}}^{T_1, T_2} \phi, \psi$; together with $T_1, T_2 \succeq S$, it follows that $\forces_{\mathcal{B}}^{S} \phi, \psi$ by Proposition 4.14. Together with $\phi, \psi \forces_{\mathcal{C}}^{P(\cdot)} q$ and $\mathcal{C} \supseteq \mathcal{B}$, we conclude that $\forces_{\mathcal{C}}^{P(S)} q$. $\ast$ E. This follows as a special case of Lemma 5.2.2, where one takes $\mathcal{B}$ and $R(\cdot)$ to be the empty base $\emptyset$ and the empty context $(\cdot)$, respectively. $\top$ I. It suffices to fix some base $\mathcal{B}$ and $S \in \mathcal{B}(A)$ satisfying $\forces_{\mathcal{B}}^{S} \emptyplus$, and the goal is to show $\forces_{\mathcal{B}}^{S} \top$. To this end, we further fix some arbitrary $\mathcal{C} \supseteq \mathcal{B}$ and $P(\cdot) \in \dot{\mathcal{B}}(A)$ satisfying $\forces_{\mathcal{C}}^{P(\emptyplus)} q$, and prove $\forces_{\mathcal{C}}^{P(S)} q$. Since $\forces_{\mathcal{B}}^{S} \emptyplus$ says $S \succeq \emptyplus$, by Proposition 4.14, $\forces_{\mathcal{C}}^{P(\emptyplus)} q$ implies $\forces_{\mathcal{C}}^{P(S)} q$. $\top$ E. This follows immediately from Lemma 5.2.3. $\to$ I. Fix some base $\mathcal{B}$ and $S \in \mathcal{B}(A)$ such that $\forces_{\mathcal{B}}^{S} \Gamma$, and the goal is to prove $\forces_{\mathcal{B}}^{S} \phi \to \psi$. By $(\to)$, this amounts to showing $\phi \forces_{\mathcal{B}}^{S \mathbin{;} (\cdot)} \psi$. So we further fix some $\mathcal{C} \supseteq \mathcal{B}$ and $T \in \mathcal{B}(A)$ satisfying $\forces_{\mathcal{C}}^{T} \phi$, and prove $\forces_{\mathcal{C}}^{S \mathbin{;} T} \psi$. By $(;)$, $\forces_{\mathcal{B}}^{S} \Gamma$ and $\forces_{\mathcal{C}}^{T} \phi$ imply $\forces_{\mathcal{C}}^{S \mathbin{;} T} \Gamma \mathbin{;} \phi$. Together with $\Gamma \mathbin{;} \phi \forces \psi$, it follows that $\forces_{\mathcal{C}}^{S \mathbin{;} T} \psi$. $\to$ E.
Given the assumptions, we assume some arbitrary base $\mathcal{B}$ and $S \in \mathcal{B}(A)$ such that $\forces_{\mathcal{B}}^{S} \Gamma \mathbin{;} \Delta$, and prove that $\forces_{\mathcal{B}}^{S} \psi$. By $(;)$, there exist $P, Q \in \mathcal{B}(A)$ satisfying $P \preceq S$ and $Q \preceq S$, such that $\forces_{\mathcal{B}}^{P} \Gamma$ and $\forces_{\mathcal{B}}^{Q} \Delta$. $\Gamma \vdash \phi \to \psi$ and $\forces_{\mathcal{B}}^{P} \Gamma$ imply $\forces_{\mathcal{B}}^{P} \phi \to \psi$, namely $\phi \forces_{\mathcal{B}}^{P \mathbin{;} (\cdot)} \psi$. $\Delta \forces \psi$ and $\forces_{\mathcal{B}}^{Q} \Delta$ imply $\forces_{\mathcal{B}}^{Q} \psi$. Then, by (Inf), it follows that $\forces_{\mathcal{B}}^{P \mathbin{;} Q} \psi$. Since $S \mathbin{;} S \succeq P \mathbin{;} Q$, it follows that $\forces_{\mathcal{B}}^{S \mathbin{;} S} \psi$, by Proposition 4.14. Therefore, $\forces_{\mathcal{B}}^{S} \psi$, by Proposition 4.21. $\land$ I. Suppose $\Gamma \forces \phi$ and $\Delta \forces \psi$, and we show that $\Gamma \mathbin{;} \Delta \forces \phi \land \psi$. So, we fix some arbitrary $\mathcal{B}$ and S satisfying that $\forces_{\mathcal{B}}^{S} \Gamma \mathbin{;} \Delta$, and show $\forces_{\mathcal{B}}^{S} \phi \land \psi$. Applied to $(;)$, $\forces_{\mathcal{B}}^{S} \Gamma \mathbin{;} \Delta$, there exist $P, Q \in \mathcal{B}(A)$ satisfying $P \preceq S$ and $Q \preceq S$, such that $\forces_{\mathcal{B}}^{P} \Gamma$ and $\forces_{\mathcal{B}}^{Q} \Delta$. $\Gamma \forces \phi$ and $\forces_{\mathcal{B}}^{P} \Gamma$ imply $\forces_{\mathcal{B}}^{P} \phi$. $\Delta \vdash \psi$ and $\forces_{\mathcal{B}}^{Q} \Delta$ imply $\forces_{\mathcal{B}}^{Q} \psi$. In order to show $\forces_{\mathcal{B}}^{S} \phi \land \psi$, we fix some $\mathcal{C} \supseteq \mathcal{B}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\phi \mathbin{;} \psi \forces_{\mathcal{C}}^{R(\cdot)} q$, and prove $\forces_{\mathcal{C}}^{R(S)} q$. Since $\forces_{\mathcal{B}}^{P} \phi$, $\forces_{\mathcal{B}}^{Q} \psi$, $P \preceq S$, and $Q \preceq S$, it follows by $(;)$ that $\forces_{\mathcal{B}}^{S} \phi \mathbin{;} \psi$. This together with $\phi \mathbin{;} \psi \forces_{\mathcal{C}}^{R(\cdot)} q$ imply $\forces_{\mathcal{C}}^{R(S)} q$. $\land$ E. This follows as a special case of Lemma 5.2.4. $\lor$ I. Without loss of generality, assume that $\Gamma \vdash \phi_1$ and show that $\Gamma \vdash \phi_1 \lor \phi_2$. So let us assume some arbitrary base $\mathcal{B}$ and $S \in \mathcal{B}(A)$ such that $\forces_{\mathcal{B}}^{S} \Gamma$, and show that $\forces_{\mathcal{B}}^{S} \phi_1 \lor \phi_2$. Under $(\lor)$, this amounts to showing that: $$\forall X \supseteq \mathcal{B},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \text{if } \phi_i \forces_{X}^{U(\cdot)} p \text{ for } i = 1, 2,\ \text{then } \forces_{X}^{U(S)} p$$ So, we fix some arbitrary $\mathcal{C} \supseteq \mathcal{B}$, $T(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\phi_i \forces_{\mathcal{C}}^{T(\cdot)} q$ for $i = 1, 2$, and then prove that $\forces_{\mathcal{C}}^{T(S)} q$. Note that $\forces_{\mathcal{B}}^{S} \Gamma$ and $\Gamma \forces \phi_1$ imply that $\forces_{\mathcal{B}}^{S} \phi_1$. This together with $\phi_1 \forces_{\mathcal{C}}^{T(\cdot)} q$ entail that $\forces_{\mathcal{C}}^{T(S)} q$. $\lor$ E. Follows immediately from Lemma 5.2.5. $\bot$ E. We assume $\Gamma \forces \bot$, and show that $\Gamma \forces \phi$. So we fix some base $\mathcal{B}$ and atomic bunch S such that $\forces_{\mathcal{B}}^{S} \Gamma$, and show that $\forces_{\mathcal{B}}^{S} \phi$. $\forces_{\mathcal{B}}^{S} \Gamma$ and $\Gamma \forces \bot$ imply $\forces_{\mathcal{B}}^{S} \bot$. Then by Lemma 5.2.6, it follows immediately that $\forces_{\mathcal{B}}^{S} \phi$. This completes the induction.
□For any base $\mathcal{B}$ and $R(\cdot) \in \dot{\mathcal{B}}(A)$, the following hold:
- If $\Gamma(\emptytimes) \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \top^{*}$, then $\Gamma(\Delta) \forces_{\mathcal{B}}^{R(\cdot)} \chi$.
- If $\Gamma(\phi, \psi) \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \phi \ast \psi$, then $\Gamma(\Delta) \forces_{\mathcal{B}}^{R(\cdot)} \chi$.
- If $\Gamma(\emptyplus) \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \top$, then $\Gamma(\Delta) \forces_{\mathcal{B}}^{R(\cdot)} \chi$.
- If $\Gamma(\phi \mathbin{;} \psi) \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \phi \land \psi$, then $\Gamma(\Delta) \forces_{\mathcal{B}}^{R(\cdot)} \chi$.
- If $\Delta \forces \phi \lor \psi$, $\Gamma(\phi) \forces_{\mathcal{B}}^{R(\cdot)} \chi$, and $\Gamma(\psi) \forces_{\mathcal{B}}^{R(\cdot)} \chi$, then $\Gamma(\Delta) \forces_{\mathcal{B}}^{R(\cdot)} \chi$.
- For any formula $\phi$, $\bot \forces_{\mathcal{B}}^{R(\cdot)} \phi$.
We proceed by induction on the size of $holeDepth(\Gamma(\cdot))$.
– base case. $holeDepth(\Gamma(\cdot)) = 0$. This means $\Gamma(\cdot)$ is of the form $(\cdot)$. The proposition to be proven becomes: if $\emptytimes \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \top^{*}$, then $\Delta \forces_{\mathcal{B}}^{R(\cdot)} \chi$. This follows immediately from Lemma 5.3.1.
– inductive step. $holeDepth(\Gamma(\cdot)) = d + 1$ for some $d \geq 0$. This $\Gamma(\cdot)$ is coherently equivalent to $\Sigma(\cdot) \circ \Theta$, where $\circ \in \{;, {,}\}$, $\Sigma(\cdot) \in \dot{\mathcal{B}}(F)$, $\Theta \in \mathcal{B}(F)$ and $holeDepth(\Sigma(\cdot)) = d$. We consider the two cases for $\circ$ separately:
– $\circ$ is $,$. Given $\Sigma(\emptytimes), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \top^{*}$, the goal is to show that $\Sigma(\Delta), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$. To this, we fix some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \Sigma(\Delta), \Theta$, and show that $\forces_{\mathcal{C}}^{R(P)} \chi$ holds as well. $\forces_{\mathcal{C}}^{P} \Sigma(\Delta), \Theta$ means that there exist $P_1, P_2 \in \mathcal{B}(A)$ such that $P_1, P_2 \succeq P$, $\forces_{\mathcal{C}}^{P_1} \Sigma(\Delta)$, and $\forces_{\mathcal{C}}^{P_2} \Theta$. This together with $\Sigma(\emptytimes), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$ imply that, for arbitrary $X \supseteq \mathcal{C}$ and $U \in \mathcal{B}(A)$, if $\forces_{X}^{U} \Sigma(\emptytimes)$, then $\forces_{X}^{R(U, P_2)} \chi$; that is, $\Sigma(\emptytimes) \forces_{\mathcal{C}}^{R((\cdot), P_2)} \chi$. Since $holeDepth(\Sigma(\cdot)) = d$, we can apply IH to $\Sigma(\emptytimes) \forces_{\mathcal{C}}^{R((\cdot), P_2)} \chi$ and $\Delta \forces \top^{*}$ to conclude that $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot), P_2)} \chi$. Since $\forces_{\mathcal{C}}^{P_1} \Sigma(\Delta)$, we have $\forces_{\mathcal{C}}^{R(P_1, P_2)} \chi$, thus $\forces_{\mathcal{C}}^{R(P)} \chi$.
– $\circ$ is $;$. Given $\Sigma(\emptytimes) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \top^{*}$, the goal is to show that $\Sigma(\Delta) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$. So we fix some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \Sigma(\Delta) \mathbin{;} \Theta$, and prove $\forces_{\mathcal{C}}^{R(P)} \chi$. By definition, $\forces_{\mathcal{C}}^{P} \Sigma(\Delta) \mathbin{;} \Theta$ says that there exists $P_1, P_2 \in \mathcal{B}(A)$ such that $P_i \succeq P$ for $i = 1, 2$, $\forces_{\mathcal{C}}^{P_1} \Sigma(\Delta)$, and $\forces_{\mathcal{C}}^{P_2} \Theta$. Spelling out $\Gamma(\emptytimes) \forces_{\mathcal{B}}^{R(\cdot)} \chi$, we have: $$\forall X \supseteq \mathcal{B},\ \forall U \in \mathcal{B}(A),\ \text{if } \exists U_1, U_2 \text{ s.t. } U_1 \succeq U,\ U_2 \succeq U,\ \forces_{X}^{U_1} \Sigma(\emptytimes),\ \forces_{X}^{U_2} \Theta,\ \text{then } \forces_{X}^{R(U)} \chi \tag{1}$$ Since $\forces_{\mathcal{C}}^{P_2} \Theta$, (1) entails: $$\forall X \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } P_2 \succeq U \text{ and } \exists U_1 \succeq U \text{ s.t. } \forces_{X}^{U_1} \Sigma(\emptytimes),\ \text{then } \forces_{X}^{R(U)} \chi$$ thus, $$\forall X \supseteq \mathcal{C},\ \forall U_1 \in \mathcal{B}(A),\ \text{if } \forces_{X}^{U_1} \Sigma(\emptytimes),\ \text{then } \forces_{X}^{R(U_1 \mathbin{;} P_2)} \chi$$ By definition, this precisely says $\Sigma(\emptytimes) \forces_{X}^{R((\cdot) \mathbin{;} P_2)} \chi$. Since $holeDepth(\Sigma(\cdot)) = d$, we apply IH to this and $\Delta \forces \top^{*}$, and conclude $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} P_2)} \chi$. Together with $\forces_{\mathcal{C}}^{P_1} \Sigma(\Delta)$, we have $\forces_{\mathcal{C}}^{R(P_1 \mathbin{;} P_2)} \chi$. Since $P_i \succeq P$ for $i = 1, 2$, by Proposition 4.14, $\forces_{\mathcal{C}}^{R(P_1 \mathbin{;} P_2)} \chi$ implies $\forces_{\mathcal{C}}^{R(P \mathbin{;} P)} \chi$, thus $\forces_{\mathcal{C}}^{R(P)} \chi$. This completes the inductive proof. Proof of Lemma 5.2.2. We proceed by induction on $holeDepth(\Gamma(\cdot))$.
– base case. $holeDepth(\Gamma(\cdot)) = 0$. That is, $\Gamma(\cdot) = (\cdot)$. Then the proposition becomes: if $\phi, \psi \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \phi \ast \psi$, then $\Delta \forces_{\mathcal{B}}^{R(\cdot)} \chi$. This follows immediately from Lemma 5.3.2.
– inductive step. $holeDepth(\Gamma(\cdot)) = d + 1$ for $d \geq 0$. There are two cases, depending on the principal context former of $\Gamma(\cdot)$ is $;$ or $,$ (note that $\Gamma(\cdot)$ must have a principal context-former given its depth).
– $\Gamma(\cdot)$ is coherently equivalent to $\Sigma(\cdot) \mathbin{;} \Theta$, where $holeDepth(\Sigma(\cdot)) = d$, and $\Theta \in \mathcal{B}(A)$. We assume the premises of the proposition as well as $\forces_{\mathcal{C}}^{S} \Gamma(\Delta)$ for some $\mathcal{C} \supseteq \mathcal{B}$ and $S \in \mathcal{B}(A)$. The goal is to prove $\forces_{\mathcal{C}}^{R(S)} \chi$. By the definition of $;$, $\forces_{\mathcal{C}}^{S} \Sigma(\Delta) \mathbin{;} \Theta$ means that there exist $P, Q \in \mathcal{B}(A)$, such that $P \succeq S$, $Q \succeq S$, $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$, and $\forces_{\mathcal{C}}^{Q} \Theta$. $\Sigma(\phi, \psi) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$ says that, for arbitrary $X \supseteq \mathcal{B}$ and $W \in \mathcal{B}(A)$, $\forces_{X}^{W} \Sigma(\phi, \psi) \mathbin{;} \Theta$ implies $\forces_{X}^{R(W)} \chi$. It is further spelled out as: $$\text{for arbitrary } X \supseteq \mathcal{B},\ W \in \mathcal{B}(A),\ \text{if } \exists U \succeq W, V \succeq W \text{ s.t. } \forces_{X}^{U} \Sigma(\phi, \psi) \text{ and } \forces_{X}^{V} \Theta,\ \text{then } \forces_{X}^{R(W)} \chi \tag{2}$$ Since $\mathcal{C} \supseteq \mathcal{B}$, and $Q \succeq S$ satisfies $\forces_{\mathcal{C}}^{Q} \Theta$, (2) entails the following: $$\forall X \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{\mathcal{C}}^{U} \Sigma(\phi, \psi),\ \text{then } \forces_{X}^{R(Q \mathbin{;} U)} \chi \tag{3}$$ This is the judgment $\Sigma(\phi, \psi) \forces_{\mathcal{C}}^{R(Q \mathbin{;} (\cdot))} \chi$, by definition. Since $holeDepth(\Sigma(\cdot)) = d$, we can apply induction hypothesis to $\Sigma(\phi, \psi) \forces_{\mathcal{C}}^{R(Q \mathbin{;} (\cdot))} \chi$ and $\Delta \forces \phi \ast \psi$, it follows that $\Gamma(\Delta) \forces_{\mathcal{C}}^{R(Q \mathbin{;} (\cdot))} \chi$. This together with $\forces_{\mathcal{C}}^{P} \Gamma(\Delta)$ implies $\forces_{\mathcal{C}}^{R(P \mathbin{;} Q)} \chi$, hence $\forces_{\mathcal{C}}^{R(S \mathbin{;} S)} \chi$ by $(P \mathbin{;} Q) \succeq (S \mathbin{;} S)$ and Proposition 4.14; hence $\forces_{\mathcal{C}}^{R(S)} \chi$ by Proposition 4.21.
– $\Gamma(\cdot)$ is coherently equivalent to $\Sigma(\cdot) \mathbin{,} \Theta$, where $\Sigma(\cdot) \in \dot{\mathcal{B}}(A)$, $\Theta \in \mathcal{B}(A)$, and $holeDepth(\Sigma(\cdot)) = d$. We assume the premises of the proposition as well as $\forces_{\mathcal{C}}^{S} \Gamma(\Delta)$ for some $\mathcal{C} \supseteq \mathcal{B}$ and $S \in \mathcal{B}(A)$. The goal is to prove $\forces_{\mathcal{C}}^{R(S)} \chi$. According to $(,)$, $\forces_{\mathcal{C}}^{S} \Sigma(\Delta), \Theta$ means that there exist $P, Q \in \mathcal{B}(A)$ satisfying $(P, Q) \succeq S$, such that $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$ and $\forces_{\mathcal{C}}^{Q} \Theta$. Also, $\Gamma(\phi, \psi) \forces_{\mathcal{B}}^{R(\cdot)} \chi$ says, for arbitrary $X \supseteq \mathcal{B}$ and $W \in \mathcal{B}(A)$, $\forces_{X}^{W} \Gamma(\phi, \psi)$ implies $\forces_{X}^{R(W)} \chi$. This, according to the form of $\Gamma(\cdot)$, boils down to the following: $$\forall X \supseteq \mathcal{B},\ \forall W \in \mathcal{B}(A),\ \text{if } \exists U, V \in \mathcal{B}(A) \text{ s.t. } U, V \succeq W,\ \forces_{X}^{U} \Sigma(\phi, \psi),\ \text{and } \forces_{X}^{V} \Theta,\ \text{then } \forces_{X}^{R(W)} \chi \tag{4}$$ Take into consideration $\mathcal{C} \supseteq \mathcal{B}$ and $\forces_{\mathcal{C}}^{Q} \Theta$, (4) entails the follows: $$\forall X \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{X}^{U} \Sigma(\phi, \psi),\ \text{then } \forces_{X}^{R(U, Q)} \chi \tag{5}$$ This is exactly $\Sigma(\phi, \psi) \forces_{\mathcal{C}}^{R((\cdot), Q)} \chi$. Now apply the induction hypothesis to $\Sigma(\phi, \psi) \forces_{\mathcal{C}}^{R((\cdot), Q)} \chi$ and $\Delta \forces \phi \ast \psi$, one get $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot), Q)} \chi$. This together with $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$ entails that $\forces_{\mathcal{C}}^{R(P, Q)} \chi$. Since $S \succeq P, Q$, it follows that $\forces_{\mathcal{C}}^{R(S)} \chi$. This completes the proof by induction.
Proof of Lemma 5.2.3. The proof follows a similar strategy as that for ∗, namely Lemma 1. In particular, it follows from a proof by induction on $holeDepth(\Gamma(\cdot)),$ whose base case is deduced from an analogy to
□We proceed by induction on the size of $holeDepth(\Gamma(\cdot))$.
– base case. $holeDepth(\Gamma(\cdot)) = 0$. That is, $\Gamma(\cdot) \equiv (\cdot)$. Then the proposition amounts to: if $\phi \mathbin{;} \psi \forces_{\mathcal{B}}^{R(\cdot)} \chi$ and $\Delta \forces \phi \land \psi$, then $\Delta \forces_{\mathcal{B}}^{R(\cdot)} \chi$. This is an immediate consequence of Lemma 5.3.3.
– inductive step. $holeDepth(\Gamma(\cdot)) = d + 1$ for some $d \geq 0$. The analysis consist of two cases wrt the principal context-former of $\Gamma(\cdot)$ being $;$ or $,$. In both cases, we assume the premises of the proposition as well as $\forces_{\mathcal{C}}^{S} \Gamma(\Delta)$ for some arbitrary fixed $\mathcal{C} \supseteq \mathcal{B}$ and S, and the goal is to show $\forces_{\mathcal{C}}^{R(S)} \chi$.
– $\Gamma(\cdot)$ is coherently equivalent to $\Sigma(\cdot) \mathbin{;} \Theta$, where $\Theta \in \mathcal{B}(A)$, $\Sigma(\cdot) \in \dot{\mathcal{B}}(A)$, and $holeDepth(\Sigma(\cdot)) = d$. By definition, $\forces_{\mathcal{C}}^{S} \Sigma(\Delta) \mathbin{;} \Theta$ means that there exist $P, Q \in \mathcal{B}(A)$ satisfying $P \succeq S$, $Q \succeq S$, such that $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$ and $\forces_{\mathcal{C}}^{Q} \Theta$. By the definition of $\Sigma(\phi \mathbin{;} \psi) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, we have that for arbitrary $X \supseteq \mathcal{B}$ and W, if $\forces_{X}^{W} \Sigma(\phi \mathbin{;} \psi) \mathbin{;} \Theta$, then $\forces_{X}^{R(W)} \chi$. This means: $$\forall X \supseteq \mathcal{C},\ \forall W \in \mathcal{B}(A),\ \text{if } \exists U, V \in \mathcal{B}(A) \text{ s.t. } U \succeq W, V \succeq W,\ \forces_{X}^{U} \Sigma(\phi \mathbin{;} \psi),\ \text{and } \forces_{X}^{V} \Theta,\ \text{then } \forces_{\mathcal{C}}^{R(W)} \chi \tag{6}$$ Since $\forces_{\mathcal{C}}^{Q} \Theta$, it follows that: $$\forall X \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{X}^{U} \Sigma(\phi \mathbin{;} \psi),\ \text{then } \forces_{X}^{R(U \mathbin{;} Q)} \chi \tag{7}$$ In other words, $\Sigma(\phi \mathbin{;} \psi) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q)} \chi$. Remember that we have $holeDepth(\Sigma(\cdot)) = d$, so we can apply the induction hypothesis to $\Sigma(\phi \mathbin{;} \psi) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q)} \chi$ and $\Delta \forces \phi \land \psi$ to conclude that $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q)} \chi$. This together with $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$ imply that $\forces_{\mathcal{C}}^{R(P \mathbin{;} Q)} \chi$; hence $\forces_{\mathcal{C}}^{R(S \mathbin{;} S)} \chi$ by Proposition 4.14 and $P \mathbin{;} Q \succeq S \mathbin{;} S$; hence $\forces_{\mathcal{C}}^{R(S)} \chi$ by Lemma 4.22.
– $\Gamma(\cdot)$ is coherently equivalent to $\Sigma(\cdot) \mathbin{,} \Theta$, where $\Sigma(\cdot) \in \dot{\mathcal{B}}(A)$, $\Theta \in \mathcal{B}(A)$, and $holeDepth(\Sigma(\cdot)) = d$. By $(,)$, $\forces_{\mathcal{C}}^{S} \Sigma(\Delta), \Theta$ means that there exist $P, Q \in \mathcal{B}(A)$ satisfying $P, Q \succeq S$, such that $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$ and $\forces_{\mathcal{C}}^{Q} \Theta$. Then $\Sigma(\phi \mathbin{;} \psi), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$ means: $$\forall X \supseteq \mathcal{B},\ \forall W \in \mathcal{B}(A),\ \text{if } \exists U, V \in \mathcal{B}(A) \text{ s.t. } U, V \succeq W,\ \forces_{X}^{U} \Sigma(\phi \mathbin{;} \psi),\ \text{and } \forces_{X}^{V} \Theta,\ \text{then } \forces_{X}^{R(W)} \chi$$ Since $\forces_{\mathcal{C}}^{Q} \Theta$, it follows that: $$\forall X \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{X}^{U} \Sigma(\phi \mathbin{;} \psi),\ \text{then } \forces_{X}^{R(U, Q)} \chi \tag{8}$$ That is, $\Sigma(\phi \mathbin{;} \psi) \forces_{\mathcal{C}}^{R((\cdot), Q)} \chi$. Then, apply the IH for $\Sigma(\cdot)$ to $\Sigma(\phi \mathbin{;} \psi) \forces_{\mathcal{C}}^{R((\cdot), Q)} \chi$ and $\Delta \forces \phi \land \psi$, it follows that $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot), Q)} \chi$. Together with $\forces_{\mathcal{C}}^{P} \Sigma(\Delta)$, it follows that $\forces_{\mathcal{C}}^{R(P, Q)} \chi$. So $\forces_{\mathcal{C}}^{R(S)} \chi$, by $P, Q \succeq S$ and Proposition 4.14. This completes the inductive proof. Proof of Lemma 5.2.5. We proceed by induction on $holeDepth(\Gamma(\cdot)).$– base case. $holeDepth(\Gamma(\cdot))$= 0. This means $\Gamma(\cdot)$ is of the form $(\cdot).$ The statement becomes: If $\phi \forces_{\mathcal{B}}^{R(\cdot)} \chi$, $\psi \forces_{\mathcal{B}}^{R(\cdot)} \chi$, and $\Delta \forces \phi \lor \psi$, then $\Delta \forces_{\mathcal{B}}^{R(\cdot)} \chi$. This follows immediately from Lemma 5.3.4.
– inductive step. $holeDepth(\Gamma(\cdot)) = d + 1$ for some $d \geq 0$. Then $\Gamma(\cdot)$ is of the form $\Sigma(\cdot) \circ \Theta$, where $\circ \in \{;, {,}\}$, $\Sigma(\cdot) \in \dot{\mathcal{B}}(A)$, $\Theta \in \mathcal{B}(A)$, and $holeDepth(\Sigma(\cdot)) = d$. We make a case distinction on $\circ$.
– $\circ$ is $;$. Given $\Sigma(\phi) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, $\Sigma(\psi) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, and $\Delta \forces \phi \lor \psi$, we assume $\forces_{\mathcal{C}}^{P} \Gamma(\Delta)$ for some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$. The goal is to show $\forces_{\mathcal{C}}^{R(P)} \chi$. First, $\forces_{\mathcal{C}}^{P} \Sigma(\Delta) \mathbin{;} \Theta$ means that there exist $Q_1, Q_2 \in \mathcal{B}(A)$ satisfying $Q_1 \succeq P$, $Q_2 \succeq P$, such that $\forces_{\mathcal{C}}^{Q_1} \Sigma(\Delta)$ and $\forces_{\mathcal{C}}^{Q_2} \Theta$. Next we show that $\Sigma(\phi) \forces_{\mathcal{B}}^{R((\cdot) \mathbin{;} Q_2)} \chi$ and $\Sigma(\psi) \forces_{\mathcal{B}}^{R((\cdot) \mathbin{;} Q_2)} \chi$ hold, which enables the application of IH. We only look at $\Sigma(\phi) \forces_{\mathcal{B}}^{R((\cdot) \mathbin{;} Q_2)} \chi$, and that for $\psi$ is exactly the same by replacing $\phi$ with $\psi$. Spelling out the definition of $\Sigma(\phi) \mathbin{;} \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, we have: $$\forall X \supseteq \mathcal{B},\ \forall W \in \mathcal{B}(A),\ \text{if } \exists U, V \in \mathcal{B}(A) \text{ s.t. } U \succeq W, V \succeq W,\ \forces_{X}^{U} \Sigma(\phi),\ \text{and } \forces_{X}^{V} \Theta,\ \text{then } \forces_{X}^{R(W)} \chi \tag{9}$$ Given $\mathcal{C} \supseteq \mathcal{B}$ and $\forces_{\mathcal{C}}^{Q_2} \Theta$, (9) implies: $$\forall Y \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{Y}^{U} \Sigma(\phi),\ \text{then } \forces_{Y}^{R(U \mathbin{;} Q_2)} \chi \tag{10}$$ This is precisely $\Sigma(\phi) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q_2)} \chi$. Now with $\Delta \forces \phi \lor \psi$, $\Sigma(\phi) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q_2)} \chi$, and $\Sigma(\psi) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q_2)} \chi$ in hand, we can apply IH to conclude $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot) \mathbin{;} Q_2)} \chi$. Together with $\forces_{\mathcal{C}}^{Q_1} \Sigma(\Delta)$, it follows that $\forces_{\mathcal{C}}^{R(Q_1 \mathbin{;} Q_2)} \chi$. Since $Q_1 \mathbin{;} Q_2 \succeq P \mathbin{;} P$, by Proposition 4.14 we have $\forces_{\mathcal{C}}^{R(P \mathbin{;} P)} \chi$, and it implies $\forces_{\mathcal{C}}^{R(P)} \chi$, by Proposition 4.21.
– $\circ$ is $,$. Given $\Sigma(\phi), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, $\Sigma(\psi), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, and $\Delta \forces \phi \lor \psi$, we assume $\forces_{\mathcal{C}}^{P} \Gamma(\Delta)$ for some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$. The goal is to show $\forces_{\mathcal{C}}^{R(P)} \chi$. First, $\forces_{\mathcal{C}}^{P} \Sigma(\Delta), \Theta$ means that there exist $Q_1, Q_2 \in \mathcal{B}(A)$ satisfying $Q_1, Q_2 \succeq P$, such that $\forces_{\mathcal{C}}^{Q_1} \Sigma(\Delta)$ and $\forces_{\mathcal{C}}^{Q_2} \Theta$. Next we show that $\Sigma(\phi) \forces_{\mathcal{B}}^{R((\cdot), Q_2)} \chi$ and $\Sigma(\psi) \forces_{\mathcal{B}}^{R((\cdot), Q_2)} \chi$ hold, which enables the application of IH. We only look at $\Sigma(\phi) \forces_{\mathcal{B}}^{R((\cdot), Q_2)} \chi$, and that for $\psi$ is exactly the same by replacing $\phi$ with $\psi$. Spelling out the definition of $\Sigma(\phi), \Theta \forces_{\mathcal{B}}^{R(\cdot)} \chi$, we have: $$\forall X \supseteq \mathcal{B},\ \forall W \in \mathcal{B}(A),\ \text{if } \exists U, V \in \mathcal{B}(A) \text{ s.t. } U, V \succeq W,\ \forces_{X}^{U} \Sigma(\phi),\ \text{and } \forces_{X}^{V} \Theta,\ \text{then } \forces_{X}^{R(W)} \chi \tag{11}$$ Given $\mathcal{C} \supseteq \mathcal{B}$ and $\forces_{\mathcal{C}}^{Q_2} \Theta$, (11) implies: $$\forall Y \supseteq \mathcal{C},\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{Y}^{U} \Sigma(\phi),\ \text{then } \forces_{Y}^{R(U, Q_2)} \chi \tag{12}$$ This is precisely $\Sigma(\phi) \forces_{\mathcal{C}}^{R((\cdot), Q_2)} \chi$. Now with $\Delta \forces \phi \lor \psi$, $\Sigma(\phi) \forces_{\mathcal{C}}^{R((\cdot), Q_2)} \chi$, and $\Sigma(\psi) \forces_{\mathcal{C}}^{R((\cdot), Q_2)} \chi$ in hand, we can apply IH to conclude $\Sigma(\Delta) \forces_{\mathcal{C}}^{R((\cdot), Q_2)} \chi$. Together with $\forces_{\mathcal{C}}^{Q_1} \Sigma(\Delta)$, it follows that $\forces_{\mathcal{C}}^{R(Q_1, Q_2)} \chi$, so $\forces_{\mathcal{C}}^{R(P)} \chi$ by $P \succeq Q_1, Q_2$ and Proposition 4.14. This completes the inductive proof.
We proceed by induction on the structure of $\phi$.
– When $\phi$ is atomic, the desired statement follows immediately from $(\bot)$.
– $\phi = \Sigma \ast \tau$. We assume some $\mathcal{C} \supseteq \mathcal{B}$ and P such that $\forces_{\mathcal{C}}^{P} \bot$. The goal is to show $\forces_{\mathcal{C}}^{R(P)} \Sigma \ast \tau$; in other words, for arbitrary $X \supseteq \mathcal{C}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, and p, if $\Sigma, \tau \forces_{X}^{U(\cdot)} p$, then $\forces_{X}^{U(R(P))} p$. So we fix some $D \supseteq \mathcal{C}$, $T \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma, \tau \forces_{D}^{T(\cdot)} q$. The goal is then to show $\forces_{D}^{T(R(P))} q$. By $(\bot)$, this follows immediately from $\forces_{\mathcal{C}}^{P} \bot$ and $D \supseteq \mathcal{C}$.
– $\phi = \top^{*}$. Given some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \bot$, we prove $\forces_{\mathcal{C}}^{R(P)} \top^{*}$. So we further fix some $D \supseteq \mathcal{C}$, $T(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\forces_{D}^{T(R(\emptytimes))} q$, and prove $\forces_{D}^{T(R(P))} q$. Again, this follows immediately from $\forces_{\mathcal{C}}^{P} \bot$ by $(\bot)$.
– $\phi = \Sigma \wand \tau$. Given some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \bot$, we prove $\forces_{\mathcal{C}}^{R(P)} \Sigma \wand \tau$; by $(\to)$, we prove $\Sigma \forces_{\mathcal{C}}^{R(P), (\cdot)} \tau$. So, assume further some $D \supseteq \mathcal{C}$ and $Q \in \mathcal{B}(A)$ satisfying $\forces_{D}^{Q} \Sigma$, the goal is to prove $\forces_{D}^{R(P), Q} \tau$. We apply IH for $\tau$ which says $\bot \forces_{\mathcal{C}}^{R(\cdot), Q} \tau$, and with $\forces_{\mathcal{C}}^{P} \bot$ we have $\forces_{D}^{R(P), Q} \tau$.
– The case for $\land$, $\top$, and $\to$ are similar to that for $\ast$, $\top^{*}$, and $\wand$, respectively, so we do not elaborate here.
– $\phi = \Sigma \lor \tau$. Given some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \bot$, we prove $\forces_{\mathcal{C}}^{R(P)} \Sigma \lor \tau$. To this end, we further fix some arbitrary $D \supseteq \mathcal{C}$, $T(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ satisfying $\Sigma \forces_{D}^{T(\cdot)} q$, $\tau \forces_{D}^{T(\cdot)} q$, and the goal is to show $\forces_{D}^{T(R(P))} q$. This follows immediately from $\forces_{\mathcal{C}}^{P} \bot$ by $(\bot)$.
– $\phi = \bot$. This immediately follows from $(\bot)$. This completes the inductive proof.
□The following results state the base cases necessary for the inductions in Lemma 5.2.
The following hold:
- If $\emptytimes \forces_{\mathcal{B}}^{T(\cdot)} \chi$ and $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \top^{*}$, then $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$.
- If $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \phi \ast \psi$ and $\phi, \psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, then $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$.
- If $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \phi \land \psi$ and $\phi \mathbin{;} \psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, then $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$.
- If $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \phi \lor \psi$, $\phi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, and $\psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, then $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$.
Assume (A) $\emptytimes \forces_{\mathcal{B}}^{T(\cdot)} \chi$ and (B) $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \top^{*}$. We require to show (C) $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$. We fix some $\mathcal{C} \supseteq \mathcal{B}$ and P such that $\forces_{\mathcal{C}}^{P} \Delta$, and the goal is to show $\forces_{\mathcal{C}}^{T(S(P))} \chi$. From (B) and $\forces_{\mathcal{C}}^{P} \Delta$, we have $\forces_{\mathcal{C}}^{S(P)} \top^{*}$. It suffices to prove the following for arbitrary $Q \in \mathcal{B}(A)$: $$\text{if } \emptytimes \forces_{\mathcal{B}}^{T(\cdot)} \chi \text{ and } \forces_{\mathcal{C}}^{Q} \top^{*},\ \text{then } \forces_{\mathcal{C}}^{T(Q)} \chi \tag{13}$$ This is because by taking Q to be S(P) in (13), one immediately has $\forces_{\mathcal{C}}^{T(S(P))} \chi$. Furthermore, since $\forces_{X}^{U} \emptytimes$ iff $U \succeq \emptytimes$, (13) is equivalent to: $$\text{if } \forces_{X}^{T(U)} \chi,\ \text{for arbitrary } X \supseteq \mathcal{B} \text{ and } U \succeq \emptytimes,\ \text{and } \forces_{\mathcal{C}}^{Q} \top^{*},\ \text{then } \forces_{\mathcal{C}}^{T(Q)} \chi \tag{14}$$ Therefore, it suffices to show: $$\text{if } \forces_{X}^{T(\emptytimes)} \chi,\ \text{for arbitrary } X \supseteq \mathcal{B},\ \text{and } \forces_{\mathcal{C}}^{Q} \top^{*},\ \text{then } \forces_{\mathcal{C}}^{T(Q)} \chi \tag{15}$$ In other words, the goal is to show: if $\forces_{\mathcal{B}}^{T(\emptytimes)} \chi$ and $\forces_{\mathcal{C}}^{Q} \top^{*}$, then $\forces_{\mathcal{C}}^{T(Q)} \chi$. We prove (15) by induction on the structure of $\chi$:
– $\chi$ is atomic, say it is some $p \in A$. By definition, $\forces_{\mathcal{C}}^{Q} \top^{*}$ means for arbitrary $X \supseteq \mathcal{C}$, $\forces_{X}^{T(\emptytimes)} p$ implies $\forces_{X}^{T(Q)} p$. The desired result obtains by choosing $X = \mathcal{C}$.
– $\chi = \Sigma \land \tau$. In order to prove $\forces_{\mathcal{C}}^{T(Q)} \Sigma \land \tau$, we fix some arbitrary $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$ and $q \in A$ such that $\Sigma \mathbin{;} \tau \forces_{D}^{R(\cdot)} q$, and the goal is to prove $\forces_{D}^{R(T(Q))} q$. Now $\forces_{\mathcal{B}}^{T(\emptytimes)} \Sigma \land \tau$ together with $\Sigma \mathbin{;} \tau \forces_{D}^{R(\cdot)} q$ entail $\forces_{D}^{R(T(\emptytimes))} q$. This together with $\forces_{\mathcal{C}}^{Q} \top^{*}$ and $D \supseteq \mathcal{C}$ imply $\forces_{D}^{R(T(Q))} q$.
– $\chi = \top$. In order to prove $\forces_{\mathcal{C}}^{T(Q)} \top$, we fix some arbitrary $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ satisfying $\forces_{D}^{R(\emptyplus)} q$, and show that $\forces_{D}^{R(T(Q))} q$. $\forces_{\mathcal{B}}^{T(\emptytimes)} \top$ together with $\forces_{D}^{R(\emptyplus)} q$ imply $\forces_{D}^{R(T(\emptytimes))} q$. This together with $\forces_{\mathcal{C}}^{Q} \top^{*}$ imply $\forces_{D}^{R(T(Q))} q$ by $(\top^{*})$.
– $\chi = \Sigma \to \tau$. We apply $(\to)$ to (15) and get: if $\Sigma \forces_{X}^{T(\emptytimes) \mathbin{;} (\cdot)} \tau$, for arbitrary $X \supseteq \mathcal{B}$, and $\forces_{\mathcal{C}}^{Q} \top^{*}$, then $\Sigma \forces_{\mathcal{C}}^{T(Q) \mathbin{;} (\cdot)} \tau$. Given the assumptions, to prove $\Sigma \forces_{\mathcal{C}}^{T(Q) \mathbin{;} (\cdot)} \tau$, we fix some $D \supseteq \mathcal{C}$ and $R \in \mathcal{B}(A)$ such that $\forces_{D}^{R} \Sigma$, and show $\forces_{D}^{T(Q) \mathbin{;} R} \tau$. From $\Sigma \forces_{X}^{T(\emptytimes) \mathbin{;} (\cdot)} \tau$ and $\forces_{D}^{R} \Sigma$, we infer $\forces_{D}^{T(\emptytimes) \mathbin{;} R} \tau$. From this and $\forces_{\mathcal{C}}^{Q} \top^{*}$, we use IH on $\tau$ to infer $\forces_{D}^{T(Q) \mathbin{;} R} \tau$.
– $\chi = \Sigma * \tau$. Given the assumptions, in order to show $\forces_{\mathcal{C}}^{T(Q)} \Sigma * \tau$, we fix some arbitrary $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma , \tau \forces_{D}^{R(\cdot)} q$, and show $\forces_{D}^{R(T(Q))} q$. From $\forces_{\mathcal{B}}^{T(\emptytimes)} \Sigma * \tau$ and $\Sigma , \tau \forces_{D}^{R(\cdot)} q$, infer $\forces_{D}^{R(T(\emptytimes))} q$. From this and $\forces_{\mathcal{C}}^{Q} \top^{*}$, we have $\forces_{D}^{R(T(Q))} q$ by $(\top^{*})$.
– $\chi = \top^{*}$. Given the assumptions, to prove $\forces_{\mathcal{C}}^{T(Q)} \top^{*}$, we fix some $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\forces_{D}^{R(\emptytimes)} q$, and prove that $\forces_{D}^{R(T(Q))} q$. From $\forces_{D}^{R(\emptytimes)} q$ and $\forces_{\mathcal{C}}^{T(\emptytimes)} \top^{*}$, infer $\forces_{D}^{R(T(\emptytimes))} q$ by $(\top^{*})$. From this and $\forces_{\mathcal{C}}^{Q} \top^{*}$, infer $\forces_{D}^{R(T(Q))} q$, by $(\top^{*})$ again.
– $\chi = \Sigma \wand \tau$.
Apply $(\wand)$ to (15), then the goal becomes: if $\Sigma \forces_{\mathcal{B}}^{T(\emptytimes),(\cdot)} \tau$ and $\forces_{\mathcal{C}}^{Q} \top^{*}$, then $\Sigma \forces_{\mathcal{C}}^{T(Q),(\cdot)} \tau$. Assume the assumptions, to show $\Sigma \forces_{\mathcal{C}}^{T(Q),(\cdot)} \tau$, we fix some $D \supseteq \mathcal{C}$ and $R \in \mathcal{B}(A)$ such that $\forces_{D}^{R} \Sigma$, and show $\forces_{D}^{T(Q),R} \tau$. From $\forces_{D}^{R} \Sigma$ and $\Sigma \forces_{\mathcal{B}}^{T(\emptytimes),(\cdot)} \tau$, infer $\forces_{D}^{T(\emptytimes),R} \tau$. From this and $\forces_{\mathcal{C}}^{Q} \top^{*}$, we infer $\forces_{D}^{T(Q),R} \tau$, by IH on $\tau$.
– $\chi = \Sigma \lor \tau$. Given the assumptions, in order to show $\forces_{\mathcal{C}}^{T(Q)} \Sigma \lor \tau$, we fix some $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ satisfying $\Sigma \forces_{D}^{R(\cdot)} q$ and $\tau \forces_{D}^{R(\cdot)} q$, and show that $\forces_{D}^{R(T(Q))} q$. From $\forces_{\mathcal{B}}^{T(\emptytimes)} \Sigma \lor \tau$, $\Sigma \forces_{D}^{R(\cdot)} q$ and $\tau \forces_{D}^{R(\cdot)} q$, it follows that $\forces_{D}^{R(T(\emptytimes))} q$ by $(\lor)$. From this and $\forces_{\mathcal{C}}^{Q} \top^{*}$, we conclude that $\forces_{D}^{R(T(Q))} q$, by $(\top^{*})$.
– $\chi = \bot$. Given the assumptions, in order to show $\forces_{\mathcal{C}}^{T(Q)} \bot$, we simply fix some arbitrary $R(\cdot) \in \dot{\mathcal{B}}(A)$ and $q \in A$, and then show $\forces_{D}^{R(T(Q))} q$. From $\forces_{\mathcal{B}}^{T(\emptytimes)} \bot$, infer $\forces_{\mathcal{C}}^{R(T(\emptytimes))} q$ by $(\bot)$. From this and $\forces_{\mathcal{C}}^{Q} \top^{*}$, we conclude that $\forces_{D}^{R(T(Q))} q$, by $(\top^{*})$. This completes the inductive proof. Proof of Lemma 5.3.2. By induction on the structure of $\chi.$ The proof follows the same line of reasoning of the additive counterpart, see Lemma 5.3.3. Proof of Lemma 5.3.3. We prove by induction on the structure of $\chi$ that, assuming (A) $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \phi \land \psi$ and (B) $\phi \mathbin{;} \psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, one has (C) $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$. To avoid repetition, we will state the shared treatment which are to be added at the front of each of the following cases: Fix some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \Delta$, the goal is to show $\forces_{\mathcal{C}}^{T(S(P))} \chi$. Note that $\forces_{\mathcal{C}}^{P} \Delta$ and (A) entail $\forces_{\mathcal{C}}^{S(P)} \phi \land \psi$.
– $\chi$ is atomic. This follows immediately from $(\land)$.
– $\chi = \Sigma \land \tau$. Spelling out the definition of the goal $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \land \tau$, it suffices to fix arbitrary $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma \mathbin{;} \tau \forces_{D}^{R(\cdot)} q$, and show $\forces_{D}^{R(T(S(P)))} q$. Apply (Inf) and $(\land)$ to (B) together with $\Sigma \mathbin{;} \tau \forces_{D}^{R(\cdot)} q$, we have: $$\forall Y \supseteq D,\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{Y}^{U} \phi \mathbin{;} \psi, \text{ then } \forces_{Y}^{R(T(U))} q$$ That is, $\phi \mathbin{;} \psi \forces_{D}^{R(T(\cdot))} q$. By $(\land)$, this and $\forces_{\mathcal{C}}^{S(P)} \phi \land \psi$ imply $\forces_{D}^{R(T(S(P)))} q$.
– $\chi = \top$. According to $(\top)$, to prove $\forces_{\mathcal{C}}^{T(S(P))} \top$, we fix some arbitrary $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\forces_{D}^{R(\emptyplus)} q$, and the goal is to prove $\forces_{D}^{R(T(S(P)))} q$. (B) together with $\forces_{D}^{R(\emptyplus)} q$ implies: $$\forall Y \supseteq D,\ \forall U \in \mathcal{B}(A),\ \text{if } \forces_{Y}^{U} \phi \mathbin{;} \psi, \text{ then } \forces_{Y}^{R(T(U))} q$$ That is, $\phi \mathbin{;} \psi \forces_{D}^{R(T(\cdot))} q$. This together with $\forces_{\mathcal{B}}^{S(P)} \phi \land \psi$ imply $\forces_{D}^{R(T(S(P)))} q$, by $(\land)$.
– $\chi = \Sigma \to \tau$. The goal $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \to \tau$ is equivalent to $\Sigma \forces_{\mathcal{C}}^{T(S(P)) \mathbin{;} (\cdot)} \tau$. So we fix some $D \supseteq \mathcal{C}$ and $Q \in \mathcal{B}(A)$ such that $\forces_{D}^{Q} \Sigma$, and show $\forces_{D}^{T(S(P)) \mathbin{;} Q} \tau$. (B) $\phi \mathbin{;} \psi \forces_{\mathcal{B}}^{T(\cdot)} \Sigma \to \tau$ together with $\forces_{D}^{Q} \Sigma$ says $\phi \mathbin{;} \psi \forces_{D}^{T(\cdot) \mathbin{;} Q} \tau$, and together with $\forces_{\mathcal{B}}^{S(P)} \phi \land \psi$, it follows that $\forces_{D}^{T(S(P)) \mathbin{;} Q} \tau$, by the IH.
– $\chi = \Sigma * \tau$. To prove $\forces_{\mathcal{C}}^{T(S(P))} \Sigma * \tau$, we further fix some $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma , \tau \forces_{D}^{R(\cdot)} q$. The goal is to prove $\forces_{D}^{R(T(S(P)))} q$. Now $\Sigma , \tau \forces_{D}^{R(\cdot)} q$ and (B) imply $\phi \mathbin{;} \psi \forces_{D}^{R(T(\cdot))} q$. This together with $\forces_{\mathcal{C}}^{S(P)} \phi \land \psi$ entail $\forces_{D}^{R(T(S(P)))} q$, according to $(\land)$.
– $\chi = \top^{*}$. Similar to the $\top$ case.
– $\chi = \Sigma \wand \tau$. Similar to the $\to$ case.
– $\chi = \Sigma \lor \tau$. In order to show $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \lor \tau$, we fix some $D \supseteq \mathcal{C}$, $R(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma \forces_{D}^{R(\cdot)} q$ and $\tau \forces_{D}^{R(\cdot)} q$. The goal is $\forces_{D}^{R(T(S(P)))} q$. Note that $\phi \mathbin{;} \psi \forces_{\mathcal{B}}^{T(\cdot)} \Sigma \lor \tau$ together with $\Sigma \forces_{D}^{R(\cdot)} q$ and $\tau \forces_{D}^{R(\cdot)} q$ imply $\phi \mathbin{;} \psi \forces_{D}^{R(T(\cdot))} q$. Apply the IH to $\forces_{\mathcal{C}}^{S(P)} \phi \land \psi$ and $\phi \mathbin{;} \psi \forces_{D}^{R(T(\cdot))} q$, it follows that $\forces_{D}^{R(T(S(P)))} q$.
– $\chi = \bot$. In order to show $\forces_{\mathcal{C}}^{T(S(P))} \bot$, we fix some arbitrary $D \supseteq \mathcal{C}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$ and $q \in A$, and show $\forces_{D}^{U(T(S(P)))} q$. Given $\phi \mathbin{;} \psi \forces_{\mathcal{B}}^{T(\cdot)} \bot$ and $D \supseteq \mathcal{B}$, we have $\phi \mathbin{;} \psi \forces_{D}^{U(T(\cdot))} q$ by (Inf) and $(\bot)$. Apply $(\land)$ to $\forces_{\mathcal{C}}^{S(P)} \phi \land \psi$ and $\phi \mathbin{;} \psi \forces_{D}^{U(T(\cdot))} q$, we conclude $\forces_{D}^{U(T(S(P)))} q$. This completes the induction. Proof of Lemma 5.3.4. We prove by induction on the structure of $\chi$ that, assume (A) $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \phi \lor \psi$, (B) $\phi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, and (C) $\psi \forces_{\mathcal{B}}^{T(\cdot)} \chi$, it follows that (D) $\Delta \forces_{\mathcal{B}}^{T(S(\cdot))} \chi$.
– $\chi$ is an atom. This follows immediately from the definition $(\lor)$.
– $\chi = \Sigma \land \tau$. Assume (A), (B), and (C). We fix some $\mathcal{C} \supseteq \mathcal{B}$ and P such that $\forces_{\mathcal{C}}^{P} \Delta$. It then suffices to show $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \land \tau$ (under (A), (B), (C)). Towards this, we further fix some $D \supseteq \mathcal{C}$, $Q(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma \mathbin{;} \tau \forces_{D}^{Q(\cdot)} q$, and show that $\forces_{D}^{Q(T(S(P)))} q$. Given (A), we have $\forces_{\mathcal{C}}^{S(P)} \phi \lor \psi$. Note that (B) and $\Sigma \mathbin{;} \tau \forces_{D}^{Q(\cdot)} q$ imply $\phi \forces_{D}^{Q(T(\cdot))} q$; (C) and $\Sigma \mathbin{;} \tau \forces_{D}^{Q(\cdot)} q$ imply $\psi \forces_{D}^{Q(T(\cdot))} q$. So apply $(\lor)$ to $\forces_{D}^{S(P)} \phi \lor \psi$, $\phi \forces_{D}^{Q(T(\cdot))} q$, and $\psi \forces_{D}^{Q(T(\cdot))} q$, we get $\forces_{D}^{Q(T(S(P)))} q$.
– $\chi = \top$. Assume (A), (B), and (C). We fix some $\mathcal{C} \supseteq \mathcal{B}$ and P such that $\forces_{\mathcal{C}}^{P} \Delta$, and it suffices to show $\forces_{\mathcal{C}}^{T(S(P))} \top$. Towards this, we fix some $D \supseteq \mathcal{C}$, $Q(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\forces_{D}^{Q(\emptyplus)} q$, and the goal is to show $\forces_{D}^{Q(T(S(P)))} q$. $\forces_{\mathcal{C}}^{P} \Delta$ and (A) entail $\forces_{\mathcal{C}}^{S(P)} \phi \lor \psi$. Note that $\forces_{D}^{Q(\emptyplus)} q$ and (B) imply $\phi \forces_{D}^{Q(T(\cdot))} q$: for arbitrary $X \supseteq D$, $U \in \mathcal{B}(A)$ such that $\forces_{X}^{U} \phi$, by (B) we have $\forces_{X}^{T(U)} \top$, so $\forces_{D}^{Q(\emptyplus)} q$ implies $\forces_{D}^{Q(T(U))} q$. Similarly, $\forces_{D}^{Q(\emptyplus)} q$ and (C) imply $\psi \forces_{D}^{Q(T(\cdot))} q$. Apply $(\lor)$ to $\forces_{\mathcal{C}}^{S(P)} \phi \lor \psi$, $\phi \forces_{D}^{Q(T(\cdot))} q$, and $\psi \forces_{D}^{Q(T(\cdot))} q$, we have $\forces_{D}^{Q(T(S(P)))} q$.
– $\chi = \Sigma \to \tau$. Assume (A), (B), and (C). We fix some $\mathcal{C} \supseteq \mathcal{B}$ and P such that $\forces_{\mathcal{C}}^{P} \Delta$. The goal is to show $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \to \tau$; that is, $\Sigma \forces_{\mathcal{C}}^{T(S(P)) \mathbin{;} (\cdot)} \tau$; that is, for arbitrary $X \supseteq \mathcal{C}$ and $U \in \mathcal{B}(A)$, if $\forces_{X}^{U} \Sigma$, then $\forces_{X}^{T(S(P)) \mathbin{;} U} \tau$. So fix some $D \supseteq \mathcal{C}$ and $Q \in \mathcal{B}(A)$ such that $\forces_{D}^{Q} \Sigma$, we show that $\forces_{D}^{T(S(P)) \mathbin{;} Q} \tau$. By the IH, it suffices to show: $$\forces_{D}^{S(P)} \phi \lor \psi \tag{16}$$ $$\phi \forces_{D}^{T(\cdot) \mathbin{;} Q} \tau \tag{17}$$ $$\psi \forces_{D}^{T(\cdot) \mathbin{;} Q} \tau \tag{18}$$
Here (16) follows immediately from (A), $\forces_{\mathcal{C}}^{P} \Delta$, and $D \supseteq \mathcal{C} \supseteq \mathcal{B}$. For (17) and (18), we simply show the former as the reasoning for the latter is similar. Using (Inf), (17) means for arbitrary $Y \supseteq D$ and $U \in \mathcal{B}(A)$, if $\forces_{Y}^{U} \phi$, then $\forces_{Y}^{T(U) \mathbin{;} Q} \tau$. So we fix some $E \supseteq D$ and $R \in \mathcal{B}(A)$ such that $\forces_{E}^{R} \phi$, and show that $\forces_{E}^{T(R) \mathbin{;} Q} \tau$. Given $\forces_{E}^{R} \phi$, $\phi \forces_{\mathcal{B}}^{T(\cdot)} \Sigma \to \tau$, and $E \supseteq \mathcal{B}$, it follows that $\forces_{E}^{T(R)} \Sigma \to \tau$; that is, $\Sigma \forces_{E}^{T(R) \mathbin{;} (\cdot)} \tau$. This together with $\forces_{D}^{Q} \Sigma$ imply that $\forces_{E}^{T(R) \mathbin{;} Q} \tau$.
– $\chi = \Sigma * \tau$. Assume (A), (B), and (C). Fix some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ such that $\forces_{\mathcal{C}}^{P} \Delta$, the goal is to show that $\forces_{\mathcal{C}}^{T(S(P))} \Sigma * \tau$. By $(*)$, this amounts to fix some $D \supseteq \mathcal{C}$, $Q(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $\Sigma , \tau \forces_{D}^{Q(\cdot)} q$, and show that $\forces_{D}^{Q(T(S(P)))} q$. By the base case, it suffices to show that: $$\forces_{D}^{S(P)} \phi \lor \psi \tag{19}$$ $$\phi \forces_{D}^{Q(T(\cdot))} q \tag{20}$$ $$\psi \forces_{D}^{Q(T(\cdot))} q \tag{21}$$
Here (19) follows immediately from assumption (A) and $\forces_{\mathcal{C}}^{P} \Delta$; we only show (21), and the argument for (20) is similar. So we fix some $E \supseteq D$ and $R \in \mathcal{B}(A)$ such that $\forces_{E}^{R} \psi$, and show that $\forces_{E}^{Q(T(R))} q$. Given $\forces_{E}^{R} \psi$, $\psi \forces_{\mathcal{B}}^{T(\cdot)} \Sigma * \tau$, and $E \supseteq \mathcal{B}$, it follows that $\forces_{E}^{T(R)} \Sigma * \tau$. Together with $\Sigma , \tau \forces_{D}^{Q(\cdot)} q$ and $E \supseteq D$, it follows by $(*)$ that $\forces_{E}^{Q(T(R))} q$.
– $\chi = \top^{*}$. It follows from the same line of reasoning for $\chi = \top$.
– $\chi = \Sigma \wand \tau$. Assume (A), (B), and (C). Fix some $\mathcal{C} \supseteq \mathcal{B}$ and $P \in \mathcal{B}(A)$ satisfying $\forces_{\mathcal{C}}^{P} \Delta$, the goal is then to show that $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \wand \tau$; in other words, by $(\wand)$ and (Inf), to show that for arbitrary $X \supseteq \mathcal{C}$ and U, if $\forces_{X}^{U} \Sigma$, then $\forces_{X}^{T(S(P)),U} \tau$. So let us fix some $D \supseteq \mathcal{C}$ and $Q \in \mathcal{B}(A)$ such that $\forces_{D}^{Q} \Sigma$, and show that $\forces_{D}^{T(S(P)),Q} \tau$. By the IH, it suffices to show that: $$\forces_{D}^{S(P)} \phi \lor \psi \tag{22}$$ $$\phi \forces_{D}^{T(\cdot),Q} \tau \tag{23}$$ $$\psi \forces_{D}^{T(\cdot),Q} \tau \tag{24}$$ As (22) follows immediately from (A) $\Delta \forces_{\mathcal{B}}^{S(\cdot)} \phi \lor \psi$, $\forces_{\mathcal{C}}^{P} \Delta$, and $D \supseteq \mathcal{C} \supseteq \mathcal{B}$, we show (23) and (24). Since the latter two are similar, we only showcase (23). Towards this, it suffices to fix some $E \supseteq D$ and $R \in \mathcal{B}(A)$ such that $\forces_{E}^{R} \phi$, and show that $\forces_{E}^{T(R),Q} \tau$. It follows from (B) $\phi \forces_{\mathcal{B}}^{T(\cdot)} \Sigma \wand \tau$, $\forces_{E}^{R} \phi$, and $E \supseteq \mathcal{B}$ that $\forces_{E}^{T(R)} \Sigma \wand \tau$; that is, $\Sigma \forces_{E}^{T(R),(\cdot)} \tau$. This together with $\forces_{D}^{Q} \Sigma$ and $E \supseteq D$ entail that $\forces_{E}^{T(R),Q} \tau$.
– $\chi = \Sigma \lor \tau$. Assume (A), (B), and (C). We fix some $\mathcal{C} \supseteq \mathcal{B}$ and P satisfying $\forces_{\mathcal{C}}^{P} \Delta$, and the goal is $\forces_{\mathcal{C}}^{T(S(P))} \Sigma \lor \tau$; which according to $(\lor)$ boils down to showing that for arbitrary $X \supseteq \mathcal{B}$, $U(\cdot)$, p, if $\Sigma \forces_{X}^{U(\cdot)} p$ and $\tau \forces_{X}^{U(\cdot)} p$, then $\forces_{X}^{U(T(S(P)))} p$. So we fix some $\mathcal{C} \supseteq \mathcal{B}$, $W(\cdot) \in \dot{\mathcal{B}}(A)$, $q \in A$ satisfying that $\Sigma \forces_{\mathcal{C}}^{W(\cdot)} q$ and $\tau \forces_{\mathcal{C}}^{W(\cdot)} q$, and show that $\forces_{\mathcal{C}}^{W(T(S(P)))} q$. By the IH, it suffices to show that: $$\forces_{\mathcal{C}}^{S(P)} \phi \lor \psi \tag{25}$$ $$\phi \forces_{\mathcal{C}}^{W(T(\cdot))} q \tag{26}$$ $$\psi \forces_{\mathcal{C}}^{W(T(\cdot))} q \tag{27}$$
Again, (25) follows from the combination of (A), $\mathcal{C} \supseteq \mathcal{B}$, and $\forces_{\mathcal{C}}^{P} \Delta$. We now prove (27), and omit the similar proof for (26). So we fix some $D \supseteq \mathcal{C}$ and $Q \in \mathcal{B}(A)$ such that $\forces_{D}^{Q} \psi$, and show that $\forces_{D}^{W(T(Q))} q$. It follows from (C) $\psi \forces_{\mathcal{B}}^{T(\cdot)} \Sigma \lor \tau$, $\forces_{D}^{Q} \psi$, and $D \supseteq \mathcal{B}$ that $\forces_{D}^{T(Q)} \Sigma \lor \tau$. By monotonicity, $\Sigma \forces_{\mathcal{C}}^{W(\cdot)} q$ and $\tau \forces_{\mathcal{C}}^{W(\cdot)} q$ imply $\Sigma \forces_{D}^{W(\cdot)} q$ and $\tau \forces_{D}^{W(\cdot)} q$, respectively. Together with $\forces_{D}^{T(Q)} \Sigma \lor \tau$, it follows by $(\lor)$ that $\forces_{D}^{W(T(Q))} q$.
– $\chi = \bot$. The reasoning is similar to that for $\top$. This completes the induction.
□6 Completeness
If $\Gamma \Vdash \phi$, then $\Gamma \vdash \phi$. We follow the strategy used by Sandqvist [40] for IPL and by the authors for IMLL [18], suitably modified for BI. We require to show that $\Gamma \Vdash \phi$ implies that there is an NBI-proof witnessing $\Gamma \vdash \phi$. To this end, we associate to each sub-formula $\rho$ of $\Gamma \cup \{\phi\}$ a unique atom $r$—denoted $\rho^{\flat}$ below, $(-)^{\flat}$ is a function from formulas to atoms—and construct a base $\mathcal{N}$ such that $r$ behaves in $\mathcal{N}$ as $\rho$ behaves in NBI. Moreover, formulae and their atomizations are semantically equivalent in any extension of $\mathcal{N}$ so that support in $\mathcal{N}$ characterizes both validity and provability—that is $\phi^{\flat} \forces_{\mathcal{N}}^{(\cdot)} \phi$ and $\phi \forces_{\mathcal{N}}^{(\cdot)} \phi^{\flat}$. When $\rho \in A$, we take $r := \rho$, but for complex $\rho$ we choose $r$ to be alien to $\Gamma \cup \{\phi\}$. We proceed with a formal treatment. Let $\Xi$ be the set of all sub-formulae of $\Gamma$ and $\phi$. Let $(\cdot)^{\flat} : \Xi \to A$ be an injection that acts as an identity on $\Xi \cap A$ (i.e., $p^{\flat} = p$ for $p \in \Xi \cap A$). Let $(\cdot)^{\natural}$ be the left-inverse of $(\cdot)^{\flat}$—that is, $$p^{\natural} := \begin{cases} \chi & \text{if } p = \chi^{\flat} \\ p & \text{otherwise} \end{cases}$$ Both extend to bunches pointwise with identity on units; that is, $$\Delta^{\flat} := \begin{cases} \phi^{\flat} & \text{if } \Delta = \phi \in \mathcal{F} \\ \emptyplus & \text{if } \Delta = \emptyplus \\ \emptytimes & \text{if } \Delta = \emptytimes \\ \Delta_1^{\flat} \mathbin{;} \Delta_2^{\flat} & \text{if } \Delta = \Delta_1 \mathbin{;} \Delta_2 \\ \Delta_1^{\flat} , \Delta_2^{\flat} & \text{if } \Delta = \Delta_1 , \Delta_2 \end{cases} \qquad P^{\natural} := \begin{cases} p^{\natural} & \text{if } P = p \in A \\ \emptyplus & \text{if } P = \emptyplus \\ \emptytimes & \text{if } P = \emptytimes \\ P_1^{\natural} \mathbin{;} P_2^{\natural} & \text{if } P = P_1 \mathbin{;} P_2 \\ P_1^{\natural} , P_2^{\natural} & \text{if } P = P_1 , P_2 \end{cases}$$ We may write $\Gamma(\Delta)^{\flat}$ and $P(Q)^{\natural}$ to denote $(\Gamma(\Delta))^{\flat}$ and $(P(Q))^{\natural}$, respectively. We construct a base $\mathcal{N}$ such that $\Sigma^{\flat}$ behaves in $\mathcal{N}$ as $\Sigma$ behaves in NBI. The base $\mathcal{N}$ contains all instances of the rules of Figure 5, which merits comparison with Figure 3, for all $p \in A$, $\Sigma, \Sigma_1, \Sigma_2, \tau \in \Xi$, and $\Delta, \Delta', \Lambda, \Lambda' \in \mathcal{B}(\Xi)$ such that $\Delta \equiv \Delta'$. Note, we need not include $\mathsf{id}^{\flat}$, $\mathsf{e}^{\flat}$, $\mathsf{w}^{\flat}$, and $\mathsf{c}^{\flat}$ because of taut., exch., weak., and cont., respectively. Theorem 6.1 (Completeness) follows from the following three properties:
– (AtComp). Let $S(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, and $\mathcal{B}$ be a base: $P \forces_{\mathcal{B}}^{S(\cdot)} p$ iff $S(P) \vdash_{\mathcal{B}} p$.
– (Flat). For any sub-formula $\xi \in \Xi$ and $\mathcal{N}' \supseteq \mathcal{N}$: $\forces_{\mathcal{N}'}^{S} \xi^{\flat}$ iff $\forces_{\mathcal{N}'}^{S} \xi$.
– (Nat). Let $S \in \mathcal{B}(A)$ and $p \in A$: if $S \vdash_{\mathcal{N}} p$, then $S^{\natural} \vdash_{\mathrm{NBI}} p^{\natural}$.
The first claim (i.e., AtComp) follows from cut. in the definition of derivability in a base (Definition 4.5) and the ground case of completeness. It is proved by induction on support according to the structure of P. The second claim (i.e., Flat) formalizes the idea that every formula $\xi$ appearing in $\Gamma \cup \{\phi\}$ behaves the same as $\xi^{\flat}$ in any base extending $\mathcal{N}$. Consequently, $\Gamma^{\flat} \forces_{\mathcal{N}'} \phi^{\flat}$ iff $\Gamma \forces_{\mathcal{N}'} \phi$ for any $\mathcal{N}' \supseteq \mathcal{N}$. The third claim (i.e., Nat) intuitively says that $\mathcal{N}$ is a faithful atomic encoding of NBI, witnessed by $(\cdot)^{\natural}$. This together with (AtComp) guarantees that every $\xi \in \Xi$ behaves in $\mathcal{N}$ as $\xi^{\flat}$ in $\mathcal{N}$, thus as $(\xi^{\flat})^{\natural} = \xi$ in NBI. It is proved by induction on derivability in a base.
Proof. (Proof of Theorem 6.1—Completeness) Assume $\Gamma \Vdash \phi$ and let $\mathcal{N}$ be the bespoke base for $\Gamma \rhd \phi$ defined as in Figure 5. By (Flat), $\Gamma^{\flat} \forces_{\mathcal{N}}^{(\cdot)} \phi^{\flat}$. Therefore, by (AtComp), $\Gamma^{\flat} \vdash_{\mathcal{N}} \phi^{\flat}$. Finally, by (Nat), $(\Gamma^{\flat})^{\natural} \vdash_{\mathrm{NBI}} (\phi^{\flat})^{\natural}$—that is, $\Gamma \vdash_{\mathrm{NBI}} \phi$. It remains only to prove the ancillary lemmas.
Let $S(\cdot) \in \dot{\mathcal{B}}(A)$ and $p \in A$ and let $\mathcal{B}$ be a base: $$P \forces_{\mathcal{B}}^{S(\cdot)} p \quad \text{iff} \quad S(P) \vdash_{\mathcal{B}} p$$
For the ‘only if’ direction, assume $P \forces_{\mathcal{B}}^{S(\cdot)} p$. By (Inf), $\forall \mathcal{X} \supseteq \mathcal{B}$ and $\forall U \in \mathcal{B}(A)$, if $\forces_{\mathcal{X}}^{U} P$, then $\forces_{\mathcal{X}}^{S(U)} p$. Set $\mathcal{X} = \mathcal{B}$ and $U = P$. Since $\forces_{\mathcal{B}}^{S(P)} p$ implies $S(P) \vdash_{\mathcal{B}} p$, it remains only to show $\forces_{\mathcal{B}}^{P} P$. This follows from Proposition 4.20.
For the ‘if’ direction, we proceed by induction on the structure of P. Throughout we assume $S(P) \vdash_{\mathcal{B}} p$, which we call the first assumption. By (Inf), the desired conclusion is equivalent to the following: $$\forall \mathcal{C} \supseteq \mathcal{B} \text{ and } \forall Q \in \mathcal{B}(A),\ \text{if } \forces_{\mathcal{C}}^{Q} P, \text{ then } \forces_{\mathcal{C}}^{S(Q)} p.$$ Therefore, let $\mathcal{C} \supseteq \mathcal{B}$ and $Q \in \mathcal{B}(A)$ be arbitrary such that $\forces_{\mathcal{C}}^{Q} P$, which we call the second assumption. We require to establish $\forces_{\mathcal{C}}^{S(Q)} p$—that is, $S(Q) \vdash_{\mathcal{C}} p$.
– P is in $A$. Trivial by the fact that derivability in a base is monotonic with respect to base-extensions (Proposition 4.14) and cut. in Definition 4.5.
– P is $\emptyplus$. By the monotonicity of derivability in a base on the first assumption, $S(\emptyplus) \vdash_{\mathcal{C}} p$. By weak., $S(\emptyplus \mathbin{;} Q) \vdash_{\mathcal{C}} p$. Hence (by exch.), $S(Q) \vdash_{\mathcal{C}} p$.
– P is $\emptytimes$. By the monotonicity of derivability in a base on the first assumption, $S(\emptytimes) \vdash_{\mathcal{C}} p$. By $(\emptytimes)$ on the second assumption, $Q \succeq \emptytimes$. In other words, $Q \equiv \emptytimes \mathbin{;} R$ for some $R \in \mathcal{B}(A)$. Therefore, $S(Q) \vdash_{\mathcal{C}} p$ obtains by weak.
– P is $P_1 \mathbin{;} P_2$. By the monotonicity of derivability in a base on the first assumption, $S(P_1 \mathbin{;} P_2) \vdash_{\mathcal{C}} p$. By $(;)$ on the second assumption, $\forces_{\mathcal{C}}^{Q} P_1$ and $\forces_{\mathcal{C}}^{Q} P_2$, since $Q \succeq Q$. Hence, by the induction hypothesis (IH), $S(Q \mathbin{;} Q) \vdash_{\mathcal{C}} p $. Whence, by cont., $ S(Q) \vdash_{\mathcal{C}} p$.
– P is $P_1 , P_2$. By the monotonicity of derivability in a base on the first assumption, $S(P_1 \mathbin{;} P_2) \vdash_{\mathcal{C}} p$. By $(,)$ on the second assumption, there are $Q_1$ and $Q_2$ such that $Q \succeq (Q_1 , Q_2)$, $\forces_{\mathcal{C}}^{Q_1} P_1$, $\forces_{\mathcal{C}}^{Q_2} P_2$. Hence, by the IH twice applied, $S(Q_1 , Q_2) \vdash_{\mathcal{C}} p$. Whence, by weak., $S(Q) \vdash_{\mathcal{C}} p$. This completes the induction.
□Next, we turn to (Flat). For this, the crucial observation is that for arbitrary sub-formula $\xi$ of $\Gamma$ or $\phi$, $\xi$ behaves the same in $\vdash_{\mathcal{N}}$ as $\xi^\flat$ in $\mathcal{N}$.
The following holds for arbitrary $\mathcal{M} \supseteq \mathcal{N}$ and sub-formulae $\sigma$ and $\tau$ of $\Gamma$ or $\phi$:
- $S \vdash_{\mathcal{M}} (\sigma \ast \tau)^\flat$ iff for arbitrary $X \supseteq \mathcal{M}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, if $U(\sigma, \tau) \vdash_{X} p$, then $U(S) \vdash_{X} p$.
- $S \vdash_{\mathcal{M}} (\sigma \wand \tau)^\flat$ iff $S, \sigma \vdash_{\mathcal{M}} \tau$.
- $S \vdash_{\mathcal{M}} \top^{*}$ iff for arbitrary $X \supseteq \mathcal{M}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, if $U(\emptytimes) \vdash_{X} p$, then $U(S) \vdash_{X} p$.
- $S \vdash_{\mathcal{M}} (\sigma \land \tau)^\flat$ iff for arbitrary $X \supseteq \mathcal{M}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, if $U(\sigma \mathbin{;} \tau) \vdash_{X} p$, then $U(S) \vdash_{X} p$.
- $S \vdash_{\mathcal{M}} (\sigma \to \tau)^\flat$ iff $S \mathbin{;} \sigma \vdash_{\mathcal{M}} \tau$.
- $S \vdash_{\mathcal{M}} \top$ iff for arbitrary $X \supseteq \mathcal{M}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, if $U(\emptyplus) \vdash_{X} p$, then $U(S) \vdash_{X} p$.
- $S \vdash_{\mathcal{M}} (\sigma \lor \tau)^\flat$ iff for arbitrary $X \supseteq \mathcal{M}$, $U(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, if $U(\sigma) \vdash_{X} p$ and $U(\tau) \vdash_{X} p$, then $U(S) \vdash_{X} p$.
- $S \vdash_{\mathcal{M}} \bot$ iff for arbitrary $U(\cdot) \in \dot{\mathcal{B}}(A)$, $p \in A$, $U(S) \vdash_{\mathcal{M}} p$.
We fix some $\mathcal{M} \supseteq \mathcal{N}$ and S. In each case, the two directions of the “if and only if” statement follows from the corresponding introduction rule and elimination rule in $\mathcal{N}$, respectively. We only demonstrate some representative cases, the others being similar:
4. We consider the two directions separately.
– Left to Right. Given $S \vdash_{\mathcal{M}} (\Sigma \land \tau)^{\flat}$, we fix some $\mathcal{O} \supseteq \mathcal{M}$, $T(\cdot) \in \dot{\mathcal{B}}(A)$, and $q \in A$ such that $T(\Sigma^{\flat} \mathbin{;} \tau^{\flat}) \vdash_{\mathcal{O}} q$. The goal is to show $T(S) \vdash_{\mathcal{O}} q$. Note that the rule $$S \vdash_{\mathcal{M}} (\Sigma \land \tau)^{\flat}, \; T(\Sigma^{\flat} \mathbin{;} \tau^{\flat}) \vdash_{\mathcal{O}} q \;\Rightarrow\; T(S) \vdash_{\mathcal{O}} q$$ is in $\mathcal{N}$, thus in $\mathcal{O}$, so applying rule., we have $T(S) \vdash_{\mathcal{O}} q$.
– Right to Left. Assume the RHS; it follows in particular that if $\Sigma^{\flat} \mathbin{;} \tau^{\flat} \vdash_{\mathcal{M}} (\Sigma \land \tau)^{\flat}$, then $S \vdash_{\mathcal{M}} (\Sigma \land \tau)^{\flat}$. Here $\Sigma^{\flat} \mathbin{;} \tau^{\flat} \vdash_{\mathcal{M}} (\Sigma \land \tau)^{\flat}$ follows from $\Sigma^{\flat} \vdash_{\mathcal{M}} \Sigma^{\flat}$, $\tau^{\flat} \vdash_{\mathcal{M}} \tau^{\flat}$, and that $\Sigma^{\flat} \vdash \Sigma^{\flat}, \tau^{\flat} \vdash \tau^{\flat} \Rightarrow \Sigma^{\flat} \mathbin{;} \tau^{\flat} \vdash (\Sigma \land \tau)^{\flat}$ is a rule in $\mathcal{N}$ (thus in $\mathcal{M}$).
6. We consider the two directions separately.
– Left to Right. Given $S \vdash_{\mathcal{M}} \top^{\flat}$, we fix some $\mathcal{O} \supseteq \mathcal{M}$, $T(\cdot) \in \dot{\mathcal{B}}(A)$, $q \in A$ such that $T(\emptyplus) \vdash_{\mathcal{O}} q$. The goal is to show $T(S) \vdash_{\mathcal{O}} q$. Note that the rule $$T(\emptyplus) \vdash_{\mathcal{O}} q, \; S \vdash_{\mathcal{O}} \top^{\flat} \;\Rightarrow\; T(S) \vdash_{\mathcal{O}} q$$ is in $\mathcal{O}$, so applying rule. to $T(\emptyplus) \vdash_{\mathcal{O}} q$ and $S \vdash_{\mathcal{O}} \top^{\flat}$, we have $T(S) \vdash_{\mathcal{O}} q$.
– Right to Left. Given the RHS, it follows in particular that, if $\emptyplus \vdash_{\mathcal{M}} \top^{\flat}$, then $S \vdash_{\mathcal{M}} \top^{\flat}$. Since the rule $\emptyplus \vdash \top^{\flat}$ is in $\mathcal{O}$, it follows that $\emptyplus \vdash_{\mathcal{M}} \top^{\flat}$, so $S \vdash_{\mathcal{M}} \top^{\flat}$.
8. We consider the two directions separately.
– Right to Left. Given the RHS, one may choose $U := (\cdot)$ and $p = \bot$ to obtain the desired result. This completes the case analysis.
□For any sub-formula $\xi$ of $\Gamma$ or $\phi$, and arbitrary $\mathcal{N}' \supseteq \mathcal{N}$, we have: $$\forces_{\mathcal{N}'}^{S} \xi^{\flat} \quad \text{iff} \quad \forces_{\mathcal{N}'}^{S} \xi \tag{\dagger}$$
Let $\mathcal{M} \supseteq \mathcal{N}$ be arbitrary. We proceed by induction on the structure of $\xi$.
– $\xi$ is atomic. By definition, $\xi^{\flat}$ is exactly $\xi$, thus $(\dagger)$ is a tautology.
– $\xi$ is $\Sigma * \tau$. This obtains as follows: $$\begin{aligned} \forces_{\mathcal{M}}^{S} (\Sigma * \tau)^{\flat} \;&\text{iff}\; S \vdash_{\mathcal{M}} (\Sigma * \tau)^{\flat} && (\text{At}) \\ &\text{iff}\; \forall \mathcal{X} \supseteq \mathcal{M},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \text{if } U(\Sigma^{\flat} , \tau^{\flat}) \vdash_{\mathcal{X}} p,\ \text{then } U(S) \vdash_{\mathcal{X}} p && (\text{Proposition 6.3.1}) \\ &\text{iff}\; \forall \mathcal{X} \supseteq \mathcal{M},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \text{if } \Sigma , \tau \forces_{\mathcal{X}}^{U(\cdot)} p,\ \text{then } \forces_{\mathcal{X}}^{U(S)} p && (\text{IH} + \text{AtComp}) \\ &\text{iff}\; \forces_{\mathcal{M}}^{S} \Sigma * \tau && (*) \end{aligned}$$
– $\xi$ is $\top^{*}$. This obtains as follows: $$\begin{aligned} \forces_{\mathcal{M}}^{S} (\top^{*})^{\flat} \;&\text{iff}\; S \vdash_{\mathcal{M}} (\top^{*})^{\flat} && (\text{At}) \\ &\text{iff}\; \forall \mathcal{X} \supseteq \mathcal{M},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \text{if } U(\emptytimes) \vdash_{\mathcal{X}} p,\ \text{then } U(S) \vdash_{\mathcal{X}} p && (\text{Proposition 6.3.6}) \\ &\text{iff}\; \forall \mathcal{X} \supseteq \mathcal{M},\ \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \text{if } \emptytimes \forces_{\mathcal{X}}^{U(\cdot)} p,\ \text{then } S \forces_{\mathcal{X}}^{U} p && (\text{IH}) \\ &\text{iff}\; \forces_{\mathcal{M}}^{S} \top^{*} && (\top^{*}) \end{aligned}$$
– $\xi$ is $\Sigma \wand \tau$. This obtains as follows: $$\begin{aligned} \forces_{\mathcal{M}}^{S} (\Sigma \wand \tau)^{\flat} \;&\text{iff}\; S \vdash_{\mathcal{M}} (\Sigma \wand \tau)^{\flat} && (\text{At}) \\ &\text{iff}\; S , \Sigma^{\flat} \vdash_{\mathcal{M}} \tau^{\flat} && (\text{Proposition 6.3.2}) \\ &\text{iff}\; \Sigma^{\flat} \forces_{\mathcal{M}}^{S,(\cdot)} \tau^{\flat} && (\text{AtComp}) \\ &\text{iff}\; \Sigma \forces_{\mathcal{M}}^{S,(\cdot)} \tau && (\text{IH} + (\text{Inf})) \\ &\text{iff}\; \forces_{\mathcal{M}}^{S} \Sigma \wand \tau && (\wand) \end{aligned}$$
– $\xi$ is $\Sigma \land \tau$. Mutatis mutandis on the $*$-case.
– $\xi$ is $\top$. Mutatis mutandis on the $\top^{*}$-case.
– $\xi$ is $\Sigma \to \tau$. Mutatis mutandis on the $\wand$-case.
– $\xi$ is $\Sigma \lor \tau$. Mutatis mutandis on the $*$-case.
– $\xi$ is $\bot$. This obtains as follows: $$\begin{aligned} \forces_{\mathcal{M}}^{S} \bot \;&\text{iff}\; S \vdash_{\mathcal{M}} \bot && (\text{At}) \\ &\text{iff}\; \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ U(S) \vdash_{\mathcal{M}} p && (\text{Proposition 6.3.8}) \\ &\text{iff}\; \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ S \forces_{\mathcal{M}}^{U(\cdot)} p && (\text{AtComp}) \\ &\text{iff}\; \forall U(\cdot) \in \dot{\mathcal{B}}(A),\ \forall p \in A,\ \forces_{\mathcal{M}}^{U(S)} p && (\text{Proposition 4.20} + (\text{Inf})) \\ &\text{iff}\; \forces_{\mathcal{M}}^{S} \bot && ((\bot)) \end{aligned}$$ This completes the induction.
Finally, Lemma Nat says that $(\cdot)^{\natural}$ lifts derivability in $\mathcal{N}$ faithfully to derivability in BI.
□Let $S \in \mathcal{B}(A)$ and $p \in A$: if $S \vdash_{\mathcal{N}} p$, then $S^{\natural} \vdash p^{\natural}$.
We proceed by induction on $S \vdash_{\mathcal{N}} p$ according to Definition 4.5.
– taut. In this case, it must be that $S = p$. The result follows by the taut-rule in NBI.
– rule. Let $\Xi$ be all the sub-formulae of $\Gamma$ and $\phi$ relative to which $(-)^{\flat}$ and $\mathcal{N}$ are constructed. We proceed by case analysis on the rules in $\mathcal{N}$. We only illustrate ${\ast}\mathsf{E}^{\flat}$, the others being similar. It must be that $S = \Gamma'(\Delta)^{\flat}$, for some $\Gamma' \in \dot{\mathcal{B}}(\Xi)$ and $\Delta \in \mathcal{B}(\Xi)$, such that $\Gamma'(\psi_1, \psi_2)^{\flat} \vdash_{\mathcal{N}} \chi^{\flat}$ and $\Delta^{\flat} \vdash_{\mathcal{N}} (\psi_1 \ast \psi_2)^{\flat}$, for some $\psi_1, \psi_2, \chi \in \Xi$. By the IH, $\Gamma'(\psi_1, \psi_2) \vdash \chi$ and $\Delta \vdash (\psi_1 \ast \psi_2)$, using that $(-)^{\natural}$ is a left-inverse of $(-)^{\flat}$. The result follows by ${\ast}\mathsf{E}$ in NBI.
– weak. It must be that $S = P(Q \mathbin{;} Q')$, for some $P \in \dot{\mathcal{B}}(A)$ and $Q, Q' \in \mathcal{B}(A)$, and $P(Q) \vdash_{\mathcal{N}} p$. By the IH, $P(Q)^{\natural} \vdash p^{\natural}$. The result follows from application of the w-rule in NBI.
– cont. Mutatis mutandis on the case for weak.
– exch. Mutatis mutandis on the case for cont.
– cut. It must be that $S = P(Q)$, for some $P \in \dot{\mathcal{B}}(A)$ and $Q \in \mathcal{B}(A)$, such that $Q \vdash_{\mathcal{N}} q$ and $S(q) \vdash_{\mathcal{N}} p$, for some $q \in A$. By the IH, both $Q^{\natural} \vdash q^{\natural}$ and $S(q)^{\natural} \vdash p^{\natural}$. The result follows from cut-admissibility for BI (Lemma 3.10). This completes the induction.
□7 Conclusion
This paper delivers a B-eS for BI.
While BI can be understood as the free combination of IPL and IMLL, both of which have been given B-eS before (see Sandqvist [41] and Gheorghiu et al. [18]), several technical challenges remain in giving BI’s B-eS. Foremost is that BI uses a more complex datastructure for contexts than either of the other logics: bunches. Relative to the earlier work, giving B-eS for IPL and for IMLL, handling bunches with the appropriate structural behaviour is the major challenge in giving a BeS for BI. 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. Importantly, BI shares many connectives and the concept of bunches with relevance logics. The treatment herein suggests a method for a systematic/uniform presentation of the B-eS for relevance logics (e.g., following the approach by Read [36]).
A reason for studying the B-eS of substructural logics in the systemsoriented sciences is that it clearly and naturally supports, within the context of BI’s usual resource reading [33] (cf. Figure 4, clauses for , and ;), 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. See [14] for a more substantive discussion of these ideas by the present authors. In [13], the authors have proposed a state-effect reading of model-theoretic and proof-theoretic semantics that explains their relationship. In this reading, when logic is used in modelling systems, M-tS captures the properties of a system, while P-tS/B-eS captures its dynamics. Since BI has a wellestablished and intuitive reading as a logic of ‘resources’, this work may be used in modelling dynamical systems in which there is some appropriate notion of resource, include automata, Petri nets, simulation modelling, etc. On the last, Kuorikoski and Reijula [21] have recently shown P-tS (in general) to be a suitable paradigm of meaning for executable models. Developing these applications in areas such as resource semantics and modelling 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. We thank the reviewers for their careful reading and valuable suggestions.
Funding This work has been partially supported by the UK EPSRC grants EP/S013008/11281 AND EP/R006865/1, and by Gheorghiu’s EPSRC Doctoral Studentship. Open Access. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
References
- Abadi, M., Logic in access control, in P. G. Kolaitis, (ed.), Logic in Computer Science—LICS, IEEE, 2003, pp. 228–233.
- Allwein, G., and J. M. Dunn, Kripke models for linear logic, The Journal of Symbolic Logic 58(2):514–545, 1993.
- Anderson, G., and D. J. Pym, A calculus and logic of bunched resources and processes, Theoretical Computer Science 614:63–96, 2016, https://doi.org/10.1016/j.tcs. 2015.11.035.
- Barwise, J., and J. Seligman, Information Flow: The Logic of Distributed Systems, Cambridge University Press, Cambridge, 1997.
- Brandom, R., Articulating Reasons: An Introduction to Inferentialism, Harvard University Press, Cambridge, 2000.
- Brotherston, J., Bunched logics displayed, Studia Logica 100(6):1223–1254, 2012, https://doi.org/10.1007/s11225-012-9449-0.
- Brunnler ¨ , K., Deep sequent systems for modal logic, Archive for Mathematical Logic 48(6):551–577, 2009, https://doi.org/10.1007/s00153-009-0137-3.
- M. Gehrke, and L. van Rooijen, 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.
- Docherty, S., Bunched Logics: A Uniform Approach, PhD thesis, University College London, 2019.
- Dummett, M., The Logical Basis of Metaphysics, Harvard University Press, Cambridge, 1991.
- Galmiche, D., D. Mery ´ , and D. Pym, The semantics of BI and resource tableaux, Mathematical Structures in Computer Science 15(6):10331088, 2005, https://doi.org/ 10.1017/S0960129505004858.
- Gheorghiu, A., and D. Pym, Semantical analysis of the logic of bunched implications, Studia Logica 111:525–571, 2023a, https://doi.org/10.1007/s11225-022-10028-z.
- Gheorghiu, A., T. Gu, and D. Pym, A note on the practice of logical inferentialism: the state-effect interpretation, definitional reflection, and completeness, in 2nd Logic and Philosophy: Historical and Contemporary Issues Conference, Vilnius, Lithuania, May 2024, 2024a, Manuscript at https://arxiv.org/pdf/2403.10546, Accessed August 2024.
- Gheorghiu, A., T. Gu, and D. Pym, Inferentialist resource semantics, in Proceedings of the 40th Mathematical Foundations of Programming Semantics (MFPS). Electronic Notes in Theoretical Informatics and Computer Science (ENTICS), 2024b, Manuscript at https://arxiv.org/abs/2402.09217, Accessed August 2024.
- Gheorghiu, A. V., and S. Marin, Focused proof-search in the logic of bunched implications, in S. Kiefer, and C. Tasson, (eds.), Foundations of Software Science and Computation Structures - FOSSACS 24, vol. 12650 of LNCS, Springer, 2021, pp. 247–267, https://doi.org/10.1007/978-3-030-71995-1 13.
- Gheorghiu, A. V., and D. J. Pym, Semantical analysis of the logic of bunched implications, Studia Logica 111:525–571, 2023, https://doi.org/10.1007/s11225-022-10028-z.
- Gheorghiu, A. V., S. Docherty, and D. J. Pym, Reductive logic, coalgebra, and proof-search: a perspective from resource semantics, in S. Palmigiano, and M. Sadrzadeh, (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.
- Gheorghiu, A. V., T. Gu, and D. J. Pym, Proof-theoretic semantics for intuitionistic multiplicative linear logic, in Proceedings of the 32nd TABLEAUX, vol. 14278, LNAI, 2023, pp. 367–385.
- Girard, J. Y., Linear logic: its syntax and semantics, in J. Y. Girard, Y. Lafont, and L. Regnier, (eds.), Advances in Linear Logic. London Mathematical Society Lecture Note Series, Cambridge University Press, 1995, p 142, https://doi.org/10.1017/ CBO9780511629150.002.
- Ishtiaq, S. S., and P. W. O’Hearn, BI as an assertion language for mutable data structures, in C. Hankin, and D. Schmidt, (eds.), Symposium on Principles of Programming Languages—POPL. Association for Computing Machinery (ACM), 2001, pp. 14–26, https://doi.org/10.1145/360204.375719.
- Jaakko Kuorikoski, S. R. Making It Count: An Inferentialist Account of Computer Simulation, 2022, https://osf.io/preprints/socarxiv/v9bmr, https://doi.org/10. 31235/osf.io/v9bmr, Accessed January 2023.
- Kripke, S. A., Semantical analysis of intuitionistic logic I, Studies in Logic and the Foundations of Mathematics 40:92–130, 1965.
- Lambek, J., and P. J. Scott, Introduction to Higher-order Categorical Logic, vol 7. Cambridge University Press, Cambridge, 1988, https://doi.org/10.5555/53626.
- 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.
- O’Hearn, P. W., and D. J. Pym, The logic of bunched implications, Bulletin of Symbolic Logic 5(2):215–244, 1999, https://doi.org/10.2307/421090.
- Piecha, T., Completeness in proof-theoretic semantics, in T. Piecha, and P. Schroeder-Heister, (eds.), Advances in Proof-theoretic Semantics, Springer, Berlin, 2016, pp. 231–251.
- Piecha, T., and P. Schroeder-Heister, Atomic systems in proof-theoretic semantics: two approaches, in A. N. Fern´ ´ andez, O. P. Martins, and J. Redmond, (eds.), Epistemology, Knowledge and the Impact of Interaction, Springer, Berlin, 2016, https:// doi.org/10.1007/978-3-319-26506-3 2.
- Piecha, T., and P. Schroeder-Heister, The definitional view of atomic systems in proof-theoretic semantics, in P. Arazim, and T. L´aviˇcka, (eds.), The Logica Yearbook
- College Publications, London, 2017, pp. 185–200.
- Piecha, T., and P. Schroeder-Heister, 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.
- Piecha, T., W. de Campos Sanz, and P. Schroeder-Heister, 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.
- Prawitz, D., Ideas and results in proof theory, in J. Fenstad, (ed.), Studies in Logic and the Foundations of Mathematics, vol 63. Elsevier, Amsterdam, 1971, pp. 235–307, https://doi.org/10.1016/S0049-237X(08)70849-8.
- Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Courier Dover Publications, 2006 [1965], https://doi.org/10.2307/2271676.
- 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.
- Pym, D. J., J. M. Spring, and P. OHearn, Why separation logic works, Philosophy and Technology 32:483–516, 2019, https://doi.org/10.1007/s13347-018-0312-8.
- Pym, D. J., E. Ritter, and E. Robinson, E., Proof-theoretic semantics in sheaves (extended abstract), in ˚A. Hirvonen, and F. Vel´azquez-Quesada, (eds.), Proceedings of the Eleventh Scandinavian Logic Symposium—SLSS 11. Scandinvavian Logic Society, 2022.
- Read, S., Relevant Logic, Basil Blackwell, 1988, https://doi.org/10.2307/2219818.
- Reynolds, J. C., Separation logic: a logic for shared mutable data structures, in G. Plotkin, (ed.), Logic in Computer Science—LICS, Springer, 2002, pp. 55–74, https:// doi.org/10.1109/LICS.2002.1029817.
- Sandqvist, T., An Inferentialist Interpretation of Classical Logic, PhD thesis, Uppsala University, 2005.
- Sandqvist, T., Classical logic without bivalence, Analysis 69(2):211–218, 2009.
- Sandqvist, T., Base-extension semantics for intuitionistic sentential logic, Logic Journal of the IGPL 23(5):719–731, 2015a, https://doi.org/10.1093/jigpal/jzv021.
- Sandqvist, T., Hypothesis-discharging rules in atomic bases, in H. Wansing, (ed.), Dag Prawitz on Proofs and Meaning, Springer, Berlin, 2015b, pp. 313–328
- Sandqvist, T., Atomic Bases and the Validity of Peirce’s Law, 2022, https:// sites.google.com/view/wdl-ucl2022/schedule#h.ttn75i73elfw, World Logic Day— University College London, Accessed June 2023.
- Schroeder-Heister, P., Validity concepts in proof-theoretic semantics, Synthese 148(3):525–571, 2006, https://doi.org/10.1007/s11229-004-6296-1.
- Schroeder-Heister, P., Proof-theoretic versus model-theoretic consequence, in M. Pelis, (ed.), The Logica Yearbook 2007, 95b360ffe9ad174fd305539813800ea23fec33de, Filosofia, 2008.
- Schroeder-Heister, P., Proof-theoretic semantics, in E. N. Zalta,(ed.), The Stanford Encyclopedia of Philosophy, Spring 2018 edn., Metaphysics Research Lab, Stanford University, 2018.
- Stafford, W., Proof-theoretic semantics and inquisitive logic, Journal of Philosophical Logic 50:1199–1229, 2021.
- Szabo, M. E., (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company, 1969, https://doi.org/10.2307/2272429.
- Tarski, A., O poj¸eciu wynikania logicznego, Przegl¸ad Filozoficzny 39, 1936.
- Tarski, A., On the concept of following logically, History and Philosophy of Logic 23(3):155–196, 2002, https://doi.org/10.1080/0144534021000036683.
- Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, Cambridge, 2000, https://doi.org/10.1017/CBO9781139168717.
- van Dalen, D., Logic and Structure, 5th edn., Universitext, Springer, 2013, https:// doi.org/10.1007/978-1-4471-4558-5. T. Gu, A. V. Gheorghiu School of Electronics and Computer Science University of Southampton University Road Southampton SO17 1BJ T. Gu, A. V. Gheorghiu, D. J. Pym Department of Computer Science University College London Gower Street London WC1E 6BT [email protected] A. V. Gheorghiu [email protected] D. J. Pym Department of Philosophy University College London Gower Street London WC1E 6BT and Institute of Philosophy University of London Malet St London WC1E 7HU [email protected]
Related on this site
This paper belongs to Gheorghiu’s research in proof-theoretic semantics; the key terms are defined in the glossary.
Related papers: Semantical Analysis of the Logic of Bunched Implications · Focused Proof-search in the Logic of Bunched Implications · Inferentialist Resource Semantics