What is known about first order logic of $\mathbb{N}$ with + and a unary predicate?

Question

In "Weak Second-Order Arithmetic and Finite Automata", Büchi claims that the first order theory of $\mathbb{N}$ with + and a predicate for recognizing powers of 2 ($Pw_2$) is expressively equivalent to the weak monadic second order theory of $\mathbb{N}$ with successor via the translation $\sum_{i \in X} 2^i \leftrightarrow X$.

His proof, however, is wrong. Büchi claims that: $$E(x,y): Pw_2(x) \wedge \exists u, v: [(y=u+x+v) \wedge (u < v) \wedge [v = 0 \vee 2x \leq v]]$$ is an expression of "$x$ occurs in the representation of $y$ as a sum of powers of 2".

Büchi then goes on to speculate on the expressive power of the first order theory of $\mathbb{N}$ with + and a unary predicate $P$, bringing in a result from Putnam's "Decidability and Essential Undecidability" that if $P$ is "is a square", then the theory is undecidable.

I'm very curious about the case where $P$ is "is a power of 2": is Büchi's theorem false or just proved incorrectly?

But I'm also curious about the general case. Have there been any breakthroughs on this problem since Büchi's time? Is there some unary predicate $P$ that does make this first order logic expressively equivalent to the regular languages?

Answer 1

We have results on two sides.

Languages with addition and exponential functions are weak.

The first order theory of $\mathbb{N}$ with addition and the function $x\to 2^x$ admits quantifier elimination in the language expanded to include $0$, $1$, $x \le y$, $\max(x-y,0)$, and a predicate for each $n$ expressing divisibility by $n$. This is explained in a paper of Cherlin and Point, also referred to in this answer. So neither that language nor the language replacing exponentiation with $Pw_2$ can define all regular sets.

Languages with addition and polynomial functions are strong.

For any polynomial, the language with addition and a predicate for that polynomial's range is strong enough to define any arithmetic set.

I don't have a reference at hand, but the idea is that if we can recognize the range of a polynomial of degree $n$, we can also recognize the differences of its consecutive values, which are the range of a polynomial of degree $n-1$, so we will be able to recognize the range of some quadratic. If that quadratic is $ax^2+bx+c$, then we can implicitly define $Q(y)=ay^2+by+c$ as the unique element of the quadratic's range which differs from the next element by $(2y+1)+\cdots+(2y+1)+b$, with $a$ additions of $2y+1$. Finally we can implicitly define $x$ times $y$ as the unique $xy$ for which $$Q(x+y)+c=Q(x)+Q(y)+xy+\cdots+xy$$ now with $2a$ additions of $xy$. From this we can define all the arithmetic sets.

Other functions and languages

Contrary to what I originally thought, we can't conclude much just from the growth rate of a function.

• The function given by $f(x^2+y)=3^{x^2}2^y$ for any $0\le y\le 2x$ is superpolynomial (and increasing). Since $z$ is a square iff $f(z)$ is odd, the language $(+,f)$ allows defining all the arithmetic sets.
• The function $g(x)=x+\lfloor \log_2(x)\rfloor$ is polynomially bounded, but $(+,g)$ has the same limited expressive power as $(+,2^x)$.

Maybe there will be a simple function which gets exactly the regular sets, but it won't be polynomial or exponential.