English

Undecidability of a weak version of MSO+U

Logic in Computer Science 2023-06-22 v5

Abstract

We prove the undecidability of MSO on ω\omega-words extended with the second-order predicate U1(X)U_1(X) which says that the distance between consecutive positions in a set XNX \subseteq \mathbb{N} is unbounded. This is achieved by showing that adding U1U_1 to MSO gives a logic with the same expressive power as MSO+UMSO+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 XX such that for some positive integer pp, ultimately either both or none of positions xx and x+px+p belong to XX.

Keywords

Cite

@article{arxiv.1807.08506,
  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= {arXiv preprint arXiv:1807.08506},
  year   = {2023}
}