Algebraic models and complete proof calculi for classical BI

We consider the classical (propositional) version, CBI, of O’Hearn and Pym’s logic of bunched implications (BI) from a model- and proof-theoretic perspective. We make two main contributions in this paper. Firstly, we present a class of algebraic models for CBI which per- mit the full range of classical multiplicative connectives to be modelled. Our models can be seen as generalisations of Abelian groups, and in- clude several computationally interesting models as concrete instances. Secondly, we give a display calculus proof system for CBI that is an instance of Belnap’s general display logic — hence cut-eliminating — and demonstrate this system to be sound and complete with respect to validity in our models. To achieve the latter, we first define a simple extension of the usual sequent calculus for BI by axioms that directly capture properties of our models, and show this extension to be sound and complete (though not cut-eliminating). Soundness and completeness of our display calculus then follows by establishing faithful translations between the display calculus and this sequent calculus