On the decidability of MSO+U on infinite trees

Abstract

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. © 2014 Springer-Verlag.