Bunched logics displayed (Q1935559)

From MaRDI portal
Revision as of 05:16, 5 March 2024 by Import240304020342 (talk | contribs) (Set profile property.)
scientific article
Language Label Description Also known as
English
Bunched logics displayed
scientific article

    Statements

    Bunched logics displayed (English)
    0 references
    0 references
    18 February 2013
    0 references
    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.
    0 references
    0 references
    bunched logic
    0 references
    display calculus
    0 references
    proof theory
    0 references
    cut elimination
    0 references

    Identifiers