算术谓词的单变量理论可判定性

我们研究了单变量第二阶（MSO）理论的可判定性，该理论作用于结构 $\langle \mathbb{N};<,P_1, \ldots,P_d \rangle$，其中 $P_1,\ldots,P_d \subseteq \mathbb{N}$ 为各种一元谓词。我们特别关注在线性递推序列研究中出现的“算术”谓词，例如固定基数幂 $k^{\mathbf{N}} = \{k^n : n \in \mathbb{N}\}$、$k$ 次方 $\mathbf{N}^k = \{n^k : n \in \mathbb{N}\}$ 以及斐波那契数列项的集合 $\mathsf{Fib} = \{0,1,2,3,5,8,13,\ldots\}$（以及其他单个非重复支配特征根的线性递推序列）。我们获得了若干新的无条件和条件可判定性结果，其中一些具体结果包括：$\bullet$ 结构 $\langle \mathbb{N};<, 2^{\mathbf{N}}, \mathsf{Fib} \rangle$ 的 MSO 理论是可判定的；$\bullet$ 结构 $\langle \mathbb{N};<, 2^{\mathbf{N}}, 3^{\mathbf{N}}, 6^{\mathbf{N}} \rangle$ 的 MSO 理论是可判定的；$\bullet$ 结构 $\langle \mathbb{N};<, 2^{\mathbf{N}}, 3^{\mathbf{N}}, 5^{\mathbf{N}} \rangle$ 的 MSO 理论在假设 Schanuel 猜想时是可判定的；$\bullet$ 结构 $\langle \mathbb{N};<, 4^{\mathbf{N}}, \mathbf{N}^2 \rangle$ 的 MSO 理论是可判定的；$\bullet$ 结构 $\langle \mathbb{N};<, 2^{\mathbf{N}}, \mathbf{N}^2 \rangle$ 的 MSO 理论与 $\langle \mathbb{N};<,S \rangle$ 的 MSO 理论是图灵等价的，其中 $S$ 是对应二进制小数展开的谓词。（由于二进制小数展开的规范性假设，相应的 MSO 理论预计为可判定的。）这些结果通过动力系统、数论和自动机理论的结合获得。