Bunched logics displayed (Q1935559): Difference between revisions

Bunched logics are substructural logics with both \textit{multiplicative} (i.e., ``intensional'') and \textit{additive} (i.e., ``extensional'') logical connectives. These logics are important in computer science. The main four bunched logics are defined. Consider the four well-known elementary logics that follow: classical logic (CL), intuitionistic logic (IL), Lambek multiplicative logic (LM), and De Morgan multiplicative logic (dMM). Then, the four main bunched logics are the following: the logic of bunched implications (BI: IL+LM), Boolean BI (BBI: CL+LM), De Morgan BI (dmBI: IL+dMM), and classical BI (CBI: CL+dMM). Bunched logics have mostly been studied from a semantical point of view due to the computational significance of the resulting models. However, the present approach is proof-theoretical. In this sense, the author claims that the present paper is the ``first proof-theoretic treatment of bunched logic as a whole to appear in the literature'' (p. 1251). The proof-theoretical tools employed are the well-known display calculi introduced by Belnap. In particular, a unified display calculus proof-theory is defined for the main bunched logics mentioned above. The main results are the following. (a) The display calculi for each one of the four logics are proven to be sound and complete with respect to an appropriate sense of these notions (Section 3). (b) It is proved that cut is eliminable in each one of the calculi by demonstrating that they meet Belnap's cut-elimination conditions (Section 4). (c) It is shown how to limit exhaustive proof-searches to finitely branching ones (Section 4). Also, the following may be noted: (d) a classical deduction theorem for both the display calculi of BBI and CBI is proved (Section 5); (e) the relationship between display and sequent calculi for BI is investigated. Finally, in a closing section (Section 7), some suggestions concerning the application of the calculi defined are made.