Modal Logics Between K^{3} and S5^{3}

Robin Hirsch, Ian Hodkinson & Agnes Kurucz

Given Kripke frames (W_{0}, R_{0}), (W_{1}, R_{1}) and (W_{2}, R_{2}), their product is defined to be the relational structure (W_{0} × W_{1} × W_{2}, R̄_{0}, R̄_{1}, R̄_{2}), where

(x_{0}, x_{1}, x_{2})R̄_{ℓ}(y_{0}, y_{1}, y_{2}) iff x_{ℓ}R_{ℓ}y_{ℓ} and x_{j} = y_{j} for j ≠ ℓ.

K^{3} and S5^{3} are the 3-modal logics (i.e., sets of formulas of the language having the Booleans and three diamonds) determined by all (ternary) product frames and all products of S5-frames, respectively.

Theorem. Every 3-modal logic between K^{3} and S5^{3} is undecidable, non-finitely axiomatizable, and lacks the product finite model property. There is no algorithm deciding whether a finite frame validates the logic.

This answers questions of Gabbay–Shehtman [1]. Thus, K^{3} is a natural example of an undecidable, recursively enumerable, Kripke complete logic which has the finite model property (for the latter, see [1]).

In the proofs we use the following result of Hirsch–Hodkinson [2]: It is undecidable whether a finite relation algebra is representable.

[1] D.M. Gabbay and V.B. Shehtman. Products of modal logics, part I. Logic Journal of the IGPL, 6:73–146, 1998.

[2] R. Hirsch and I. Hodkinson. Representability is not decidable for finite relation algebras. Trans. Amer. Math. Soc., to appear.

Addresses Robin Hirsch: University College London, Dept. of Computing Imperial College, 180 Queen’s Gate, London SW7 2BZ, UK

E-mail: R.Hirsch@cs.ucl.ac.uk

Ian Hodkinson: Imperial College London

E-mail: imh@doc.ic.ac.uk

Agnes Kurucz: Imperial College London

E-mail: kuag@doc.ic.ac.uk