English

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

Logic in Computer Science 2023-06-22 v4 Logic

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)C_{\aleph_1}(x) of the modal μ\mu-calculus and prove that all the formulas in this fragment are 1\aleph_1-continuous. For each formula ϕ(x)\phi(x) of the modal μ\mu-calculus, we construct a formula ψ(x)C1(x)\psi(x) \in C_{\aleph_1 }(x) such that ϕ(x)\phi(x) is κ\kappa-continuous, for some κ\kappa, if and only if ϕ(x)\phi(x) is equivalent to ψ(x)\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 C0(x)C_{\aleph_0}(x) studied by Fontaine and the fragment C1(x)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 ϕ(x)\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 ω1\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, ω1\omega_1 by using the binary operator symbol + gives rise to a closure ordinal.

Cite

@article{arxiv.1704.03772,
  title  = {$\aleph_1$ and the modal $\mu$-calculus},
  author = {Maria João Gouveia and Luigi Santocanale},
  journal= {arXiv preprint arXiv:1704.03772},
  year   = {2023}
}
R2 v1 2026-06-22T19:15:42.442Z