The fusion Ll ? Lr of two normal modal logics formulated in languages with disjoint sets of modal operators is the smallest normal modal logic containing Ll [ Lr. This paper proves that decidability, interpolation, uniform interpolation, and Halld?encompleteness are preserved under forming fusions of normal polyadic polymodal logics. Those problems remained open in [Fine & Schurz [3]] and [Kracht & Wolter [10]]. The paper defines the fusion `l ? `r of two classical modal consequence relations and proves that decidability transfers also in this case. Finally, these results are used to prove a general decidability result for modal logics based on superintuitionistic logics.

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.