MSO+U

Monadic second order logic extended with the unbounded quantifier is undecidable when dealing with infinite words.

The difficulty of mso+u comes from the interaction between the unbounding quantifier and quantification over possibly infinite sets. This motivated the study of wmso+u, which is the variant of mso+u where set quantification is restricted to finite sets. On infinite words, satisfiability of wmso+u is decidable, and the logic has an automaton model [?]. Similar results hold for infinite trees [?]. The results from [?] have been used to decide properties of ctl*[?]. Currently, the strongest decidability result in this line is about wmso+u on infinite trees extended with quantification over infinite paths [?]. The latter result entails decidability of problems such as the realisability problem for promptltl[?], deciding the winner in cost parity games [?], or deciding certain properties of energy games [?].

While the above results showed that fragments mso+u can be decidable, and can be used to prove results not directly related to the logic itself, it was not known whether the full logic was decidable. The first evidence that mso+u can be too expressive was given in [?], where it was shown that mso+u can define languages of infinite words that are arbitrarily high in the projective hierarchy from descriptive set theory. This result was used in [?], where it was shown that, modulo a certain assumption from set theory (namelyv=l), the mso+u theory of the complete binary tree is undecidable. The result from [?] implies that there can be no algorithm which decides mso+u on the complete binary tree, and which has a correctness proof in the zfc axioms of set theory.

References
Bojańczyk, M., Parys, P., & Toruńczyk, S. (2015). The MSO+ U theory of (N,<) is undecidable. arXiv preprint arXiv:1502.04578.