2026-08-16T06:18:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5722 2024-03-06T10:36:55Z ddc:004 open_access

The MSO+U Theory of (N,<) Is Undecidable Bojanczyk, Mikolaj Parys, Pawel Torunczyk, Szymon automata logic unbounding quantifier bounds undecidability 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,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mikolaj Bojanczyk and Pawel Parys and Szymon Torunczyk 2016 Is Part Of LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2016.21 urn:nbn:de:0030-drops-57223 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.21 eng https://creativecommons.org/licenses/by/3.0/legalcode