# 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 '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:
Dave: How do you get around the fact that $\times$ is definable? –  Andres Caicedo Jan 19 '11 at 3:51
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