# Typographical Number Theory

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.

## Scope

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.

## Syntax

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 | Sn
Variable   ::= 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 of A or B and bound in the other)
|  <A∨B>    (no var free in one of A or B and bound in the other)
|  <A⊃B>    (no var free in one of A or B and bound in the other)
|  ∃v:A     (v free in A)
|  ∀v:A     (v free in A)
```

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.

## Inference Rules

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 `∀u:A` is a theorem then so are A and `A{t/u}` provided 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 `∀u:A`, provided u is not free in the premise of any fantasy containing A
• Rule of Interchange: The strings `∀u:~` and `~∃u:` are interchangeable anywhere inside a theorem to produce a new theorem
• Symmetry of Equality: If `s=t` is a theorem then so is `t=s`
• Transitivity of Equality: If `r=s` and `s=t` are theorems then so is `r=t`
• Add S: If `r=t` is a theorem then so is `Sr=St`
• Drop S: If `Sr=St` is a theorem then so is `r=t`
• Rule of Induction: If `A{0/u}` and `∀u:<A⊃A{Su/u}>` are both theorems, then so is `∀u:A`

The notation `A{t/u}` denotes the formula made from replacing all free occurrences of variable 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.

## Semantics

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

### Interpretation

• `0` zero
• `S` successor
• `=` numeric equals
• `+` addition
• `•` multiplication
• `∃` there exists
• `∀` for all

### Examples

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 a2 over b2 is equal to the square root of 2.
• There are no two numbers a and b, such that a2 over b2 is equal to 2.
• There are no two numbers a and b, such that a2 equals 2 times b2.
• For all numbers a and b, if a2 equals twice b2, 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)>>>`

### Understanding the Restrictions on the Inference Rules

#### The Restriction on Specification

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!
```

#### The Restriction on Generalization

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.

Exercise: Continue the erroneous derivation above to eventually get to a theorem that says 1=2.

## Metalogic

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

## Interesting Facts

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