Duality for modal μ-logics

The modal mu-calculi are extensions of propositional modal logics with least and greatest fixpoint operators. They have significant expressive power, being capable to encode properly temporal notions alien to standard modal systems. We focus here on Kozen's [21] mu-calculi, both finitary and infinitary. Based on an extension of the classical modal duality to the case of positive modal algebras that we present, we prove a Stone-type duality for positive modal mu-calculi which specializes to a duality for the Boolean modal mu-logics. Thus we extend while also improving on results published in [3]. The main improvements are: (1) extension to the negation-free case, (2) a presentation of the algebraic models of the logics in a syntax-free manner, (3) an explicit duality for the case of the finitary mu-calculus, missing in [3], and (4) a completeness result for the (negation-free or not) finitary modal mu-calculus in Kripke semantics. The special case of completeness for the Boolean mu-calculus is an improvement over that presented in [3] but weaker than the theorem of [35]. The duality presented here seems to be closer to Abramsky's domain theory in logical form [1] as the latter is based on a more general duality for distributive lattices. And it has the potential to extensions for modal mu-calculi on a non-classical (intuitionistic, relevant) propositional basis, yielding appropriate completeness theorems. (C) 1998 - Elsevier Science B.V. All rights reserved.