Title: MSO+nabla is undecidable,
Abstract: This paper is about an extension of monadic second-order logic over infinite
trees, which adds a quantifier that says "the set of branches \pi which satisfy
a formula \phi(\pi) has probability one". This logic was introduced by
Michalewski and Mio; we call it MSO+nabla following Shelah and Lehmann. The
logic MSO+nabla subsumes many qualitative probabilistic formalisms, including
qualitative probabilistic CTL, probabilistic LTL, or parity tree automata with
probabilistic acceptance conditions. We consider the decision problem: decide
if a sentence of MSO+nabla is true in the infinite binary tree? For sentences
from the weak variant of this logic (set quantifiers range only over finite
sets) the problem was known to be decidable, but the question for the full
logic remained open. In this paper we show that the problem for the full logic
MSO+nabla is undecidable.