The Finite Model Property of Quasi-transitive Modal Logic
The finite model property of the quasi-transitive modal logic K_2^3=K⊕ p p is proved. This modal logic is conservatively extended to the tense logic Kt_2^3. We present a Gentzen sequent calculus Gt_2^3 for Kt_2^3 which admits cut elimination. The sequent calculus Gt_2^3 is shown to have the finite model property by a construction of finite syntactic model. It follows that Kt_2^3 has the finite model property. And the quasi-transitive modal logic K_2^3 has the finite model property.
READ FULL TEXT