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

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

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