 |
|
Session 6. Computational Logic |
MSO+U |
| Mikołaj Bojańczyk, University of Warsaw, |
|
mso+u is an extension of monadic second-order logic, which
adds a quantifier U, called the unbounding quantifier. A formula
\(\mathsf U X\varphi(X)\) says that \(\phi(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. 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\)).
|
| Print version |