A Family of Decidable Bi-intuitionistic Modal Logics

Abstract

We investigate intuitionistic logics extended both with the co-implication connective of Hilbert-Brouwer logic and with diamond and box modalities. We use a Kripke semantics based on frames with two 'forth' confluence conditions on the modal relation with respect to the intuitionistic relation. We give sound and strongly complete axiomatisations for entailment on this class of frames, and give similar axiomatisations for the subclasses of frames satisfying any combination of reflexivity, transitivity, and seriality. We then prove that all of these logics are decidable, by proving that they have the finite frame property.