Undecidability of a weak version of MSO+U

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

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2020-02, Vol.16, Issue 1
Main Authors: Penelle, Vincent, Bojanczyk, Mikolaj, Daviaud, Laure, Guillon, Bruno, Sreejith, A. V.
Format: Article
Language:English
Subjects:
Computer Science
computer science - logic in computer science
Logic in Computer Science
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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$.
ISSN:1860-5974
DOI:10.23638/LMCS-16(1:12)2020