Finite model property for an intuitionistic modal logic (Q1428978)

This paper establishes that an intuitionistic bi-modal version of the normal modal logic \({\mathbf K}\mathbf{5}\) has the finite model property. The logic is bi-modal because, within an intuitionistic framework, the modal operators \(\square\) and \(\lozenge\) are not interdefinable. This calls for a pair of modal accessibility relations within the standard Kripke frame for intuitionistic logic. That this logic \({\mathbf i}{\mathbf n}{\mathbf t}{\mathbf K}\mathbf{5}_{\square\lozenge}\) has the finite model property is proved through the filtration method. This, however, requires a detour through an extension of the language to include two additional modal operators \(\square^\infty\) and \(\lozenge^\infty\), which might be thought of as the transitive closures of the basic operators. Since \({\mathbf i}{\mathbf n}{\mathbf t}{\mathbf K}\mathbf{5}_{\square\lozenge}\) has the finite model property and is finitely axiomatizable, it is decidable.