The Finite Model Property of Quasi-transitive Modal Logic

Abstract

The finite model property of quasi-transitive modal logic ${\mathsf{K}}_2^3=\mathsf{K}\oplus \square \square p\to \square \square \square p$ is established. This modal logic is conservatively extended to the tense logic ${\mathsf{Kt}}_2^3$. We present a Gentzen sequent calculus $\mathsf{G}$ for ${\mathsf{Kt}}_2^3$. The sequent calculus $\mathsf{G}$ has the finite algebra property by a finite syntactic construction. It follows that ${\mathsf{Kt}}_2^3$ and ${\mathsf{K}}_2^3$ have the finite model property.

11 pages