MSO+U is an extension of monadic second-order logic, which adds a quantifier U, called the unbounding quantifier. A formula UX.phi(X) says that phi(X) is true for arbitrarily big finite sets X. The weak fragment (only quantification over finite sets) is decidable over infinite words and trees, while the full logic is undecidable over infinite trees. The decidability results for trees use profinite techniques, while the undecidability results uses descriptive set theory (in fact, the undecidability result is conditional on the set-t heoretic assumption V=L).