The Logic of Bunched Implications.

The Logic of Bunched Implications.

[David J. Pym]

We, Peter O'Hearn and David Pym, are pleased to announce
our new paper, ``The Logic of Bunched Implications''.

We hope it will be of interest to readers of `categories'.  BI
is a relevant logic which extends both linear and intuitionistic
logic. It has a semantics of proofs based on `doubly closed categories',

which carry two monoidal closed structures, one of which is cartesian
in models of BI. A rich class of models is provided by Day's tensor
product construction on  the category of presheaves over a small
monoidal category. It also comes with a lambda calculus, a truth
semantics
and a computational interpretation as a logic of resources, quite
different from
that of linear logic.

The paper is available at:

        http://www.dcs.qmw.ac.uk/~pym
and
        http://www.dcs.qmw.ac.uk/~ohearn

where drafts of various companion and related papers can/will be
found.

P.W.O'Hearn and D.J. Pym
Queen Mary & Wesfield College,
University of London



Abstract.

Introduce a logic BI in which a multiplicative (or linear)
and an additive (or intuitionistic) implication live side by
side. The propositional version of BI arises from an analysis
of the proof-theoretic relationship between conjunction and
implication, and may be viewed as a merging of intuitionistic
logic and multiplicative, intuitionistic linear logic. The
predicate version of BI includes, in addition to standard
additive quantifiers, multiplicative (or intensional)
quantifiers ``forall-new'' and ``exist-new'' which arise from
observing restrictions on structural rules on the level of terms
as well as propositions. We discuss computational interpretations,
based on sharing, at both the propositional and predicate levels.