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