On Combining Intuitionistic and S4 Modal Logic
| Autor: | João Rasga, Cristina Sernadas |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2024 |
| Předmět: | |
| Zdroj: | Bulletin of the Section of Logic, Vol 53, Iss 3, Pp 321-344 (2024) |
| Druh dokumentu: | article |
| ISSN: | 0138-0680 2449-836X |
| DOI: | 10.18778/0138-0680.2024.11 |
| Popis: | We address the problem of combining intuitionistic and S4 modal logic in a non-collapsing way inspired by the recent works in combining intuitionistic and classical logic. The combined language includes the shared constructors of both logics namely conjunction, disjunction and falsum as well as the intuitionistic implication, the classical implication and the necessity modality. We present a Gentzen calculus for the combined logic defined over a Gentzen calculus for the host S4 modal logic. The semantics is provided by Kripke structures. The calculus is proved to be sound and complete with respect to this semantics. We also show that the combined logic is a conservative extension of each component. Finally we establish that the Gentzen calculus for the combined logic enjoys cut elimination. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|