Classical BI: Its Semantics and Proof Theory
We present Classical BI (CBI), a new addition to the family of bunched logics which originates in O'Hearn and Pym's logic of bunched implications BI. CBI differs from existing bunched logics in that its multiplicative connectives behave classically rather than intuitionistically (including...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2010-07-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1014/pdf |
| _version_ | 1827322907565490176 |
|---|---|
| author | James Brotherston Cristiano Calcagno |
| author_facet | James Brotherston Cristiano Calcagno |
| author_sort | James Brotherston |
| collection | DOAJ |
| description | We present Classical BI (CBI), a new addition to the family of bunched logics
which originates in O'Hearn and Pym's logic of bunched implications BI. CBI
differs from existing bunched logics in that its multiplicative connectives
behave classically rather than intuitionistically (including in particular a
multiplicative version of classical negation). At the semantic level,
CBI-formulas have the normal bunched logic reading as declarative statements
about resources, but its resource models necessarily feature more structure
than those for other bunched logics; principally, they satisfy the requirement
that every resource has a unique dual. At the proof-theoretic level, a very
natural formalism for CBI is provided by a display calculus \`a la Belnap,
which can be seen as a generalisation of the bunched sequent calculus for BI.
In this paper we formulate the aforementioned model theory and proof theory for
CBI, and prove some fundamental results about the logic, most notably
completeness of the proof theory with respect to the semantics. |
| first_indexed | 2024-04-25T01:37:20Z |
| format | Article |
| id | doaj.art-13ccea08a6244d5c98bc8a7a6fd13928 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:20Z |
| publishDate | 2010-07-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-13ccea08a6244d5c98bc8a7a6fd139282024-03-08T09:12:33ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742010-07-01Volume 6, Issue 310.2168/LMCS-6(3:3)20101014Classical BI: Its Semantics and Proof TheoryJames BrotherstonCristiano CalcagnoWe present Classical BI (CBI), a new addition to the family of bunched logics which originates in O'Hearn and Pym's logic of bunched implications BI. CBI differs from existing bunched logics in that its multiplicative connectives behave classically rather than intuitionistically (including in particular a multiplicative version of classical negation). At the semantic level, CBI-formulas have the normal bunched logic reading as declarative statements about resources, but its resource models necessarily feature more structure than those for other bunched logics; principally, they satisfy the requirement that every resource has a unique dual. At the proof-theoretic level, a very natural formalism for CBI is provided by a display calculus \`a la Belnap, which can be seen as a generalisation of the bunched sequent calculus for BI. In this paper we formulate the aforementioned model theory and proof theory for CBI, and prove some fundamental results about the logic, most notably completeness of the proof theory with respect to the semantics.https://lmcs.episciences.org/1014/pdfcomputer science - logic in computer sciencef.4.1 |
| spellingShingle | James Brotherston Cristiano Calcagno Classical BI: Its Semantics and Proof Theory Logical Methods in Computer Science computer science - logic in computer science f.4.1 |
| title | Classical BI: Its Semantics and Proof Theory |
| title_full | Classical BI: Its Semantics and Proof Theory |
| title_fullStr | Classical BI: Its Semantics and Proof Theory |
| title_full_unstemmed | Classical BI: Its Semantics and Proof Theory |
| title_short | Classical BI: Its Semantics and Proof Theory |
| title_sort | classical bi its semantics and proof theory |
| topic | computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/1014/pdf |
| work_keys_str_mv | AT jamesbrotherston classicalbiitssemanticsandprooftheory AT cristianocalcagno classicalbiitssemanticsandprooftheory |