First Order Logic: Formula for $y$ is the sum of non-negative powers of $2$ As the title states, is it possible to write down a first order formula that states that $y$ can be written as the sum of non-negative powers of $2$. 
I have been trying for the past hour or two to get a formula that does so (if it is possible), but It seems to not work.
Here's my attempt: 
Let $\varphi(y)$ be the formula $(\exists n < 2y)(\exists v_0 < 2)\cdots (\exists v_n < 2)(y = v_0\cdot 1 + v_1\cdot 2 + \cdots + v_n2^n)$. 
In the above, the $\mathcal{L}$-language is $\{+,\cdot, 0, s\}$ where $s$ is the successor function. But the problem with the formula above is that when $n$ is quantified existentially as less than $2y$, $n$ does not appear in $2^n$ when we write it out as products of $2$ $n$ times. I think this is the problem. 
My other attempts at this problem happen to be the same issue, where $n$ is quantified but does not appear in the statement, such as the example provided above.
If you can give me any feedback, that would be great. Thanks for your time.
Edit: I guess that when I write $2^n$, I mean $(s(s(0)))^n$.

In the natural numbers, the formula $\theta(x) \equiv x = x$ works. Think about binary notation. 
More seriously, once you have developed the machinery to quantify over finite sequences, it is not so hard to write down the formula. Let $\phi(x)$ define the set of powers of 2. The formula will look like this:
$$
(\exists \sigma)(\exists \tau)[\, (\forall n < |\sigma|)[\phi(\sigma(n))] \land |\tau| = |\sigma| + 1 \land \tau(0) = 0 \land (\forall n < |\sigma|) [ \tau(n+1) = \tau(n) + \sigma(n)] \land x =\tau(|\tau|)]
$$
