Uniformization on thin trees

As the axiom of choice implies, for every relation R ⊆ X × Y there exists a graph of a total function f: πX (R) → Y that is contained in R (such a graph is called a uniformization of R). A natural question asks in which cases such a function f is definable. A particular instance of this problem is, when R is an mso-definable set of pairs of trees and we ask about mso-definable f. This question is known as Rabin’s uniformization question. The negative answer to this question was given by Gurevich and Shelah [GS83] (see [CL07] for a simplified proof). They proved that there is no mso formula ψ(x, X) that chooses from every non-empty subset X of the complete binary tree a unique element x of X. This result is known as undefinability of a choice function on the complete binary tree. On the other hand, the formula saying that x is the ≤-minimal element of X is a choice formula on ω-words. In [Sie75, LS98, Rab07] it is proved that any mso-definable relation on ω-words admits an mso-definable uniformization.