Constructive S4 modal logics with the finite birelational frame property

Philippe Balbiani, Martín Diéguez, David Fernández-Duque +1

The logics $CS4$ and $IS4$ are the two leading intuitionistic variants of the modal logic $S4$. Whether the finite model property holds for each of these…