Mikołaj Bojańczyk, Pawel Parys, Szymon Torunczyk
The MSO+U theory of (N, <) is undecidable. CoRR, 2015 PDF
Mikołaj Bojańczyk, Tomasz Gogacz, Henryk Michalewski, Michal Skrzypczak
On the Decidability of MSO+U on Infinite Trees. ICALP (2), 2014 PDF
These papers show that MSO+U (a quantitative extension of MSO) is undecidable. The 2014 paper shows that MSO+U is undecidable over infinite trees, and with an additional set-theoretic assumption called V=L. The 2015 paper (preprint) deprecates the 2014 one by showing undecidability already on infinite words, and not using any set-theoretic assumptions. This group of undecidability results should be contrasted with the decidability results on weak MSO+U.