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$.

Food4Thought
  • 43
  • 7
  • 1
    It is well known that the exponential formula is first order definable in the (standard) natural numbers (with the language you have stated in the question), you can find this on any book about Peano arithmetic or Gödel incompletenes theorem. However, for your particular question you do not need this (at least if you are thinking in the standard model), because all natural numbers are the sum of non-negative powers of 2. – boumol Apr 14 '13 at 11:26
  • Since exponentiation is not part of your langugae, you should start with the (still quite easy) task to formalize "$a$ is a power of two" as $\forall x\forall y\colon ssx\cdot y=a\to \exists z\colon ssx=z+z$ (at least if we have the Peano axioms at hand) – Hagen von Eitzen Apr 14 '13 at 11:27
  • @boumol: I guess if we are considering a standard model, then $\varphi(y)$ would be a first-order formula asserting that every positive integer has a unique binary expansion. – Food4Thought Apr 14 '13 at 11:35
  • @HagenvonEitzen: I'm not seeing the big picture as to why we need to formulize the formula "$a$ is a power of two". Is it because we want to have exponentiation in our language? – Food4Thought Apr 14 '13 at 11:39

1 Answers1

1

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|)] $$

Carl Mummert
  • 81,604
  • I had half a mind posting this answer myself. – Asaf Karagila Apr 14 '13 at 12:37
  • It is a question of whether we want a formula that defines the set of numbers that can be written that way, or if we want a formula that really says that the number is a sum of powers of two. For the latter, the solution is to first go through the the machinery to allow for quantification over finite sequences. With that in place it is relatively straightforward to formalize "there is a sequence of powers of 2 whose sum is $x$". – Carl Mummert Apr 14 '13 at 12:40
  • Ah, thanks for the comment on both formulas. The latter one was what I was more interested in. It seems that in a standard model (correct me if I'm wrong), quantifying over a variable which specifies exponentiation, e.g. $\phi(x) \equiv \exists n (2^n = x)$, works, but in other models, there may be problems with this formula. Thanks again. – Food4Thought Apr 14 '13 at 13:08
  • @Food4Thought: I think you are not getting the point of Carl's remark. When you say "$\exists n (2^n = x)$", how do you pretend to write this formula (and so with a fixed number of symbols) just using the vocabulary $+,\cdot,0,s$ ? Is this a formula? – boumol Apr 14 '13 at 13:23
  • @boumol: I guess I am not getting the point then. I'll take another stab at maybe what his point is. We need to define a specific sequence, which is essentially a map from the natural numbers to the powers of two. This takes care of having exponentiation as you mentioned in your first post above, boumol. I guess that "$\exists n (2^n = x)$" cannot possibly be written as a formula in the language $+, \cdot, 0 ,s$. Thus, we need to have exponentiation in our language to write the formula "$\exists n(2^n=x)$", but this can be defined, as you mentioned in your first post, in the standard model. – Food4Thought Apr 14 '13 at 17:25