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}$ 为各种一元谓词。我们特别关注线性递归序列研究中产生的"算术"谓词，例如固定底数的幂集 $\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$ 的 MSO 理论是图灵等价的，其中 $S$ 是对应于 $\sqrt{2}$ 的二进制展开的谓词。（由于 $\sqrt{2}$ 的二进制展开被广泛认为是规范的，相应的 MSO 理论预计是可判定的。）这些结果是通过利用并融合动力系统、数论和自动机理论中的技术而获得的。