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?

  • 1
    $\begingroup$ Büchi arithmetic is not quite the same, but you can find a lot of information there. $\endgroup$ Commented Oct 19, 2022 at 16:17
  • $\begingroup$ 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". $\endgroup$
    – TomKern
    Commented Oct 19, 2022 at 18:37
  • 1
    $\begingroup$ 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. $\endgroup$
    – TomKern
    Commented Oct 24, 2022 at 20:34

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.