In this talk I will prove that it is not possible to define a choice function in monadic second-order logic (MSO) over the infinite binary tree. Such a choice function would be given by a formula that has one free set variable and one free element variable, and for each non-empty set of nodes the formula becomes true for exactly one element from this set. This result has first been obtained by Gurevich and Shelah in 1983 using set theoretic methods. The proof presented in this talk is (in my opinion) much simpler, and is completely based on automata theoretic arguments.

A consequence of this result is that MSO-definable relations of infinite trees cannot be uniformized in MSO (where a uniformization of a binary relation is a function that is a subset of the relation and has the same domain as the relation). One can also use the result to show that there are nondeterministic automata on infinite trees that are not equivalent to an unambiguous automaton, i.e., an automaton that has at most one accepting run for each input.