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?
 A: 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))
$$
A: Henning, above, got the correct way to phrase your answer.
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$.)
A: 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)$$
A: 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$ 
