Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK

TL;DR

The paper tackles the decidability of membership for the intuitionistic modal logics $\mathbf{FIK}$ and $\mathbf{LIK}$ by integrating terminating tableau ideas with the finite-frame property of $\mathbf{IK}$ through a selective filtration. It constructs a canonical model, introduces the notions of tips and clips, and develops a saturation-based decision procedure that systematically repairs defects to yield a finite saturated frame. The main contributions are a new, simpler decidability proof, a canonical and saturated model framework, and a finite-frame property that underpins decidability results for these logics. This work provides a practical decision procedure and a methodological template that could extend to other intuitionistic modal systems and their $S4$-like variants.

Abstract

In this note, by integrating ideas concerning terminating tableaux-based procedures in modal logics and finite frame property of intuitionistic modal logic IK, we provide new and simpler decidability proofs for FIK and LIK.

Theorems & Definitions (42)

• Lemma 1
• Lemma 2
• Lemma 3
• Lemma 4
• Lemma 5: Heredity Property
• Lemma 6
• Proposition 1
• Lemma 7
• Lemma 8
• Lemma 9