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:
a + b = 50, then a < 50.
b is a power of 2.
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) | (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.
The rules of TNT include all rules of the Propositional Calculus plus the following:
∀a:~Sa=0
∀a:(a+0)=a
∀a:∀b:(a+Sb)=S(a+b)
∀a:(a•0)=0
∀a:∀b:(a•Sb)=((a•b)+a)
∀u:A
is a theorem then so are A and A{t/u}
provided t contains no variables that are bound in A
∀u:A, provided
u is not free in the premise of any fantasy containing A
∀u:~ and
~∃u: are interchangeable anywhere
inside a theorem to produce a new theorem
s=t
is a theorem then so is t=s
r=s
and s=t are theorems then so is
r=t
r=t is a theorem then so is Sr=St
Sr=St is a theorem then so is r=t
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.
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
∃.
∀a:~0=Sa
~∃a:(a•a)=SSSSS0
∃a:((SS0•a)+1)=SSSSSSS0
∀a:∀b:<~a=b⊃~Sa=Sb>
∃a:SSSSSSSS0=(SSS0+Sa)
~∃a:∃b:(SSa•SSb)=SSSSSSSSSSS0
∃a:<∃b:(b•SS0)=a∧~∃c:∃d:(SSc•SSd)=a>
∀a:∃b:~∃c∃d:(a+Sb)=(SSc•SSd)
∀a:∀b:<((a•a)=SS0•(b•b))⊃a=0>
<~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: