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(;+,xx2) is undecidable, since a=bc holds iff a+a=(b+c)2b2c2 (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+3x+2, g(x)=xlogx+1x3, and h(x)=2x3/5+logx2n

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 x1/2x<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

limxf(x)x= and limxf(x)xd=0 (1)

for an integer d2. 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

limxf(x)xε= and limxf(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 f1(f(x))x, we get a function that looks similar to xlogx, 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

limxf(x)xn= and limxf(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

limxf(x)xd= and limxf(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{nnx}, and the ceiling x of x to be min{nnx}. We define the nearest integer of x to be x=x1/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{|xn||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 limxf(x)/g(x)<;

  • f(x)g(x) if limxf(x)/g(x)=0;

  • f(x)g(x) if limxf(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 xd|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 xx0 and y0, 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)+yf(x)++y1(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 td1|f(t)|td for some d. Then we have Rx,d(y)ydf(x)/xd for sufficiently large x and all 0yx. (The constant implicit in the asymptotic notation depends only on f).

Proof.

Recall that for any xx0 and y0 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)/td0 as t. Since f(d) is a Hardy field function and is eventually monotone, we have

|Rx,d(y)|ydd!|f(d)(x)|ydf(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)=n1f1(x)+n2f2(x)++nkfk(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)|/logx=, 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 xd1f(x)xd for some d3. In particular, we initially exclude the case where f(x)xd1, 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-(d1) polynomial p such that for all 0m<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 xd1f(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-(d1) Taylor polynomial and RN,d(m) is the corresponding remainder term. Assuming, as we may that N>M, for 0mM, by Proposition 2.4 we have |RN,d(m)|Mdf(N)/Nd. Since f(N)/Nd0 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-(d1) polynomial p, in the sense that for all 0m<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 0m<M we have f(N+m)>k+(1/2)>p(m) with k then f(N+m)=k+1k=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 0m<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-(d1) integer-valued polynomial p such that for all 0m<M we have |f(N+m)p(m)|<ε. Above, we require that the polynomial p should have degree exactly d1, as opposed to at most d1; this requirement will play an important role in later considerations.

Lemma 3.2.

Let f be a Hardy field function such that xd1f(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 0m<M. Recall also that the coefficients of PN,d are given by

PN,d(m)=k=0d1f(k)(N)k!mk.

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

p(m)=k=0d1f(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(d1)/(d1). For each 0kd 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)=c0f(x)+c1f(x)++cd1f(d1)(x)/(d1)! with c0,c1,,cd1 we have h(x)f(x)/x, where is the first index with c0. 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 de). In either case, we have |h(x)q(x)|1, as needed. We conclude that the sequence (f(N),f(N),,f(d1)(N)/(d1)!)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 0k<d we have:

f(k)(N)k!/ε2dMk.

Therefore, we have the estimate

|PN,d(m)p(m)|k=0d1f(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(d1)(N)/(d1)!, 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 d3. 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) Δmf: is given by

Δmf(n)=f(n+m)f(n)

and the symmetric discrete derivative fm: is given by

fm(n)=ΔmΔnf(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 r1 and integers n0,n1,,nr we write fr(n0,n1,,nr) for nrnr1n1f(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 r1 then Δmp is a polynomial with degree r1 and leading coefficient rarm. If r=0 then Δmp=0.

  2. (b)

    If r2 then mp is a polynomial with degree r1 and leading coefficient rarm. If r=0 or r=1 then mp=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 r2, Δmp and mp 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 r1 and the claim has already been proved for all r<r.

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

ar(x+m)rarxr=k=1r(rk)armkxrk,

where the right side is a degree-(r1) polynomial with leading coefficient rarm, as needed.

For brevity, we write fr(a,b) for fr(a,b,1,1,,1) whenever r1. 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 r1p(n,m)=r!arnm.

Proof.

Iterating Lemma 3.5 we see that r1p(n,m) is a polynomial function of n with degree 1 and leading coefficient r!arm. To see that all the remaining coefficients are zero, it is enough to recall that r1p(n,m) is a symmetric function of n and m, and that r1p(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 r0 and let f:[N,N+M) be a sequence such that Δ1r+1f(n)=0 for Nn<N+Mr1. Then f coincides with a polynomial of degree at most r.

Proof.

For any polynomial p of degree at most r we have Δ1r+1p=0, so we may freely replace f with fp. Applying Lagrange interpolation, we may thus assume that f(N)=f(N+1)==f(N+r)=0. Since Δ1r+1f(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 Nn<N+Mr1 then also f(n+r+1)=0. Reasoning by induction with respect to n we thus conclude that f(m)=0 for all Nm<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 1a,b,cM we can use Lemma 3.6 to express the property that ab=c as d2p(a,b)=d2p(c,1). We now put this plan into practice.

Lemma 3.8.

Let d2 and let πd(N,M) be the sentence given by

c00m<Md:Δ1d1f(N+m)=c.

Then πd(N,M) holds if and only if there exists a polynomial p with degree exactly d1 such that f(N+m)=p(m) for all 0m<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 d1 on [N,N+m). If p had degree strictly less than d1 then, by repeated application of Lemma 3.5, we would have Δ1d1f(N+m)=0c, contradicting πd(N,M). Thus, p has degree exactly d1, as needed.

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

Lemma 3.9.

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

M>max(n,m,q)N:πd(N,M)Δ1d3ΔnΔmf(N)=Δ1d2Δqf(N).

Assume that f enjoys property Pd and n,m,q1. Then, for n,m,q we have that μd(n,m,q) holds if and only if q=nm.

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 d1 such that f(N+m)=p(m) for 0m<M. The equality between the discrete derivatives in the definition of μ(n,m,q) can now more simply be expressed as d2p(n,m)=d2p(q,1). By Lemma 3.6, this implies that nm=q, as needed.

Next, suppose that q=nm. Pick M=q+1. By Pd, we can find N and a polynomial p of degree exactly d1 such that f(N+m)=p(m) for 0m<M. By Lemma 3.8, πd(N,M) holds. By Lemma 3.5, we have d2p(n,m)=(d1)!ad1nm=(d1)!ad1q=d2p(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 d3 and each Hardy field function f with xd1f(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 xd1f(x)xd for some d3. Presently, we will instead assume that f(x)xd1 (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(d1)(N)/(d1)!),

is not equidistributed modulo 1. Indeed, the top coefficient f(d1)(N)/(d1)! 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Δmrh(n)|2rε

for all integers r1 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)xd1 for some d3. 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-(d1) polynomial PN,d, in the sense that we have |f(N+m)PN,d(m)|<1/10 for all 0m<M. Recall that the leading coefficient of PN,d is f(d1)(N)/(d1)!, 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 0m<M.

Note that, since p is a polynomial of degree d1, we can apply Lemma 3.6 to it and get that d2p(n,m)=(d1)!αnm. 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

|Δ1d3ΔnΔmf(N)(d1)!αnm|2d1,

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

FN(a,b,c)=Δ1d3ΔaΔbf(N)Δ1d2Δcf(N).

The estimate obtained above implies that we have

|FN(a,b,c)(d1)!α(abc)|2d.

Fix an integer D1002d/min(1,(d1)!α). The estimate above allows us to prove the following lemma:

Lemma 3.12.

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

Proof.

For the rightwards direction of proof, first suppose that abc. Since abc is a non-zero integer, it follows that |DabDc|D. So the following equalities hold:

|FN(Da,b,Dc)| |(d1)!αD(abc)||FN(a,b,c)(d1)!α(abc)|
(d1)!αD|abc|2d(d1)!αD2d>2d.

For the leftwards direction of proof, suppose that ab=c. Then DabDc=0 as well. It follows that |FN(Da,b,Dc)|2d as required.

Note that |FN(Da,b,Dc)| 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

N0NN0:|FN(Da,b,Dc)|2d.

It follows from the preceding discussion (in particular Lemma 3.12) that μ(a,b,c) holds if and only if ab=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 xd1f(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 xf(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 0m<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 0m<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 xf(x)x2. Then there exists x1x0 such that λ(N,M,n) holds for all N,M,n satisfying the following conditions:

  1. (a)

    Nx1;

  2. (b)

    f(N)/<1/4;

  3. (c)

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

  4. (d)

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

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+12f′′(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|=|12f′′(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)mnm|<1/8. Combining this with equation (5), we get

|f(N+m)f(N)nm|<116+18<14. (6)

It remains to deal with rounding. We have

f(N+m)f(N)nm =f(N+m)f(N)nmf(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)+nmf(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 xf(x)x2. Then for any real x1x0 and ε0,ε1,ε2>0 there exists integer n0 such that for each nn0 there exists integer N satisfying the following conditions:

  1. (a)

    Nx1;

  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 nn0 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

NM>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=nm. 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 nm and nm we can define (nn)m by distributivity. To this end, define the following formula:

μ1(n,m,p) =defn,n′′,p,p′′(μ0(n,m,p)μ0(n′′,m,p′′)
n=n′′np=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 nm=p.

Proof.

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

For the leftwards direction of proof, given that nm=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=nm 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 f1(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 f1; 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)mk(f(k)mkn).

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)=f1(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 mm0.

Proof.

Recall that we assume that f:[x0,) is a strictly increasing function. Under this assumption, the inverse f1:[f(x0),) can be characterised as f1(y)=min{x|f(x)y}. For an integer mm0 and real x we have f(x)m1/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)m12}
={x|xf1(m12)}={x|xg(m)12}.

Restricting our attention to integers, we conclude that

{n|nb(m)} ={n|f(n)m}
={n|n+12g(m)}={n|ng(m)}.

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

Now, g is a Hardy field function, as f1 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 xg(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 n0x0 such that for nn0 we have f(n)<δn. Taking m0=f(n0), it follows that for all mm0 we have f1(m)>(1/δ)m. Thus, xf1(x) and consequently xg(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 X0x1 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>X31. 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 X1X0ε1/(5ε2)10.

By the same token, we have X2X1,X3X210, which in particular implies that N3N110 (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 N1NN3 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 N1NN3 such that f(N)/<ε0. We will in fact show that for each arc A/ with length 2ε0 there exists N with N1NN3 such that f(N)mod1A. Consider the function f~(N)=f(N)nN. Since f~(N)f(N)mod1, in the previous condition we may equally well require that f~(N)mod1A. By the mean value theorem, for N1N<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 N1NN3 with f~(N) intersecting I. By the mean value theorem, we have

N3N1X3X12 f(X3)f(X1)maxX1xX3f′′(x)2
=f(X3)f(X1)f′′(X1)22ε15ε2210ε1.

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

f(N3)f(N1) (N3N1)minN1xN3f(x)
=(N3N1)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 N1NN3 with f~(N)A~. This completes the argument.