The MSO+U theory of (N, <) is undecidable

Mikołaj Bojańczyk, Paweł Parys, Szymon Toruńczyk

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