Closure Ordinals of the Two-Way Modal $$\mu $$-Calculus

The closure ordinal of a \(\mu \)-calculus formula \(\varphi (x)\) is the least ordinal \(\alpha \), if it exists, such that, in any model, the least fixed point of \(\varphi (x)\) can be computed in at most \(\alpha \) many steps, by iteration of the meaning function associated with \(\varphi (x)\), starting from the empty set. In this paper we focus on closure ordinals of the two-way modal \(\mu \)-calculus. Our main technical contribution is the construction of a two-way formula \(\varphi _n\) with closure ordinal \(\omega ^n\) for an arbitrary \(n\in \omega \). Building on this construction, as our main result we define a two-way formula \(\varphi _\alpha \) with closure ordinal \(\alpha \) for an arbitrary \(\alpha