# 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 :) – Rashi 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? – Rashi Jan 31 '12 at 17:59
@ThomasAndrews Yes, TNT does have the ->. (Sorry, I have yet to learn how to insert mathematical symbols) – Rashi 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. – Rashi Jan 31 '12 at 18:22

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

-
I suppose SSa denotes (SS0+a). In that case, this may not hold true. – Ezhil V Jan 29 '15 at 15:46
@EzhilV: $SSa$ denotes $S(S(a))$. (One can prove $SSa=SS0+a$, but the latter is a different expression). – Henning Makholm Jan 29 '15 at 17:01
@HenningMakholm Thanks. I was not aware of that. I could not find it in Hofstadter's book. – Ezhil V Jan 30 '15 at 3:46

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 would express this as follows using the original notation: $$\forall c:\forall d: \mathtt{\sim} b=(S(Sc \cdot SS0) \cdot d)$$ Or equivalently $$\mathtt{\sim} \exists c:\exists d: b=(S(Sc \cdot SS0) \cdot d)$$ Please note that negation in the first formula applies to the whole equality and that the negation in the second formula applies to the whole formula.

From Fundamental Theorem of Arithmetic we know that power of two cannot have divisors other than two. This is exactly what we are using in the formulas above where $S(Sc \cdot SS0)$ stands for $2c+1, c>0$, i.e. any odd number greater than $1$. $Sc$ is used in $S(Sc \cdot SS0)$ in order to avoid the situation when $c=0$ and $d=b$ used in formula $S(c \cdot SS0)$ turn the equality into $b=b$ for any $b$.

These formulas detect all the powers starting from $2^0, 2^1, 2^2, \ldots$

-