Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof

Kuniaki Tamura

The modal mu-calculus, introduced by Dexter Kozen, is an extension of modal logic with fixpoint operators. Its axiomatization, Koz, was introduced at the same time and is an extens…