Rich Sequences and Decidability of Arithmetic Theories

Abstract

We develop a new framework for proving the undecidability of first-order theories of structures of the form $⟨\mathbb{N};+,P⟩$, $⟨\mathbb{N};<,f⟩$, and $⟨\mathbb{N};+,f⟩$, where $P\subseteq \mathbb{N}$ and $f:\mathbb{N}\to \mathbb{N}$. It is based on the recent proof of Hieronymi and Schulz that the first-order theory of $⟨\mathbb{N};+,\{2^n:n\in \mathbb{N}\},\{3^n:n\in \mathbb{N}\}⟩$ is undecidable, and capable of transforming various randomness results about integer sequences into undecidability proofs. We apply our method to a large class of integer linear recurrence sequences, as well as various special functions, in particular showing that the first-order theories of $⟨\mathbb{N};+,\{u_n:n\in \mathbb{N}\}\cap \mathbb{N}⟩$, $⟨\mathbb{N};<,n\mapsto \max \{0,u_n\}⟩$, and $⟨\mathbb{N};<,\varphi ⟩$ are undecidable, where $(u_n{)}_{n\in \mathbb{N}}$ is any integer LRS with exactly two non-repeated dominant roots satisfying a non-degeneracy assumption, and $\varphi$ is Euler's totient function.