A simple loopcheck for intuitionistic K

In this paper, we present an algorithm for establishing decidability and finite model property of intuitionistic modal logic IK. These two results have been previously established independently by proof theoretic and model theoretic techniques respectively. Our algorithm, by contrast, enables us to establish both properties at the same time and simplifies previous approaches. It implements root-first proof search in a labelled sequent calculus that employs two binary relations: one corresponding to the modal accessibility relation and the other to the preorder relation of intuitionistic models. As a result, all the rules become invertible, hence semantic completeness could be established directly by extracting a (possibly infinite) countermodel from a failed proof attempt. To obtain the finite model property, we rather introduce a simple loopcheck ensuring that root-first proof search always terminates. The resulting finite countermodel displays a layered structure akin to that of intuitionistic first-order models.