Abstract 1 Introduction 2 Hardy fields 3 Proof of the super-linear case 4 Proof of the near-linear case 5 Proof of the sub-linear case References Appendix A Omitted Proofs

Decidability of Extensions of Presburger Arithmetic by Hardy Field Functions

Hera Brown ORCID Department of Computer Science, University of Oxford, UK Jakub Konieczny111While working on this paper, the second-named author worked at the University of Oxford. He currently works at the Kyiv School of Economics. ORCID Department of Mathematics, Kyiv School of Economics, Ukraine
Department of Computer Science, University of Oxford, UK
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 Th(ℤ;<,+,⌊f⌉), where f is a Hardy field function and ⌊⋅⌉ 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 Th(ℤ;<,+,⌊f⌉) is undecidable.

Keywords and phrases:
Arithmetic theories, Hardy fields, Undecidability
Funding:
Jakub Konieczny: supported by UKRI Fellowship EP/X033813/1.
Copyright and License:
[Uncaptioned image] © Hera Brown and Jakub Konieczny; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation → Logic and verification
Editors:
Meena Mahajan, Florin Manea, Annabelle McIver, and Nguyễn Kim Thắng

1 Introduction

Presburger arithmetic, the first-order theory Th⁢(ℕ;+) of the natural numbers with addition, is known to be decidable [12], whereas Peano arithmetic, the extension of Presburger arithmetic by multiplication Th⁢(ℕ;+,×), is known to be undecidable [6]. The undecidability of Peano arithmetic provides a method that can be used to show that various other extensions of Presburger arithmetic are undecidable; if multiplication can be defined in such an extension, then that extension is undecidable. For instance, the extension of Presburger arithmetic with the squaring function Th⁢(ℕ;+,x↦x2) is undecidable, since a=b⁢c holds iff a+a=(b+c)2−b2−c2 (This observation appears to first have been made by Tarski [16] and then more generally by Büchi [5]).

This leads to the question of whether any extension of Presburger arithmetic by a polynomial-like function in general is undecidable. It is easy to see that, for integer-valued polynomials p of degree greater than 2, the extension of Presburger arithmetic by that polynomial Th⁢(ℕ;+,p) is undecidable. This is because we can define multiplication in the extension in much the same way as we could with the squaring function. Bès [2] surveys further decidable and undecidable extensions of Presburger arithmetic, some of which are shown to be undecidable by defining multiplication in Presburger arithmetic.

1.1 New Results

Hardy field functions (with polynomially bounded growth), discussed in detail in Section 2, are a far-reaching generalisation of polynomial sequences which is often studied in combinatorial number theory and ergodic theory, see e.g. [3], [4], [7] and [13]. They are particularly well-behaved from the point of view of analysis, which often allows one to adapt arguments originally applied to polynomials to this wider class of functions.

While we postpone proper definition of Hardy field functions, for now we point out that they contain all logarithmico-exponential functions – that is, the functions that can be built up from the basic arithmetical operations over the reals (addition, multiplication, subtraction, division), exponentiation and the taking of logarithms. Thus, for instance

f⁢(x)=x2+3⁢x+2, g⁢(x)=x⁢log⁡x+1x3, and ⁢h⁢(x)=2x3/5+log⁡x−2⁢n

are all Hardy field functions.

Since we are interested in extensions of Presburger arithmetic – which concerns the integers – and since Hardy field functions generally take real values, we need a way to construct integer-valued variants of Hardy field functions. For this we recall that, for x∈ℝ, the operator ⌊x⌉ denotes the best integer approximation of x, meaning that ⌊x⌉−1/2≤x<⌊x⌉+1/2. We will also occasionally use the floor and the ceiling functions, ⌊x⌋ and ⌈x⌉, respectively. For a function f we let ⌊f⌉ denote the function that rounds f to the nearest integer (i.e. ⌊f⌉(x)=⌊f(x)⌉=⌈f(x)−(1/2)⌉). Another technical issue we need to deal with is that Hardy field functions are generally defined only on an interval [x0,∞) rather than on all of ℝ. For the sake of simplicity, by convention, we extend any Hardy field function to ℝ by assigning the value 0 outside of the domain of definition. We are ultimately interested in evaluating the functions under consideration on large integers, so this issue does not affect the reasoning.

We now consider a question raised in [9]: Given a Hardy field function whose rate of growth is polynomial and faster than linear, is the first-order theory Th(ℤ;<,+,⌊f⌉) (Note that Th⁢(ℤ;<,+) is equivalent to Th⁢(ℕ;+)) decidable? In this paper we answer this question negatively. Formally, we prove the following theorem:

Theorem 1.1.

Let f:[x0,∞)→ℝ be a Hardy field function such that

limx→∞f⁢(x)x=∞ and limx→∞f⁢(x)xd=0 (1)

for an integer d≥2. Then the first-order theory of Th(ℤ;<,+,⌊f⌉) is undecidable.

Similarly, we can also deal with Hardy field functions whose rate of growth is slower than linear but not too slow.

Theorem 1.2.

Let f:[x0,∞)→ℝ be a Hardy field function such that

limx→∞f⁢(x)xε=∞ and limx→∞f⁢(x)x=0 (2)

for some ε>0. Then the first-order theory of Th(ℤ;<,+,⌊f⌉) is undecidable.

Broadly, then, the extension of Presburger arithmetic by most polynomial-like Hardy field functions yields an undecidable theory, as expected.

1.2 Proof Outline

We prove Theorem 1.1 in two parts; we first treat the super-linear case, where the Hardy field function f grows faster than a quadratic polynomial, and the near-linear case, where f grows faster than a linear polynomial but slower than a quadratic polynomial. Building on these results, we then prove Theorem 1.2, or the sub-linear case, where f grows slower than a linear function, separately.

In the super-linear case, we define multiplication using the fact that, over specific and arbitrarily large intervals, f can be closely approximated by a Taylor polynomial. By differentiating such polynomials, we can define multiplication between arbitrarily large numbers, and so define multiplication generally.

In the near-linear case, we use the near-linear growth of f to define an interval where f looks like a linear function. We show that there are sufficiently many of these intervals to define multiplication over a restricted domain. By taking difference sets, we then extend this restricted domain to the whole of ℤ×ℤ. This defines multiplication generally.

In the sub-linear case, we use the fact that the inverse of f can be approximated in our theory, as well as the fact that the inverse of f grows faster than x, to define a near-linear or super-linear rounded Hardy field function. We then apply Theorem 1.1, and undecidability follows.

1.3 Future directions

1.3.1 Weakening of conditions

In proving Theorem 1.1, we use only a few properties that Hardy field functions have, namely that they are d-times differentiable and have well-behaved Taylor approximations. It would be interesting to see which broader classes of functions also satisfy these requirements, as well as seeing how these requirements may be weakened further (particularly with regards to the equidistribution results that are required in the proof of Theorem 1.1).

1.3.2 Extension to non-polynomial functions

The proofs above also focus on the case where f grows only polynomially quickly, but it might be interesting to see what non-polynomial Hardy field functions provide undecidable extensions of Presburger arithmetic. It seems that functions that grow exponentially or faster, and their inverses, would provide decidable extensions of Presburger arithmetic by ideas similar to Semënov’s [14, 15]. But functions that grow between polynomially and exponentially fast seem more interesting.

In particular, it seems that using the function f⁢(x)=2x we can define a function with polynomial growth. Taking f−1⁢(f′⁢(x))−x, we get a function that looks similar to x⁢log⁡x, and by the results of this paper rounding this function and extending Presburger arithmetic by it leads to an undecidable theory. This then raises the question of how far this idea can be generalised:

Question 1.3.

Given a Hardy field function f:[x0,∞)→ℝ such that

limx→∞f⁢(x)xn=∞ and limx→∞f⁢(x)mx=0 (3)

for all integers n and m>1, is the first-order theory of Th(ℤ;<,+,⌊f⌉) decidable?

1.3.3 Generalisation to other theories

Given that the theory of Skolem arithmetic, namely Th⁢(ℕ;×), is decidable [2], it would be interesting to see whether the similar theory of Th(ℕ;×,⌊f⌉) is decidable as well. This relates to a question raised by Korec [11] as to whether the theory Th⁢(ℕ;×,X) is decidable, where X is the image of some polynomial function. In particular, it would be interesting to see whether Hardy field functions can in general be used to define addition as well as multiplication, and so used to show undecidability of the above theory. This leads us to the following question:

Question 1.4.

Let f:ℝ→ℝ be a Hardy field function such that

limx→∞f⁢(x)xd=∞ and limx→∞f⁢(x)xd+1=0 (4)

for an integer d>1. Is the first-order theory of Th(ℤ;×,⌊f⌉) decidable?

A similar question would be to see if just the theory Th(ℕ;⌊f⌉) is decidable.

1.4 Notation

We let ℕ be the set of nonnegative integers {0,1,2,…}. For x∈ℝ, we define the integer part ⌊x⌋ of x to be max⁡{n∈ℤ∣n≤x}, and the ceiling ⌈x⌉ of x to be min⁡{n∈ℤ∣n≥x}. We define the nearest integer of x to be ⌊x⌉=⌈x−1/2⌉. When applying the nearest integer function to a function generally, we write ⌊f⌉(x) for ⌊f⁢(x)⌉. We also write the circle norm of x as ‖x‖ℝ/ℤ=min⁡{|x−n||n∈ℤ} to denote the distance of x to the nearest integer.

2 Hardy fields

We define Hardy fields as follows. Let B be a set of equivalence classes of continuous real-valued functions in one variable, where we say that two such functions f and g are equivalent when they eventually agree, i.e., when there exists some x0 such that, for all x>x0, we have f⁢(x)=g⁢(x). Such equivalence classes are also called germs at infinity. The set B naturally gives rise to a ring (B,+,×). We say that a Hardy field is a subfield of the ring (B,+,×) that is closed under differentiation. A Hardy field function is a function that belongs to a Hardy field, or more precisely whose germ at infinity belongs to the union of all Hardy fields.

The union of all Hardy fields is large enough to include a variety of interesting functions. This includes, as mentioned in Section 1.1, the class of logarithmico-exponential functions built up from real polynomials, exponentiation, and the taking of logarithms. This gives us both a natural class of examples of Hardy field functions, as well as a natural class of functions to compare general Hardy field functions to.

Hardy field functions exhibit many properties that make them well suited to analytic arguments. As a first instance of this principle, because of the fact that every Hardy field function is asymptotically comparable to 0, we have the following standard fact (e.g. presented in [7]).

Lemma 2.1.

Let f:ℝ→ℝ be a Hardy field function. Then f is either eventually positive, eventually negative, or eventually zero. Likewise, f is either eventually increasing, eventually decreasing, or eventually constant.

As a consequence, it makes sense to compare rates of growth of different Hardy field functions. Given two eventually positive functions f and g belonging to the same Hardy field, we write:

  • ■

    f⁢(x)≪g⁢(x) if limx→∞f⁢(x)/g⁢(x)<∞;

  • ■

    f⁢(x)≺g⁢(x) if limx→∞f⁢(x)/g⁢(x)=0;

  • ■

    f⁢(x)∼g⁢(x) if limx→∞f⁢(x)/g⁢(x)∈(0,∞).

Note that f⁢(x)≪g⁢(x) holds if and only if either f⁢(x)≺g⁢(x) or f⁢(x)∼g⁢(x).

In particular, throughout we consider Hardy field functions f:[x0,∞)→ℝ; by this we mean that f behaves as usual on the half-line [x0,∞), and that f⁢(x)=0 for all x<x0. We pick x0 such that f is either strictly increasing or strictly decreasing over the interval [x0,∞), which by Lemma 2.1 we are licenced to do. This does not affect the correctness of our arguments when applied to Hardy field functions generally, but merely simplifies proofs.

Lemma 2.2.

Let f,g:[x0,∞)→ℝ be eventually positive functions belonging to the same Hardy field. Then either f⁢(x)≺g⁢(x) holds, f⁢(x)∼g⁢(x) holds, or f⁢(x)≻g⁢(x) holds. Further, exactly one of the above holds.

One convenient feature of Hardy field functions is that their derivatives have a rate of growth that is easy to describe, as shown in the following result.

Lemma 2.3 ([7, Lem. 2.1]).

Let f:[x0,∞)→ℝ be a Hardy field function that satisfies x−d≪|f⁢(x)|≪xd for some d∈ℕ. Then |f′⁢(x)|≪|f⁢(x)|/x.

Another convenient feature of Hardy field functions is that they can be accurately approximated by their Taylor expansions. Given a function f:[x0,∞)→ℝ that has sufficiently many derivatives, for x≥x0 and y≥0, we can always consider the length-ℓ Taylor expansion f⁢(x+y)=Px,ℓ⁢(y)+Rx,ℓ⁢(y), where Px,ℓ is the Taylor polynomial

Px,ℓ⁢(y)=f⁢(x)+y⁢f′⁢(x)+⋯+yℓ−1(ℓ−1)!⁢f(ℓ−1)⁢(x),

and Rx,ℓ is the remainder term (which we can consider to be defined simply as Rx,ℓ⁢(y)=f⁢(x+y)−Px,ℓ⁢(y)). Since Hardy field functions do have sufficiently many derivatives, we can consider such Taylor expansions of Hardy field functions. We will use the following standard estimate (similar results can be found e.g. in [7] or [10, Prop. 2.9]).

Proposition 2.4.

Let f:[x0,∞)→ℝ be a Hardy field function that satisfies td−1≪|f⁢(t)|≺td for some d∈ℕ. Then we have Rx,d⁢(y)≪yd⁢f⁢(x)/xd for sufficiently large x and all 0≤y≤x. (The constant implicit in the asymptotic notation depends only on f).

Proof.

Recall that for any x≥x0 and y≥0 there exists z∈[0,y] such that Rx,d⁢(y)=yd/d!⁢f(d)⁢(x+z). Iterating Lemma 2.3 d times, we see that f(d)⁢(t)≪f⁢(t)/td→0 as t→∞. Since f(d) is a Hardy field function and is eventually monotone, we have

|Rx,d⁢(y)|≤ydd!⁢|f(d)⁢(x)|≪yd⁢f⁢(x)/xd.

◀

We will also need the following results on distribution of Hardy field sequences. (We point out that [4] in fact provides if and only if statements, but we will only be interested in one direction).

Theorem 2.5 ([4, Thm. 1.9]).

Let f1,f2,…,fk be functions belonging to the same Hardy field. Suppose that for each n1,n2,…,nk∈ℤ, not all zero, and for every polynomial p⁢(x)∈ℚ⁢[x], letting g⁢(x)=n1⁢f1⁢(x)+n2⁢f2⁢(x)+⋯+nk⁢fk⁢(x)−p⁢(x), we have limx→∞|g⁢(x)|=∞. Then the sequence (f1⁢(n)mod1,f2⁢(n)mod1,…,fk⁢(n)mod1)n=0∞ is dense in ℝk/ℤk.

▶ Remark 2.6.

Note that, on the stronger condition that limx→∞|g⁢(x)|/log⁡x=∞, the sequence (f1⁢(n)mod1,f2⁢(n)mod1,…,fk⁢(n)mod1)n=0∞ is also uniformly distributed in ℝk/ℤk [4, Thm. 1.8].

3 Proof of the super-linear case

In this section we will prove Theorem 1.1 in the case where when f⁢(x)≫x2. Broadly speaking, we will prove that all such Hardy field functions have what will be called the Pd property, which expresses that a function looks like a polynomial over arbitrarily long intervals. From that, we will introduce the Pdℤ property, which expresses that f looks like an integer-valued polynomial over arbitrarily long intervals. We will then show that if f has the Pdℤ property, then the first-order theory Th(ℤ;<,+,⌊f⌉) is undecidable. A key step of the argument is differentiating the polynomial given by the Pdℤ property.

To begin with, we conduct the proof under the additional assumption that xd−1≺f⁢(x)≺xd for some d≥3. In particular, we initially exclude the case where f⁢(x)∼xd−1, which we cover in a separate Subsection 3.5. The proof in the latter case follows along broadly similar lines. However, failure of certain equidistribution results forces us to introduce some new ideas.

3.1 The 𝑷𝒅 property

We first introduce the Pd property, which holds of a function when that function can be approximated arbitrarily closely, and over arbitrarily long intervals, by some polynomial of degree less than d. Formally, we will say that a function f:[x0,∞)→ℝ has property Pd for some d∈ℕ if for each M∈ℕ and ε>0 there exists some N∈ℕ and a degree-(d−1) polynomial p such that for all 0≤m<M we have |f⁢(N+m)−p⁢(m)|<ε. A convenient feature of Hardy field functions with polynomial growth is that they enjoy the property Pd, as shown in the following lemma.

Lemma 3.1.

Let f be a Hardy field function such that xd−1≪f⁢(x)≺xd for some d∈ℕ. Then f has the Pd property.

Proof.

Pick any M∈ℕ and ε>0, and let N be a large integer, to be determined in the course of the argument. Recall that we can expand f⁢(N+m) as PN,d⁢(m)+RN,d⁢(m), where PN,d⁢(m) is the degree-(d−1) Taylor polynomial and RN,d⁢(m) is the corresponding remainder term. Assuming, as we may that N>M, for 0≤m≤M, by Proposition 2.4 we have |RN,d⁢(m)|≪Md⁢f⁢(N)/Nd. Since f⁢(N)/Nd→0 as N→∞, picking sufficiently large N we can ensure that |RN,d⁢(m)|≤ε, as needed. ◀

3.2 The 𝑷𝒅ℤ property

Recall that we are ultimately interested not in a Hardy field function f but rather in its integer-valued rounding ⌊f⌉. Like in the previous section, let us suppose for a moment that on some interval [N,N+M) the Hardy field function f is closely approximated by a degree-(d−1) polynomial p, in the sense that for all 0≤m<M we have |f⁢(N+m)−p⁢(m)|<ε for some small constant ε>0. In this situation, it is not necessarily the case that ⌊f⌉ is closely approximated by ⌊p⌉. Indeed, if for some 0≤m<M we have f⁢(N+m)>k+(1/2)>p⁢(m) with k∈ℤ then ⌊f(N+m)⌉=k+1≠k=⌊p(m)⌉. As a first step, we would like to avoid this behaviour, which is most easily accomplished by requiring that ‖f⁢(N+m)‖ℝ/ℤ and ‖p⁢(m)‖ℝ/ℤ are both small. Secondly, we note that (in the regime where M is much larger than d) the only way for ‖p⁢(m)‖ℝ/ℤ to be small for all 0≤m<M is if p is closely approximated by an integer-valued polynomial, i.e. a polynomial q such that q⁢(ℤ)⊆ℤ (since we only use this statement as a source of intuition, we leave it admittedly vague). This motivates us to introduce a property Pdℤ, which is an analogue of the property Pd discussed earlier. We will say that a function f:[x0,∞)→ℝ has property Pdℤ for some d∈ℕ if for each M∈ℕ and ε>0 there exists N∈ℕ and a degree-(d−1) integer-valued polynomial p such that for all 0≤m<M we have |f⁢(N+m)−p⁢(m)|<ε. Above, we require that the polynomial p should have degree exactly d−1, as opposed to at most d−1; this requirement will play an important role in later considerations.

Lemma 3.2.

Let f be a Hardy field function such that xd−1≺f⁢(x)≺xd for some d∈ℕ. Then f has the Pdℤ property.

Proof.

Pick any M∈ℕ and ε>0. Recall from the proof of Lemma 3.1 that for sufficiently large N we can accurately approximate f on [N,N+M) using the Taylor expansion PN,d, meaning that |f⁢(N+m)−PN,d⁢(m)|<ε/2 for all 0≤m<M. Recall also that the coefficients of PN,d are given by

PN,d⁢(m)=∑k=0d−1f(k)⁢(N)k!⁢mk.

Consider the polynomial p obtained from PN,d by applying rounding to each coefficient:

p(m)=∑k=0d−1⌊f(k)⁢(N)k!⌉mk.

Since p has integer coefficients, it is clearly integer-valued. Our plan is to show that, for a judicious choice of N, the circle norms of coefficients of PN,d are small and consequently f is closely approximated by p.

We will apply Theorem 2.5 to the functions f,f′,…,f(d−1)/(d−1). For each 0≤k≤d we have f(k)⁢(x)∼f⁢(x)/xk by repeated application of Lemma 2.3. As a consequence, for any non-trivial linear combination h⁢(x)=c0⁢f⁢(x)+c1⁢f′⁢(x)+⋯+cd−1⁢f(d−1)⁢(x)/(d−1)! with c0,c1,…,cd−1∈ℤ we have h⁢(x)∼f⁢(x)/xℓ, where ℓ is the first index with cℓ≠0. Thus, for any polynomial q with degree e we have |h⁢(x)−q⁢(x)|∼f⁢(x)/xℓ if d−ℓ>e or |h⁢(x)−q⁢(x)|∼xe otherwise (that is, if d−ℓ≤e). In either case, we have |h⁢(x)−q⁢(x)|≻1, as needed. We conclude that the sequence (f⁢(N),f′⁢(N),…,f(d−1)⁢(N)/(d−1)!)N=0∞ is dense modulo 1, and in particular it includes points with arbitrarily small circle norms. Hence, we can find N such that for all 0≤k<d we have:

‖f(k)⁢(N)k!‖ℝ/ℤ≤ε2⁢d⁢Mk.

Therefore, we have the estimate

|PN,d⁢(m)−p⁢(m)|≤∑k=0d−1‖f(k)⁢(N)k!‖ℝ/ℤ⁢Mk≤ε/2.

Combining this with the previously mentioned estimate on |f⁢(N+m)−PN,d⁢(m)| we conclude that |f⁢(N+m)−p⁢(m)|<ε, as needed. Finally, increasing N if necessary, we may assume that the leading coefficient of p, i.e. ⌊f(d−1)⁢(N)/(d−1)!⌉, is non-zero. ◀

3.3 Discrete derivatives

Using Lemma 3.2, for a Hardy field function f satisfying the assumptions of Theorem 1.1, we can find arbitrarily long intervals [N,N+M) where ⌊f⌉ agrees with some integer-valued polynomial p. The goal of the next two subsections is to prove the following lemma, asserting that this property implies that the theory Th(ℤ;<,+,⌊f⌉) is undecidable.

Lemma 3.3.

Let f:[x0,∞)→ℝ be a function that satisfies the Pdℤ property for some d≥3. Then the theory Th(ℤ;<,+,⌊f⌉) is undecidable.

A key ingredient of the proof of Lemma 3.3 is the notion of differentiation for sequences indexed by integers, which will ultimately help us define multiplication. To this end, we introduce the discrete derivative and the symmetric discrete derivative of a function:

Definition 3.4.

Given a function f:ℤ→ℝ and an integer m, the discrete derivative (also known as finite difference) ⁢Δm⁡f:ℤ→ℝ is given by

⁢Δm⁡f⁢(n)=f⁢(n+m)−f⁢(n)

and the symmetric discrete derivative ⁢fm:ℤ→ℝ is given by

⁢fm⁢(n)=⁢Δm⁡⁢Δn⁡f⁢(0)=f⁢(n+m)−f⁢(n)−f⁢(m)+f⁢(0).

Of course, the discrete derivative of an integer-valued function is again integer-valued. We also point out that the discrete derivative operators commute: Δm⁢Δn=Δn⁢Δm. The symmetric derivative, as the name suggests, is a symmetric function of the arguments: ⁢fm⁢(n)=⁢fn⁢(m). For reasons of symmetry, given an integer r≥1 and integers n0,n1,…,nr we write ⁢fr⁢(n0,n1,…,nr) for ⁢nr⁢…nr−1⁢n1⁢f⁢(n0).

A particularly useful feature of the discrete derivative (symmetric or otherwise) is that its application to a polynomial yields a polynomial of degree one less. As a consequence, its repeated application only leaves the leading term of the function to be considered. We make this observation concrete in the following result.

Lemma 3.5.

Let m be an integer and let p be a polynomial of degree r with leading coefficient ar.

  1. (a)

    If r≥1 then Δm⁢p is a polynomial with degree r−1 and leading coefficient r⁢ar⁢m. If r=0 then Δm⁢p=0.

  2. (b)

    If r≥2 then m⁢p is a polynomial with degree r−1 and leading coefficient r⁢ar⁢m. If r=0 or r=1 then m⁢p=0.

Proof.

It is straightforward to verify by an explicit computation that item (a) holds for r=0 and item (b) holds for r=0,1. For r≥2, Δm⁢p and m⁢p differ only by a constant (equal to p⁢(m)−p⁢(0)) so it suffices to prove item (a).

We proceed by induction on r, the case r=0 already having been considered. Thus, we may assume that r≥1 and the claim has already been proved for all r′<r.

We may write p⁢(x)=ar⁢xr+p~⁢(x) where deg⁡p~<r. By the inductive assumption, Δm⁢p~ is a polynomial of degree strictly less than r−1 (or identically zero if r=1), so it suffices to deal with the leading term. We can explicitly compute that

ar⁢(x+m)r−ar⁢xr=∑k=1r(rk)⁢ar⁢mk⁢xr−k,

where the right side is a degree-(r−1) polynomial with leading coefficient r⁢ar⁢m, as needed.

◀

For brevity, we write ⁢fr⁢(a,b) for ⁢fr⁢(a,b,1,1,…,1) whenever r≥1. As an application of Lemma 3.5 we almost immediately get the following formula.

Lemma 3.6.

Let p be a polynomial with degree r and leading coefficient ar. Then r−1⁢p⁢(n,m)=r!⁢ar⁢n⁢m.

Proof.

Iterating Lemma 3.5 we see that r−1⁢p⁢(n,m) is a polynomial function of n with degree 1 and leading coefficient r!⁢ar⁢m. To see that all the remaining coefficients are zero, it is enough to recall that r−1⁢p⁢(n,m) is a symmetric function of n and m, and that r−1⁢p⁢(0,0)=0. ◀

In the direction opposite to Lemma 3.5, we have the following characterisation of polynomials in terms of discrete derivatives. It is a standard observation, for instance following from discussion in [8, Section 2.6]; we include a proof here for completeness.

Lemma 3.7.

Let r≥0 and let f:[N,N+M)→ℝ be a sequence such that Δ1r+1⁢f⁢(n)=0 for N≤n<N+M−r−1. Then f coincides with a polynomial of degree at most r.

Proof.

For any polynomial p of degree at most r we have Δ1r+1⁢p=0, so we may freely replace f with f−p. Applying Lagrange interpolation, we may thus assume that f⁢(N)=f⁢(N+1)=⋯=f⁢(N+r)=0. Since Δ1r+1⁢f⁢(n)=0 for all n where it is defined, we see that if we have f⁢(n)=f⁢(n+1)=⋯=f⁢(n+r)=0 for some N≤n<N+M−r−1 then also f⁢(n+r+1)=0. Reasoning by induction with respect to n we thus conclude that f⁢(m)=0 for all N≤m<N+M. In particular, f is a polynomial of degree at most r. ◀

3.4 Emulating multiplication

Using the results obtained in Section 3.3, we next show how to use property Pdℤ to emulate multiplication. Recall that Pdℤ implies that we can find arbitrarily long intervals [N,N+M) where ⌊f⌉ agrees with an integer-valued polynomial p (in the sense that ⌊f⌉(N+m)=p(m)). What is more, we can use Lemma 3.7 to detect intervals with the property mentioned above. Given such an interval, for 1≤a,b,c≤M we can use Lemma 3.6 to express the property that a⁢b=c as d−2⁢p⁢(a,b)=d−2⁢p⁢(c,1). We now put this plan into practice.

Lemma 3.8.

Let d≥2 and let πd⁢(N,M) be the sentence given by

∃c≠0∀0≤m<M−d:Δ1d−1⌊f⌉(N+m)=c.

Then πd⁢(N,M) holds if and only if there exists a polynomial p with degree exactly d−1 such that ⌊f⌉(N+m)=p(m) for all 0≤m<M.

Proof.

Suppose that πd⁢(N,M) holds. Applying Δ1 once more, we conclude from Lemma 3.7 that ⌊f⌉ agrees with a polynomial p of degree at most d−1 on [N,N+m). If p had degree strictly less than d−1 then, by repeated application of Lemma 3.5, we would have Δ1d−1⌊f⌉(N+m)=0≠c, contradicting πd⁢(N,M). Thus, p has degree exactly d−1, as needed.

Suppose now that there exists a polynomial p with degree exactly d−1 such that ⌊f⌉(N+m)=p(m) for all 0≤m<M. Then, by repeated application of Lemma 3.5, we have Δ1d−1⌊f⌉(N+m)=(d−1)!ad−1, where ad−1 is the leading coefficient of p. Thus, setting c=(d−1)!⁢ad−1 we see that πd⁢(N,M) holds. ◀

Lemma 3.9.

Let d≥3 and let μd⁢(n,m,q) be the sentence given by

∃M>max(n,m,q)∃N:πd(N,M)∧Δ1d−3ΔnΔm⌊f⌉(N)=Δ1d−2Δq⌊f⌉(N).

Assume that f enjoys property Pdℤ and n,m,q≥1. Then, for n,m,q∈ℕ we have that μd⁢(n,m,q) holds if and only if q=n⁢m.

Proof.

Suppose that μ⁢(n,m,q) holds. Pick admissible M and N. Since, in particular, πd⁢(N,M) holds, we know from Lemma 3.8 that there exists a polynomial p of degree d−1 such that ⌊f⌉(N+m)=p(m) for 0≤m<M. The equality between the discrete derivatives in the definition of μ⁢(n,m,q) can now more simply be expressed as d−2⁢p⁢(n,m)=d−2⁢p⁢(q,1). By Lemma 3.6, this implies that n⁢m=q, as needed.

Next, suppose that q=n⁢m. Pick M=q+1. By Pdℤ, we can find N and a polynomial p of degree exactly d−1 such that ⌊f⌉(N+m)=p(m) for 0≤m<M. By Lemma 3.8, πd⁢(N,M) holds. By Lemma 3.5, we have d−2⁢p⁢(n,m)=(d−1)!⁢ad−1⁢n⁢m=(d−1)!⁢ad−1⁢q=d−2⁢p⁢(q,1). Hence μ⁢(n,m,q) holds, as needed. ◀

Proof of Lemma 3.3.

It follows from Lemma 3.9 that multiplication on ℕ is definable in Th(ℤ;<,+,⌊f⌉), and extending it to ℤ is immediate. Since Th⁢(ℤ;<,+,×) is undecidable, so is Th(ℤ;<,+,⌊f⌉). ◀

Combining Lemmas 3.2 and 3.3, we conclude that for each d≥3 and each Hardy field function f with xd−1≺f⁢(x)≺xd, the theory Th(ℤ;<,+,⌊f⌉) is undecidable. This completes the proof of the first case of Theorem 1.1.

3.5 Generalisation to exactly polynomial growth

Finally, we show how the argument in the earlier sections generalises to sequences with exactly polynomial growth. Recall that previously we considered a Hardy field function f with xd−1≺f⁢(x)≺xd for some d≥3. Presently, we will instead assume that f⁢(x)∼xd−1 (note that we make this choice instead of the more natural f⁢(x)∼xd for the sake of consistency with earlier considerations).

A significant part of the previously presented argument goes through without any change. Indeed, it remains the case that f enjoys the Pd property and can be accurately approximated by the Taylor polynomial PN,d. Unfortunately, we are not able to establish the Pdℤ property. When we try to repeat the previous argument, the d-tuple formed by the coefficients of PN,d, namely

(f⁢(N),f′⁢(N),f′′⁢(N)/2,…,f(d−1)⁢(N)/(d−1)!),

is not equidistributed modulo 1. Indeed, the top coefficient f(d−1)⁢(N)/(d−1)! can easily be shown to converge to a constant, and the behaviour of the remaining coefficients is potentially more complicated.

Because of the aforementioned limitation, we adapt the remainder of the argument to use property Pd instead of Pdℤ. This introduces some complications since we are forced to apply discrete derivatives to functions of the form ⌊p⌉, where p is a polynomial, rather than to polynomials. Fortunately, the following lemma allows us to control errors arising from the rounding operation; we will apply it to h(n)=p(n)−⌊p(n)⌉.

Lemma 3.10.

Let h:ℤ→ℝ be a sequence with |h⁢(n)|≤ε for all n∈ℤ. Then

|Δm1⁢Δm2⁢…⁢Δmr⁢h⁢(n)|≤2r⁢ε

for all integers r≥1 and all n,m1,m2,…,mr∈ℤ.

Proof.

For r=1, the result follows from a straightforward computation. For r>1, we use a standard inductive argument. ◀

Using Lemma 3.10, we define a coarser variant of multiplication, which we then bootstrap to a definition of multiplication. This finishes the proof of the relevant case of Theorem 1.1. We now put the strategy discussed above into practice. Formally, we establish the following result.

Proposition 3.11.

Let f:[x0,∞)→ℝ be a Hardy field function where f⁢(x)∼xd−1 for some d≥3. Then the theory Th(ℤ;<,+,⌊f⌉) is undecidable.

Proof.

Fix an integer M and let N be sufficiently large such that the Hardy field function f is closely approximated by the degree-(d−1) polynomial PN,d, in the sense that we have |f⁢(N+m)−PN,d⁢(m)|<1/10 for all 0≤m<M. Recall that the leading coefficient of PN,d is f(d−1)⁢(N)/(d−1)!, which converges to some non-zero constant α as N→∞. Let p be the polynomial obtained from PN,d by replacing the leading coefficient with α. Picking larger N if necessary, we may freely assume that |f⁢(N+m)−p⁢(m)|<1/10 for all 0≤m<M.

Note that, since p is a polynomial of degree d−1, we can apply Lemma 3.6 to it and get that d−2⁢p⁢(n,m)=(d−1)!⁢α⁢n⁢m. Bearing in mind that we aim to adapt Lemma 3.9, we use Lemma 3.10 with h(m)=⌊f(N+m)⌉−p(m) and ϵ=1 to approximate

|Δ1d−3ΔnΔm⌊f⌉(N)−(d−1)!αnm|≤2d−1,

provided that 0≤n,m<M. This motivates us to consider, for 0≤a,b,c<M, the quantity FN⁢(a,b,c) defined as follows:

FN(a,b,c)=Δ1d−3ΔaΔb⌊f⌉(N)−Δ1d−2Δc⌊f⌉(N).

The estimate obtained above implies that we have

|FN⁢(a,b,c)−(d−1)!⁢α⁢(a⁢b−c)|≤2d.

Fix an integer D≥100⋅2d/min⁡(1,(d−1)!⁢α). The estimate above allows us to prove the following lemma:

Lemma 3.12.

Let 0≤a,b,c<M. Then |FN⁢(D⁢a,b,D⁢c)|≤2d holds for all sufficiently large N if and only if a⁢b=c.

Proof.

For the rightwards direction of proof, first suppose that a⁢b≠c. Since a⁢b−c is a non-zero integer, it follows that |D⁢a⁢b−D⁢c|≥D. So the following equalities hold:

|FN⁢(D⁢a,b,D⁢c)| ≥|(d−1)!⁢α⁢D⁢(a⁢b−c)|−|FN⁢(a,b,c)−(d−1)!⁢α⁢(a⁢b−c)|
≥(d−1)!⁢α⁢D⁢|a⁢b−c|−2d≥(d−1)!⁢α⁢D−2d>2d.

For the leftwards direction of proof, suppose that a⁢b=c. Then D⁢a⁢b−D⁢c=0 as well. It follows that |FN⁢(D⁢a,b,D⁢c)|≤2d as required. ◀

Note that |FN⁢(D⁢a,b,D⁢c)| is definable in Th(ℤ;<,+,⌊f⌉). Thus, Lemma 3.12 allows us to define multiplication in Th(ℤ;<,+,⌊f⌉). More formally, let μ′⁢(a,b,c) denote the formula

∀N0⁢∃N≥N0:|FN⁢(D⁢a,b,D⁢c)|≤2d.

It follows from the preceding discussion (in particular Lemma 3.12) that μ′⁢(a,b,c) holds if and only if a⁢b=c, because Lemma 3.12 holds for any sufficiently large N. Recalling that Th⁢(ℤ;<,+,×) is undecidable and that multiplication is definable in Th(ℤ;<,+,⌊f⌉), we conclude that Th(ℤ;<,+,⌊f⌉) is undecidable. ◀

▶ Remark 3.13.

One could use the techniques used here in order to establish Theorem 1.1 also in the case where xd−1≺f⁢(x)≺xd. We take the route discussed earlier because we consider it to be more elegant, and because it has the added advantage of allowing us to identify the property Pdℤ.

▶ Remark 3.14.

We note that previously, we were able to establish undecidability of Th(ℤ;<, +,⌊f⌉) as a consequence purely of the property Pdℤ. This is in contrast with the argument discussed presently, which uses a property strictly stronger than Pd, namely that f is closely approximable by a polynomial on the interval [N,N+M) for all N that are sufficiently large (as a function of M). It would be interesting to determine if the property Pd by itself is sufficient to establish undecidability. The key difficulty to this approach is finding a suitable analogue of Lemma 3.8.

4 Proof of the near-linear case

In this section, we prove the second case of Theorem 1.1 where f grows super-linearly but sub-quadratically i.e. when x≺f⁢(x) and f⁢(x)≺x2. To this end, we first define multiplication over a limited domain, using the fact that over certain intervals f can be closely approximated by a linear function. We then use difference sets to extend this definition of multiplication to the whole of ℤ×ℤ and thus show Th(ℤ;<,+,⌊f⌉) undecidable.

4.1 Multiplicative intervals

We first define a property λ⁢(N,M,n) which, informally, states that over the interval [N,N+M) the function ⌊f⌉ defines an arithmetic progression with step n. Formally, we define λ by

λ(N,M,n)=def∀ 0≤m<M:⌊f⌉(N+m+1)=⌊f⌉(N+m)+n.

It is routine to show that λ⁢(N,M,n) holds if and only if for all 0≤m<M we have ⌊f⌉(N+m)−⌊f⌉(N)=mn. Our next step is to establish sufficient conditions for λ⁢(N,M,n) to hold.

Lemma 4.1.

Let f:[x0,∞)→ℝ be a Hardy field function with x≺f⁢(x)≺x2. Then there exists x1≥x0 such that λ⁢(N,M,n) holds for all N,M,n∈ℕ satisfying the following conditions:

  1. (a)

    N≥x1;

  2. (b)

    ‖f⁢(N)‖ℝ/ℤ<1/4;

  3. (c)

    |f′⁢(N)−n|<1/(8⁢M);

  4. (d)

    f′′⁢(N)<1/(8⁢M2).

Proof.

Informally speaking, we first approximate f⁢(N+m) by f⁢(N)+f′⁢(N)⁢m, then approximate f′⁢(N) by n, and finally apply rounding to conclude that ⌊f⌉(N+m)=⌊f⌉(N)+mn.

Formally, our first goal is to show that

|f⁢(N+m)−f⁢(N)−f′⁢(N)⁢m|<116. (5)

Towards this end, we consider the Taylor expansion of f at N. We have

f⁢(N+m)=f⁢(N)+f′⁢(N)⁢m+12⁢f′′⁢(N+t)⁢m2

for some t∈[0,m]. Thus, the expression on the right side of equation (5) is

|f⁢(N+m)−f⁢(N)−f′⁢(N)⁢m|=|12⁢f′′⁢(N+t)⁢m2|≤M22⁢|f′′⁢(N+t)|.

Since f⁢(x)≺x2, we know that f′′⁢(x)≺1, meaning that f′′⁢(x)→0 as x→∞. As a consequence, f′′ is eventually decreasing, and picking x1 sufficiently large we may assume that f′′ is decreasing on [N,∞). Thus, condition (a) allows us to simplify our estimate to

|f⁢(N+m)−f⁢(N)−f′⁢(N)⁢m|≤M22⁢|f′′⁢(N)|≤116,

where the last inequality follows from condition (d). This completes the proof of (5).

In order to approximate f′⁢(N) by n we simply use condition (c), which immediately yields that |f′⁢(N)⁢m−n⁢m|<1/8. Combining this with equation (5), we get

|f⁢(N+m)−f⁢(N)−n⁢m|<116+18<14. (6)

It remains to deal with rounding. We have

⌊f⌉(N+m)−⌊f⌉(N)−nm =⌊f(N+m)⌉−⌊f(N)⌉−nm⌊f(N+m)−⌊f(N)⌉−nm⌉.

Bearing in mind that ⌊x⌉=0 for all x with |x|<1/2, in order to show that ⌊f⌉(N+m)=⌊f⌉(N)+nm, it suffices to estimate that

|f(N+m)−⌊f(N)⌉−nm| ≤14+|f(N)+nm−⌊f(N)⌉−nm|
=14+‖f⁢(N)‖ℝ/ℤ<12

Note that the first inequality follows from (6), and the last one from condition (2). ◀

In the following lemma, we show how the conditions of Lemma 4.1 hold sufficiently often.

Lemma 4.2.

Let f:[x0,∞)→ℝ be a Hardy field function with x≺f⁢(x)≺x2. Then for any real x1≥x0 and ε0,ε1,ε2>0 there exists integer n0 such that for each n≥n0 there exists integer N satisfying the following conditions:

  1. (a)

    N≥x1;

  2. (b)

    ‖f⁢(N)‖ℝ/ℤ<ε0;

  3. (c)

    |f′⁢(N)−n|<ε1;

  4. (d)

    f′′⁢(N)<ε2.

We omit the proof of Lemma 4.2 here and leave the full proof for the appendix.

Combining Lemmas 4.1 and 4.2, we immediately obtain the following consequence.

Corollary 4.3.

For each M there exists n0 such that for all n≥n0 there exists N such that λ⁢(N,M,n) holds.

4.2 Restricted multiplication

In the previous subsection, we established sufficient conditions for λ⁢(N,M,n) to hold. We now show how we can use λ to define a restricted form of multiplication. Towards this end, we consider the condition μ0⁢(n,m,p) given by

∃N∃M>m:λ(N,M,n)∧(⌊f⌉(N+m)=⌊f⌉(N)+p).

Recalling that λ⁢(N,M,n) implies that ⌊f⌉(N+m)=⌊f⌉(N)+nm, we immediately see that if μ0⁢(n,m,p) holds then p=n⁢m. Thus, μ0 defines multiplication on the (definable) set D0⊆ℤ×ℤ consisting of the pairs (n,m) such that μ0⁢(n,m,p) holds.Corollary 4.3 now translates into the following statement.

Corollary 4.4.

For each m∈ℕ there exists tm such that [tm,∞)×{m}⊆D0.

Our next goal is to extend the definition of multiplication from D0 to all of ℤ×ℕ.

4.3 Difference sets and total multiplication

Finally, we show that we can extend the restricted multiplication defined by μ0 using difference sets. Informally, we rely on the fact that once we have defined n⁢m and n′⁢m we can define (n−n′)⁢m by distributivity. To this end, define the following formula:

μ1⁢(n,m,p) =def∃n′,n′′,p′,p′′(μ0(n′,m,p′)∧μ0(n′′,m,p′′)
∧n=n′′−n′∧p=p′′−p′).

This lets us prove the following lemma.

Lemma 4.5.

Let m∈ℕ and n,p∈ℤ. Then the formula μ1⁢(n,m,p) holds if and only if n⁢m=p.

Proof.

For the rightwards direction of proof, we know already that if μ0⁢(n,m,p) holds then n⁢m=p. Given that n′⁢m=p′ and n′′⁢m=p′′, with n=n′′−n′ and p=p′′−p′, we can show by a routine computation that n⁢m=p. So the rightwards direction of proof is shown.

For the leftwards direction of proof, given that n⁢m=p, we fix m. By Corollary 4.4, we know there exists some natural tm such that [tm,∞)×{m}⊆D0. Thus we know that multiplication on pairs (n1,m) is defined by μ0 when n1>tm. So take n′=tm and n′′=tm+n, and likewise take p′=n′⁢m and p′′=n′′⁢m. It follows that μ0⁢(n′,m,p′) and μ0⁢(n′′,m,p′′) both hold, and further that n=n′′−n′ and p=p′′−p′ hold. Therefore μ1⁢(n,m,p) holds, as required. ◀

Once multiplication is defined on ℕ×ℤ is it immediate to extend it to ℤ×ℤ. Thus, by Lemma 4.5, we can define multiplication over the whole domain of ℤ×ℤ in the theory Th(ℤ;<,+,⌊f⌉). It follows that the theory Th(ℤ;<,+,⌊f⌉) is undecidable, completing the proof of Theorem 1.1.

5 Proof of the sub-linear case

We now move to prove Theorem 1.2. Recall that here we assume f grows at least as fast as xε for some ε>0 but more slowly than x. Using this, we define a function which approximates f−1⁢(x−(1/2))+(1/2). Given that the latter function is a Hardy field function which grows faster than x, we apply Theorem 1.1 and show that the theory Th(ℤ;<,+,⌊f⌉) is undecidable.

Note that throughout we use the fact that, if f is a Hardy field function, then so is f−1; we take this fact from [1, Theorem 1.7].

Proof of Theorem 1.2.

Let f:[x0,∞)→ℝ be a Hardy field function where xε≺f⁢(x) and f⁢(x)≺x both hold for some ε>0.

Define the function b(m)=min{n∈ℤ|⌊f⌉(n)≥m}, which behaves roughly like the inverse of ⌊f⌉. Formally, we define b⁢(m) in our theory as the unique value of n satisfying the formula ⌊f⌉(n)≥m∧∀k(⌊f⌉(k)≥m→k≥n).

Increasing the value of x0 if necessary, we may freely assume that f is strictly increasing. Additionally, we define the function g:[y0,∞)→ℝ by g⁢(y)=f−1⁢(y−(1/2))+(1/2), where y0 is sufficiently large for the above definition to be well-posed. The main lemma we need to prove Theorem 1.2 is the following.

Lemma 5.1.

There exists an integer m0 such that b(m)=⌊g(m)⌉ for all integers m≥m0.

Proof.

Recall that we assume that f:[x0,∞)→ℝ is a strictly increasing function. Under this assumption, the inverse f−1:[f⁢(x0),∞)→ℝ can be characterised as f−1⁢(y)=min⁡{x∈ℝ|f⁢(x)≥y}. For an integer m≥m0 and real x we have f⁢(x)≥m−1/2 if and only if ⌊f⌉(x)≥m, directly from the definition of the nearest integer function. Thus, we know that

{x∈ℝ|⌊f⌉(x)≥m} ={x∈ℝ|f⁢(x)≥m−12}
={x∈ℝ|x≥f−1⁢(m−12)}={x∈ℝ|x≥g⁢(m)−12}.

Restricting our attention to integers, we conclude that

{n∈ℤ|n≥b⁢(m)} ={n∈ℤ|⌊f(n)⌉≥m}
={n∈ℤ|n+12≥g(m)}={n∈ℤ|n≥⌊g(m)⌉}.

Thus, we have b(m)=⌊g(m)⌉, as needed. ◀

Now, g is a Hardy field function, as f−1 is. Thus, Theorem 1.1 can be applied to show the theory Th(ℤ;<,+,⌊g⌉) undecidable. We do this using the following lemma.

Lemma 5.2.

We have x≺g⁢(x)≺x1/ε.

Proof.

Increasing x0 if necessary, we may freely assume that f is strictly increasing on [x0,∞). We know that for each δ>0 there exists n0≥x0 such that for n≥n0 we have f⁢(n)<δ⁢n. Taking m0=f⁢(n0), it follows that for all m≥m0 we have f−1⁢(m)>(1/δ)⁢m. Thus, x≺f−1⁢(x) and consequently x≺g⁢(x), as needed. The proof that g⁢(x)≺x1/ε is entirely analogous. ◀

By Lemma 5.2 the theory Th(ℤ;<,+,⌊g⌉) is undecidable. Since by Lemma 5.1 we can define ⌊g⌉ in Th(ℤ;<,+,⌊f⌉), it follows that the theory Th(ℤ;<,+,⌊f⌉) is undecidable as well. This concludes the proof of Theorem 1.2. ◀

References

  • [1] Matthias Aschenbrenner and Lou van den Dries. Asymptotic differential algebra. Contemporary Mathematics, 373:49–85, 2004.
  • [2] Alexis Bès. A survey of arithmetical definability. Bull. Belg. Math. Soc. Simon Stevin, pages 1–54, 2001. A tribute to Maurice Boffa.
  • [3] Michael D. Boshernitzan. An extension of Hardy’s class l of “orders of infinity”. Journal d’Analyse Mathématique, 39(1):235–255, December 1981.
  • [4] Michael D. Boshernitzan. Uniform distribution and Hardy fields. J. Anal. Math., 62:225–240, 1994.
  • [5] J. Richard Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(1-6):66–92, 1960.
  • [6] Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345–363, 1936. Available from: http://www.jstor.org/stable/2371045.
  • [7] Nikos Frantzikinakis. Equidistribution of sparse sequences on nilmanifolds. J. Anal. Math., 109:353–395, 2009.
  • [8] Ronald L. Graham, Donald Ervin Knuth, and Oren. Patashnik. Concrete mathematics. Addison-Wesley, Reading, Mass, 1990.
  • [9] Jakub Konieczny. Decidability of extensions of presburger arithmetic by generalised polynomials, 2024.
  • [10] Jakub Konieczny and Clemens Müllner. Bracket words along Hardy field sequences. Ergodic Theory Dynam. Systems, 44(9):2621–2648, 2024.
  • [11] Ivan Korec. A list of arithmetical structures complete with respect to the first-order definability. Theoret. Comput. Sci., 257:115–151, 2001.
  • [12] Mojżesz Presburger. Über die Vollständigkeit eines gewissen systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pages 92–101, 1929.
  • [13] Florian K. Richter. Uniform distribution in nilmanifolds along functions from a hardy field. Journal d’Analyse Mathématique, 149(2):421–483, December 2022.
  • [14] A L Semenov. On certain extensions of the arithmetic of addition of natural numbers. Mathematics of the USSR-Izvestiya, 15(2):401, April 1980.
  • [15] A L Semënov. Logical theories of one-place functions on the set of natural numbers. Mathematics of the USSR-Izvestiya, 22(3):587, June 1984.
  • [16] Alfred Tarski. Undecidability of the Elementary Theory of Groups, volume 13 of Studies in Logic and the Foundations of Mathematics, pages 75–86. Elsevier, 1953.

Appendix A Omitted Proofs

In this appendix we give a proof of Lemma 4.2.

Proof of Lemma 4.2.

Decreasing ε0,ε1,ε2 if necessary (in this order), we may freely assume that ε0,ε1,ε2<1/10 and we have the inequalities:

ε1 <103⁢ε0, ε1ε2 >25ε1+5>50.

(The motivation behind these inequalities will become apparent in the course of the argument). Picking a sufficiently large value of n0 we may freely assume that there exists X0≥x1 such that f′⁢(X0)=n, f′′⁢(X0)<ε2, and f,f′,f′′ are strictly monotone on [X0,∞). Let X1,X2,X3 be specified by

f′⁢(X1) =n+15⁢ε1, f′⁢(X2) =n+25⁢ε1, f′⁢(X3) =n+35⁢ε1.

Let also N1=⌈X1⌉<X1+1 and N3=⌊X3⌋>X3−1. Note that f′⁢(X1)−f′⁢(X0)=ε1/5 and f′′⁢(x)≤f′′⁢(X0)≤ε2 for x∈[X0,X1], so the mean value theorem implies that X1−X0≥ε1/(5⁢ε2)≥10.

By the same token, we have X2−X1,X3−X2≥10, which in particular implies that N3−N1≥10 (which is not strictly speaking necessary, but ensures that all the points under consideration appear in the order we expect). For all integers N with N1≤N≤N3 we have:

N ≥x1, n+15⁢ε1 ≤f′⁢(N)≤n+35⁢ε1, 0<f′′⁢(N)≤ε2,

which implies that N satisfies three out of the four desired conditions.

It remains to show that there exists N with N1≤N≤N3 such that ‖f⁢(N)‖ℝ/ℤ<ε0. We will in fact show that for each arc A⊆ℝ/ℤ with length 2⁢ε0 there exists N with N1≤N≤N3 such that f⁢(N)mod1∈A. Consider the function f~⁢(N)=f⁢(N)−n⁢N. Since f~⁢(N)≡f⁢(N)mod1, in the previous condition we may equally well require that f~⁢(N)mod1∈A. By the mean value theorem, for N1≤N<N3, the value of the expression

f~⁢(N+1)−f~⁢(N)=f⁢(N+1)−f⁢(N)−n

belongs to the interval [15⁢ε1,35⁢ε1]. Since 3⁢ε1/5<2⁢ε0, it follows that, for each interval I of length 2⁢ε0 contained in the interval [f⁢(N1),f⁢(N3)], there exists some N with N1≤N≤N3 with f~⁢(N) intersecting I. By the mean value theorem, we have

N3−N1≥X3−X1−2 ≥f′⁢(X3)−f′⁢(X1)maxX1≤x≤X3⁡f′′⁢(x)−2
=f′⁢(X3)−f′⁢(X1)f′′⁢(X1)−2≥2⁢ε15⁢ε2−2≥10ε1.

As a consequence, using the mean value theorem yet again, we get

f⁢(N3)−f⁢(N1) ≥(N3−N1)⁢minN1≤x≤N3⁡f′⁢(x)
=(N3−N1)⁢f′⁢(N1)≥10ε1⋅ε15=2.

Thus, we can find an interval A~⊆[f⁢(N1),f⁢(N3)] such that A~mod1=A, and we can find N with N1≤N≤N3 with f~⁢(N)∈A~. This completes the argument. ◀