# Why do we have free variables in mu-calculus?

I'm reading the Model Chekcing book of E. M. Clarke and in the chapter about µ-calculus there is an example formula $$f = \mu Z. ((q \mathrel{\mathrm{AND}} Y) \mathrel{\mathrm{OR}} \langle a \rangle Z)$$ As the author has mentioned, here $Y$ is a free variable, and we need an association list to pair $Y$ with the corresponding states. But why do we need it? Can it be replaced by an atomic proposition?

If you define the $$\mu$$-calculus to not allow free variables, you would have the problem that the components of a well-formed formula are not again well-formed formulas.
Consider a well-formed formula "$$\mu Z . \varphi$$", such that $$Z$$ occurs freely in $$\varphi$$ and $$\varphi$$ has no other free variables. If you were to exclude formulas with free variables from your definition, $$\varphi$$ would not be a well-formed formula.
This would make structural induction on formulas more complicated. For example the semantics of formulas (the set of states in which the formula holds) is usually defined inductively: You define the semantics of "$$\mu Z . \varphi$$" in terms of the semantics of $$\varphi$$. If your definition says $$\varphi$$ is not a well-formed formula, you would have to extended the induction to also cover these non-well-formed cases. If you have to consider these cases every time you do structural induction, you haven't really gained anything from excluding them in your definition.