The MSO+U theory of (N,
Mikołaj Bojańczyk, Paweł Parys, Szymon Toruńczyk · arXiv (Cornell University) · 2015
We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,