The Semantics and Proof Theory of the Logic of Bunched Implications
By: by David J. Pym
Series: Applied Logic Series -- 26; Applied Logic Series -- 26
Publisher: Springer Netherlands
Published: 2002
Place of publication: Dordrecht
Language: eng
Format: [electronic resource] /
Number of pages: 290
ISBN-13: 9789048160723; 9789401700917
Subjects: Philosophy (General); Computer science; Logic
Description: This monograph provides a thorough account of the model theory, proof theory and computational interpretations of BI, the logic of bunched implications, which freely combines intuitionistic logic and multiplicative intuitionistic linear logic. Starting, on the one hand, from elementary observations about modelling resources and, on the other, from a desire to develop a system of logic within which additive (or extensional) and multiplicative (or intensional) implications co-exist with equal logical status, we give natural deduction, lambda-calculi, sequent calculus, categorical semantics, Kripke models, topological models, logical relations and computational interpretations for both propositional and predicate BI, within which both additive and multiplicative quantifiers also co-exist. This monograph will be of interest to graduate students and researchers in mathematical logic, philosophical logic, computational logic and theoretical computer science.
Notes: Online full text is restricted to subscribers.

Also available in print.

Mode of access: World Wide Web.
Table of contents: title: List of Figures; title: List of Tables; title: Preface; title: Acknowledgments; title: Foreword; title: Introduction; title: Part I: Propositional BI. 1. Introduction to Part I. 2. Natural Deduction for Propositional BI. 3. Algebraic, Topological, Categorical. 4. Kripke Semantics. 5. Topological Kripke Semantics. 6. Propositional BI as a Sequent Calculus. 7. Towards Classical Propositional BI. 8. Bunched Logical Relations. 9. The Sharing Interpretation, I; title: Part II: Predicate BI. 10. Introduction to Part II. 11. The Syntax of Predicate BI. 12. Natural Deduction & Sequent Calculus For Predicate BI. 13. Kripke Semantics for Predicate BI. 14. Topological Kripke Semantics for Predicate BI. 15. Resource Semantics, Type Theory & Fibred Categories. 16. The Sharing Interpretation, II; title: Bibliography; title: Index.