The Finite Model Property of Quasi-transitive Modal Logic

TL;DR

This paper proves the finite model property for a specific quasi-transitive modal logic and its extension to tense logic, using a Gentzen sequent calculus with finite algebra properties.

Contribution

It establishes the finite model property for $ extsf{K}_2^3$ and $ extsf{Kt}_2^3$ through a novel sequent calculus with finite algebra construction.

Findings

Finite model property proven for $ extsf{K}_2^3$ and $ extsf{Kt}_2^3$

Development of a Gentzen sequent calculus $ extsf{G}$

Sequent calculus has finite algebra property

Abstract

The finite model property of quasi-transitive modal logic $\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box 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.