How to express “b is a power of 10” – Typographical Number Theory in Gödel Escher Bach

how do you express “b is a power of 10”.

Since Rory already covered the problems with your approach, I'll tackle the question of finding a different solution. In my first attempt to do so, I have made a mistake, so I'm completely rewriting my answer. It is now inspired by this post by Anders Kaseorg, although the wording is mine.

All powers at once

The main problem is that you can't simply write down a recursive definition. You can't have the formula build on itself. One way to tackle this is by speaking about all powers of ten, at least up to the given number, simultaneously. Lacking sets, we have to represent this as a single number. We can't do digit shifting in base 10 yet, but we can express powers of ten in some prime base.

Some nomenclature up front. I'll use $a$ to denote the free variable, the input, the thing we want to check the predicate for. $p$ will be a prime number used as number base, $t$ the base-$p$ number used to encode our powers of ten. $d$ will often be a digit or element of that set of powers of ten.

To keep things understandible, I'll define abbreviations for semantic units. But note that every such abbreviation only builds on those I have defined before, not itself or the ones coming afterwards. Therefore you could expand the abbreviations level by level to get back to the strict notation of TNT. I'll do so towards the end of this post.

Step by step

isPrime(p)

When is a number prime? If it itself is not less than $2$ and not the product of two integers greater or equal to $2$. (I write $\neg$ instead of $\sim$ for negation.)

$$\text{isPrime}(p):=\;\;\langle\exists i:p=\textsf{SS}i\;\wedge\;\neg\;\exists j:\exists k:p=\textsf{SS}j\cdot\textsf{SS}k\rangle$$

primePower(p, q)

To write digit operations in a base-$p$ number, we'll need to talk about powers of $p$. When is some $q$ a power of $p$? If $q$ is non-zero and contains no other prime factors. (I prefer to write implication as $\rightarrow$ not $\supset$.)

\begin{align*} \text{primePower}(p,q):=\;\;&\Bigl\langle\neg\;q=\textsf 0\;\wedge\\&\forall g:\forall h:\big\langle q=\textsf{SS}g\cdot\textsf{SS}h\;\rightarrow\;\langle\neg\;\text{isPrime}(\textsf{SS}g)\;\vee\;\textsf{SS}g=p\rangle\big\rangle\Bigr\rangle \end{align*}

digitOf(p, t, d)

When is $d$ a digit of a base-$p$ number $t$? If $t=(e\cdot p+d)\cdot p^k+f$ for some $e,f,k$ with $d<p$ and $f<p^k$.

\begin{align*} \text{digitOf}(p,t,d):=\;\;&\exists e:\exists f:\exists q:\big\langle \langle\exists c:p=d+\textsf{S}c\;\wedge\;\exists c:q=f+\textsf{S}c\rangle\;\wedge\\&\langle t=(e\cdot p+d)\cdot q+f\;\wedge\;\text{primePower}(p,q)\rangle\big\rangle\end{align*}

contains(p, t, d)

Having base-$p$ numbers represent sets is a beautiful idea, but one has to be careful about zeros: every integer contains an infinite number of leading zeros. But we don't want any zeros in our set of powers of ten, so we can exclude zeros.

$$\text{contains}(p, t, d):=\;\;\langle\neg\;d=0\;\wedge\;\text{digitOf}(p, t, d)\rangle$$

powersOfTen(p, t)

Now we can start talking about powers of ten. When does a base-$p$ number $t$ describe sufficiently many powers of ten? Originally I'd start this by saying it must contain $1=10^0$ and for every $d$ it must contain $10\cdot d$, and no other numbers except for these. But we'll eventually quantify this number as $\exists t$, so all requirement about what it must contain can be avoided. The only important thing is writing down what it must not contain, i.e. expressing that it should contain nothing but powers of ten. For every number it contains, there must be a lower power of ten which it also contains, with one as the obvious exception.

\begin{align*} \text{powersOfTen}(p,t):=\;\;&\forall d:\Big\langle\text{contains}(p,t,d)\;\rightarrow\;\big\langle d=\textsf{S0}\;\vee\\&\exists b:\langle d=\textsf{SSSSSSSSSS0}\cdot b\;\wedge\;\text{contains}(p,t,b)\rangle\big\rangle\Big\rangle \end{align*}

powerOfTen(a)

So when is a number a power of ten? If it contained in the powers of ten number, for some suitable prime $p$.

\begin{align*} \text{powerOfTen}(a):=\;\;&\exists p:\bigl\langle\text{isPrime}(p)\;\wedge\\& \exists t:\langle\text{powersOfTen}(p,t)\;\wedge\;\text{contains}(p,t,a)\rangle\bigr\rangle\end{align*}

We didn't require $p>a$, but the existential quantification of $t$ takes care of that. Likewise, we at no point made any statement about the order of digits inside $t$. Any order will do, and repetitions are fine as well.

The formulation is not optimized for brevity. Instead, I tried to make each definition capture a mathematical idea as precisely as possible, even if that meant covering corner cases which are irrelevant for the application at hand. For example, if in the $\text{digitOf}$ formulation I had written $\textsf Sq$ for $p^k$ instead of $q$, then the case of $q=0$ in $\text{primePower}$ would become irrelevant.

All together

If you plug everything together, you get the following pretty unreadable expression:

$$ \exists p:\langle \\ \langle\exists i:p=\textsf{SS}i\;\wedge\;\neg\;\exists j:\exists k:p=\textsf{SS}j\cdot\textsf{SS}k\rangle \\ \;\wedge\;\exists t:\langle \forall d:\langle \\ \langle\neg\;d=0\;\wedge\; \\ \exists e:\exists f:\exists q:\langle\langle\exists c:p=d+\textsf Sc\;\wedge\;\exists c:q=f+\textsf Sc\rangle\;\wedge\;\langle t=(e\cdot p+d)\cdot q+f\;\wedge\; \\ \langle\neg\;q=\textsf 0\;\wedge\;\forall g:\forall h:\langle q=\textsf{SS}g\cdot\textsf{SS}h\;\rightarrow\;\langle\neg\; \\ \langle\exists i:\textsf{SS}g=\textsf{SS}i\;\wedge\;\neg\;\exists j:\exists k:\textsf{SS}g=\textsf{SS}j\cdot\textsf{SS}k\rangle \\ \;\vee\;\textsf{SS}g=p\rangle\rangle\rangle \rangle\rangle \rangle \\ \;\rightarrow\;\langle d=\textsf{S0}\;\vee\;\exists b:\langle d=\textsf{SSSSSSSSSS0}\cdot b\;\wedge\; \\ \langle\neg\;b=0\;\wedge\; \\ \exists e:\exists f:\exists q:\langle\langle\exists c:p=b+\textsf Sc\;\wedge\;\exists c:q=f+\textsf Sc\rangle\;\wedge\;\langle t=(e\cdot p+b)\cdot q+f\;\wedge\; \\ \langle\neg\;q=\textsf 0\;\wedge\;\forall g:\forall h:\langle q=\textsf{SS}g\cdot\textsf{SS}h\;\rightarrow\;\langle\neg\; \\ \langle\exists i:\textsf{SS}g=\textsf{SS}i\;\wedge\;\neg\;\exists j:\exists k:\textsf{SS}g=\textsf{SS}j\cdot\textsf{SS}k\rangle \\ \;\vee\;\textsf{SS}g=p\rangle\rangle\rangle \rangle\rangle \rangle \rangle\rangle\rangle \\ \;\wedge\; \langle\neg\;a=0\;\wedge\; \\ \exists e:\exists f:\exists q:\langle\langle\exists c:p=a+\textsf Sc\;\wedge\;\exists c:q=f+\textsf Sc\rangle\;\wedge\;\langle t=(e\cdot p+a)\cdot q+f\;\wedge\; \\ \langle\neg\;q=\textsf 0\;\wedge\;\forall g:\forall h:\langle q=\textsf{SS}g\cdot\textsf{SS}h\;\rightarrow\;\langle\neg\; \\ \langle\exists i:\textsf{SS}g=\textsf{SS}i\;\wedge\;\neg\;\exists j:\exists k:\textsf{SS}g=\textsf{SS}j\cdot\textsf{SS}k\rangle \\ \;\vee\;\textsf{SS}g=p\rangle\rangle\rangle \rangle\rangle \rangle \rangle\rangle $$

If you look closely, you can recognize three similar block, corresponding to the three $\text{contains}$ instances. That might help you find your bearings.

Alternatives

The above is one possible formulation, but there are many others. The post by Anders Kaseorg formulated $\text{primePower}$ not in terms of “every prime factor must be equal to $p$” but instead “every factor must be divisible by $p$”. In the expanded form this is certainly shorter, but since my formulation is what first came to my mind, I'll keep it the way it is.

Instead of writing $t$ as a set of all powers of ten, one could also make it a sequence of such powers. In that case you'd say that every pair of subsequent digits has a power of ten between them. But since we still need the $\text{contains}$ predicate to eventually check whether $a$ is contained, working exclusively on sets makes things simpler.

How is exponentiation defined in Peano arithmetic? is a more general variant of this question here. The answers there don't use base-$p$ numbers, but instead the Chinese remainder theorem to express a sequence in a single number. The great benefit there is that the index into the sequence is only a factor in some product in the accompanying formulas. In my approach, it's the exponent of the prime, so I need extra predicates to formulate that. So indexing is easier with the Chinese remainder theorem. On the other hand, seeing how the data is stored in the number is harder. Even if you're rationally perfectly convinced that the theorem works as advertised, I still think it's harder to establish a kind of gut understanding for how the single number (or rather pair of numbers, in my case $t$ and $p$) represents a sequence. That's the reason I prefer the base-$p$ numbers. Their approach is however better suited if you not only want to establish that $a$ is a power of ten, but also characterize the exponent, like check whether $a=10^b$ for $a,b$ given as free variables. The use of a sequence with easy indexing pays off in that setup.

Another common tool to represent sequences as single numbers is by using a pairing function to denote the sequence. The first element of the pair would be an element of the list, the second the remaining list except for that first element. But this is a recursive data structure, and we had enough trouble expressing the simpler recursive concepts above, so I'd not follow that approach here. The same goes for the idea of representing a set by writing down as many distinct primes as the set has elements, and then using the set elements as exponents for the primes. To decode this, you again have to not only recognize powers of primes, but also to identify the exponent. Once you can express such things, the answer to this problem here is a pretty trivial application of that.

You should spell out your abbreviations, since they are not universal. I assume you mean "Typographical Number Theory" in the book "Gödel, Escher, Bach" by Douglas R. Hofstadter.

Your TNT statement is wrong. First, you want your formula to be about $d$, but you bound $d$ in an existence quantifier. So, remove the $\exists d:$ to get a statement about $d$.

Also, your formula just says that $a=2$, $b=5$, $c$ is a natural number, and the equation basically says $d=10c^2$.

I also worked on this problem a bit when I read (the first half of) Gödel, Escher, Bach, and the answer will be much more complicated than you have set out here. I got some ideas but I never finished the answer: too much time involved. I never even got to the second half of the book!

ADDED

If I recall correctly, I was able to get a statement for "b is a power of 2" by saying something like "2 is the only prime divisor of b," and similarly for "b is a power of 5." I could then say "b is a power of 2 times a power of 5" but I never did find a way to ensure that the exponents of 2 and of 5 are the same.

Step 1: We can encode any finite sequence in just a few numbers

Any finite sequence $a_0,a_2,\ldots,a_n$ of (natural) numbers can be encoded as a predicate $$\begin{align}P(x,k,\alpha,\beta,n)&\iff x\text{ is the $k$th term of thes given equence $a_0,\ldots,a_n$}\\&\iff k\le n\land x=\alpha\bmod{((k+1)\beta+1)}\\&\iff\exists t\colon n=k+t\land \exists t\colon \alpha\cdot x+t\cdot S(\beta\cdot Sk)\land \exists t\colon x+t=\beta\cdot Sk\end{align}$$ where the existence of suitable $\alpha,\beta$ is guaranteed by the Chinese Remainder Theorem. All we need is that the numbers $\beta+1,2\beta+1,\ldots,(n+1)\beta+1$ are coprime and $>a_k$, which can be achieved by letting $\beta$ a multiple of $(n+1)!$.

Example: $\alpha=1981297324554360860$, $\beta=2016$ can be used to encode (any inital seqgment of) the sequence $1,10,100,1000,10000,7101,6944,15819,\ldots$; especially, the first few terms happen to coincide with the first few powers of ten.

Step 2: We can talk about recursive sequences by using finite sequences

Assume we define a sequence by its initial term $a_0$ and a recursion $a_n=f(a_{n-1})$ (where we can express $f$ in TNT). Then we can encode the property that $x$ equals $a_n$ as $$\begin{align}R(x,n)\iff\exists \alpha\exists\beta\colon &\quad P(a_0,0,\alpha,\beta,n)\\&\land P(x,n,\alpha,\beta,n)\\&\land\forall k\forall y\colon\bigl(( k<n\land P(y,k,\alpha,\beta,n))\to P(f(y),Sk,\alpha,\beta,n)\bigr)\\ \end{align}$$

Example: If $f(y)=10\cdot y$ and $a_0=1$, then the numbers $\alpha,\beta$ from the previous example make the statement $R(10000,4)$ true.

Step 3: We can encode "$b$ is a power of $10$"

This is just $$\exists n\colon R(b,n) $$ where $R$ is defined as in step 2 using $f(y)=10y$ and $a_0=1$.

Exercise: Recognize the methods of the two steps just described in the following:

∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉