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.

翻译：我们引入FIK，一种由满足前向汇合条件的Kripke模型所刻画的自然直觉主义模态逻辑。我们给出了该逻辑的完全Hilbert风格公理化系统，并为其提出了一种双嵌套演算。该演算不仅提供了判定过程，还实现了反模型提取：对于给定公式的任何失败推导，我们通过该演算都能获得其有限反模型。