Knocking Down Boxes: The FMP for $\mathbf{K} \oplus \Box^{m+k} p \to \Box^m p$

TL;DR

The paper addresses the open problem of whether modal logics of the form $\mathbf{K} \oplus \Diamond^n p \to \Diamond^m p$ with $n>m>1$ have the finite model property (FMP). It proves that any logic axiomatized by formulas of the form $\Diamond^n p \to \Diamond^m p$ (for $n>m>1$) indeed has the FMP, by combining a Representation Lemma with a Filtration Lemma. The Representation Lemma constructs depth-respecting p-morphisms to realize required $R$-paths and depth constraints, while the Filtration Lemma builds finite quotients using $k$-bisimilarity to preserve subformulas up to modal depth $k$. Consequently, $\mathbf{K} \oplus \Phi$ has the FMP for any (potentially infinite) set $\Phi$ of formulas of the form $\Diamond^n p \to \Diamond^m p$ with $n>m>1$, yielding decidability when $\Phi$ is finite. This work introduces a new approach to a long-standing open problem in completeness theory and extends finite-model techniques to a broad class of modal reduction principles.

Abstract

It is a long-standing open problem whether modal logics of the form $\mathbf{K} \oplus \Box^n p \to \Box^m p$ for $n>m>1$ have the finite model property (FMP). We solve this by showing that any modal logic axiomatized by formulas of the form $\Box^n p \to \Box^m p$ where $n>m>1$ has the FMP.

Figures (1)

• Figure 1: Illustration of the key part of the argument, when $\textnormal{d}(x)\leq k-n$, for $m=2,n=3$, so $|x|R^f|y_1|R^f|z|\Rightarrow \exists |w_1|, |w_2|: |x|R^f|w_1|R^f|w_2|R^f|z|$.

Theorems & Definitions (17)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Lemma 2.6: Representation
• Lemma 2.7: Filtration
• Theorem 2.8
• proof
• Corollary 2.9
• proof