$\aleph_1$ and the modal $μ$-calculus

Abstract

For a regular cardinal $κ$, a formula of the modal $μ$-calculus is $κ$-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of $κ$-directed sets. We define the fragment $C_{\aleph_1}(x)$ of the modal $μ$-calculus and prove that all the formulas in this fragment are $\aleph_1$-continuous. For each formula $ϕ(x)$ of the modal $μ$-calculus, we construct a formula $ψ(x) \in C_{\aleph_1 }(x)$ such that $ϕ(x)$ is $κ$-continuous, for some $κ$, if and only if $ϕ(x)$ is equivalent to $ψ(x)$. Consequently, we prove that (i) the problem whether a formula is $κ$-continuous for some $κ$ 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 $μ$-calculus. An ordinal $α$ is the closure ordinal of a formula $ϕ(x)$ if its interpretation on every model converges to its least fixed-point in at most $α$ steps and if there is a model where the convergence occurs exactly in $α$ steps. We prove that $ω_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, $ω$, $ω_1$ by using the binary operator symbol + gives rise to a closure ordinal.