Intuitionistic S4 is decidable
Abstract
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.
Keywords
Cite
@article{arxiv.2304.12094,
title = {Intuitionistic S4 is decidable},
author = {Marianna Girlando and Roman Kuznets and Sonia Marin and Marianela Morales and Lutz Straßburger},
journal= {arXiv preprint arXiv:2304.12094},
year = {2023}
}
Comments
13 pages conference paper + 26 pages appendix with examples and proofs