Brett McLean

Constructive S4 modal logics with the finite birelational frame property

The logics \(\mathsf {CS4} \) and \(\mathsf {IS4} \) are the two leading intuitionistic variants of the modal logic \(\mathsf {S4} \) . Whether the finite model property holds for each of these logics have been long-standing open problems. In this paper, we resolve the first of t...