Models for stronger normal intuitionistic modal logics (Q1096613)

This paper, a sequel to the one reviewed above (see Zbl 0634.03014), which dealt with intuitionistic analogues of the modal system \({\mathbb{K}}\), deals similarly with intuitionistic analogues of systems stronger than \({\mathbb{K}}\), and, in particular, analogues of S4 and S5. For these propositional logics Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given, and soundness and completeness are proved with respect to these models. It is shown how the holding of formulae characteristic for particular logics is equivalent to conditions for the relations of the models. Modalities in these logics are also investigated. It is shown that in intuitionistic S4 with the necessity operator primitive there are finitely many modalities, whereas with the possibility operator primitive there are infinitely many.