A Complete Deductive System for the mu-Calculus

Abstract

The propositional mu-calculus as introduced by Kozen in [12] is considered. In that paper a finitary axiomatisation of the logic was presented but its completeness remained an open question. Here a different finitary axiomatisation of the logic is proposed and proved to be complete. The two axiomatisations are compared.