{'fraction_non_alphanumeric': 0.06110316118121504, 'fraction_numerical': 0.007102901001691167, 'mean_word_length': 3.9078082104322287, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Classical BI: Its Semantics and Proof Theory

We present Classical BI (CBI), a new addition to the family of bunched logics which originates in O'Hearn and Pym's logic of bunched implications BI. CBI differs from existing bunched logics in that its multiplicative connectives behave classically rather than intuitionistically (including in particular a multiplicative version of classical negation). At the semantic level, CBI-formulas have the normal bunched logic reading as declarative statements about resources, but its resource models necessarily feature more structure than those for other bunched logics; principally, they satisfy the requirement that every resource has a unique dual. At the proof-theoretic level, a very natural formalism for CBI is provided by a display calculus \`a la Belnap, which can be seen as a generalisation of the bunched sequent calculus for BI. In this paper we formulate the aforementioned model theory and proof theory for CBI, and prove some fundamental results about the logic, most notably completeness of the proof theory with respect to the semantics.


Introduction
Substructural logics, whose best-known varieties include linear logic, relevant logic and the Lambek calculus, are characterised by their restriction of the use of the so-called structural proof principles of classical logic [44]. These may be roughly characterised as those principles that are insensitive to the syntactic form of formulas, chiefly weakening (which permits the introduction of redundant premises into an argument) and contraction (which allows premises to be arbitrarily duplicated). For example, in linear logic, only formulas prefixed with a special "exponential" modality are subject to weakening and contraction, while in relevant logic it is usual for contraction but not weakening to be permitted.
Bunched logic is a relatively new area of substructural logic, but one that has been receiving increasing attention amongst the logical and computer science research communities in recent years. In bunched logic, the restriction on the use of structural proof principles is achieved by allowing the connectives of a standard "additive" propositional logic, which admits weakening and contraction, to be freely combined with those of a second "multiplicative" propositional logic, which does not. In contrast to linear logic, whose restricted treatment of additive connectives yields a natural constructive reading of proofs as computations [1], the inclusion of unrestricted additives in bunched logics gives rise to a simple Kripke-style truth interpretation according to which formulas can be understood as declarative statements about resource [40]. This resource reading of bunched logic has found substantial application in computer science, most notably in the shape of separation logic, which is a Hoare logic for program verification based upon various bunched logic models of heap memory [45]. The proof theory of bunched logic also differs markedly from the proof theory of linear logic, which is typically formulated in terms of sequent calculi whose sequents have the usual flat context structure based on lists or (multi)sets. However, since bunched logics contain both an (unrestricted) additive logic and a multiplicative one, proof systems for bunched logic employ both additive and multiplicative structural connectives for forming contexts (akin to the comma in standard sequent calculus). This gives rise to proof judgements whose contexts are trees -originally termed "bunches" -built from structural connectives and formulas.
Although the main ideas necessary to develop bunched logic can retrospectively be seen to have been present in earlier work on relevant logics, it first emerged fairly recently with the introduction of BI, O'Hearn and Pym's logic of bunched implications [36]. Semantically, BI can be seen to arise by considering the structure of cartesian doubly closed categories -i.e. categories with one cartesian closed structure and one symmetric monoidal closed structure [39]. Concretely, such categories correspond to a combination of standard intuitionistic logic with multiplicative intuitionistic linear logic 1 (MILL), and thus one has the following propositional connectives 2 for BI: Additive: ⊤ ⊥ ¬ ∧ ∨ → Multiplicative: ⊤ * * - * (where ¬ is the intuitionistic negation defined by ¬F = F → ⊥). As well as the semantics based on the aforementioned categories, BI can be given an algebraic semantics: one simply requires that the algebraic structure for BI has both the Heyting algebra structure required to interpret intuitionistic logic, and the residuated commutative monoid structure required to interpret MILL. By requiring a Boolean algebra instead of the Heyting algebra, one obtains the variant logic Boolean BI (BBI), which can be seen as a combination of classical logic and MILL [40,39]. Most of the computer science applications of bunched logic are in fact based on BBI rather than BI; for example, the heap model used in separation logic is a model of BBI [26].
A natural question from a logician's standpoint is whether bunched logics exist in which the multiplicative connectives behave classically, rather than intuitionistically (and do not simply collapse into their additive equivalents). A computer scientist might also enquire whether such a logic could, like its siblings, be understood semantically in terms of resource. In this paper, we address these questions by presenting a new addition to the bunched logic family, which we call Classical BI (CBI), and whose additives and multiplicatives both behave classically. In particular, CBI features multiplicative analogues of the additive falsity, negation, and disjunction, which are absent in the other bunched logics. Thus CBI can be seen as a combination of classical logic and multiplicative classical linear logic (MLL).
Proof-theoretic perspective: The proof theory of BI (cf. [39,36]) can be motivated by the observation that the presence of two implications → and - * should give rise to two contextforming operations, which correspond to the conjunctions ∧ and * at the meta-level. This situation is illustrated by the following (intuitionistic) sequent calculus right-introduction rules for the implications: Γ; F 1 ⊢ F 2 (→R) Γ ⊢ F 1 - * F 2 For similar reasons, there should also be two different "empty contexts" or structural units, which are the structural equivalents of ⊤ and ⊤ * respectively. Accordingly, the contexts Γ on the left-hand side of the sequents in the rules above are not sets or sequences, as in standard sequent calculi, but rather bunches: trees whose leaves are formulas or structural units and whose internal nodes are either semicolons or commas. The crucial difference between the latter two operations is that weakening and contraction are possible for the additive semicolon but not for the multiplicative comma. Since BI is intuitionistic in both its additive and multiplicative components, bunches arise only on the left-hand side of sequents, with a single formula on the right. In order to take into account the bunched contexts in BI sequents, the left-introduction rules for logical connectives are then formulated so as to apply at arbitrary positions within a bunch 3 . E.g., the left-introduction rules for the two implications can be formulated as: where Γ(∆) denotes a bunch Γ with a distinguished sub-bunch occurrence ∆. In contrast, the right-introduction rules need take into account only the top level of bunches, as in the right-introduction rules above for the implications.
For a classical bunched logic like CBI, it would appear natural from a proof-theoretic perspective to consider a full two-sided sequent calculus, in which semicolon and comma in bunches on the right of sequents correspond to the additive and multiplicative disjunctions. Unfortunately, it is far from clear whether there exists such a sequent calculus admitting cut-elimination, or a similar natural deduction system satisfying normalisation (see [5,39] for some discussion of the difficulties).
In Section 3, we address this rather unsatisfactory situation by formulating a display calculus proof system for CBI that satisfies cut-elimination, with an attendant subformula property for cut-free proofs. Display calculi were first introduced in the setting of Belnap's display logic [2], which is a generalised framework that can be instantiated to give consecution calculià la Gentzen for a wide class of logics. Display calculi are characterised by the fact that any proof judgement may always be rearranged so that a chosen structure occurrence appears alone on one side of the proof turnstile. Remarkably, Belnap also showed that cut-elimination is guaranteed for any display calculus whose proof rules satisfy 8 simple syntactic conditions. It is a straightforward matter to instantiate Belnap's display logic so as to obtain a display calculus for CBI, and to show that it meets the conditions for cut-elimination. Moreover, our display calculus is sound and complete with respect to validity in our class of CBI-models. Soundness follows by showing directly that each of the proof rules preserves CBI-validity. The proof of completeness, which is presented in Section 4, is by reduction to a completeness result for modal logic due to Sahlqvist.
Applications: Bunched logic (especially BBI) and its resource semantics has found application in several areas of computer science, including polymorphic abstraction [15], type systems for reference update and disposal [3], context logic for tree update [10] and, most ubiquitously, separation logic [45] which forms the basis of many contemporary approaches to reasoning about pointer programs (recent examples include [37,14,13]).
Unfortunately, the fact that CBI is a non-conservative extension of BBI appears to rule out the naive use of CBI for reasoning directly about some BBI-models such as the separation logic heap model, which is not a CBI-model. On the other hand, non-conservativity indicates that CBI can reasonably be expected to have different applications to those of BI and BBI. In Section 5 we consider a range of example CBI-models drawn from quite disparate areas of mathematics and computer science, including bit arithmetic, regular languages, money, generalised heaps and fractional permissions. In Section 6 we suggest some directions for future applications of CBI, and discuss some related work.
This paper is a revised and expanded version of [6], including several new results. We have endeavoured to include detailed proofs where space permits.

Frame semantics and validity for CBI
In this section we define CBI, a fully classical bunched logic featuring additive and multiplicative versions of all the usual propositional connectives (cf. [39]), via a class of Kripke-style frame models. We also compare the resulting notion of CBI-validity with validity in BBI.
Our CBI-models are based on the relational commutative monoids used to model BBI [22,10]. In fact, they are special cases of these monoids, containing extra structure: an involution operation '−' on elements and a distinguished element ∞ that characterises the result of combining an element with its involutive dual. We point the reader to Section 5 for a range of examples of such models.
In the following, we first recall the usual frame models of BBI, and then give the additional conditions required for such models to be CBI-models. Note that we write P(X) for the powerset of a set X. Definition 2.1 (BBI-model). A BBI-model is a relational commutative monoid, i.e. a tuple R, •, e , where e ∈ R and • : R×R → P(R) are such that • is commutative and associative, with r • e = {r} for all r ∈ R. Associativity of • is understood with respect to its pointwise extension to P(R) × P(R) → P(R), given by X • Y = def x∈X,y∈Y x • y.
Note that we could equally well represent the operation • in a BBI-model R, •, e as a ternary relation, i.e. • ⊆ R × R × R, as is typical for the frame models used for modal logic [4] and relevant logic [44]. We view • as a binary function with type R × R → P(R) because BBI-models are typically understood as abstract models of resource, in which • is understood as a (possibly non-deterministic) way of combining resources from the set R.
We remark that, in our original definition of CBI-models [6], both ∞ and −x for x ∈ R were defined as subsets of R, rather than elements of R. However, under such circumstances both −x and ∞ are forced to be singleton sets by the other conditions on CBI-models 4 . Thus there is no loss of generality in requiring −x and ∞ to be elements of R. Proposition 2.3 (Properties of CBI-models). If R, •, e, −, ∞ is a CBI-model then: Proof.
(1) By definition of CBI-models, and using commutativity of We prove that the two bi-implications hold by showing three implications. Suppose first that z ∈ x • y. Using associativity of •, we have: For the second implication, suppose that −x ∈ y • −z. By the first implication and part 1 above and commutativity of •, we then have as required: Finally, for the third implication, suppose that −y ∈ x • −z. Using the first and second implications together we obtain −−z ∈ y • −−x, i.e. z ∈ x • y as required. This completes the proof.
We note that for any CBI-model R, •, e, −, ∞ based on a fixed underlying BBI-model R, •, e , part 2 of Proposition 2.3 implies that the element ∞ is determined by the choice of '−', while the CBI-model axiom in Definition 2.2 ensures that, conversely, '−' is determined by the choice of ∞. We include both '−' and ∞ in our model definition only for convenience.
We now define the syntax of formulas of CBI, and their interpretation inside our CBImodels. We assume a fixed, countably infinite set V of propositional variables. Definition 2.4 (CBI-formula). Formulas of CBI are given by the following grammar: where P ranges over V. We treat the negations ¬ and ∼ as having greater precedence than the other connectives, and use parentheses to disambiguate where necessary. As usual, we write F ↔ G as an abbreviation for (F → G) ∧ (G → F ).
We remark that the connectives of CBI-formulas are the standard connectives of BBIformulas, plus a multiplicative falsity ⊥ * , negation ∼ and disjunction * ∨. In order to define the interpretation of our formulas in a given model, we need as usual environments which interpret the propositional variables, and a satisfaction or "forcing" relation which interprets formulas as true or false relative to model elements in a given environment.
Definition 2.5 (Environment). An environment for either a CBI-model R, •, e, −, ∞ or a BBI-model R, •, e is a function ρ : V → P(R) interpreting propositional variables as subsets of R. An environment for a model M will sometimes be called an M -environment. Definition 2.6 (CBI satisfaction relation). Let M = R, •, e, −, ∞ be a CBI-model. Satisfaction of a CBI-formula F by an M -environment ρ and an element r ∈ R is denoted r |= ρ F and defined by structural induction on F as follows: We remark that the above satisfaction relation for CBI is just an extension of the standard satisfaction relation for BBI with the clauses for ⊥ * , ∼ and * ∨. The interpretations of ⊥ * and * ∨, however, may be regarded as being determined by the interpretation of the multiplicative negation ∼ since, as we expect the classical relationships between multiplicative connectives to hold, we may simply define ⊥ * to be ∼⊤ * and F * ∨ G to be ∼(∼F * ∼G). The interpretation of ∼ itself will not surprise readers familiar with relevant logics, since negation there is usually semantically defined by the clause: x |= ∼A ⇔ x * |= A where x and x * are points in a model related by the somewhat notorious "Routley star", the philosophical interpretation of which has been the source of some angst for relevant logicians (see e.g. [43] for a discussion). In the setting of CBI, the involution operation '−' in a CBImodel plays the role of the Routley star. A more prosaic reason for our interpretation of ∼ is that it yields the expected semantic equivalences between formulas. Other definitions such as, e.g., the superficially appealing r |= ρ ∼F ⇔ −r |= ρ F do not work, because the model operation '−' does not itself behave like a negation (it is not antitonic with respect to entailment, for instance). For example, in analogy to ordinary classical logic, we would expect that r |= ρ F - * G iff r |= ρ ∼(F * ∼G). However, satisfaction of - * involves universal quantification while satisfaction of * involves existential quantification, strongly suggesting that the incorporation of a Boolean negation into ∼ is necessary to ensure such an outcome. One can also observe that the following is true in any CBI-model: −r |= ρ F ⇔ ∞ ∈ r • −r and −r |= ρ F ⇔ ∃r ′ , r ′′ . r ′′ ∈ r • r ′ and r ′ |= ρ F and r ′′ = ∞ i.e. −r |= ρ F ⇔ ∀r ′ , r ′′ . r ′′ ∈ r • r ′ and r ′ |= ρ F implies r ′′ = ∞ By interpreting ⊥ * and ∼ as we do in Definition 2.6, we immediately obtain r |= ρ ∼F iff r |= ρ F - * ⊥ * , another desired equivalence. Definition 2.7 (Formula validity). We say that a CBI-formula F is true in a CBI-model M = R, •, e, −, ∞ iff r |= ρ F for any M -environment ρ and r ∈ R. F is said to be (CBI)-valid if it is true in all CBI-models. Truth of BBI-formulas in BBI-models, and BBI-validity of formulas, is defined similarly. Lemma 2.8 (CBI equivalences). The following formulas are all CBI-valid: We fix an arbitrary CBI-model M and M -environment ρ. For each of the equivalences F ↔ G we require to show r |= ρ F ⇔ r |= ρ G. These follow directly from the definition of satisfaction, plus the properties of CBI-models given by Proposition 2.3. We show three of the cases in detail.
One might be tempted to think that, since CBI-models are BBI-models and the definition of satisfaction for CBI coincides with that of BBI when restricted to BBI-formulas, CBI and BBI might well be indistinguishable under such a restriction. Our next result establishes that this is by no means the case. Proposition 2.9 (Non-conservative extensionality). CBI is a non-conservative extension of BBI. That is, every BBI-valid formula is also CBI-valid, but there is a BBI-formula that is CBI-valid but not BBI-valid.
Proof. To see that BBI-valid formulas are also CBI-valid, let M = R, •, e, −, ∞ be a CBImodel, whence M ′ = R, •, e is a BBI-model. For any BBI-valid formula F we have that F is true in M ′ , and thus F is also true in M (because the definition of satisfaction of F coincides in CBI and BBI for BBI-formulas). Since M was arbitrarily chosen, F is CBI-valid as required. Now let P be a propositional variable and let I and J be abbreviations for BBI-formulas defined as follows: In a BBI-model R, •, e , the formula I denotes "nonextensible" elements of R, i.e. those elements r ∈ R such that r • r ′ = ∅ for all r ′ = e: r |= ρ I ⇔ ∀r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ and r ′ |= ρ ¬⊤ * implies r ′′ |= ρ ⊥ ⇔ ∀r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ implies r ′ |= ρ ¬⊤ * ⇔ ∀r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ implies r ′ = e ⇔ ∀r ′ ∈ R. r ′ = e implies r • r ′ = ∅ The formula J is satisfied by an arbitrary element of R iff there exists some element of R that satisfies the proposition P and is nonextensible: r |= ρ J ⇔ ∃r 1 , r 2 ∈ R. r ∈ r 1 • r 2 and r 1 |= ρ ⊤ and r 2 |= ρ ⊤ * ∧ ¬(P - * ¬I) ⇔ ∃r 1 , r 2 ∈ R. r ∈ r 1 • r 2 and r 2 |= ρ ⊤ * and r 2 |= ρ P - * ¬I ⇔ e |= ρ P - * ¬I ⇔ ∃r ′ , r ′′ ∈ R. r ′′ ∈ e • r ′ and r ′ |= ρ P but r ′′ |= ρ ¬I ⇔ ∃r ′ ∈ R. r ′ ∈ ρ(P ) and r ′ |= ρ I Note that in any CBI-model R, •, e, −, ∞ , for any r ∈ R we have r • −r = ∅ since ∞ ∈ r • −r by definition. Since ∞ is the unique element x ∈ R such that −x = e by Proposition 2.3, it follows that if r |= ρ I then r = ∞. Thus, in CBI-models, if r |= ρ I and r |= ρ J then r = ∞ ∈ ρ(P ), so the BBI-formula I ∧ J → P is CBI-valid. To see that I ∧J → P is not BBI-valid, consider the three-element model {e, a, b}, •, e , where • is defined by: e • x = x • e = {x} for all x ∈ {e, a, b}, and x • y = ∅ for all other x, y ∈ {e, a, b}. It is easy to verify that • is both commutative and associative and that e is a unit for •, so {e, a, b}, •, e is indeed a BBI-model. Now define an environment ρ for this model by ρ(P ) = {a}. We have both a |= ρ I and b |= ρ I because a and b are both nonextensible in the model, and b |= ρ J because a |= ρ I and a ∈ ρ(P ). Then we have b |= ρ I ∧ J but b |= ρ P , so I ∧ J → P is false in this model and hence not BBI-valid.
If R, •, e, −, ∞ is a CBI-model and the cardinality of x • y is ≤ 1 for all x, y ∈ R, then we understand • as a partial function R × R ⇀ R in the obvious way. The following proposition shows that, if we were to restrict our class of CBI-models to those in which the binary operation is a partial function rather than a relation, we would obtain a different notion of validity. In other words, CBI is sufficiently expressive to distinguish between partial functional and relational CBI-models. Proposition 2.10 (Distinction of partial functional and relational CBI-models). CBIvalidity does not coincide with validity in the class of partial functional CBI-models. That is, there is a CBI-formula that is not generally valid, but is true in every CBI-model R, •, e, −, ∞ in which • is a partial function.
Proof. Let K and L be abbreviations for CBI-formulas defined as follows: In a CBI-model R, •, e, −, ∞ , the formula K is satisfied by those model elements that can be extended by ∞ to obtain e: r |= ρ K ⇔ ∃r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ and r ′ |= ρ ¬⊥ * but r ′′ |= ρ ¬⊤ * ⇔ ∃r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ and r ′ = ∞ and r ′′ = e ⇔ e ∈ r • ∞ Similarly, the formula L is satisfied by those elements that, whenever they are extended by ∞, always yield e: r |= ρ L ⇔ ∀r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ and r ′ |= ρ ¬⊥ * implies r ′′ |= ρ ⊤ * ⇔ ∀r ′ , r ′′ ∈ R. r ′′ ∈ r • r ′ and r ′ = ∞ implies r ′′ = e ⇔ r • ∞ ⊆ {e} Let M = R, •, e, −, ∞ be a CBI-model in which • is a partial function, let ρ be an Menvironment and let r ∈ R. Suppose that r |= ρ K, so that e ∈ r • ∞ by the above. Since • is a partial function, the cardinality of r • ∞ is at most 1, so we must have r • ∞ = {e}, i.e., r |= ρ L. Thus the formula K → L is true in M , and so valid with respect to partial functional CBI-models. To see that K → L is not generally valid, we must provide a CBI-model in which it is false. Consider the three-element model {e, a, ∞}, •, e, −, ∞ , where − is defined by −e = ∞, −a = a, −∞ = e and • is defined as follows: In this model e is a unit for • and • is commutative by construction. It can also easily be verified that • is associative (e.g., a • (a • ∞) = {e, a, ∞} = (a • a) • ∞) and that −x is the unique element such that ∞ ∈ x • −x for all x ∈ {e, a, ∞}. Thus {e, a, ∞}, •, e, −, ∞ is indeed a CBI-model (and we note that • is not a partial function). Now for any environment ρ we have a |= ρ K since e ∈ a • ∞, but a |= ρ L since a ∈ a • ∞. Thus K → L is false in this model, and hence invalid.
Our proof of Proposition 2.10 does not transfer straightforwardly to BBI because it crucially relies upon the fact that, in CBI, we can write down a formula (¬⊥ * ) that is satisfied by exactly one model element (∞), which is not the unit e in general. Subsequent to submission of this paper, however, it has been shown by Larchey-Wendling and Galmiche that BBI is indeed incomplete with respect to partial functional models [30].
3. DL CBI : a display calculus proof system for CBI In this section, we present DL CBI , a display calculus for CBI based on Belnap's general display logic [2], which provides a generic framework for obtaining formal Gentzen-style consecution calculi for a large class of logics. Display calculi are akin to sequent calculi in that logical connectives are specified by a pair of introduction rules introducing the connective on the left and right of proof judgements respectively. However, the proof judgements of display calculi have a richer structure than an ordinary sequent, and thus we require a corresponding set of meta-level rules (called display postulates) for manipulating this structure. This ensures the characteristic, and very useful display property of display calculi: any proof judgement may be rearranged so that any given part of the judgement appears alone on one side of the turnstile (without loss of information). In addition to its conceptual elegance, this property ensures that cut-elimination holds for any display calculus whose structural rules obey a few easily verified conditions (cf. [2]). Our display calculus DL CBI indeed satisfies these cut-elimination conditions. Furthermore, it is sound and complete with respect to our CBI-models.
Belnap's original formulation of display logic treats an arbitrary number of "families" of propositional connectives. The necessary structural connectives, display postulates and logical introduction rules are then ascribed automatically to each family, with only the structural rules governing the family chosen freely. For CBI, it is obvious that there are two complete families of propositional connectives, one additive and one multiplicative. Thus the formulation of DL CBI can be viewed as arising more or less directly from Belnap's general schema.
The proof judgements of DL CBI , called consecutions, are built from structures which generalise the bunches used in existing proof systems for BI (cf. [39]). Definition 3.1 (Structure / consecution). A DL CBI -structure X is constructed according to the following grammar: where F ranges over CBI-formulas. If X and Y are structures then X ⊢ Y is said to be a consecution. Figure 1 gives a summary of the structural connectives of our display calculus and their semantic reading as antecedents (or premises) and consequents (or conclusions) in a consecution. However, the presence of the meta-level negations ♯ and ♭ in our structures leads to a subtler notion of antecedent and consequent parts of consecutions than the simple left-right division of sequent calculus. Informally, moving inside a meta-level negation flips the interpretation of its immediate substructure. For example, if ♯X or ♭X is an antecedent part then the substructure X should be interpreted as a consequent part, and vice versa. This notion is made formal by the following definition. Figure 1: The structural connectives of DL CBI .

Connective Arity Antecedent meaning Consequent meaning
Definition 3.2 (Antecedent part / consequent part). A structure occurrence W is said to be a part of another structure Z if W occurs as a substructure of Z (in the obvious sense). W is said to be a positive part of Z if W occurs inside an even number of occurrences of ♯ and ♭ in Z, and a negative part of Z otherwise. A structure occurrence W is said to be an antecedent part of a consecution X ⊢ Y if it is a positive part of X or a negative part of Y . W is said to be a consequent part of X ⊢ Y if it is a negative part of X or a positive part of Y .
To give the formal interpretation of our consecutions in the following definition, we employ a pair of mutually recursive functions to capture the dependency between antecedent and consequent interpretations.

Definition 3.3 (Consecution validity).
For any structure X we mutually define two formulas Ψ X and Υ X by induction on the structure of X as follows: We write a proof rule with a double line between premise and conclusion to indicate that it is bidirectional, i.e., that the roles of premise and conclusion may be reversed. A figure with three consecutions separated by two double lines is used to abbreviate two bidirectional rules in the obvious way.
there is a derivation of one from the other using only the display postulates given in Figure 2.
The display postulates for DL CBI are essentially Belnap's original display postulates, instantiated (twice) to the additive and multiplicative connective families of CBI. The only difference is that our postulates build commutativity of the comma and semicolon into the notion of display-equivalence, since in CBI both the conjunctions and both the disjunctions are commutative.
The fundamental characteristic of display calculi is their ability to "display" structures occurring in a consecution by rearranging it using the display postulates.
Proof. Essentially, one uses the display postulates to move any structure surrounding W to the opposite side of the consecution, or to eliminate any preceding occurrences of ♯ and ♭ (note that for each possible position of W in X ⊢ Y there are display postulates allowing the topmost level of structure above W to be moved away or eliminated). Moreover, each of the display postulates preserves antecedent and consequent parts of consecutions, so that W must end up on the correct side of the consecution at the end of this process. The details are straightforward.
Example 3.6. The antecedent part Y of the consecution ♭(X, ♯Y ) ⊢ Z; ♭W can be displayed as follows: The proof rules of DL CBI are given in Figure 3. The identity rules consist of the usual identity axiom for propositional variables, a cut rule and a rule for display equivalence. The logical rules follow the division between left and right introduction rules familiar from sequent calculus. Note that, since we can appeal to Theorem 3.5, the formula introduced by a logical rule is always displayed in its conclusion. Both the identity rules and the logical rules are the standard ones for display logic, instantiated to CBI. The structural rules of DL CBI implement suitable associativity and unitary laws on both sides of consecutions, plus weakening and contraction for the (additive) semicolon.
Identity rules: Figure 3: The proof rules of DL CBI . W, X, Y, Z range over structures, F, G range over CBIformulas and P ranges over V.
The identity axiom of DL CBI is postulated only for propositional variables 5 , but can be recovered for arbitrary formulas. We say a consecution is cut-free provable if it has a DL CBI proof containing no instances of (Cut). Proposition 3.7. F ⊢ F is cut-free provable in DL CBI for any formula F .
Proof. By structural induction on F .
Proof. The DL CBI proof rules satisfy the conditions shown by Belnap in [2] to be sufficient for cut-elimination to hold. We state these conditions and indicate how they are verified in Appendix A.
The following corollary of Theorem 3.8 uses the notion of a subformula of a CBI-formula, defined in the usual way.
Proof. If X ⊢ Y is provable then it has a cut-free proof by Theorem 3.8. By inspection of the DL CBI rules, no rule instance in this proof can have in its premises any formula that is not a subformula of a formula occurring in its conclusion. Thus a cut-free proof of X ⊢ Y cannot contain any formulas which are not subformulas of formulas in X ⊢ Y .
Proof. If ∅ ⊢ ∅ were DL CBI -provable then, by the subformula property (Corollary 3.9) there is a proof of ∅ ⊢ ∅ containing no formula occurrences anywhere. But every axiom of DL CBI contains a formula occurrence, so this is impossible. Then ∅ ⊢ ∅ cannot be provable either, otherwise ∅; ∅ ⊢ ∅; ∅ is provable by applying (WkL) and (WkR), whence ∅ ⊢ ∅ is provable by applying (∅L) and (∅R), which is a contradiction.
Our main technical results concerning DL CBI are the following.
Proof. It suffices to show that each proof rule of DL CBI is locally sound in that validity of the conclusion follows from the validity of the premises. In the particular case of the display rule (≡ D ), local soundness follows by establishing that each display postulate (see Figure 2) is locally sound. We show how to deal with some sample rule cases.
Since the premise X ⊢ F is valid and r ′ |= ρ Ψ X by assumption, we have r ′ |= ρ F . Then, since r |= ρ F - * G and r ′′ ∈ r • r ′ , we have r ′′ |= ρ G. Finally, since the premise G ⊢ Y is valid by assumption, we have r ′′ |= ρ Υ Y as required.
•, e, −, ∞ be a CBI-model, let r ∈ R and suppose r |= ρ F * ∨ G, whence we require to show r |= ρ Υ X * ∨ Υ Y . So, let r 1 , r 2 ∈ R be such that −r ∈ r 1 • r 2 , whence we require to show either −r 1 |= ρ Υ X or −r 2 |= ρ Υ Y . Since −r ∈ r 1 • r 2 and r |= ρ F * ∨ G, we have either r 1 |= ρ F or r 2 |= ρ G. Then, since the premises F ⊢ X and G ⊢ Y are assumed valid, we have the required conclusion in either case.
Case (MD1a). We show how to treat one direction of this display postulate; the reverse direction is symmetric.
We give the proof of Theorem 3.12 in Section 4. We remark that, although cut-free proofs in DL CBI enjoy the subformula property, they do not enjoy the analogous "substructure property", and cut-free proof search in our system is still highly non-deterministic due to the presence of the display postulates and structural rules, the usage of which cannot be straightforwardly constrained in general. In Figure 4 we give a sample cut-free proof of the consecution ∼¬F ⊢ ¬∼F , which illustrates the problems. The applications of display-equivalence are required in order to apply the logical rules, as one would expect, but our derivation also makes essential use of contraction, weakening and a unitary law. It is plausible that the explicit use of at least some of these structural rules can be eliminated by suitable reformulations of the logical rules. However, the inherent nondeterminism in proof search cannot be removed by refining DL CBI without loss of power since, by soundness and completeness, provability in DL CBI is equivalent to validity in CBI, which has been recently shown undecidable by the first author and Kanovich [7]. This is not fundamentally surprising, since at least some displayable logics are known to be undecidable; indeed, one of Belnap's original applications of display logic was in giving a display calculus for the full relevant logic R, which was famously proven undecidable by Urquhart [48]. (Unfortunately, we cannot distinguish decidable display calculi from undecidable ones in general; the decidability of an arbitrary displayable logic was itself shown undecidable by Kracht [29].) Nonetheless, we argue that there are good reasons to prefer our DL CBI over arbitrary complete proof systems (e.g. Hilbert systems) without cut-elimination. Display calculi inherit the main virtues of traditional Gentzen systems: they distinguish structural principles from logical ones, and make explicit the considerable proof burden that exists at the meta-level, but nevertheless retain a theoretically very elegant and symmetric presentation. Furthermore, as a result of the subformula property one has in display calculi what might be called a property of "finite choice" for proof search: for any consecution there are only finitely many ways of applying any rule to it in a backwards fashion 6 .

Completeness of DL CBI
In this section we prove completeness of our display calculus DL CBI with respect to validity in CBI-models. As in the case of the analogous result for BBI in [10], our result hinges on a general completeness theorem for modal logic due to Sahlqvist. However, we also require an extra layer of translation between Hilbert-style proofs and proofs in DL CBI .
Our proof is divided into three main parts. First, in subsection 4.1, we reinvent CBI as a modal logic by defining a class of standard modal frames, with associated modalities corresponding to the standard CBI-model operations, that satisfy a certain set of modal logic axioms. By appealing to Sahlqvist's completeness theorem, we obtain a complete Hilbertstyle proof theory for this class of frames. It then remains to connect the modal presentation of CBI to our standard presentation. In subsection 4.2, we show that the aforementioned class of modal frames is exactly the class of CBI-models given by Definition 2.2. Then, in subsection 4.3, we show how to translate any modal logic proof into a DL CBI proof. Thus we obtain the DL CBI -provability of any valid consecution.
4.1. CBI as a modal logic. In this subsection we define the semantics of a modal logic corresponding to CBI, and obtain a complete proof theory with respect to this semantics, all using standard modal techniques (see e.g. [4]).
We first define ML CBI frames, which are standard modal frames with associated modalities corresponding to the CBI-model operations in Definition 2.2. We extend • to P(R) × P(R) → P(R), and − to P(R) → P(R), in the same pointwise manner as in Definition 2.2. If e is a singleton set then the frame is said to be unitary.
where P ranges over V. We remark that we read e, ∞, −, •, −• as modalities (with the obvious arities). We regard → as having weaker precedence than these modalities, and use parentheses to disambiguate where necessary.
The satisfaction relation for modal logic formulas in ML CBI frames is defined exactly as in Definition 2.6 for the additive connectives, and the modalities are given a "diamond" possibility interpretation: We remark that the −• modality -which does not correspond directly to a CBI-model operation but should be read informally as ¬(A 1 - * ¬A 2 ) -will be helpful later in giving a modal axiomatisation of CBI-models; see Defn. 4.1.6. We could alternatively employ a modality corresponding directly to - * , but it is much more technically convenient to work exclusively with "diamond" modalities.
Given any set A of modal logic axioms, we define A-models to be those ML CBI frames in which every axiom in A holds. The standard modal logic proof theory corresponding to the class of A-models is given by the following definition (cf. [4]).
Definition 4.1.3 (Modal logic proof theory). The modal logic proof theory generated by a set A of modal logic axioms, denoted by LA, consists of some fixed finite axiomatisation of propositional classical logic, extended with the following axioms and proof rules: where A, B, C range over modal logic formulas, P, Q, R are propositional variables, and A ↔ B is as usual an abbreviation for (A → B) ∧ (B → A).
Note that the axioms and rules for the modalities which are added to A by Definition 4.1.3 are just the axioms and rules of the standard modal logic K, instantiated to each of our "diamond"-type modalities e, ∞, −, • and −•. We emphasise that, by definition, the latter are diamond modalities rather than logical connectives. In particular, the modality '−' is not a negation (−A should be understood informally as the CBI-formula ∼¬A), and is monotonic rather than antitonic with respect to entailment, as embodied by the rule (⋄−). Similarly, the −• modality is monotonic in its left-hand argument because it is a diamond modality and not an implication.
We now state a sufficient condition, due to Sahlqvist, for completeness of LA to hold with respect to the class of A-models.
where P ranges over V. A very simple Sahlqvist formula is a modal logic formula of the form S → A + , where S is a very simple Sahlqvist antecedent and A + is a modal logic formula which is positive in that no propositional variable P in A + may occur inside the scope of an odd number of occurrences of ¬.
Theorem 4.1.5 (Sahlqvist [4]). Let A be a set of modal logic axioms consisting only of very simple Sahlqvist formulas. Then the modal logic proof theory LA is complete with respect to the class of A-models. That is, if a modal logic formula F is valid with respect to A-models then it is provable in LA.
Definition 4.1.6 (Modal logic axioms for CBI). The axiom set AX CBI consists of the following modal logic formulas, where P, Q, R are propositional variables:   (1) M is the disjoint union of the models M x for x ∈ e.
Proof. The required properties follow straightforwardly from the properties of CBI-models given by Definition 2.2 and Proposition 2.3. Proof. We first show that −x is a singleton by contradiction, using the fact that −−x = {x} must hold for any set x, as a consequence of axioms (8) and (9).
We prove that ∞ is a singleton by deriving ∞ = −e. Using the axioms in Definition 4.1.6, we will show that e −• X = X must hold for any set X. This fact, together with axioms (10) and (11) instantiated with P = e gives the desired consequence ∞ = −e.
It remains to show e −• X = X. Axioms (6) and (7) give the two directions of: for any p, q, r ∈ R, and axioms (1), (2) and (3) give, for any x ∈ R: x • e = {x} Therefore we have that, for any x ∈ R:  Proof. First observe that in any ML CBI frame R, •, −•, e, −, ∞ , the AX CBI axioms (6) and (7) hold iff we have, for all X, Y in P(R): Let M be a CBI-model. Then axioms (6) and (7) (6) and (7), it follows that R, •, e, −, ∞ = M ′ , hence − is surjective. Definition 4.2.5 (Translation of CBI-formulas to modal logic formulas). We define a function − from CBI-formulas to modal logic formulas by induction on the structure of CBIformulas, as follows: where P in the first clause ranges over V. We extend the domain of − to DL CBI consecutions by: X ⊢ Y = Ψ X → Υ Y where Ψ − and Υ − are the functions given in Definition 3.3.
In the following, we write F [G/P ] to denote the result of substituting the formula G for all occurrences of the propositional variable P in the formula F . This notation applies both to CBI-formulas and to modal logic formulas. Proof. Let F be a CBI-formula and A a modal logic formula. We define F ≃ A to hold iff for all environments ρ, and all r ∈ R, the following holds: The proof is divided into two parts. The first part establishes the following properties: We show one interesting case (7). By Lemma 2.8 we have that P 1 * ∨ P 2 is equivalent to ∼(∼P 1 * ∼P 2 ), therefore it is sufficient to prove ∼(∼P 1 * ∼P 2 ) ≃ ¬−(¬−P 1 • ¬−P 2 ). By (6) we have ∼P i ≃ ¬−P i for i ∈ {1, 2}, hence by (1) and (3) we obtain (∼P 1 * ∼P 2 ) ≃ (¬−P 1 • ¬−P 2 ). Thus by (1) and (6) we conclude ∼(∼P 1 * ∼P 2 ) ≃ ¬−(¬−P 1 • ¬−P 2 ), as required.
The second part establishes F ≃ F by induction on the structure of F , using the results from the first part.
Proof. By definition, X ⊢ Y is valid iff Ψ X → Υ Y is true in every CBI-model M . By Lemma 4.2.6, this is equivalent to: Since − is a bijection onto unitary AX CBI -models by Lemma 4.2.4, this is equivalent to: Ψ X → Υ Y is true in all unitary AX CBI -models i.e. Ψ X → Υ Y is valid wrt. unitary AX CBI -models.
By combining Proposition 4.2.7 and Corollary 4.1.9 we obtain the following key intermediate result towards completeness for DL CBI :

4.3.
From modal logic proofs to DL CBI proofs. Definition 4.3.1 (Translation from modal logic formulas to CBI-formulas). We define a function − from modal logic formulas to CBI-formulas by induction on the structure of CBI-formulas, as follows:  Proof. First, we note that all of the proof rules of LAX CBI , except (Subst), are easily derivable in DL CBI under the embedding. The rule (Subst) is admissible in DL CBI (under the embedding) because each of its proof rules is closed under the substitution of arbitrary formulas for propositional variables; in the case of the axiom rule (Id) this requires an appeal to Proposition 3.7. It remains to show that ∅ ⊢ A is DL CBI -derivable for every axiom A of LAX CBI . The AX CBI axioms are mainly straightforward, with the chief exceptions being axioms (6) and (7). (We remark that axioms (8) and (9) are straightforward once one has DL CBI proofs that ¬ and ∼ commute; see Figure 4 for a proof of ∼¬F ⊢ ¬∼F .) In the case of AX CBI axiom (6), we need to show the consecution ∅ ⊢ Q ∧ (R * P ) → (R ∧ ¬(P - * ¬Q)) * ⊤ is provable in DL CBI . We give a suitable derivation in Figure 5. The treatment of AX CBI axiom (7) is broadly similar. It remains to treat the generic modal logic axioms of LAX CBI , which again are mainly straightforward and involve showing distribution of the modalities over ∨. E.g., in the case of the axiom (−•∨L) we require to show that ∅ ⊢ ¬((P ∨ Q) - * We give a derivation of one direction of this bi-implication in Figure 6. The other direction of the bi-implication, and the other axioms, are derived in a similar fashion.
The following corollary of Proposition 4.3.2 is immediate by induction over the structure of LAX CBI proofs.
We write F ⊣⊢ G, where F and G are CBI-formulas, to mean that both F ⊢ G and G ⊢ F are provable (in DL CBI ), and call F ⊣⊢ G a derivable equivalence (of DL CBI ). We observe that derivable equivalence in DL CBI is indeed an equivalence relation: it is reflexive by Proposition 3.7, symmetric by definition and transitive by the DL CBI rule (Cut). Lemma 4.3.4. F ⊣⊢ F is a derivable equivalence of DL CBI for any CBI-formula F .
With this in mind, we now proceed by structural induction on F . The base cases, in which F = F , are immediate since F ⊣⊢ F is a derivable equivalence of DL CBI by Proposition 3.7. Most of the other cases are straightforward using the induction hypothesis and the fact that ¬¬F ⊣⊢ F is easily seen to be a derivable equivalence of DL CBI . We show one direction of the only non-trivial case, F = F 1 * ∨ F 2 , in Figure 7. The reverse direction is similar. Proposition 5.1 (Abelian groups as CBI-models). Any Abelian group R, •, e, − can be understood as a CBI-model R, •, e, −, e . Conversely, if R, •, e, −, ∞ is a CBI-model with • a partial function, then imposing the condition ∞ = e forces • to be total, whence R, •, e, − is an Abelian group.
Proof. (⇒) Let R, •, e, − be an Abelian group. To see that R, •, e is a BBI-model, we just note that • is associative and commutative and that e is the unit of • by the group axioms. By the uniqueness of group inverses, we then have that −x is the unique y such that e ∈ x • y. Thus R, •, e, −, e is a CBI-model, as required.
(⇐) Let R, •, e, −, ∞ be a CBI-model with ∞ = e and • a partial function. First note that, by the latter two facts, we have −x • x = ∞ = e for all x ∈ R. Now for any x, y ∈ R we observe that − To see that R, •, e, − is an Abelian group, we first observe that, since • is a total function by the above, R, •, e is a total commutative monoid by the conditions imposed on BBI-models. The uniqueness of group inverses then follows immediately from the CBImodel conditions and the fact that ∞ = e.
The following example, which looks at some typical resource interpretations of CBIformulas inside an Abelian group model, builds on the "vending machine" model for BI given by Pym, O'Hearn and Yang [40], which itself was inspired by Girard's well-known "Marlboro and Camel" illustration of linear logic [23].
Example 5.2 (Personal finance). Let Z, +, 0, − be the Abelian group of integers under addition with identity 0, where − is the usual unary minus. This group can be understood as a CBI-model Z, +, 0, −, 0 by Proposition 5.1. We view the elements of this model as financial resources, i.e money (which we shall measure in pounds sterling, £), with positive and negative integers representing respectively credit and debt. We read the CBI-satisfaction relation £m |= ρ F informally as "£m is enough to make F true", and show how to read some example CBI-formulas according to this interpretation.
Let C and W be atomic formulas denoting respectively the ability to buy cigarettes costing £5 and whisky costing £20, so that we have £m |= ρ C ⇔ m ≥ 5 and £m |= ρ W ⇔ m ≥ 20. Then the formula C ∧ W denotes the ability to buy cigarettes and the ability to buy whisky (but not necessarily to buy both together): In contrast, the formula C * W denotes the ability to buy both cigarettes and whisky together: £m |= ρ C * W ⇔ ∃m 1 , m 2 ∈ Z. £m = £m 1 + £m 2 and £m 1 |= ρ C and £m 2 |= ρ W ⇔ ∃m 1 , m 2 ∈ Z. m = m 1 + m 2 and m 1 ≥ 5 and m 2 ≥ 20 ⇔ m ≥ 25

J. BROTHERSTON AND C. CALCAGNO
The multiplicative implication C - * W denotes the fact that if one acquires enough money to buy cigarettes then the resulting balance of funds is sufficient to buy whisky: We remark that all of the above formulas are BBI-formulas, and so would be interpreted in exactly the same way in the BBI-model Z, +, 0 . Let us examine the multiplicative connectives that are particular to CBI. We have £m |= ρ ⊥ * ⇔ m = 0, so that ⊥ * simply denotes the fact that one has either some credit or some debt. (This is exactly the interpretation of the formula ¬⊤ * , a collapse induced by the fact that e and ∞ coincide in the Abelian group model.) Now consider the formula ∼C. We have: So ∼C denotes the fact that one's debt, if any, is strictly less than the price of a pack of cigarettes. As for the multiplicative disjunction, C * ∨ W , we have: It is not immediately obvious how to read this formula informally. However, observing that C * ∨ W is semantically equivalent to ∼C - * W and to ∼W - * C, the meaning becomes perfectly clear: if one spends strictly less than the price of a pack of cigarettes, then one will still have enough money to buy whisky, and vice versa.
We remark that, in fact, there is a logic in the relevantist mould, called Abelian logic, whose models are exactly the lattice-ordered Abelian groups [33]. Proposition 5.3 (Effect algebras as CBI-models). Effect algebras, which arise in the mathematical foundations of quantum-mechanical systems [20], are exactly CBI-models R, •, e, −, ∞ such that • is a partial function and ∞ is nonextensible (i.e. x • ∞ is undefined for all x = e).
The CBI-models constructed in the next examples are all effect algebras.
Example 5.4 (Languages). Let Σ be an alphabet and let L(Σ) be any set of languages over Σ that is closed under union and complement and contains the empty language ǫ (e.g., the set of regular languages over Σ). Write Σ * for the set of all words over Σ, and note that Σ * ∈ L(Σ). Let L 1 + L 2 be the union of disjoint languages L 1 and L 2 , with L 1 + L 2 undefined if L 1 and L 2 are not disjoint. Clearly L(Σ), +, ǫ is a partial commutative monoid. Furthermore, for any language L, its complement L = Σ * \ L is the unique language such that L + L = Σ * . Thus L(Σ), +, ǫ, · , Σ * is a CBI-model. To see that it is also an effect algebra, just notice that + is a partial function and Σ * is nonextensible because Σ * + L is undefined for any L = ǫ.
Example 5.5 (Action communication). Let A be any set of objects (to be understood as CCS-style "actions" [34]), define the set A = {a | a ∈ A} to be disjoint from A, and let elements 0, τ ∈ A ∪ A, whence we write B = def A ∪ A ∪ {0, τ }. We extend the operation · to B → B by 0 = def τ and a = def a, and define a partial binary operation · | · with type B × B ⇀ B as follows: The operation · | · models a very simplistic version of communication between actions: communication with the empty action 0 has no effect, communication between a pair of dual actions b and b (which may be read, e.g., as "send b" and "receive b") results in the "successful communication" action τ , and all other communications are disallowed. It is easy to check that B, ·|·, 0 is a partial commutative monoid. Furthermore, for any b ∈ B, we clearly have b the unique element with b | b = τ . Thus B, · | · , 0, · , τ is a CBImodel. Furthermore, it is clearly an effect algebra, because · | · is a partial function and τ is nonextensible.
Example 5.6 (Generalised heaps). A natural question is whether the heap models of BBI employed in separation logic (see e.g. [11]) are also CBI-models. Consider the basic heap model given by the partial commutative monoid H, •, e , where H = def N ⇀ fin Z is the set of heaps (i.e. partial functions mapping finitely many natural numbers to integers), h 1 • h 2 is the union of partial functions h 1 and h 2 when their domains are disjoint (and undefined otherwise), and e is the function with empty domain. Unfortunately, no choice of ∞ for H, •, e gives rise to a CBI-model.
However, it is possible to embed the set of heaps H above into a more general structure H ′ , • ′ , e ′ , where H ′ = def N → P(Z) is the set of (total) functions from natural numbers to sets of integers (we may additionally require that h(n) = ∅ for finitely or cofinitely many n ∈ N). Then • ′ : H ′ × H ′ ⇀ H ′ is defined by: if h 1 (n) and h 2 (n) are disjoint for all n, then (h 1 • ′ h 2 )(n) = h 1 (n) ∪ h 2 (n), otherwise h 1 • ′ h 2 is undefined. The unit e ′ is defined by e ′ (n) = ∅ for all n ∈ N. A CBI-model H ′ , • ′ , e ′ , −, ∞ is then obtained by defining ∞(n) = Z and (−h)(n) = Z \ h(n) for all n ∈ N.
We note that this model behaves quite differently than H, •, e : generalised heaps with overlapping domains can be composed providing that their contents do not overlap for any point in the domain. We consider the interpretation of some "separation logic-like" formulas inside this model. Let X ⊆ Z be some fixed set of integers and define the atomic formula 4 → X by the following: h |= ρ 4 → X ⇔ h(4) = X i.e., the formula 4 → X denotes those generalised heaps with contents exactly X at location 4. This can be seen as the set-based analogue of the → predicate in standard separation logic [45] (with fixed arguments for simplicity, as we are working in a propositional setting). Then we have, for example: so that the formula (4 → X) * ⊤ denotes the general heaps which contain every element of X at location 4. If we then take the multiplicative negation of this formula, we have, using the above: x ∈ h(4) i.e., this formula denotes the general heaps containing some element from X at location 4. So, in this case, the multiplicative negation has the effect of changing a universal quantifier to an existential one. The meaning of multiplicative disjunctions, however, is typically very complicated. For example, picking a second set Y ⊆ Z and defining the atomic formula 4 → Y in the same way as 4 → X, we have, using previous derivations: so that this disjunction denotes those general heaps that either contain one of X and Y , or are missing a single common element from X and Y , at location 4. We give a short proof of the last equivalence above, since it is not especially obvious.
We note that a number of general categorical constructions for effect algebras have recently appeared in [27].
Our next examples differ both from Abelian groups in that e and ∞ are non-identical, and from effect algebras in that ∞ is extensible. Indeed, as shown by our Example 5.8 below, fixing the monoidal structure of a CBI-model does not in general determine the choice of ∞.
Example 5.7 (Bit arithmetic). Let n ∈ N and observe that an n-bit binary number can be represented as an element of the set {0, 1} n . Let XOR and NOT be the usual logical operations on binary numbers. Then the following is a CBI-model: In this model, the resources e and ∞ are the n-bit representations of 0 and 2 n −1 respectively. Example 5.8 (Integer modulo arithmetic). Consider the monoid Z n , + n , 0 , where Z n is the set of integers modulo n, and + n is addition modulo n. We can form a CBI-model from this monoid by choosing, for any m ∈ Z n , ∞ = def m and −k = def m − n k (where − n is subtraction modulo n).
Example 5.9 (Syntactic models). Given an arbitrary monoid R, •, e , we give a syntactic construction to generate a CBI-model R ′ , • ′ , e ′ , − ′ , ∞ ′ . Consider the set T of terms given by the grammar: t ∈ T ::= r ∈ R | ∞ | t · t | −t and let ≈ be the least congruence such that: We write T /≈ for the quotient of T by the relation ≈, and [t] for the equivalence class of t. The required CBI-model We now consider some general ways of composing CBI-models.
We need to check that R, •, e is a BBI-model. The commutativity of • is immediate by the commutativity of • 1 and • 2 . Similarly, x • e = {x} for all x ∈ R because e = e 1 is a unit of • 1 and e = e 2 is a unit of • 2 . To see that • is associative, we let x, y, z ∈ R and show that x • (y • z) = (x • y) • z by case analysis.
Case: at least one of x, y, z is e. We are immediately done by the fact that e is a unit for •.
Case: at least one of x, y, z is ∞. We may assume that none of x, y, z is e, since these possibilities are covered by the previous case, and so it follows by assumption that ∞ 1 and Case: all of x, y, z ∈ R 1 . We may assume by the previous cases that none of x, y, z is either e or ∞, so we have x • (y • z) = x • 1 (y • 1 z) and (x • y) • z = (x • 1 y) • 1 z, whence we are done by the associativity of • 1 .
Case: all of x, y, z ∈ R 2 . Similar to the case above.
Case: none of the above. We have x • (y • z) = ∅ = (x • y) • z since x • y = ∅ whenever x ∈ R 1 , y ∈ R 2 and neither x nor y is e or ∞. This covers all the cases, so • is indeed associative.
Now to see that R, •, e, −, ∞ is a CBI-model, given x ∈ R we need to show that −x is the unique y ∈ R such that ∞ ∈ x • y. It is easily verified that ∞ ∈ x • −x for all We remark that the restrictions on ∞ 1 and ∞ 2 in Lemma 5.10 are needed in order to ensure the associativity of •. For example, if x ∈ R 1 and y ∈ R 2 and x, y = e then (x • y) Lemma 5.11 (Generalised Cartesian product of CBI-models). Let A be an ordered set and write ⊗ a∈A x a for an ordered tuple indexed by the elements of A. Suppose that M a = R a , • a , e a , − a , ∞ a is a CBI-model for each a ∈ A. Then R, •, ⊗ a∈A e a , −, ⊗ a∈A ∞ a is a CBI-model, where R denotes the A-ordered Cartesian product of the sets R a , and the operations • : R × R → P(R) and − : R → R are defined as follows: In the following, all uses of notation should be understood as ranging over all a ∈ A (we suppress the explicit subscript for legibility). First, we need to check that R, •, ⊗ a∈A e a is a BBI-model. The commutativity of • follows immediately from its definition and the commutativity of each • a . To see that ⊗ a∈A e a is a unit for • we observe: ⊗ a∈A x a • ⊗ a∈A e a = wa∈xa•aea {⊗ a∈A w a } = wa∈{xa} {⊗ a∈A w a } = {⊗ a∈A x a } Next we need to check that • is associative. Using the the standard extension of • to P(R) × P(R) → P(R) we have: as required by the associativity of each • a . Now, to see that R, •, ⊗ a∈A e a , −, ⊗ a∈A ∞ a is a CBI-model, it just remains to check that the required conditions on − and ⊗ a∈A ∞ a hold. We have by definition: (− a x a ) for all a ∈ A we have ⊗ a∈A ∞ a ∈ ⊗ a∈A x a • −(⊗ a∈A x a ) as required. To see that −(⊗ a∈A x a ) is the unique element of R satisfying this condition, suppose ⊗ a∈A ∞ a ∈ ⊗ a∈A x a • ⊗ a∈A y a . Then for each a ∈ A we would have ∞ a ∈ x a • a y a , which implies y a = − a x a for each a ∈ A and thus ⊗ a∈A y a = ⊗ a∈A ∞ a as required. This completes the verification.
We remark that, as well as standard Cartesian product constructions, Lemma 5.11 gives a canonical way of extending CBI-models to heap-like structures mapping elements of an ordered set A into model values by taking M a to be the same CBI-model for each a ∈ A. For example, our "money" model of Example 5.2 extends via Lemma 5.11 to a model of maps from a set of identifiers to the integers, which can be understood as financial "asset portfolios" mapping identifiers (commodities) to integers (assets or liabilities). Such a model might potentially form the basis of a Hoare logic for financial transactions in the same way that the heap model of BBI underpins separation logic. The following example shows another application.
Then PermDG, ⊕, 0, −, 1 is a CBI-model. One can check this directly, but we can also reconstruct the model using our general constructions. First, one verifies easily that both the "deny fragment" and the "guarantee fragment" of FractionDG given by the tuples: are CBI-models. Noting that 1 is nonextensible in both models, we can apply Lemma 5.10 to obtain the disjoint union of these models, which is exactly FractionDG, ⊕, 0, −, 1 . By applying Lemma 5.11 (taking A to be Actions and M a to be FractionDG, ⊕, 0, −, 1 for all a ∈ Actions) we then obtain the CBI-model PermDG, ⊕, 0, −, 1 .
We end this section by addressing the general question of whether there are embeddings of arbitrary BBI-models into CBI-models. This is not trivial for the following reason. Consider a BBI-model R, •, e with • a function and z = x 1 • y = x 2 • y with x 1 = x 2 . In any simple extension of this model into a CBI-model R ′ , • ′ , e ′ , −, ∞ with R ⊆ R ′ and • ⊆ • ′ , we are forced to have both −x 1 ∈ y • ′ −z and −x 2 ∈ y • ′ −z by the CBI-model conditions (see Proposition 2.3, part 3), while −x 1 = −x 2 . Thus any such extension of the functional BBI-model R, •, e into a CBI-model is forced to be relational. Our construction below shows how a general embedding from BBI-models to CBI-models may be obtained, which can be viewed as being weakly canonical in the sense that it is an injection.
Proposition 5.13 (CBI-extension of BBI-models). Let R, •, e be a BBI-model and define a second, disjoint copy R of R by R = def {r | r ∈ R}. Define −x = x for all x ∈ R and −x = x for all x ∈ R. Finally, define the binary relation ⊕ over R ∪ R by the following: Then R ∪ R, ⊕, e, −, e is a CBI-model. Moreover, the construction of R ∪ R, ⊕, e, −, e from R, •, e is injective.
Proof. We start by stating the following elimination principle for ⊕ which follows directly from its introduction rules (⊕1) and (⊕2).
Elimination principle. If z ∈ x ⊕ y then the following hold: (1) z ∈ R iff x, y ∈ R, and if x, y, z ∈ R then z ∈ x • y.
(2) z ∈ R iff either x ∈ R and y ∈ R, or x ∈ R and y ∈ R. Furthermore: • if x ∈ R and y, z ∈ R then y ′ ∈ x • z ′ , where y ′ = y and z ′ = z; • if y ∈ R and x, z ∈ R then x ′ ∈ z ′ • y, where x ′ = x and z ′ = z. With this principle in place we carry out the main proof. First, we need to check that R ∪ R, ⊕, e is a BBI-model, i.e., that ⊕ is commutative and associative, and satisfies We tackle the last of these requirements first. Since R, •, e is a BBI-model we have x ∈ x • e = e • x = {x} for all x ∈ R. Thus, for all x ∈ R, we have x ∈ x ⊕ e by (⊕1) and x ∈ x ⊕ e by (⊕2). That is, x ∈ x ⊕ e for all x ∈ R ∪ R. Now suppose y ∈ x ⊕ e. Since e ∈ R, there are two cases to consider by the elimination principle. If both x, y ∈ R then we have y ∈ x • e = {x}, thus y = x. Otherwise, both x, y ∈ R and x ′ ∈ y ′ • e = {y ′ }, where x ′ = x and y ′ = y. Thus x ′ = y ′ and, since · is injective, x = y. So x ⊕ e = {x} for all x ∈ R ∪ R as required.
To see that ⊕ is commutative, let z ∈ x ⊕ y, and consider the cases given by the elimination principle. First, suppose that all of x, y, z ∈ R and z ∈ x • y. Since R, •, e is a BBI-model, • is commutative, so z ∈ y • x. Thus by (⊕1) we have z ∈ y ⊕ x. Next, suppose that x ∈ R, y, z ∈ R and y ′ ∈ x • z ′ , where y ′ = y and z ′ = z. By (⊕2) we then have z ∈ y ⊕ x. The case where y ∈ R and x, z ∈ R is symmetric. Thus z ∈ x ⊕ y implies z ∈ y ⊕ x, so x ⊕ y = y ⊕ x for any x, y ∈ R ∪ R, i.e. ⊕ is commutative.
It remains to show that ⊕ is associative, i.e. that (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z) for any x, y, z ∈ R ∪ R. We divide into cases as follows: Case: at least two of x, y, z are in R. The elimination principle implies that x ⊕ y = ∅ whenever both x, y ∈ R and, furthermore, z ∈ R whenever z ∈ x ⊕ y and either x ∈ R or y ∈ R. Combined with the pointwise extension of ⊕ to sets of elements, this implies that (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z) = ∅.
Case: none of x, y, z are in R. The elimination principle implies that (x ⊕ y) ⊕ z = (x • y) • z and x ⊕ (y ⊕ z) = x • (y • z). We are then done since • is associative by assumption.
Case: exactly one of x, y, z is in R. We show how to treat the case where x ∈ R; the other cases are similar. We write Since • is associative and commutative, x ′ ∈ w ′ • (y • z). By (⊕1), it is certainly the case that y • z ⊆ y ⊕ z, whence we obtain x ′ ∈ w ′ • (y ⊕ z) = (y ⊕ z) • w ′ . Thus, by (⊕2), we obtain w ∈ x ⊕ (y ⊕ z).
To see that R ∪ R, ⊕, e, −, ∞ is a CBI-model, we just need to check that for any x ∈ R ∪ R, x is the unique element such that ∞ = e ∈ x ⊕ x. Suppose first that x ∈ R. Since x•e = {x}, we have e ∈ x⊕x by (⊕2). To see that x is unique, suppose that e ∈ x⊕y. By part 2 of the elimination principle, we must have y = y ′ and y ′ ∈ x • e = {x}. Thus y ′ = x so y = x as required. When x ∈ R, we have x = y for some y ∈ R and the reasoning is exactly dual to the case above, since • is commutative. This completes the proof.
Another interesting possibility for obtaining CBI-models from arbitrary BBI-models would be to extend the well-known Grothendieck completion -which constructs the canonical Abelian group corresponding to a total commutative monoid -to the relational setting. From a category-theoretic perspective, it would be interesting to see whether the obvious forgetful functor from CBI-models to BBI-models has a left-adjoint, which would give the truly canonical CBI-model corresponding to any BBI-model.

Related and future work
We consider related work, and directions for future work, from several perspectives.
Bunched logics: In his monograph on BI [39], Pym observed that it made sense to think not of one bunched logic but rather a family of bunched logics, characterised by the strengths of their additive and multiplicative components. We reprise his diagram of the bunched logic family, suitably updated, in Figure 8. CBI is the strongest member of this family, boasting two classical negations and being characterised by an underlying Boolean algebra in its additive component and a de Morgan algebra in the multiplicative component. Indeed, Pym anticipated the formulation of CBI as presented here in at least two important respects: he observed that a relevantist approach to multiplicative negation (which we take by using the involution operation '−' in our models in place of the Routley star) is classically compatible with the other multiplicative connectives; and he noted the problems with cut-elimination seemingly inherent in a two-sided sequent calculus for bunched logic. In this paper, we provide two key missing links. First, our display calculus DL CBI and its cut-elimination theorem, obtained by following Belnap's original methodology for display logic [2], provides a well-behaved proof theory for CBI. (Subsequently, the first author has given in [5] a unified display calculus proof theory for all four bunched logics in Figure 8.) Second, and perhaps more importantly, we also provide the connection to Kripke-style resource models with precisely the structure necessary to interpret CBI. Our soundness and completeness results establishing the correspondence between validity and provability, plus cut-elimination for DL CBI , can be taken as strong evidence that the formulation of CBI we present here may  be considered canonical. We also establish nonconservativity of CBI over BBI, and its incompleteness with respect to partial functional models. We remark that the bunched logic dMBI (standing for "de Morgan BI") in the diagram, which combines intuitionistic additives with classical multiplicatives, has not been investigated in any great detail, to our knowledge, but it is closely related to the relevant logic RW. See the section on relevant logics below for a comparison.
Relevant logics: CBI, like its bunched logic predecessors, owes a historical debt to the extensive work on relevant logics and takes many of its mathematical cues from the development of these logics, as described in the case of BI by O'Hearn and Pym [36]. Indeed, as they point out, if one understands by "relevant logics" nothing but logics whose logical connectives are understood primarily in terms of the structural rules which they must respect (cf. [41]), then bunched logics are relevant logics. However, in bunched logics, the philosophical ideal of relevance has been entirely sacrificed in favour of full-strength additives as equal partners alongside the multiplicatives. The justification for doing so is semantic; in the Kripke models of bunched logics, one has a simple truth reading of formulas in terms of resources, in which the additives have their standard meanings. In other words, while relevant logic seeks to exclude the paradoxes of material implication, in the setting of bunched logic we regard these paradoxes as being perfectly justifiable in terms of our resource models.
Retrospectively, CBI can be obtained in terms of relevant logics by a series of surgeries on the axiomatisation of the full system R and its corresponding class of Kripke models (see e.g. [44]) in the following way. First, drop the axiom of multiplicative contraction from R (so that the corresponding condition Rxxx on the ternary relation R in the Kripke models of R does not necessarily hold) to obtain the well-known relevant logic RW (a.k.a. C). Then one can add both the additive intuitionistic implication → and falsum ⊥, which are barred from relevant logics in order to exclude various logical principles which contravene the philosophical notion of relevance (e.g. the classical tautology A∧B → A). This addition is conservative over the language of RW because → and ⊥ can already be interpreted in its Kripke models using the ordering ≤ on points in the model in the usual intuitionistic way (a fact exploited by Restall in order to formulate display calculi for RW and other relevant logics [42]). At this point we have obtained a characterisation of the bunched logic dMBI, whence to obtain CBI we strengthen the implication → into the (additive) classical implication, which corresponds to taking ≤ in the corresponding Kripke models to be the identity ordering. The situation is also similar to that for the classical relevant logics introduced by Meyer and Routley [31,32], which feature traditional Boolean negation alongside the relevantist negation employing the Routley star -though, again, multiplicative contraction must be removed and the additives given their full classical strength.
Similarly, it would not surprise a relevantist that CBI can be given a display calculus presentation, as display logic historically served as one of the main proof-theoretic tools in formulating sensible proof systems for relevant and other substructural logics. Indeed, one might deduce that this was the main intention behind Belnap's original formulation of display logic [2], in which the choice of structural rules for a particular logic are identified as the principal factor affecting cut-elimination. We note that Goré has shown how to automatically generate display calculi for a general class of substructural logics based on Dunn's gaggle theory [25], and it seems more than likely that his techniques could equally well be used to obtain DL CBI . Similarly, the correct formulation of DL CBI could have been deduced from Restall's display calculi for the relevant logic DW and its various extensions including RW [42]. In both the aforementioned cases, however, the modelling power is in considerable excess of what is needed to obtain our display calculus for CBI, which falls directly under Belnap's original description of displayable logics in [2] because it features classical negation in both its additive and multiplicative connective families.
Linear logic: Readers may wonder about the relationship between CBI and classical linear logic (CLL), which also features a full set of propositional multiplicative connectives, and is a nonconservative extension of intuitionistic linear logic (ILL) [47]. The differences between the two are intuitively obvious when comparing our money model of CBI (Example 5.2) alongside Girard's corresponding Marlboro / Camel example [23]. In particular, formulas in our model are read as declarative statements about resources (i.e. money), whereas linear logic formulas in Girard's model are typically read as procedural statements about actions. Compared to CLL, CBI has the advantage of a simple, declarative notion of truth relative to resource, but this advantage appears to come at the expense of CLL's constructive interpretation of proofs.
Of course, the typical reading of BI departs from that of ILL in a similar way (see [36] for a discussion), and indeed it seems that the main differences between CBI and CLL are inherited from the wider differences between bunched logic and linear logic in general. These differences are not merely conceptual, but are also manifested at the technical level of logical consequence. For example, P −• Q ⊢ P → Q is a theorem of linear logic for any propositions P and Q, via the encoding of additive implication P → Q as !P −• Q, but P - * Q ⊢ P → Q is not a theorem of bunched logic. Similarly, distributivity of additive conjunction ∧ over additive disjunction ∨ holds in bunched logics, but fails in linear logics. Further differences are highlighted in [7].
Interestingly, however, there is an intersection between CBI-models and the CLL-models obtained from the phase semantics of classical linear logic [23]. A CBI-model R, •, e, −, ∞ in which the monoid operation • is a total function, rather than a relation, is a special instance of a phase space, used to provide a phase model of CLL. This can be seen by taking the linear logic "perp" ⊥ to be the set R \ {∞}, whence the linear negation X ⊥ on sets X ⊆ R becomes −X. In the linear logic terminology, every subset X of R is then a "fact" in the sense that (X ⊥ ) ⊥ = −−X = X. It seems somewhat curious that there is a subclass of models where CBI and CLL agree, since known interesting phase models of linear logic are relatively few whereas there appear to be many interesting CBI-models (cf. Section 5). However, one can argue that this subclass is faithful to the spirit of neither logic. On the one hand, the restriction to a total monoid operation in CBI-models rules out many natural examples where resource combination is partial (or indeed relational). On the other hand, it seems certain that the induced subclass of CLL phase models will be at odds with the coherence semantics of CLL proofs.
Applications: The main application of BBI so far has been the use of separation logic in program analysis. There are now several program analysis tools [12,13,16,49,35] which use logical and semantic properties of the heap model of BBI at their core. These tools typically define a suitable fragment of separation logic with convenient algebraic properties, and use it in custom lightweight theorem provers and abstract domains. We suggest that our work on CBI could be relevant in this area as a foundation for richer resource models. In this paper we have already given several new models and model constructions which, though relatively simple in their present form, are suggestive of the applicability of CBI to more complex domains (cf. Section 5). In particular, we have observed that several models introduced recently for reasoning about concurrent access to resources are CBI models, e.g. fractional permissions as used in deny-guarantee reasoning (cf. Example 5.12).
More speculatively, our display calculus DL CBI might form a basis for the design of new theorem provers, which could easily employ the powerful (and historically difficult to use) implication - * since, in CBI, it can be reexpressed using more primitive connectives. Moreover, the notion of dual or negative resource might be employed in extended theorem proving questions, such as the frame inference problem F ⊢ G * X where the frame X is computed essentially by subtracting G from F . A similar problem is the bi-abduction question, which forms the basis of the compositional shape analysis in [9] and has the form F * X ⊢ G * Y , interpreted as an obligation to find formulae to instantiate X and Y such that the implication holds. This question arises at program procedure call sites, where F is the procedure's precondition, G is the current precondition at the call point, X is the resource missing, and Y is the leftover resource. We speculate that such inferences could be explained in terms of an ordinary proof theory, providing that multiplicative negation is supported, as in CBI.
Finally, CBI could be applied to the study of other logics. For example, Kleene's 3-valued logic [28] can be modelled using a subset of CBI's connectives. Consider the twoelement CBI model given by {e, ∞}, •, e, −, ∞ , where ∞ • ∞ = ∅ (note that • and − are then determined by the CBI-model axioms). There are CBI-formulas denoting each of the subsets of {e, ∞}: ⊤, ⊥, ⊤ * , ∞ (where ∞ is used as an abbreviation for ¬⊥ * ). To model 3-valued logic we focus on ⊤, ⊥, ∞, with ∞ playing the role of the third logical value, "unknown". A direct calculation shows that the connectives ∧, ∨, and ∼ indeed generate the truth tables required by 3-valued logic. For example, we have ∞ ∨ ∼∞ = ∞ ∨ ∞ = ∞. We speculate that CBI could be applied to other situations in logic where a non-standard notion of negation is used.
We believe that, aside from its intrinsic technical interest, our development of CBI contributes to the picture of bunched logic and its connections to computer science as a whole, as well as to the broader area of substructural logics in general. Although our suggestions regarding specific applications of CBI are necessarily still somewhat speculative at this early stage in its existence, we hope that the foundations established in this paper will provide a solid platform upon which such applications can, in time, be constructed.