Gödel, Escher, Bach: b is a power of 10. [closed]

Question

I’d like to verify if my formula correctly expresses that a number is a power of $ 10 $, using the $ \sf{TNT} $ language provided by Hofstadter in his famous book Gödel, Escher, Bach: An Eternal Golden Braid. Although Hofstadter uses ‘$ b $’ to express the desired number, I’ll use ‘$ a $’ just for the sake of clarity. I’ll use common numerals for shortening the formula. Here we go:

$$\exists b: \exists c: \exists d: \exists e: (a = 1) \\ $$ $$\lor (((\neg (b = 0) \land (a = 10 \cdot b)) \supset ((b = 10 \cdot c) \lor (b = 1))) \\ $$ $$\land (((c = d \cdot e) \land \neg \exists f:(d = 10 \cdot f)) \supset (d = 1))) $$

Answer 1

This is too long for a comment, but it seems that your formula is not correct. In fact, your formula is true in the natural numbers for any value of $a$ simply by taking $b=0$, which fulfills the clause on the second line by denying the antecedent of the implication, and also $c=d=1$ and $e=2$, which fulfills the clause on the last line also by denying the antecedent. Thus, for any value of $a$, even when it is not a power of $10$, we may find values witnessing your existential assertion, and so it does not express the desired property.

To express the property that $a$ is a power of ten in the first-order language of arithmetic (where only the ring operations $+$ and $\cdot$ are allowed), one will have to use some kind of Gödel coding of sequences, in order to encode the recursive definition of the powers of $10$. That is, you want to say something like, $a$ is a power of $10$ if and only if there is a number $r$ coding a sequence of numbers (and this is the difficult part, but it is doable using the Chinese remainder theorem or other tricks, the standard Gödel coding ideas) that starts with $1$ and multiplies by a factor of $10$ in each successive step, such that $a$ appears on the sequence.

Answer 2

You should probably read this very nice blog post by David Speyer, which concerns exactly this problem (and more importantly, the technical parts of the Gödel incompleteness theorem).