An Easy Completeness Proof for the Modal μ-Calculus on Finite Trees

We give a complete axiomatization for the modal mu-calculus on finite trees. While the completeness of our axiomatization already follows from a. more powerful result by Igor Walukiewicz in [11], our proof is easier and uses very different tools, inspired from model theory. We show that our approach generalizes to certain axiomatic extensions, and to the extension of the it-calculus with graded modalities. We hope that the method might be helpful for other completeness proofs as well.