A Kruskal Decision Procedure for Intuitionistic Modal Logic IK4

Abstract

We prove decidability of Simpson's intuitionistic modal logic IK by working directly with cut-free nested proofs. Once the end formula is fixed, only finitely many combinations of input and output formulae can occur at a node, although the modal tree itself remains unbounded. We order these nested sequents by rooted homeomorphic embedding: weakening may add input formulae, while transitivity allows a modal edge to be stretched into a non-empty path. Kruskal's theorem makes rooted homeomorphic embedding a well-quasi-order, but does not by itself make backward application of the rules effective: an inference may still occur inside an arbitrarily large context. The finite-support lemma shows that a minimal predecessor need retain only the positions used by the inference, the images of the chosen basis elements, and the branch points joining them. Together with an effective enumeration of bounded rule instances, this bound makes the minimal predecessors computable. Backward closure from the initial sequents gives an increasing sequence of finitely based upward-closed sets. The sequence eventually stabilises, and its stable value is the set of provable nested sequents. At that point, finitely many cut-free proofs suffice: every other provable nested sequent is obtained from one of them by weakening along an embedding. Their maximum height gives a uniform proof-height bound.