Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Mirna Džamonja

TL;DR

The paper addresses the decidability of Monadic Second Order logic on the real order when the set quantifiers range over Borel subsets, proving Rabin-style decidability for this natural extension and confirming Shelah's conjecture in the Borel setting. It develops a novel coding framework based on well-levelled orders and the Cantor tree $T^{1+\alpha}$ to represent $\Sigma_\alpha$ and $\Pi_\alpha$ sets as sets of branches, then translates MSO formulas over these codes into the decidable $S2S$ theory via Rabin automata. The main results include Theorem (main) establishing decidability and Corollary (strongmain) showing interpretability of the weaker, level-wise theory in $S2S$, along with an effective Borel determinacy theorem. Together these yield a robust automata-theoretic and descriptive-set-theoretic approach to reasoning about the real order with Borel-set quantifiers, linking automata, MSO, and Borel hierarchies in a concrete decision procedure.

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.

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

TL;DR

The paper addresses the decidability of Monadic Second Order logic on the real order when the set quantifiers range over Borel subsets, proving Rabin-style decidability for this natural extension and confirming Shelah's conjecture in the Borel setting. It develops a novel coding framework based on well-levelled orders and the Cantor tree to represent and sets as sets of branches, then translates MSO formulas over these codes into the decidable theory via Rabin automata. The main results include Theorem (main) establishing decidability and Corollary (strongmain) showing interpretability of the weaker, level-wise theory in , along with an effective Borel determinacy theorem. Together these yield a robust automata-theoretic and descriptive-set-theoretic approach to reasoning about the real order with Borel-set quantifiers, linking automata, MSO, and Borel hierarchies in a concrete decision procedure.

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.
Paper Structure (14 sections, 17 theorems, 33 equations)

This paper contains 14 sections, 17 theorems, 33 equations.

Table of Contents

  1. Introduction
  2. Well-levelled orders and their basic properties
  3. The Polish Topology of $[T^{1+\alpha}]$
  4. Coding of the Borel Sets
  5. Decidability of $T^{1+\alpha}$
  6. The recursive correspondance between MSO formulas over $T$ and Rabin automata
  7. Towards the automata associated to $n$-tuples of subsets of $T^{1+\alpha}$
  8. Translating into $S2S$
  9. Translation between MSO-formulas over $T^{1+\alpha}$ and those over $T$
  10. Subsets of $T^{1+\alpha}$ and branches in $[T^{1+\alpha}]$
  11. Choosing the $\sigma$-representation by open sets in an MSO-definable way
  12. Decidability of MSO over the real order with Borel Set Quantifiers
  13. Effective Borel Determinacy
  14. Closing Remarks

Key Result

Proposition 2.5

(1) If $P$ is a well-levelled order and $Q\subseteq P$ is a sub-order which is downward closed, then $Q$ is well-levelled and ${\mathsf {wl}}(Q)\le {\mathsf {wl}}(P)$. (2) Every well-levelled order is well-founded.

Theorems & Definitions (43)

  • proof
  • Definition 2.3
  • Example 2.4
  • Proposition 2.5
  • proof
  • Definition 2.8
  • Remark 2.9
  • Lemma 2.11
  • proof
  • Definition 2.12
  • ...and 33 more