弱版本MSO+U的不可判定性

我们证明了在$\omega$-词上的MSO扩展以二阶谓词$U_1(X)$(其表示集合$X \subseteq \mathbb{N}$中相邻位置之间的距离无界)的不可判定性。这是通过证明将$U_1$添加到MSO中得到一种与$MSO+U$具有相同的表达能力的逻辑来实现的,而$MSO+U$是一种满足性不可判定的$\omega$-词上的逻辑。作为推论,我们证明了如果在MSO中允许量化最终周期的位置集合,即对于某个正整数$p$,最终要么位置和$x+p$都属于$X$,要么都不属于$X$的集合$X$,则$\omega$-词上的MSO变得不可判定。