The variable hierarchy of the $mu$-calculus is strict

The modal μ-calculus L μ attains high expressive power by extending basic modal logic with monadic variables and binding them to extremal fixed points of definable operators. The number of variables occurring in a formula provides a relevant measure of its conceptual complexity. In a previous paper with Erich Grädel we have shown, for the existential fragment of L μ , that this conceptual complexity is also reflected in an increase of semantic complexity, by providing examples of existential formulae with k variables that are not equivalent to any existential formula with fewer than k variables. In this paper, we prove an existential preservation theorem for the family of L μ -formulae over at most k variables that define simulation closures of finite strongly connected structures. Since hard formulae for the level k of the existential hierarchy belong to this family, it follows that the bounded variable fragments of the full modal μ-calculus form a hierarchy of strictly increasing expressive power.