Christof Löding

Title: Definability questions for MSO


A famous result by Rabin states that monadic second-order logic (MSO) on the infinite binary tree is decidable. This result makes MSO on the infinite binary tree an interesting logic and motivates the study of its expressive power. In this talk we present natural objects that cannot be defined in MSO, in particular choice functions and well-orderings over the infinite binary tree, and we give some examples how these generic results can be used for other definability questions and to solve questions about automata on infinite trees.