Baire category quantifier in monadic second order logic

Abstract

We consider Rabin’s Monadic Second Order logic (MSO) of the full binary tree extended with Harvey Friedman’s “for almost all” second-order quantifier (∀*) with semantics given in terms of Baire Category. In Theorem 1 we prove that the new quantifier can be eliminated (MSO+∀* =MSO). We then apply this result to prove in Theorem 2 that the finite–SAT problem for the qualitative fragment of the probabilistic temporal logic pCTL* is decidable. This extends a previous result of Bràzdil, Forejt, Křetìnský and Kučera valid for qualitative pCTL.