Abstract

Polymodal logics with functional modalities are natural generalisations of the well-known Segerberg's Tomorrow Logic SL [8] and Tomorrow-Yesterday Logic SL.t [7]. Extensions of these two logics were later studied by A.A. Muchnik [3]. But systematic investigation of logics with functional modalities was started in Segerberg's paper [9] and continued by F. Bellissima [1] and M. Kracht [6]. Logics of this kind can be interpreted as fragments of propositional dynamic logics of deterministic computations. They are also applied in mathematical linguistics [5]. This family is very large; one can easily construct undecidable modal logics of this type, moreover, there is no hope to obtain a reasonable classification here [6, Section 9.4].Nevertheless, we can try to describe explicitly some of its subfamilies. A natural class are the logics, in which all modalities commute. The minimal logics with commuting modalities are the products SLn described in [4, Section 14]. The semantics of SLn is given by the set Nn with the relations represented by n correspondent coordinate shift functions.We consider arbitrary extensions of SLn and especially of SL.tn. We show that all extensions of SL.tn have the finite model property and thus finitely axiomatisable of them are decidable. Moreover, we give a complete description of finitely axiomatisable extensions of SL.tn: they can be presented as finite intersections of logics of n-generated Abelian groups. By the same method we also give new proofs of Muchnik's theorems on pretabularity of the logics SL and SL.t [3].1