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

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,934

External links

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

Through your library

Similar books and articles

From if to bi.Samson Abramsky & Jouko Väänänen - 2009 - Synthese 167 (2):207 - 230.
Full intuitionistic linear logic.Martin Hyland & Valeria de Paiva - 1993 - Annals of Pure and Applied Logic 64 (3):273-291.
Bi-Simulating in Bi-Intuitionistic Logic.Guillermo Badia - 2016 - Studia Logica 104 (5):1037-1050.
Coherence in linear predicate logic.Kosta Došen & Zoran Petrić - 2009 - Annals of Pure and Applied Logic 158 (1-2):125-153.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.

Analytics

Added to PP
2009-01-28

Downloads
93 (#228,596)

6 months
20 (#152,456)

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.
The Ambiguity of Quantifiers.Francesco Paoli - 2005 - Philosophical Studies 124 (3):313-330.
Plans, affordances, and combinatory grammar.Mark Steedman - 2002 - Linguistics and Philosophy 25 (5):723-753.

View all 30 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.
Linear Logic.Jean-Yves Girard - 1987 - Theoretical Computer Science 50:1–101.
Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
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 10 references / Add more references