DUALITY AND THE COMPLETENESS OF THE MODAL MU-CALCULUS

We consider the modal mu-calculus due to Kozen, which is a finitary modal logic with least and greatest fixed points of monotone operators. We extend the existing duality between the category of modal algebras with homomorphisms and the category of descriptive modal frames with contractions to the case of having fixed point operators. As a corollary, we obtain completeness results for two proof systems due to Kozen (finitary and infinitary) with respect to certain classes of modal frames. The rules are sound in every model, not only for validity.