We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it directly.

Abstract We investigate intuitionistic modal logics with locally interpreted $$\square $$ □ and $$\lozenge $$ ◊ . The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. Additionally, we present bi-nested calculi for LIK and these extensions, providing both a decision procedure and a procedure of finite countermodel extraction.