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

Question

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?

Answer 1

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

Answer 2

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

Answer 3

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