MSO+U

MSO+U is an extension of monadic second-order logic, which adds a quantifier U, called the unbounding quantifier. A formula U X. φ ( X ) says that φ ( X ) is true for arbitrarily big finite sets X. Languages definable in MSO+U look like they admit finite state recognisers. For instance consider the left Myhill-Nerode equivalence: finite words w and w ' are equivalent if for every infinite word u, either both or none of the words wu, w ' u are in the language. It is not difficult to show that languages recognised in MSO+U have finitely many equivalence classes under this relation. In the talk, I will discuss two results: a positive result about decidability of Weak MSO+U, and a negative result about undecidability of MSO+U on infinite trees. The positive result is that finite state recognisers do exist when set quantification is restricted to finite sets, i. e. in Weak MSO+U. With finite set quantification only, the logic admits automata models for both infinite words and infinite trees, and is decidable. The negative result is about MSO+U over infinite words and trees. (The negative result is joint work with Tomasz Gogacz, Henryk Michalewski and Michał Skrzypczak.) This logic turns out to be dangerously expressive already over infinite words, e. g. it can recognise languages that are arbitrarily high in the projective hierarchy known from descriptive complexity. This topological complexity can be combined with Shelah's proof of undecidability of MSO over the real numbers, to show that MSO+U is undecidable over infinite trees (under the set-theoretic assumption that V = L ).

Authors

• Mikołaj Bojańczyk

Keywords

No keywords are indexed for this paper.