On the Decidability of Monadic Theories of Arithmetic Predicates

1. Problem Statement

The paper investigates the decidability of the Monadic Second-Order (MSO) theory of structures of the form $\langle \mathbb{N}; <, P_1, \dots, P_d \rangle$, where $P_i$ are unary predicates (subsets of natural numbers). While Büchi's theorem established the decidability of $\langle \mathbb{N}; < \rangle$, the addition of arithmetic predicates often leads to undecidability (e.g., the set of prime numbers).

The authors focus on "arithmetic" predicates arising from Linear Recurrence Sequences (LRS), specifically:

• Geometric progressions: $k^{\mathbb{N}} = \{k^n : n \in \mathbb{N}\}$.
• Power sets: $\mathbb{N}^k = \{n^k : n \in \mathbb{N}\}$.
• Linear recurrence terms: Such as the Fibonacci sequence $\text{Fib} = \{F_n\}$.

The core challenge is determining whether the MSO theory remains decidable when multiple such predicates are combined simultaneously. Existing techniques (like the contraction method) often handle single predicates but fail to capture the complex interactions between multiple predicates.

2. Methodology

The authors employ a multi-disciplinary approach combining automata theory, dynamical systems, number theory, and word combinatorics. Their general framework proceeds in three main steps:

1. Reduction to Automaton Acceptance:
   Using Büchi's construction, the MSO decision problem for a structure $S$ is reduced to the Automaton Acceptance Problem ($Acc_\alpha$) for the characteristic word $\alpha$ of the predicates. $\alpha$ is an infinite word over $\{0,1\}^d$ where the $n$-th letter indicates membership in each $P_i$.

2. Compression to Order Words:
   The authors introduce the Order Word ($\beta$), a compressed version of $\alpha$ that retains only the relative ordering of elements in the predicates (removing "gaps" of zeros). They prove that for effectively procyclic and effectively sparse predicates, the acceptance of $\alpha$ is Turing-equivalent to the acceptance of $\beta$. This reduces the problem from analyzing the full characteristic word to analyzing the sequence of intersections.

3. Dynamical Systems Modeling:
   The order word $\beta$ is modeled as a trajectory in a dynamical system.

   • Case 1 (LRS with single dominant root): The order word corresponds to a cutting sequence (billiard word) generated by a linear flow on a torus $\mathbb{T}^d$. The decidability depends on the properties of this flow (e.g., Kronecker's theorem on density).
   • Case 2 (Mixed powers and geometric progressions): The order word is linked to base-$b$ expansions of algebraic numbers via the map $x \mapsto \{bx\}$.

3. Key Contributions and Results

A. Linear Recurrence Sequences (Single Dominant Root)

The paper addresses structures $\langle \mathbb{N}; <, P_1, \dots, P_d \rangle$ where each $P_i$ is the value set of an LRS with a single, non-repeated dominant root (e.g., $a_i \rho_i^n$).

• Unconditional Decidability (Theorem 4.4):
  If the numbers $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are linearly independent over $\mathbb{Q}$, the MSO theory is decidable.

  • Example: $\langle \mathbb{N}; <, 2^{\mathbb{N}}, 3^{\mathbb{N}} \rangle$ is decidable.
  • Example: $\langle \mathbb{N}; <, 2^{\mathbb{N}}, 3^{\mathbb{N}}, 6^{\mathbb{N}} \rangle$ is decidable (since $1/\log 2, 1/\log 3, 1/\log 6$ are linearly dependent, but the specific structure allows reduction).
  • Example: $\langle \mathbb{N}; <, 2^{\mathbb{N}}, \text{Fib} \rangle$ is decidable.

• Conditional Decidability (Theorem 4.5 & 4.6):
  Assuming Schanuel's Conjecture (a major conjecture in transcendental number theory), the MSO theory is decidable for any such predicates, even if the logarithmic independence condition fails.

  • Example: $\langle \mathbb{N}; <, 2^{\mathbb{N}}, 3^{\mathbb{N}}, 5^{\mathbb{N}} \rangle$ is decidable under Schanuel's conjecture.
  • Note: The conjecture is only required for the termination of the algorithm; if it terminates, the result is unconditionally correct.

• Non-Uniform Decidability (Theorem 4.9):
  For any fixed set of parameters $a_i, \rho_i$, there exists an algorithm to decide the MSO theory. The algorithm is non-uniform because it "hard-codes" the ideal of polynomial relations between the logarithms of the parameters.

B. Mixed Predicates: Powers and Geometric Progressions

The paper studies structures $\langle \mathbb{N}; <, \{q n^d\}, \{p b^n\} \rangle$.

• Turing Equivalence (Theorem 5.1):
  The MSO theory of such structures is Turing-equivalent to the MSO theory of the base-$b$ expansions of specific algebraic numbers derived from $p, q, b, d$.

  • Specifically, it links the theory to the expansions of $\{\eta\}, \{\eta \zeta\}, \dots, \{\eta \zeta^{d-1}\}$, where $\eta = \sqrt[d]{p/q}$ and $\zeta = \sqrt[d]{1/b}$.

• Specific Results:

  • $\langle \mathbb{N}; <, \mathbb{N}^2, 2^{\mathbb{N}} \rangle$ is Turing-equivalent to the MSO theory of the binary expansion of $\sqrt{2}-1$.
  • If the expansion of an irrational algebraic number is disjunctive (every finite word appears infinitely often), its MSO theory is decidable.
  • Conjecture: Since irrational algebraic numbers are widely believed to be normal (and thus disjunctive), the MSO theory of $\langle \mathbb{N}; <, \mathbb{N}^2, 2^{\mathbb{N}} \rangle$ is likely decidable.
  • $\langle \mathbb{N}; <, 4^{\mathbb{N}}, \mathbb{N}^2 \rangle$ is unconditionally decidable (as the relevant expansions are periodic).

4. Significance and Impact

1. Bridging Fields: The paper successfully unifies techniques from symbolic dynamics (cutting sequences, torus translations), number theory (Baker's theorem, Schanuel's conjecture), and automata theory (transducers, profinite periodicity) to solve long-standing open problems in logic.
2. Handling Interactions: It provides the first systematic framework for handling multiple arithmetic predicates simultaneously, moving beyond the "single predicate" focus of previous decades.
3. Conditional Results: By leveraging Schanuel's conjecture, the authors provide a path to decidability for cases that are currently out of reach for unconditional proofs (e.g., involving $\log 2, \log 3, \log 5$).
4. Hardness Bounds: The paper clarifies the boundary between decidability and undecidability. It shows that the problem subsumes the Skolem Problem and Positivity Problem for LRS, implying that unconditional decidability for general LRS is unlikely without breakthroughs in Diophantine approximation.
5. New Decidable Classes: It establishes new unconditional decidability results for combinations like $\langle \mathbb{N}; <, 2^{\mathbb{N}}, \text{Fib} \rangle$ and $\langle \mathbb{N}; <, 2^{\mathbb{N}}, 3^{\mathbb{N}}, 6^{\mathbb{N}} \rangle$.

5. Conclusion

The paper demonstrates that the decidability of MSO theories for arithmetic predicates is deeply tied to the dynamical properties of the sequences generating them. While unconditional decidability is limited by open problems in number theory (like the Skolem problem), the authors provide a robust conditional framework (via Schanuel's conjecture) and new unconditional results for specific, practically relevant combinations of predicates. The work suggests that the "randomness" (disjunctivity) of algebraic number expansions is the key to unlocking decidability for mixed arithmetic structures.