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

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

Answer 1

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.