# Hofstadter's TNT: b is a power of 2 - is my formula doing what it is supposed to?

If you've read Hofstadter's Gödel, Escher, Bach, you must have come across the problem of expressing 'b is a power of 2' in Typographical Number Theory. An alternative way to say this is that every divisor of b is a multiple of 2 or equal to 1. Here's my solution:
b:~Ea:Ea':Ea'':( ((a.a')=b) AND ~(a=(a''.SS0) OR a=S0) )
It is intended to mean: no divisor of b is odd or not equal to 1. E, AND and OR are to be replaced by the appropriate signs. Is my formula OK? If not, could you tell me my mistake?

-
I spelled out the abbreviations and added links. Please take into account that others may not be as familiar with things as you are and you can save a lot of readers a lot of time by investing a little bit of time just once in spelling out abbreviations and perhaps adding links. –  joriki Jan 31 '12 at 17:30
Thank you, it seems like I have a lot to learn :) –  Rada Jan 31 '12 at 17:34
For curious readers, it appears from the Wikipedia article that "Typographical Number Theory" is just Hofstadter's cutesy name for Peano Arithmetic, expressed in standard predicate calculus. –  Henning Makholm Jan 31 '12 at 17:37
@Rashi: Nicely done! Now, can you figure out how to express that 'n is a power of 10'? (It's a shame that Hofstadter doesn't devote some time to this, as it's IMHO one of the most fundamentally important notions in Peano Arithmetic!) –  Steven Stadnicki Jan 31 '12 at 18:18
@Rashi It is an inordinately hard problem - even being able to do the powers of 2 is quite an accomplishment! Powers of 10 require an entirely new approach, and I believe any explicit formula must be inordinately long. A hint to get you started: look up the notion of a pairing function, and codes for finite sequences... –  Steven Stadnicki Jan 31 '12 at 18:38

Your idea is sound, but the particular formula you propose $$\neg\exists a:\exists a':\exists a'':( ((a\cdot a')=b) \land \neg (a=(a''\cdot SS0) \lor a=S0) )$$ does not quite express it. The problem is that the quantifier for $a''$ has too large scope -- what your formula says is that it will prevent $b$ from being a power of two if there is some even number that is different from some factor of $b$. For example, your formula claims that $2$ itself is not a power of two, because you can make $((a\cdot a')=2) \land \neg (a=(a''\cdot SS0) \lor a=S0)$ true by setting $a=2$, $a'=1$, $a''=42$. The first part is true because $2\cdot 1$ is indeed $2$, and the second (negated) part is true because it is neither the case that $2=42\cdot SS0$ nor $2=S0$.

What you want is $$\neg\exists a:\exists a':( ((a\cdot a')=b) \land \neg (\exists a'':(a=(a''\cdot SS0)) \lor a=S0) )$$ Moving the quantifier inside one negation switches the "burden of proof" -- now it says that there isn't any number that is half of $a$, rather than there is some number that isn't half of $a$.

Or perhaps more directly expressed: $$\forall c:\Big(\exists d:( c\cdot d = b )\to \big(c=S0 \lor \exists a:(c=SS0\cdot a)\big)\Big)$$

-
I'm not sure TNT has the $\rightarrow$, but this still lets you rephrase by substituting $\neg X\lor Y$ for $X\rightarrow Y$. –  Thomas Andrews Jan 31 '12 at 17:58
Yes, I stumbled upon that second formula while I was searching the internet, trying to find out if my solution was good. I can't deny it is much more straightforward and beautiful than mine, back when I was trying to solve the problem it didn't occur to me that I could use the if-then relation. As of the position of the quatnifier for a'', I am afraid I don't understand how it changes the formula. Could you please explain me? –  Rada Jan 31 '12 at 17:59
@ThomasAndrews Yes, TNT does have the ->. (Sorry, I have yet to learn how to insert mathematical symbols) –  Rada Jan 31 '12 at 18:03
@Rashi, I have tried to add some more explanation. –  Henning Makholm Jan 31 '12 at 18:08
Thank you very, very much :) Now I understand. –  Rada Jan 31 '12 at 18:22

Another approach is to phrase it as an implication: For all $a,a'$, if $b=a\cdot a'$ then $a$ is even or one. This can then be expressed as:

$$\forall a:\forall a': \neg(b=a\cdot a') \lor (a=S0) \lor (\exists a'': a = a''\cdot SS0)$$

The advantage to this formulation is that there is one fewer negative. (You need to realize that the phrase "$X$ implies $Y$" is equivalent to $\neg X \lor Y$.)

-

I think more elegant is to assert that every prime divisor is two

$$\forall a:\forall c:(((SSa \cdot SSc=b) \land (\neg\exists d: \exists e:SSd \cdot SSe=SSa)))\to (a=0))$$

-