Undecidability of a weak version of MSO+U

Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon +2

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 \…