## 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. – Andres Caicedo Jan 18 2011 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:
 Dave: How do you get around the fact that $\times$ is definable? – Andres Caicedo Jan 19 2011 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 2011 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 2011 at 4:05 Oh! Of course. @Dave: Thanks for the reference. – Andres Caicedo Jan 19 2011 at 4:23 And thanks Andres for also for your reference, but I haven't chased it down yet. – David Feldman Jan 19 2011 at 5:04