The monadic second-order theory of (ℕ,<), S1S, is decidable (it essentially describes ω-automata). Undecidability of the monadic theory of (ℝ,<) was proven by Shelah. Previously, Rabin proved decidability if the monadic quantifier is restricted to Fσ-sets. We discuss decidability for Borel sets. Moreover, the Boolean combinations of Fσ-sets form an elementary substructure. Under determinacy hypotheses, the proof extends to larger classes of sets.
