We investigate the decidability of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N};<,P_1, \ldots,P_k \rangle$, for various unary predicates $P_1,\ldots,P_k \subseteq \mathbb{N}$. We focus in particular on "arithmetic" predicates arising in the study of linear recurrence sequences, such as fixed-base powers $\mathsf{Pow}_k = \{k^n : n \in \mathbb{N}\}$, $k$-th powers $\mathsf{N}_k = \{n^k : n \in \mathbb{N}\}$, and the set of terms of the Fibonacci sequence $\mathsf{Fib} = \{0,1,2,3,5,8,13,\ldots\}$ (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following: $\bullet$ The MSO theory of $\langle \mathbb{N};<,\mathsf{Pow}_2, \mathsf{Fib} \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_6 \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_5 \rangle$ is decidable assuming Schanuel's conjecture; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_4, \mathsf{N}_2 \rangle$ is decidable; $\bullet$ The MSO theory of $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{N}_2 \rangle$ is Turing-equivalent to the MSO theory of $\langle \mathbb{N};<,S \rangle$, where $S$ is the predicate corresponding to the binary expansion of $\sqrt{2}$. (As the binary expansion of $\sqrt{2}$ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.) These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.

翻译：我们研究结构 $\langle \mathbb{N};<,P_1, \ldots,P_k \rangle$（其中 $P_1,\ldots,P_k \subseteq \mathbb{N}$ 为各种一元谓词）的一元二阶（MSO）理论的可判定性。特别地，我们聚焦于线性递推序列研究中出现的“算术”谓词，例如固定底数的幂集 $\mathsf{Pow}_k = \{k^n : n \in \mathbb{N}\}$、$k$ 次幂集 $\mathsf{N}_k = \{n^k : n \in \mathbb{N}\}$，以及斐波那契数列项集 $\mathsf{Fib} = \{0,1,2,3,5,8,13,\ldots\}$（对其他具有单个非重复主导特征根的线性递推序列类似）。我们获得了若干新的无条件与有条件可判定性结果，精选示例如下：$\bullet$ 结构 $\langle \mathbb{N};<,\mathsf{Pow}_2, \mathsf{Fib} \rangle$ 的 MSO 理论可判定；$\bullet$ 结构 $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_6 \rangle$ 的 MSO 理论可判定；$\bullet$ 在假设 Schanuel 猜想成立的前提下，结构 $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{Pow}_3, \mathsf{Pow}_5 \rangle$ 的 MSO 理论可判定；$\bullet$ 结构 $\langle \mathbb{N};<, \mathsf{Pow}_4, \mathsf{N}_2 \rangle$ 的 MSO 理论可判定；$\bullet$ 结构 $\langle \mathbb{N};<, \mathsf{Pow}_2, \mathsf{N}_2 \rangle$ 的 MSO 理论与结构 $\langle \mathbb{N};<,S \rangle$（其中 $S$ 为对应于 $\sqrt{2}$ 二进制展开的谓词）的 MSO 理论图灵等价。（由于 $\sqrt{2}$ 的二进制展开被广泛认为具有正规性，相应的 MSO 理论预计也是可判定的。）这些结果通过利用并融合动力系统、数论及自动机理论的技术获得。