Abstract

The aim of this paper is to give successful Kripke-type semantics for a class of intuitionistic modal calculi dened through the auxiliary of a special class of theorems derived in classical \bimodal calculi", , First it is shown that the procedure used to obtain IMC's can be applied to a large number of cases, thus yielding intutionistic analogues of C2; D2; E2; T; T; E3; E4; ET; T; S 4 ; E2; EB; E5; B; S 5 ; P C; E; L. We then restrict our attention to the set C of those calculi above which have the necessitation rule as primitive. Letting () range over C, we con- sider the bimodal system C and the corresponding intuitionistic modal system () IC