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.


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:

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 | Sn
Variable   ::= a | b | c | d | e | v'
Term       ::= n | v | St | (s+t) | (st)
Formula    ::= s=t
            |  ~A
            |  <AB>    (no var free in one of A or B and bound in the other)
            |  <AB>    (no var free in one of A or B and bound in the other)
            |  <AB>    (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:

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:




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.



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 .

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:


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.


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: