On Uniformization in the Full Binary Tree

A function f uniformizes a relation R(X,Y) if R(X,f(X)) holds for every X in the domain of R. The uniformization problem for a logic L asks whether for every L-definable relation there is an L-definable function that uniformizes it. Gurevich and Shelah proved that no Monadic Second-Order (MSO) definable function uniformizes relation "Y is a one element subset of X" in the full binary tree. In other words, there is no MSO definable choice function in the full binary tree. The cross-section of a relation R(X,Y) at D is the set of all E such that R(D,E) holds. Hence, a function that uniformizes R chooses one element from every non-empty cross-section. The relation "Y is a one element subset of X" has finite and countable cross-sections. We prove that in the full binary tree the following theorems hold: ▶ Theorem (Finite cross-sections) If every cross-section of an MSO definable relation is finite, then it has an MSO definable uniformizer. ▶ Theorem (Uncountable cross-section) There is an MSO definable relation R such that every MSO definable relation included in R and with the same domain as R has an uncountable cross-section.