Undecidability results for arithmetic with special integer sequences
Rich Sequences and Decidability of Arithmetic Theories
Logic in Computer ScienceFormal Languages and Automata Theory
Summary
Some questions about numbers and formulas can never be completely solved by any computer or algorithm. This paper develops a new way to show that certain logical questions about numbers added to special sequences or functions are impossible to decide perfectly. The authors build on earlier work to apply this method to many integer sequences and important functions like Euler’s totient. Their work reveals limits on what can be computed or reasoned about in arithmetic systems that include these sequences and functions.
What this means in practice
- •For formal methods engineers: Recognize systems using integer sequences or totient function that have undecidable properties to avoid futile attempts at full automatic verification.
- •For computational number theorists: Use undecidability results to understand which arithmetic problems involving special integer sequences and functions cannot be fully algorithmically resolved.
A theory result. No direct application yet.
Authors
Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine
Abstract
We develop a new framework for proving the undecidability of first-order theories of structures of the form $\langle \mathbb{N}; +, P \rangle$, $\langle \mathbb{N}; <, f \rangle$, and $\langle \mathbb{N}; +, f\rangle$, where $P \subseteq \mathbb{N}$ and $f \colon \mathbb{N} \to \mathbb{N}$. It is based on the recent proof of Hieronymi and Schulz that the first-order theory of $\langle \mathbb{N}; +, \{2^n \colon n \in \mathbb{N}\}, \{3^n \colon n \in \mathbb{N}\}\rangle$ 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 $\langle \mathbb{N}; +, \{u_n \colon n \in \mathbb{N}\} \cap \mathbb{N}\rangle$, $\langle\mathbb{N}; <, n \mapsto \max\{0,u_n\}\rangle$, and $\langle \mathbb{N}; <, φ\rangle$ 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 $φ$ is Euler's totient function.