Is this a proper rendering for "$b$ is a power of 2" using TNT from Gödel, Escher, Bach

Question

In the book "Gödel, Escher, Bach" by Hofstadter introduces the system of "Typographical Number Theory". One of the exercises is to write 'b is a power of 2', I ended up coming up with the following $<(a \cdot c)=b \supset \exists a':(SS0 \cdot a')=a \land \exists c': (SS0 \cdot c')=c>$ My interpretation into English of the phrase is "$a$ and $c$ being factors of $b$ implies that both and $a$ and $c$ are even" which I believe only holds true for $b$ that are powers of 2. Is this a valid way of writing 'b is a power of 2' in the system, and if it is/isn't how can I be sure.

Answer 1

Your formula doesn't quite work as written, because every number has $1$ as a factor. For example, $8$ is a power of $2$, but we have $1\cdot 8 = 8$, and $1$ is not even.

But the basic idea is correct. You can express "$b$ is a power of $2$" by "every factor of $b$ except for $1$ is even". I would write this as follows: $$\forall a\, ((\exists c\, a\cdot c = b) \rightarrow (a = S0 \lor \exists d\, (a = SS0\cdot d)))$$

I'm not sure my notation matches Hofstadter's (for example I strongly prefer $\rightarrow$ to $\supset$ as a symbol for implication), but I trust you can make the notational adjustments necessary to translate my formula into a formula of TNT.

---

In the comments, you write "How can I be certain that there does not exist some spooky counter example?". You can be certain by proving it!

Suppose $n$ is a natural number. We want to prove that $n$ is a power of $2$ if and only if every factor of $n$ is either even or equal to $1$.

If $n$ is a power of $2$, then by uniqueness of prime factorization, the only prime number dividing $n$ is $2$. If $n$ has an odd factor $m$ with $m\neq 1$, then $m$ has an odd prime factor $p$, which is also an odd prime factor of $n$, contradiction.

Conversely, if every factor of $n$ is either even or equal to $1$, then since $1$ is not prime and $2$ is the only even prime, the only prime number appearing in the prime factorization of $n$ is $2$, so $n$ is a power of $2$.

Answer 2

Make sure to universally quantify the $a$ and $c$. And yes, then your formula works since then it implies that $b$ has no factors other than $2$