Undecidability of MSO+U

As explained in Chap. 9, mso+u logic is an extension of mso that allows to express quantitative properties of structures. One of the consequences of the big expressive power of mso+u is that many decision problems about other quantitative formalisms can be reduced to mso+u. An example is the reduction [CL08] of the non-deterministic index problem to a certain boundedness problem that can be further reduced to mso+u on infinite trees. Therefore, decidability of mso+u would be a very desirable result.