Let $L_P = \{+, \geq; 0, 1\} $.
The first-order theory of $\mathbb{N}$ in the language $L = L_P \cup \{exp_2\}$, where $exp_2$ the function which sends a natural number $n$ to $2^n$, is decidable.
Show that there is an algorithm which, given any diophantine equation $f(x) = 0$ ($x$ is a tuple of $m$ variables and $f$ a polynomial in $x$ over $\mathbb{Z}$), decides whether that has or does not have solutions in the set $\{2^n: n \in N\}^m$.
To sho this we have to reduce the one problem to the other, right?
Could you give me some hints for the reduction?
Here is a possible sketch for a proof.
Step 1. Rewrite the diophantine equation $f(x) = 0$ as $f_+(x) = f_-(x)$, where the coefficients of $f_+$ and $f_-$ are all in $\mathbb{N}$.
Step 2. Rewrite each monomial $c_{r_1, \dotsm, r_k}x_1^{r_1} \dotsm x_k^{r_k}$ of $f_+$ and $f_-$ as a sum of monomial with coefficients $1$ (for instance $3x_1^2x_3 = x_1^2x_3 + x_1^2x_3 + x_1^2x_3$).
Step 3. Observe that if $m(x_1, \dotsm, x_r) = x_1^{r_1} \dotsm x_k^{r_k}$, then $$m(2^{n_1}, \dotsm, 2^{n_k}) = 2^{r_1n_1 + \dotsm + r_kn_k} = 2^{\overbrace{n_1 + \dotsm + n_1}^{r_1 times}\ + \ \dotsm\ + \ \overbrace{n_k + \dotsm + n_k}^{r_k times} } $$ You can now express the fact that the diophantine equation $f(x) = 0$ has a solution in the set of powers of $2$ by a first order formula involving only $+$ and $\exp_2$.