Gheorghiu, Alexander;
Pym, David;
(2023)
Semantical Analysis of the Logic of Bunched Implications.
Studia Logica: An International Journal for Symbolic Logic
10.1007/s11225-022-10028-z.
(In press).
Preview |
Text
Pym_s11225-022-10028-z.pdf Download (1MB) | Preview |
Abstract
We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a meta-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the object-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using the space of reductions as a medium for showing the behavioural equivalence of reduction in the sequent calculus for the object-logic and in the validity calculus. Rather than study the technique in general, we illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL (without negation) are also treated. Intuitively, BI is the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic, which renders its meta-theory is quite complex. The literature on BI contains many similar, but ultimately different, algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth’s clause for disjunction instead of Kripke’s). It is this complexity that motivates us to use BI as a case-study for this approach to semantics.
| Type: | Article |
|---|---|
| Title: | Semantical Analysis of the Logic of Bunched Implications |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/s11225-022-10028-z |
| Publisher version: | https://doi.org/10.1007/s11225-022-10028-z |
| Language: | English |
| Additional information: | 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/. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10162331 |
Archive Staff Only
 |
View Item |
