Some notes on Hofstadter’s Typographical Number Theory

Standard

In Godel, Escher, Bach: An Eternal Golden Braid, Douglas Hofstadter outlines his axiomatic “Typographical Number Theory” and sets certain problems for the reader – one is to show that b (a variable) is a power of 2.

These are my notes in trying to demonstrate this (hopefully understandable to anyone who knows a bit of symbolic logic and has a passing knowledge of Peano’s axioms.

My reasoning runs like this: if a number is a power of two then it has no prime factors other than 2 (and 1, if we count that as a prime) – see the earlier entry on the fundamental theorem of arithmetic.

A prime (a) in TNT:

\exists a: \sim \exists a^{\prime}: \sim \exists a^{\prime\prime}: < a^{\prime}.a^{\prime\prime}=a \wedge \sim a^{\prime} = 0 \wedge \sim a^{\prime} = S0 \wedge \sim a^{\prime\prime} = 0 \wedge \sim a^{\prime\prime} = S0>

First Update: Now realise there is a simpler way of stating a prime in TNT – namely that there is no two numbers bigger than one the product of which is the number we seek:

\exists a: \sim \exists a^{\prime}: \exists a^{\prime\prime}: SSa^{\prime}.SSa^{\prime\prime} = a

Second update:

So, we have a definition for a prime, a, and we can set  a to a prime other than 2.

\exists d: \exists a: \sim \exists a^{\prime}: \exists a^{\prime\prime}: <SSa^{\prime}.SSa^{\prime\prime} = a \wedge \sim a = SS0>

Then

\exists b: \exists c: \sim \exists a: \sim \exists a^{\prime}: \exists a^{\prime\prime}: <SSa^{\prime}.SSa^{\prime\prime} = a \wedge \sim a = SS0 \wedge \sim b = a.c>

I think this is a sufficient definition for “b is a power of 2”, as we know that all numbers are products of primes and we have ruled out any prime other 2 being a factor of b. Is that right?

On further thought I don’t think that’s enough, because we need to specify that b is a multiple of 2.

So what about this?

\exists b: \exists c: \exists d: \sim \exists a: \sim \exists a^{\prime}: \exists a^{\prime\prime}: <SSa^{\prime}.SSa^{\prime\prime} = a \wedge \sim a = SS0 \wedge \sim b = a.c \wedge b = SS0.d>

So has that nailed it?