On the Decidability of MSO+U on Infinite Trees

This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in zfc. This is because the theory is undecidable, under a set-theoretic assumption consistent with zfc, namely that there exists of projective well-ordering of 2 ω of type ω 1. We use Shelah’s undecidability proof of the MSO theory of the real numbers.