Mikołaj Bojańczyk

MSO+U is undecidable

April 9, 2015
  1. Mikołaj Bojańczyk, Pawel Parys, Szymon Torunczyk
    The MSO+U theory of (N, <) is undecidable. CoRR, 2015   PDF

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


Leave a Reply

Your email address will not be published.