# Theory of addition and a predicate that recognizes powers of 2

What is the complexity of the theory of addition (Presburger arithmetic) augmented by a unary predicate that recognizes powers of 2?

-
Hi David. Are you familiar with the work of Richard? It is not exactly on Presburger arithmetic, so it may not be relevant. In any case: Denis Richard, "All arithmetical sets of powers of primes are first-order definable in terms of the successor function and the coprimeness predicate", Special volume on ordered sets and their applications (L'Arbresle, 1982), Discrete Math. 53 (1985), 221–247. –  Andrés Caicedo Jan 18 '11 at 20:51

The theory of the natural numbers with addition and $x\mapsto 2^x$ is decidable. One reference is the Cherlin-Point paper "On extensions of Presburger arithmetic". It can be found on Francoise Point's webpage:

http://www.logique.jussieu.fr/~point/papiers/cherlin_point86.pdf

-
Dave: How do you get around the fact that $\times$ is definable? –  Andrés Caicedo Jan 19 '11 at 3:51
@Andres et al. I made silly mistake writing the preamble to my question. But Dave Marker's answer corrects my mistake and answers my question. Thanks!! –  David Feldman Jan 19 '11 at 3:58
I've edited my mistake out of the question now! (One could define multiplication if one had $2^{(\cdot)}$ and $a^{(\cdot)}$ provided $a$ equals a power of $2$.) –  David Feldman Jan 19 '11 at 4:05
Oh! Of course. @Dave: Thanks for the reference. –  Andrés Caicedo Jan 19 '11 at 4:23
And thanks Andres for also for your reference, but I haven't chased it down yet. –  David Feldman Jan 19 '11 at 5:04