Intuitionistic S4 (IS4) is one of the intuitionistic variants of modal logic S4. Its semantics was defined by Fisher Servi in terms of birelational models, and it comprises two reflexive and transitive accessibility relations: one corresponding to the accessibility relation of modal logic S4 and the other corresponding to the order relation of intuitionistic Kripke frames. The question of whether IS4 is decidable has been open for almost 30 years, since Simpson posed it in his PhD thesis. We show that IS4 is decidable by performing proof search in a fully labelled sequent calculus for IS4, closely matching the birelational semantics. Our search algorithm outputs either a proof or a finite counter-model, thus additionally establishing the finite model property for intuitionistic S4.

In this talk, I will first introduce IS4 and discuss the strategies to establish decidability through proof search in the modal and intuitionistic case. Then, I will sketch the main ingredients of our proof search algorithm.

This talk is based on joint work with Roman Kuznets, Marianela Morales and Lutz Straßburger

A preprint is available here: https://arxiv.org/abs/2304.12094