On two-dimensional products of modal logics

Products of Kripke frames are natural relational structures for modelling the interaction between different modal operators, representing notions such as time, space, knowledge, actions. The product construction shows up in various disguises in many logical formalisms, such as algebras of relations in algebraic logic, finite variable fragments of classical, intuitionistic and modal predicate logics, temporal-epistemic logics, dynamic topological logics, modal and temporal description logic. It is known that n-products of modal logics have in general a very complex behaviour for n>2. For example, every logic between KxKxK and S5xS5xS5 is non finitely axiomatisable, and both its satisfiability and its finite-frame problem are undecidable. However, no such examples were known in the n=2 case. On the contrary, a big class of binary products of modal logics is known to be finitely axiomatisable, every 2-product of two Horn axiomatisable logics is in this class. In this talk I will present some recent contributions to the understanding of this construction. In [1] the first examples of two-dimensional products of finitely axiomatisable modal logics that are not finitely axiomatisable were presented. In particular, we show that any axiomatisation of some bimodal logics that are determined by classes of product frames with linearly ordered first components (K4.3) must be infinite in two senses: It should contain infinitely many propositional variables, and formulas of arbitrarily large modal nesting-depth. In [2], we consider one of these logics (K4.3xS5) that is outside the scope of both the known finite axiomatisation results, and the non-finite axiomatisability results of [1]. We show how the approach in [1] fails in this case and extract a decision procedure to decide whether a finite frame is a frame for it. We will discuss whether this result bring us any closer to either proving non-finite axiomatisability of K4.3xS5, or finding an explicit, possibly infinite, axiomatisation of it. References: [1] A. Kurucz and S. Marcelino: Non-finitely axiomatisable two-dimensional modal logics, Journal of Symbolic Logic, vol. 77 (2012) [2] A. Kurucz and S. Marcelino: Finite frames for K4.3xS5 are decidable, Advances in Modal Logic, Volume 9, College Publications (2012)