Sérgio Marcelino (SQIG, Instituto de Telecomunicações e IST)
07/02/2014 Sextafeira, 7 de Fevereiro de 2014, 14h30, Sala B201, IIIUL
Instituto para a Investigação Interdisciplinar da Universidade de Lisboa
On twodimensional 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, temporalepistemic logics, dynamic topological logics, modal and temporal description logic.
It is known that nproducts 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 finiteframe 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 2product 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 twodimensional 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 nestingdepth.
In [2], we consider one of these logics (K4.3xS5) that is outside the scope of both the known finite axiomatisation results, and the nonfinite 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 nonfinite axiomatisability of K4.3xS5, or finding an explicit, possibly infinite, axiomatisation of it.
References:
[1] A. Kurucz and S. Marcelino: Nonfinitely axiomatisable twodimensional 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) 
