Separability and decidability results for varieties of Jónsson dynamic algebras

Abstract

Dynamic algebras are algebraic counterparts of dynamic logics: prepositional logical systems endowed with a set of modal operators. In [18], B. Jónsson introduced dynamic algebras as Boolean algebras with unary operators, the indices of which range over a given Kleene algebra. On the other hand, V. R. Pratt and D. Kozen proposed a two-sorted approach to dynamic algebras, which was followed in the early papers on the topic, such as Fischer and Ladner and Németi. For a recent overview of the field cf. [4]. In the present paper we investigate connections (as well as diversities) between these two approaches. Our main aim is to transfer (where possible) two-sorted results on separability and decidability to the one-sorted case and to extend them to broad classes of varieties of Jónsson dynamic algebras. In particular, as a consequence of such considerations, we obtain a decidability result on Kleene algebras.