Gu, Tao;
Gheorghiu, Alexander V;
Pym, David J;
(2025)
Proof-theoretic Semantics for the Logic of Bunched Implications.
Studia Logica
10.1007/s11225-025-10202-z.
(In press).
Preview |
Text
Pym_s11225-025-10202-z.pdf Download (1MB) | Preview |
Abstract
The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist’s B-eS for IPL, deferring an analysis of proof-theoretic validity (in the sense of Dummett and Prawitz) to another occasion. Essential to BI’s formulation in proof-theoretic terms is the concept of a ‘bunch’ of hypotheses, a notion familiar from relevance logic. Bunches amount to trees whose internal vertices are labelled with either the IMLL or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the ‘resource interpretation’ of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the ‘number-of-uses’ interpretation of propositions in linear logic. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling.
| Type: | Article |
|---|---|
| Title: | Proof-theoretic Semantics for the Logic of Bunched Implications |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/s11225-025-10202-z |
| Publisher version: | https://doi.org/10.1007/s11225-025-10202-z |
| Language: | English |
| Additional information: | Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. |
| Keywords: | Science & Technology, Arts & Humanities, Physical Sciences, Mathematics, Logic, Philosophy, Science & Technology - Other Topics, Semantics, Proof theory, Proof-theoretic semantics, Substructural logic, Bunched implications, ATOMIC SYSTEMS, BI |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10213118 |
Archive Staff Only
 |
View Item |
