By formalizing a theory of numbers we can gain insight into computation
and logic. Hofstadter's TNT is one formalization of number theory worth
studying.

Hofstadter's Typographical Number Theory (TNT) is a formalization of the natural numbers (0, 1, 2, 3, ...) and addition and multiplication.

It can formalize statements such as:

- 22 is prime.
- Every number is the sum of three distinct numbers.
- 2 is not a square.
- 101 is odd.
- 3 evenly divides 27.
- 1729 is the sum of two cubes.
- There are infinitely many prime numbers.
- Every prime is the sum of two even numbers and 1.
- Different numbers have different successors.
- Exactly three numbers are equal to their own square.
- If
`a`

+`b`

= 50, then a < 50. - Exactly two numbers are less than 4.
`b`

is a power of 2.- Every even number is the sum of two primes.
- The factorial of 5 is 120.

Some of the preceding statements may be false. I never claimed that they were true; I only claimed that TNT could express them.

The symbols are:

0 S a b c d e ' ( ) + • = < > ~ ∧ ∨ ⊃ ∃ ∀ : [ ]

The set of **formulae**, also known as **well-formed strings**, is defined
recursively as follows, with `n` ranging over numerals, `u` and `v` over
variables, `r`, `s` and `t` over terms, and `A` and `B`
over formulae:

Numeral ::= 0 | SnVariable ::= a | b | c | d | e |v' Term ::=n|v| St| (s+t) | (s•t) Formula ::=s=t| ~A| <A∧B> (no var free in one ofAorBand bound in the other) | <A∨B> (no var free in one ofAorBand bound in the other) | <A⊃B> (no var free in one ofAorBand bound in the other) | ∃v:A(vfree inA) | ∀v:A(vfree inA)

The restrictions above aren't technically necessary (and in fact not all formulations of number theory bother with them), but they do simplify certain things and they don't hurt.

The rules of TNT include all rules of the Propositional Calculus plus the following:

- Axiom 1:
`∀a:~Sa=0`

- Axiom 2:
`∀a:(a+0)=a`

- Axiom 3:
`∀a:∀b:(a+Sb)=S(a+b)`

- Axiom 4:
`∀a:(a•0)=0`

- Axiom 5:
`∀a:∀b:(a•Sb)=((a•b)+a)`

- Rule of Specification: If
`∀`

is a theorem then so are`u`:`A``A`and

provided`A`{`t`/`u`}`t`contains no variables that are bound in`A` - Rule of Generalization: If
`A`is a theorem in which`u`is free, then so is`∀`

, provided`u`:`A``u`is not free in the premise of any fantasy containing`A` - Rule of Interchange: The
strings
`∀`

and`u`:~`~∃`

are interchangeable anywhere inside a theorem to produce a new theorem`u`: - Symmetry of Equality: If

is a theorem then so is`s`=`t``t`=`s` - Transitivity of Equality: If

and`r`=`s`

are theorems then so is`s`=`t``r`=`t` - Add S: If

is a theorem then so is`r`=`t``S`

`r`=S`t` - Drop S: If
`S`

is a theorem then so is`r`=S`t``r`=`t` - Rule of Induction: If

and`A`{0/`u`}`∀`

are both theorems, then so is`u`:<`A`⊃`A`{S`u`/`u`}>`∀`

`u`:`A`

The notation

denotes the
formula made from replacing all free occurrences of variable `A`{`t`/`u`}`u` with
term `t` in formula `A`. For example:

<r∨t>⊃<∃r:(Sr=t)∧r>{(SSS0+0)/r}

denotes

<(SSS0+0)∨t>⊃<∃r:(Sr=t)∧(SSS0+0)>

Of course, in Hofstadter's TNT, you wouldn't really have a variable that was free in part of a formula and bound in another, so "all free occurrences" is really more of an all or nothing kind of thing.

We'll give only the interpretation of the symbols here. For a formal semantics, you can consult books on mathematical logic.

`0`

zero`S`

successor`=`

numeric equals`+`

addition`•`

multiplication`∃`

there exists`∀`

for all

It takes some experience to encode mathematical thoughts in TNT. Here are a few examples to get you started. Make sure to practice at home (just like you practice your musical instruments, dance, and martial arts).

Be aware of how we introduce "for all" or "for every" or "there exists," and how
"is" means equals, and lots of other tricks. Note how `⊃`

naturally
goes with `∀`

and how `∧`

naturally goes with
`∃`

.

- 0 is not the successor of any number.
- For all numbers
`a`, 0 is not the successor of`a`. - For all numbers
`a`, it is not the case that 0 is the successor of`a`. `∀a:~0=Sa`

- 5 is not a square.
- There does not exist a number
`a`such that`a`times`a`equals 5. - It is not the case that there exists a number
`a`such that`a`times`a`equals 5. `~∃a:(a•a)=SSSSS0`

- 7 is odd.
- There exists a number
`a`such that 2 times`a`plus 1 equals 7. `∃a:((SS0•a)+1)=SSSSSSS0`

- Different numbers have different successors.
- For all numbers
`a`and`b`, if`a`and`b`are different, then so are the successor of`a`and the successor of`b`. `∀a:∀b:<~a=b⊃~Sa=Sb>`

- 8 is greater than 3.
- There exists a nonzero number
`b`such that 8 equals 3 plus`b`. - There exists a number
`a`such that 8 equals 3 plus the successor of`a`. `∃a:SSSSSSSS0=(SSS0+Sa)`

- 11 is prime.
- There do not exist numbers
`c`and`d`, both greater than 1, such that`c`time`d`equals 11. `~∃a:∃b:(SSa•SSb)=SSSSSSSSSSS0`

- Some prime numbers are even.
- There exists a prime number which is even.
- There exists a number that is both prime and even.
`∃a:<∃b:(b•SS0)=a∧~∃c:∃d:(SSc•SSd)=a>`

- There are infinitely many primes.
- For every number
`a`, there exists a number, greater than`a`, that is prime. `∀a:∃b:~∃c∃d:(a+Sb)=(SSc•SSd)`

- The square root of 2 is irrational.
- There are no two numbers
`a`and`b`, such that the square root of`a`^{2}over`b`^{2}is equal to the square root of 2. - There are no two numbers
`a`and`b`, such that`a`^{2}over`b`^{2}is equal to 2. - There are no two numbers
`a`and`b`, such that`a`^{2}equals 2 times`b`^{2}. - For all numbers
`a`and`b`, if`a`^{2}equals twice`b`^{2}, then`a`equals 0. `∀a:∀b:<((a•a)=SS0•(b•b))⊃a=0>`

`b`is a power of 2.`b`> 0 and all divisors of`b`are either 1 or even.`<~b=0 ∧∀a:<∃c:(a•Sc)=b⊃<a=S0∨∃d:a=(Sd+Sd)>>>`

When doing a specification, you cannot substitute a term containing bound variables in
the target formula because of the chance they would get **captured**. For example,
given the theorem:

∀a:∃b:b=Sa

it is harmless to do specification by substituting `SS0`

for `a` (Try it!),
but you **cannot** specify by substituting `b`

for `a`, because the
`b`

will get captured:

∃b:b=Sb -- NOOOOOOOO!

We use generalization to put back a universal quantifer after specialization. For example:

∀a:∀b:(a+Sb)=S(a+b) -- axiom 3 ∀b:(Sa+Sb)=S(Sa+b) -- specification (Sa for a) ∀a:∀b:(Sa+Sb)=S(Sa+b) -- generalization

However, if you generalize over a variable that is free in the premise of a fantasy, you can get into trouble:

[ a=0 -- assumption ∀a:a=0 -- generalization (ILLEGAL) Sa=0 -- specification ] <a=0⊃Sa=0> -- fantasy (AAAAAARRRRRRGGGGGH!)

This is not going to go well.

TNT is sound, but not complete nor decidable. Gödel is famous for showing this.

Here are some interesting points about TNT covered in GEB:

- TNT seems to be "as strong as it gets." Adding (reasonable) new axioms and inference rules doesn't change the set of theorems; doing so just makes derivations shorter.
- Gödel showed that TNT is incomplete and that it cannot prove its own consistency. Actually he proved this result for the system PM and all related systems (which includes TNT).
- Without the rule of induction, the system would be weaker, and you can introduce the interesting concept of ω-inconsistency.
- TNT is actually strong enough to reason about formal systems in general (Chapter 9).