paperbot · PL 论文追踪

全部论文 待读 收藏

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

ℵ1 与模态 μ-演算
LMCS vol.Volume 15, Issue 42019匹配度 1/10 · 该论文研究模态 μ-演算的连续性片段与闭包序数,属于纯逻辑与自动机理论,与用户关注的 PL 与 AI/LLM/Agent 交叉、静态分析、浮点程序分析或贝叶斯程序分析均无直接关联。引用 2 inbox
Maria João Gouveia, Luigi Santocanale
crossref: 2026-09-10

AI 速览

一句话:证明模态 μ-演算的连续性片段仅有 ℵ0 与 ℵ1 两类,并刻画闭包序数。

本文研究模态 μ-演算公式在变量上的 κ-连续性:公式解释为单变量函数时单调,并保持 κ-有向并。作者定义片段 C_{ℵ1}(x),证明其中公式均 ℵ1-连续;进而对任意公式 φ(x) 构造 ψ(x)∈C_{ℵ1}(x),使 φ 对某正则基数 κ 连续当且仅当 φ 等价于 ψ。由此证明“某 κ 连续”可判定,并在等价意义下说明由连续性确定的片段只有 Fontaine 的 C_{ℵ0}(x) 和新的 C_{ℵ1}(x)。最后应用于闭包序数,证明 ω1 是闭包序数,闭包序数对序数和封闭,因此由 0、1、ω、ω1 经 + 构造的表达式均为闭包序数。

问题
如何刻画模态 μ-演算公式的 κ-连续性片段,并确定哪些序数可作为闭包序数。
方法
定义 ℵ1-连续片段 C_{ℵ1}(x),为每个公式构造该片段中的等价代表,并证明连续性片段只有两个,再分析最小不动点迭代的收敛序数。
评估
论文给出可判定性、片段二分和闭包序数封闭性等理论证明,并证明 ω1 是闭包序数;属于逻辑与语义分析,无实验评估。
原文摘要(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 $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 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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot750,
  title = {$\aleph_1$ and the modal $\mu$-calculus},
  author = {Maria João Gouveia and Luigi Santocanale},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 4},
  year = {2019},
  doi = {10.23638/lmcs-15(4:1)2019}
}