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.
展开▼
