The logic of bunched implications. (English) Zbl 0930.03095
Summary: We introduce a logic \({\mathbf B}{\mathbf I}\) in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of \({\mathbf B}{\mathbf I}\) 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 \({\mathbf B}{\mathbf I}\) can be seen categorically: models of propositional \({\mathbf B}{\mathbf I}\)’s proofs are given by bi-Cartesian 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 \({\mathbf B}{\mathbf I}\) includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers \(\forall_{{\mathbf n}{\mathbf e}{\mathbf w}}\) and \(\exists_{{\mathbf n}{\mathbf e}{\mathbf w}}\) 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.
MSC:
| 03F52 | Proof-theoretic aspects of linear logic and other substructural logics |
| 03G30 | Categorical logic, topoi |
| 03B20 | Subsystems of classical logic (including intuitionistic logic) |
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
Keywords:
multiplicative quantifiers; proof-theoretic relationship between conjunction and implication; merging of intuitionistic logic and multiplicative intuitionistic linear logic; bi-Cartesian doubly closed categories; restrictions on structural rules; computational interpretationsReferences:
| [1] | DOI: 10.1016/0743-1066(89)90031-9 · Zbl 0681.68022 · doi:10.1016/0743-1066(89)90031-9 |
| [2] | DOI: 10.1016/0168-0072(91)90068-W · Zbl 0721.03037 · doi:10.1016/0168-0072(91)90068-W |
| [3] | Introduction to higher-order categorical logic (1986) · Zbl 0596.03002 |
| [4] | DOI: 10.1016/0304-3975(88)90100-4 · Zbl 0648.68016 · doi:10.1016/0304-3975(88)90100-4 |
| [5] | I, Formal systems and recursive functions pp 92– (1965) |
| [6] | Mathematical logic (1968) |
| [7] | DOI: 10.1093/logcom/8.6.809 · Zbl 0915.03022 · doi:10.1093/logcom/8.6.809 |
| [8] | DOI: 10.1006/inco.1994.1036 · Zbl 0807.68016 · doi:10.1006/inco.1994.1036 |
| [9] | Proceedings of AMAST ’96 pp 391– (1996) |
| [10] | DOI: 10.1016/0168-0072(93)90093-S · Zbl 0781.03044 · doi:10.1016/0168-0072(93)90093-S |
| [11] | Theoretical Computer Science pp 1– (1987) · Zbl 0734.68002 |
| [12] | Handbook of philosophical logic III pp 117– (1986) |
| [13] | Semantics for relevant logics 49 pp 1059– (1972) |
| [14] | Substructural logics pp 1– (1993) |
| [15] | Substructural logics pp 327– (1993) · Zbl 0840.03011 |
| [16] | Category seminar, Sydney pp 55– (1974) |
| [17] | Reports of the midwest category seminar pp 1– (1970) |
| [18] | Categories in computer science and logic pp 371– (1989) |
| [19] | DOI: 10.1017/CBO9780511569807.016 · doi:10.1017/CBO9780511569807.016 |
| [20] | A structure for plans and behaviour (1977) |
| [21] | Mathematical foundations of programming semantics, eleventh annual conference (1995) |
| [22] | Proceedings of computer science logic ’94, Kazimierz, Poland (1995) |
| [23] | Substructural logics pp 31– (1993) |
| [24] | Proceedings of CSL ’97 (1997) |
| [25] | Journal of Philosophical Logic 11 pp 375– (1982) |
| [26] | Algorithmic languages: Proceedings of the international symposium on algorithmic languages pp 345– (1981) |
| [27] | Conference record of the fifth annual acm symposium on principles of programming languages pp 39– (1978) |
| [28] | Entailment: the logic of relevance and necessity II (1992) · Zbl 0921.03025 |
| [29] | Relevant logic: a philosophical examination of inference (1987) |
| [30] | Entailment: the logic of relevance and necessity, volume I (1975) · Zbl 0323.02030 |
| [31] | DOI: 10.1093/logcom/4.2.175 · Zbl 0797.03054 · doi:10.1093/logcom/4.2.175 |
| [32] | DOI: 10.1016/0304-3975(93)90181-R · Zbl 0791.03003 · doi:10.1016/0304-3975(93)90181-R |
| [33] | Electronic Notes in Theoretical Computer Science 17 pp 24– (1998) |
| [34] | Algol-like languages two (1997) |
| [35] | Theoretical Computer Science · Zbl 0867.68002 |
| [36] | Typed {\(\lambda\)}-calculus and applications (1999) |
| [37] | Technical Report 2 (1982) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
