MSO logic of the real order with the set quantifiers ranging over the Borel sets

TL;DR

This paper proves that the monadic second-order logic of the real order, with set quantifiers over Borel sets, is decidable, confirming a long-standing conjecture and extending Rabin's 1969 result.

Contribution

It establishes the decidability of MSO logic over the reals with quantification over Borel sets, filling a gap between known decidable and undecidable cases.

Findings

Decidability of MSO over Borel sets of reals confirmed.

Weaker MSO theories with hierarchy-level quantifiers are also decidable.

The weaker theory is interpretable in S2S.

Abstract

A celebrated 1969 theorem of Michael Rabin is that the MSO theory of the real order where the monadic quantifier is allowed only to range over the sets of rational numbers, is decidable. In 1975 Saharon Shelah proved that if the monadic quantifier is allowed to range over all subsets of the reals, the resulting MSO theory is undecidable. He conjectured that when we allow the monadic quantifier to range over the Borel subsets of the reals, the resulting MSO theory is decidable. We confirm this conjecture. Namely, the MSO theory of the real order where the set quantifier is allowed to range over the Borel sets, is decidable. If we only ask for the decidability in the language where each level of the Borel hierarchy is allowed a quantifier to denote sets of that level in the hierarchy, then we obtain a weaker MSO theory, which is not inly decidable but also interpretable in S2S.