This paper is about mso+u, an extension of monadic secondorder 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 settheoretic 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.
展开▼
