Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A fully labelled proof system for intuitionistic modal logics

Sonia Marin 1 Marianela Morales 2, 3, 4 Lutz Straßburger 2, 3, 4
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
4 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Labelled proof theory has been famously successful for modal logics by mimicking their relational seman- tics 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 preorder 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-02390454
Contributor : Lutz Straßburger <>
Submitted on : Thursday, January 28, 2021 - 9:40:19 AM
Last modification on : Saturday, January 30, 2021 - 3:28:54 AM

File

document.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02390454, version 3

Collections

Citation

Sonia Marin, Marianela Morales, Lutz Straßburger. A fully labelled proof system for intuitionistic modal logics. 2019. ⟨hal-02390454v3⟩

Share

Metrics

Record views

30

Files downloads

98