Aleph1 and the Modal mu-Calculus

Abstract

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 C1 (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 C1 (x) such that phi(x) is kappa-continuous, for some kappa, if and only if psi(x) is equivalent to phi(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 C0(x) studied by Fontaine and the fragment C1 (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 fixed-point 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.