The logic of bunched implications

We consider a classical (propositional) version, CBI, of O'Hearn and Pym's logic of bunched implications (BI) from a model- and prooftheoretic perspective. We present a class of classical models of BI which extend the usual BI-models, based on partial commutative monoids, with an algebraic notion of "resource negation". This class of models gives rise to natural definitions of multiplicative falsity, negation and disjunction. We demonstrate that a sequent calculus proof system for CBI is sound with respect to our classical models by translating CBI sequent proofs into proofs in BI+ , a sound extension of sequent calculus for BI.

• Type: Journal
• Year: 1999
• Where: BSL
• Authors: Peter W. O'Hearn, David J. Pym
• Keywords: BSL 1999, Classical Models, Partial Commutative Monoids, Sequent Calculus