Abstract

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.