Gödel, Escher, Bach: $b$ is a power of $10$.

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 a: \exists b: \exists c: \exists d: \exists e: \neg \exists f: (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 (d = 10 \cdot f)) \supset (d = 1)))$$

-
why are you existentially quantifying b, if you are trying to write a prediate about b? (and I guess you meant a) –  user58512 Feb 26 '13 at 15:11
@Sean I disagree; I think the question is clear: Does the given formula correctly express the property of being a power of 10? –  MJD Feb 26 '13 at 16:40
More clever, I'd say, not necessarily more advanced. What I think of as the standard solution, which I wrote up in the first part of this blogpost sbseminar.wordpress.com/2009/12/07/… , uses nothing beyond the Chinese Remainder Theorem. –  David Speyer Feb 26 '13 at 17:04
Is it correct to say that you can easily define $a$ is a power of $p$ by $$\forall x,y, \exists z, a = xy \to (x = pz \wedge x=1)$$ but for composite numbers things are much more difficult? –  user58512 Feb 26 '13 at 17:13
@user58512 There is an easy solution for $p$ prime, and things are much more difficult for composite numbers. I think your formula might have some typos. –  David Speyer Feb 26 '13 at 17:19

As user58512 says, I think you are trying to write a sentence for "$a$ is a power of $10$", which means you don't want an $\exists a$ at the front. In the following, I'll take the liberty of making things more readable by replacing $\supset$ with $\implies$, using $( \ )$ instead of $< \ >$ and using $\neq$.

Your sentence doesn't work. I will show that it is true for $a=20$. Take $b = 2$ and take $c$, $d$ and $e$ to be anything. Then your sentence reads

$\neg \exists f : 20=1 \vee [ (( 2 \neq 0 \wedge 20=10 \cdot 2 ) \implies (2=10 \cdot c \vee 2=1) ) \wedge \ldots]$

I can stop right there without expanding the rest. Indeed, there is no such $f$. The equality $20=1$ is false. The two conditions in the hypothesis of the implication are true; the two conditions in the conclusion of the implication are false. So we have

$\neg \exists f: FALSE \vee [ (TRUE \implies FALSE) \wedge \ldots]$

Indeed, there is no $f$ which can make this true.

Unfortunately, your sentence is garbled enough that I can't tell what you intended to write. I don't think there is any solution as short you are attempting.

Let me suggest trying to paraphrase your sentence in English first, and moving your quantifiers ($\exists$ and $\forall$) as close as possible (but not closer!) to the things they are meant to quantify. That might make the level of minor errors low enough that we could see what you are trying to do.

-
For those who are interested in the "how I found this", I rewrote the portion inside the quantifiers into DNF en.wikipedia.org/wiki/Disjunctive_normal_form. So the sentence wound up looking like $\cdots \neg \exists_f (A \vee B \vee C \vee D) \wedge (E \vee F \vee G \vee H)$. It was easy to choose $(b,c,d,e)$ so that $A$, $B$, $C$ and $D$ were all false: they didn't even have $f$ in them! Although DNF is much worse than a good attempt to write a clean statement, I find it is often better than a student's haphazard attempt. –  David Speyer Feb 26 '13 at 16:50