一句话：证明 MSO 在 ω-词上加谓词 U1 后与 MSO+U 等表达力因而不可判定，并推出最终周期集合量化亦不可判定。
本文研究 ω-词上一元二阶逻辑 MSO 的扩展的可判定性。作者引入二阶谓词 U1(X)，它断言集合 X⊆ℕ 中相邻位置之间的距离无界，并证明在该逻辑中可满足性问题不可判定。核心方法是证明 MSO 加上 U1 与已知可满足性不可判定的 MSO+U 具有相同表达力，从而把不可判定性传递给较弱扩展。作为推论，论文进一步证明，若允许 MSO 在 ω-词上对最终周期位置集合进行量化，即存在正周期 p，使得最终每个位置 x 与 x+p 要么同时属于要么同时不属于该集合，则 MSO 也可满足性不可判定。结果凸显 ω-词上 MSO 扩展在加入看似较弱的集合性质或量化机制后，其判定问题会迅速变得不可判定。
We prove the undecidability of MSO on $\omega$-words extended with the second-order predicate $U_1(X)$ which says that the distance between consecutive positions in a set $X \subseteq \mathbb{N}$ is unbounded. This is achieved by showing that adding $U_1$ to MSO gives a logic with the same expressive power as $MSO+U$, a logic on $\omega$-words with undecidable satisfiability. As a corollary, we prove that MSO on $\omega$-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets $X$ such that for some positive integer $p$, ultimately either both or none of positions $x$ and $x+p$ belong to $X$.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BojanczykDGPS19,
title = {Undecidability of a weak version of MSO+U},
author = {Mikołaj Bojańczyk and Laure Daviaud and Bruno Guillon and Vincent Penelle and A. V. Sreejith},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:12)2020}
}