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

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

-
–  Asaf Karagila Mar 1 '13 at 3:12

## closed as off topic by Andy Putman, Eric Wofsey, Qiaochu Yuan, Bill Johnson, Mark SapirMar 1 '13 at 3:58

Questions on MathOverflow are expected to relate to research level mathematics within the scope defined by the community. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about reopening questions here.If this question can be reworded to fit the rules in the help center, please edit the question.

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.