This paper deals with the varieties of monadic Heyting algebras, algebraic models of intuitionistic modal logic MIPC. We investigate semisimple, locally finite, finitely approximated and splitting varieties of monadic Heyting algebras as well as varieties with the disjunction and the existence properties. The investigation of monadic Heyting algebras clarifies the correspondence between intuitionistic modal logics over MIPC and superintuitionistic predicate logics and provides us with the solutions of several problems raised by Ono [35].

We prove strong completeness of the □-version and the ◊-version of a Gödel modal logic based on Kripke models where propositions at each world and the accessibility relation are both infinitely valued in the standard Gödel algebra [0,1]. Some asymmetries are revealed: validity in the first logic is reducible to the class of frames having two-valued accessibility relation and this logic does not enjoy the finite model property, while validity in the second logic requires truly fuzzy accessibility relations and this (...) logic has the finite model property. Analogues of the classical modal systems D, T, S4 and S5 are considered also, and the completeness results are extended to languages enriched with a discrete well ordered set of truth constants. (shrink)

This paper investigates (modal) extensions of Heyting-Brouwer logic, i.e., the logic which results when the dual of implication (alias coimplication) is added to the language of intuitionistic logic. We first develop matrix as well as Kripke style semantics for those logics. Then, by extending the Gö;del-embedding of intuitionistic logic into S4, it is shown that all (modal) extensions of Heyting-Brouwer logic can be embedded into tense logics (with additional modal operators). An extension of the Blok-Esakia-Theorem is proved for this embedding.

In this article we deal with Glivenko type theorems for intuitionistic modal logics over Prior's MIPC. We examine the problems which appear in proving Glivenko type theorems when passing from the intuitionistic propositional logic Intto MIPC. As a result we obtain two different versions of Glivenko's theorem for logics over MIPC. Since MIPCcan be thought of as a one-variable fragment of the intuitionistic predicate logic Q-Int, one of the versions of Glivenko's theorem for logics over MIPCis closely related to that (...) for intermediate predicate logics obtained by Umezawa [27] and Gabbay [15]. Another one is rather surprising. (shrink)