Chopping More Finely: Finite Countermodels in Modal Logic via the Subdivision Construction

TL;DR

The paper introduces the Subdivision Construction, a new method for establishing the finite model property in broad classes of modal logics, by constructing finite countermodels using stable canonical rules.

Contribution

It presents a novel construction technique for proving the finite model property in modal logics based on stable canonical formulas and rules.

Findings

Proves the finite model property for logics axiomatized by stable canonical formulas.

Identifies a class of union-splittings with Kripke incompleteness degree 1.

Provides a finite countermodel construction method applicable to various modal rule systems.

Abstract

We present a new method, the Subdivision Construction, for proving the finite model property (the fmp) for broad classes of modal logics and modal rule systems. The construction builds on the framework of stable canonical rules, and produces a finite modal space, dually, a finite modal algebra, that serves as a finite countermodel of such rules, yielding the fmp. We apply the Subdivision Construction to prove the fmp for logics and rule systems axiomatized by stable canonical formulas and rules of finite modal algebras of finite height. As a consequence, we identify a class of union-splittings in $\mathsf{NExt}(\mathsf{K4})$ with degree of Kripke incompleteness 1.