The logic of bunched implications

Bulletin of Symbolic Logic 5 (2):215-244 (1999)
  Copy   BIBTEX

Abstract

We 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; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers ∀ new and ∃ 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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,139

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
52 (#287,506)

6 months
15 (#133,312)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

David Pym
University College London

Citations of this work

From if to bi.Samson Abramsky & Jouko Väänänen - 2009 - Synthese 167 (2):207 - 230.
Plans, affordances, and combinatory grammar.Mark Steedman - 2002 - Linguistics and Philosophy 25 (5-6):723-753.
The Ambiguity of Quantifiers.Francesco Paoli - 2005 - Philosophical Studies 124 (3):313-330.

View all 26 citations / Add more citations

References found in this work

Entailment: The Logic of Relevance and Necessity.[author unknown] - 1975 - Studia Logica 54 (2):261-266.
Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
Linear Logic.Jean-Yves Girard - 1987 - Theoretical Computer Science 50:1–102.
Display logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.
Semantics for relevant logics.Alasdair Urquhart - 1972 - Journal of Symbolic Logic 37 (1):159-169.

View all 11 references / Add more references