Gödel, Escher, Bach An Eternal Golden Braid by Douglas R. Hofstadter

You may recognize Peano's fifth postulate as the principle of mathe-

matical induction-another term for a hereditary argument. Peano hoped

that his five restrictions on the concepts "Genie", "djinn", and "meta" were

so strong that if two different people formed images in their minds of the

concepts, the two images would have completely isomorphic structures. For

example, everybody's image would include an infinite number of distinct

djinns. And presumably everybody would agree that no djinn coincides

with its own meta, or its meta's meta, etc.

Peano hoped to have pinned down the essence of natural numbers in

his five postulates. Mathematicians generally grant that he succeeded, but

that does not lessen the importance of the question, "How is a true state-

ment about natural numbers to be distinguished from a false one?" And to

answer this question, mathematicians turned to totally formal systems, such

as TNT. However, you will see the influence of Pea no in TNT, because all

of his postulates are incorporated in TNT in one way or another.

New Rules of TNT: Specification and Generalization

Now we come to the new rules of TNT. Many of these rules will allow us to

reach in and change the internal structure of the atoms of TNT. In that

sense they deal with more "microscopic" properties of strings than the rules

of the Propositional Calculus, which treat atoms as indivisible units. For

example, it would be nice if we could extract the string -50=0 from the

first axiom. To do this we would need a rule which permits us to drop a

universal quantifier, and at the same time to change the internal structure

of the string which remains, if we wish. Here is such a rule:

RULE OF SPECIFICATION: Suppose u is a variable which occurs inside the

string x. If the string Vu: x is a theorem, then so is x, and so are any

strings made from x by replacing u, wherever it occurs, by one and

the same term.

(Restriction: The term which replaces u must not contain any variable

that is quantified in x.)

The rule of specification allows the desired string to be extracted from

Axiom 1. It is a one-step derivation:

Va:-5a=0

-50=0

axiom

specification

Notice that the rule of specification will allow some formulas which contain

free variables (i.e., open formulas) to become theorems. For example, the

following strings could also be derived from Axiom 1, by specification:

-5a=0

-5(c+550)=0

There is another rule, the rule of generalization, which allows us to put

Typographical Number Theory^217