The Borel monadic theory of order is decidable

The monadic theory of $(\mathbb{R},\le )$ with quantification restricted to Borel sets is decidable. The Boolean combinations of $F_{\sigma }$ sets form an elementary substructure of the Borel sets. Under determinacy hypotheses, the proof extends to larger classes of sets.