Finite Model Property of Pretransitive Modal Logic

02/26/2018

∙

by   Zhe Lin, et al.

∙

0

∙

share

The finite model property of the pretransitive modal logic K_2,3=K⊕ p→ p is proved. This modal logic is conservatively extended to the tense logic K_2,3^t. We present a Gentzen sequent calculus G_2,3^t for K_2,3^t which admit cut elimination. The sequent calculus G_2,3^t is shown to have the finite model property by a construction of finite syntactic model. It follows that the tense logic K_2,3^t has the finite model property. Hence the pretransitive modal logic K_2,3 has the finite model property.