David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Bulletin of Symbolic Logic 5 (2):215-244 (1999)
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
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Paulo Oliva (2008). An Analysis of Gödel's Dialectica Interpretation Via Linear Logic. Dialectica 62 (2):269–290.
Andreja Prijatelj (1996). Bounded Contraction and Gentzen-Style Formulation of Łukasiewicz Logics. Studia Logica 57 (2-3):437 - 456.
Tomasz Połacik (1994). Second Order Propositional Operators Over Cantor Space. Studia Logica 53 (1):93 - 105.
Philip Kremer (1997). On the Complexity of Propositional Quantification in Intuitionistic Logic. Journal of Symbolic Logic 62 (2):529-544.
Richard Zach (2004). Decidability of Quantified Propositional Intuitionistic Logic and S4 on Trees of Height and Arity ≤Ω. Journal of Philosophical Logic 33 (2):155-164.
Mitsuhiro Okada (1987). A Weak Intuitionistic Propositional Logic with Purely Constructive Implication. Studia Logica 46 (4):371 - 382.
Morten H. Sørensen & Paweł Urzyczyn (2010). A Syntactic Embedding of Predicate Logic Into Second-Order Propositional Logic. Notre Dame Journal of Formal Logic 51 (4):457-473.
Mitsuhiro Okada & Kazushige Terui (1999). The Finite Model Property for Various Fragments of Intuitionistic Linear Logic. Journal of Symbolic Logic 64 (2):790-802.
Yves Lafont (1996). The Undecidability of Second Order Linear Logic Without Exponentials. Journal of Symbolic Logic 61 (2):541-548.
Samson Abramsky & Jouko Väänänen (2009). From If to Bi. Synthese 167 (2):207 - 230.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #466,277 of 1,139,892 )
Recent downloads (6 months)1 ( #165,020 of 1,139,892 )
How can I increase my downloads?