MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question

closed as off topic by Andy Putman, Eric Wofsey, Qiaochu Yuan, Bill Johnson, Mark Sapir Mar 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.

share|cite|improve this answer
A detailed description of the required formula (rather, of what is needed to write a detailed formula) can be seen here:… – Andrés E. Caicedo Mar 1 '13 at 3:56

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

share|cite|improve this answer

Not the answer you're looking for? Browse other questions tagged or ask your own question.