Decidability of Extensions of Presburger Arithmetic by Hardy Field Functions

TL;DR

This paper investigates the logical decidability of extended Presburger arithmetic with Hardy field functions, showing most such extensions are undecidable especially when functions grow polynomially fast or sub-linearly.

Contribution

It establishes the undecidability of Presburger arithmetic extended by Hardy field functions under various growth conditions, advancing understanding of logical boundaries.

Findings

Most extensions with Hardy field functions are undecidable.

Undecidability occurs when functions grow polynomially faster than x.

Undecidability also occurs for functions growing sub-linearly but polynomially.

Abstract

We study the extension of Presburger arithmetic by the class of sub-polynomial Hardy field functions, and show the majority of these extensions to be undecidable. More precisely, we show that the theory $\mathrm{Th}(\mathbb{Z}; <, +, \lfloor f \rceil)$, where $f$ is a Hardy field function and $\lfloor \cdot \rceil$ the nearest integer operator, is undecidable when $f$ grows polynomially faster than $x$. Further, we show that when $f$ grows sub-linearly quickly, but still as fast as some polynomial, the theory $\mathrm{Th}(\mathbb{Z}; <, +, \lfloor f \rceil)$ is undecidable.