The results of the thesis involve a number of methods of descriptive set theory. One of themost common examples is topological hardness: sometimes it is enough to find topologically hard language to obtain some negative results of non-definability. An instance of this approach areChaps. 9 and 10 where negative results about decidability of MSO+U are given. First, in Chap. 9 examples of MSO+U-definable languages lying arbitrarily high in the projective hierarchy are given. In consequence there can be no simple automata model capturing MSO+U on ω-words. The topological hardness of MSO+U is later used in Chap. 10 to prove that the MSO+U theory of the complete binary tree cannot be decidable in the standard sense. Also, topological hardness is used in Chap. 5 to prove that index bounds computed by the proposed algorithm (see Sect. 5.4.1, page 79) are tight.Additionally, the dichotomy proved in Chap. 6 involves topological hardness: a regular language of thin trees is either wmso-definable or ∏1/1-hard. © Springer International Publishing Switzerland 2016.