Undecidability of a weak version of MSO+U

TL;DR

This paper proves that extending monadic second-order logic on infinite words with a predicate for unbounded gaps makes the logic undecidable, by showing it matches the power of a known undecidable logic.

Contribution

It demonstrates that adding the predicate $U_1$ to MSO on $$-words results in a logic with the same expressive power as $MSO+U$, leading to undecidability.

Findings

MSO+$U_1$ has the same expressive power as MSO+U.

Adding $U_1$ makes MSO on $$-words undecidable.

Undecidability also holds when quantifying over ultimately periodic sets.

Abstract

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$.