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