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?