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

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?

• Büchi arithmetic is not quite the same, but you can find a lot of information there. Commented Oct 19, 2022 at 16:17
• I am curious about the history of how this mistake got corrected into Büchi arithmetic, but I'm more interested in the specific case of various unary predicates; this is what Büchi is interested in in "Weak Second-Order Arithmetic and Finite Automata". Commented Oct 19, 2022 at 18:37
• I just found A. L. Semenov's "On Certain Extensions of the Arithmetic of Addition of Natural Numbers" (1980), which seems to address this exact question. I'll answer my own question if I can make sense of it. Commented Oct 24, 2022 at 20:34

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.