Bi-intuitionistic Boolean Bunched Logic
James Brotherston and Jules Villard
We formulate and investigate a bi-intuitionistic extension, BiBBI,
of the well known bunched logic Boolean BI (BBI), obtained by
combining classical logic with *full intuitionistic linear logic*
as considered by Hyland and de Paiva (as opposed to standard
multiplicative intuitionistic linear logic). Thus, in addition to
the multiplicative conjunction "*" with its adjoint implication and
unit, which are provided by BBI, our logic also features an
intuitionistic multiplicative *disjunction*, with its adjoint
co-implication and unit. "Intuitionism" for the multiplicatives
means here that disjunction and conjunction are related by a *weak
distribution* principle, rather than by De Morgan equivalence.
We formulate a Kripke semantics for BiBBI in which all the above
multiplicatives are given an intuitionistic reading in terms of
resource operations. Our main theoretical result is that validity
according to this semantics exactly coincides with provability in
our logic, given by a standard Hilbert-style axiomatic proof
system. In particular, we isolate the Kripke frame conditions
corresponding to various natural logical principles of FILL, which
allows us to present soundness and completeness results that are
modular with respect to the inclusion or otherwise of these axioms
in the logic. Completeness follows by embedding BiBBI into a
suitable modal logic and employing the famous Sahlqvist
completeness theorem.
We also investigate the Kripke models of BiBBI in some detail,
chiefly in the hope that BiBBI might be used (like BBI) to underpin
program verification applications based on separation logic.
Interestingly, it turns out that the heap-like memory models of
*separation logic* are also models of BiBBI, in which disjunction
can be interpreted using a natural notion of *heap intersection*.