Back to Search
Start Over
A fully labelled proof system for intuitionistic modal logics.
- Source :
- Journal of Logic & Computation; Apr2021, Vol. 31 Issue 3, p998-1022, 25p
- Publication Year :
- 2021
-
Abstract
- Labelled proof theory has been famously successful for modal logics by mimicking their relational semantics within deductive systems. Simpson in particular designed a framework to study a variety of intuitionistic modal logics integrating a binary relation symbol in the syntax. In this paper, we present a labelled sequent system for intuitionistic modal logics such that there is not only one but two relation symbols appearing in sequents: one for the accessibility relation associated with the Kripke semantics for normal modal logics and one for the pre-order relation associated with the Kripke semantics for intuitionistic logic. This puts our system in close correspondence with the standard birelational Kripke semantics for intuitionistic modal logics. As a consequence, it can be extended with arbitrary intuitionistic Scott–Lemmon axioms. We show soundness and completeness, together with an internal cut elimination proof, encompassing a wider array of intuitionistic modal logics than any existing labelled system. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 0955792X
- Volume :
- 31
- Issue :
- 3
- Database :
- Complementary Index
- Journal :
- Journal of Logic & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 151741870
- Full Text :
- https://doi.org/10.1093/logcom/exab020