
For a regular cardinal $\kappa$, a formula of the modal $\mu$calculus is
$\kappa$continuous in a variable x if, on every model, its interpretation as a
unary function of x is monotone and preserves unions of $\kappa$directed sets.
We define the fragment $C_{\aleph_1}(x)$ of the modal $\mu$calculus and prove
that all the formulas in this fragment are $\aleph_1$continuous. For each
formula $\phi(x)$ of the modal $\mu$calculus, we construct a formula $\psi(x)
\in C_{\aleph_1 }(x)$ such that $\phi(x)$ is $\kappa$continuous, for some
$\kappa$, if and only if $\phi(x)$ is equivalent to $\psi(x)$. Consequently, we
prove that (i) the problem whether a formula is $\kappa$continuous for some
$\kappa$ is decidable, (ii) up to equivalence, there are only two fragments
determined by continuity at some regular cardinal: the fragment
$C_{\aleph_0}(x)$ studied by Fontaine and the fragment $C_{\aleph_1}(x)$. We
apply our considerations to the problem of characterizing closure ordinals of
formulas of the modal $\mu$calculus. An ordinal $\alpha$ is the closure
ordinal of a formula $\phi(x)$ if its interpretation on every model converges
to its least fixedpoint in at most $\alpha$ steps and if there is a model
where the convergence occurs exactly in $\alpha$ steps. We prove that
$\omega_1$, the least uncountable ordinal, is such a closure ordinal. Moreover
we prove that closure ordinals are closed under ordinal sum. Thus, any formal
expression built from 0, 1, $\omega$, $\omega_1$ by using the binary operator
symbol + gives rise to a closure ordinal.

It is a consequence of existing literature that least and greatest
fixedpoints of monotone polynomials on Heyting algebrasthat is, the alge
braic models of the Intuitionistic Propositional Calculusalways exist, even
when these algebras are not complete as lattices. The reason is that these
extremal fixedpoints are definable by formulas of the IPC. Consequently, the
$\mu$calculus based on intuitionistic logic is trivial, every $\mu$formula
being equiv alent to a fixedpoint free formula. We give in this paper an
axiomatization of least and greatest fixedpoints of formulas, and an algorithm
to compute a fixedpoint free formula equivalent to a given $\mu$formula. The
axiomatization of the greatest fixedpoint is simple. The axiomatization of the
least fixed point is more complex, in particular every monotone formula
converges to its least fixedpoint by Kleene's iteration in a finite number of
steps, but there is no uniform upper bound on the number of iterations. We
extract, out of the algorithm, upper bounds for such n, depending on the size
of the formula. For some formulas, we show that these upper bounds are
polynomial and optimal.

It is a consequence of existing literature that least and greatest
fixedpoints of monotone polynomials on Heyting algebrasthat is, the algebraic
models of the Intuitionistic Propositional Calculusalways exist, even when
these algebras are not complete as lattices. The reason is that these extremal
fixedpoints are definable by formulas of the IPC. Consequently, the
$\mu$calculus based on intuitionistic logic is trivial, every $\mu$formula
being equivalent to a fixedpoint free formula. We give in this paper an
axiomatization of least and greatest fixedpoints of formulas, and an algorithm
to compute a fixedpoint free formula equivalent to a given $\mu$formula. The
axiomatization of the greatest fixedpoint is simple. The axiomatization of the
least fixedpoint is more complex, in particular every monotone formula
converges to its least fixedpoint by Kleene's iteration in a finite number of
steps, but there is no uniform upper bound on the number of iterations. We
extract, out of the algorithm, upper bounds for such n, depending on the size
of the formula. For some formulas, we show that these upper bounds are
polynomial and optimal.