Decidability of extensions of Presburger arithmetic by generalised polynomials

TL;DR

This work studies the decidability of extending Presburger arithmetic by generalised polynomials and proves that a concrete quadratic generalised polynomial $g$ yields an undecidable theory for $(\mathbb{Z};<,+,g)$. The authors build a bridge from the analytic properties of $g$ to logical definability by showing $g$ agrees with a quadratic on long arithmetic progressions, enabling a weak form of multiplication to be defined and used to interpret multiplication in Robinson’s sense. The proof combines discrete differentiation, equidistribution of fractional parts, and carefully crafted arithmetic progressions to define divisibility and multiplicative structure within the first-order language, ultimately establishing undecidability. The results illuminate the boundary between decidability and undecidability for arithmetic extensions and set the stage for further exploration of generalised polynomials, Hardy field sequences, and sparse sequences in this context.

Abstract

We show that the extension of Presburger arithmetic by a quadratic generalised polynomial of a specific form is undecidable.

Theorems & Definitions (36)

• Conjecture 1.1
• Theorem A
• Corollary 1.2
• Theorem B
• Proposition 1.3
• proof
• Proposition 2.1
• Lemma 2.2
• proof
• proof : Proof of Prop. \ref{['prop:Pres+Q-undecidable']}