Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal systemK based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. This paper lays the ground for (...) an investigation of intuitionistic analogues of systems stronger thanK. A brief survey is given of the existing literature on intuitionistic modal logic. (shrink)

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 generalize Priestley duality for distributive lattices to a duality for distributive meet-semilattices. On the one hand, our generalized Priestley spaces are easier to work with than Celani’s DS-spaces, and are similar to Hansoul’s Priestley structures. On the other hand, our generalized Priestley morphisms are similar to Celani’s meet-relations and are more general than Hansoul’s morphisms. As a result, our duality extends Hansoul’s duality and is an improvement of Celani’s duality.

This paper, a sequel to Models for normal intuitionistic modal logics by M. Boi and the author, which dealt with intuitionistic analogues of the modal system K, deals similarly with intuitionistic analogues of systems stronger than K, and, in particular, analogues of S4 and S5. For these prepositional 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. (shrink)

Hilbert algebras provide the equivalent algebraic semantics in the sense of Blok and Pigozzi to the implication fragment of intuitionistic logic. They are closely related to implicative semilattices. Porta proved that every Hilbert algebra has a free implicative semilattice extension. In this paper we introduce the notion of an optimal deductive filter of a Hilbert algebra and use it to provide a different proof of the existence of the free implicative semilattice extension of a Hilbert algebra as well as a (...) simplified characterization of it. The optimal deductive filters turn out to be the traces in the Hilbert algebra of the prime filters of the distributive lattice free extension of the free implicative semilattice extension of the Hilbert algebra. To define the concept of optimal deductive filter we need to introduce the concept of a strong Frink ideal for Hilbert algebras which generalizes the concept of a Frink ideal for posets. (shrink)

A Q -Heyting algebra is an algebra of type such that is a Heyting algebra and the unary operation ∇ satisfies the conditions ∇0=0, a ∧∇ a = a , ∇=∇ a ∧∇ b and ∇=∇ a ∨∇ b , for any a , b ∈ H . This paper is devoted to the study of the subvariety QH L of linear Q -Heyting algebras. Using Priestley duality we investigate the subdirectly irreducible linear Q -Heyting algebras and, as consequences, we (...) derive some properties of the lattice of subvarieties of QH L and find equational bases for some of these subvarieties. (shrink)