Creating and sharing knowledge for telecommunications

Finite frames for K4.3 × S5 are decidable

Marcelino, S. ; Kurucz, A.

Finite frames for K4.3 × S5 are decidable, Proc Advances in Modal Logic - AiML, Copenhagen, Denmark, Vol. 9, pp. 411 - 436, August, 2012.

Digital Object Identifier: 0


If a modal logic L is finitely axiomatisable, then it is of course decidable whether a finite frame is a frame for L: one just has to check the finitely many axioms in it. If L is not finitely axiomatisable, then this might not be the case. For example, it is shown in [7] that the finite frame problem is undecidable for every L between the product logics K×K×K and S5×S5×S5. Here we show that the finite frame problem for the modal product logic K4.3 × S5 is decidable. K4.3 × S5 is outside the scope of both the finite axiomatisation results of [4], and the non-finite axiomatisability results of [11]. So it is not known whether K4.3 × S5 is finitely axiomatisable. Here we also discuss whether our results bring us any closer to either proving non-finite axiomatisability of K4.3×S5, or finding an explicit, possibly infinite, axiomatisation of it.