Undecidability of a weak version of MSO+U

Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon, Vincent Penelle, A. V. Sreejith

Research output: Contribution to journalArticlepeer-review

5 Downloads (Pure)


We prove the undecidability of mso on ω-words extended with the second-order predicate U1(X) which says that the distance between consecutive positions in a set X ⊆ N is unbounded. This is achieved by showing that adding U1 to mso gives a logic with the same expressive power as mso+U, a logic on ω-words with undecidable satisfiability. As a corollary, we prove that mso on ω-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.

Original languageEnglish
Article number12
JournalLogical Methods in Computer Science
Issue number1
Publication statusPublished - 11 Feb 2020


  • MSO logic
  • Undecidability

Cite this