Gödel, Escher, Bach: An Eternal Golden Braid (42 page)

∨
~S0=0>

which can be derived in the same way as
∨
-P>
was derived.

Before we give more rules, let us give the five
axioms
of
TNT
: Axiom 1:
Va:~Sa=O

Axiom 2:
Va:(a+O)=a

Axiom 3:
Va:Vb:(a+Sb)=S(a+b)

Axiom 4:
Va:(a-O)=O

Axiom 5:
Va:Vb:(a-Sb)=((a-b)+a)

(In the austere versions, use
a
' instead of
b
.) All of them are very simple to understand.

Axiom 1 states a special fact about the number 0; Axioms 2 and 3 are concerned with the nature of addition; Axioms 4 and 5 are concerned with the nature of multiplication, and in particular with its relation to addition.

The Five Peano Postulates

By the way, the interpretation of Axiom 1-"Zero is not the successor of any natural number"-is one of five famous properties of natural numbers first explicitly recognized by the mathematician and logician Giuseppe Peano, in 1889. In setting out his postulates, Peano was following the path of Euclid in this way: he made no attempt to formalize the principles of reasoning, but tried to give a small set of properties of natural numbers from which everything else could be derived by reasoning. Peano's attempt might thus be considered "semiformal". Peano's work had a significant influence, and thus it would be good to show Peano's five postulates. Since the notion of "natural number" is the one which Peano was attempting to define, we will not use the familiar term "natural number", which is laden with connotation. We will replace it with the undefined term
djinn
, a word which comes fresh and free of connotations to our mind. Then Peano's five postulates place five restrictions on djinns. There are two other undefined terms:
Genie
, and
meta
. I will let you figure out for yourself what usual concept each of them is supposed to represent. The five Peano postulates:

(1) Genie is a djinn.

(2) Every djinn has a mesa (which is also a djinn).

(3) Genie is not the mesa of any djinn. (4) Different djinns have different metas.

(5) If Genie has X, and each djinn relays X to its mesa, then all djinns get X.

In light of the lamps of the
Little Harmonic Labyrinth
, we should name the set of
all
djinns "
GOD
". This harks back to a celebrated statement by the German mathematician and logician Leopold Kronecker, archenemy of Georg Cantor: "God made the natural numbers; all the rest is the work of man."

You may recognize Peano's fifth postulate as the principle of mathematical induction-another term for a hereditary argument. Peano he that his five restrictions on the concepts "Genie", "djinn", and "mesa" so strong that if two different people formed images in their minds o concepts, the two images would have completely isomorphic structures. example, everybody's image would include an infinite number of distinct djinns. And presumably everybody would agree that no djinn coins 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 that does not lessen the importance of the question, "How is a true statement about natural numbers to be distinguished from a false one?" At answer this question, mathematicians turned to totally formal systems, as
TNT
. However, you will see the influence of Peano 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 reach in and change the internal structure of the atoms of
TNT
. In sense they deal with more

"microscopic" properties of strings than the of the Propositional Calculus, which treat atoms as indivisible units. example, it would be nice if we could extract the string
-SO=O

from the first axiom. To do this we would need a rule which permits us to di universal quantifier, and at the same time to change the internal strut of the string which remains, if we wish. Here is such a rule:

RULE OF SPECIFICATION: Suppose u is a variable which occurs inside string x. If the string
V
u:x is a theorem, then so is x, and so an strings made from x by replacing u, wherever it occurs, by one the same term.

(
Restriction
: The term which replaces
u
must not contain any vat that is quantified in x.)

The rule of specification allows the desired string to be extracted Axiom 1. It is a one-step derivation:

Va -Sa=0

axiom 1

~S0=0

specification

Notice that the rule of specification will allow some formulas which co: free variables (i.e., open formulas) to become theorems. For example following strings could also be derived from Axiom 1, by specification:

Sa=0

~S(c+SSO)=0

There is another rule, the
rule of generalization
, which allows us to put back the universal quantifier on theorems which contain variables that became free as a result of usage of specification. Acting on the lower string, for example, generalization would give:

Vc:~S(c+SSO)=O

Generalization undoes the action of specification, and vice versa. Usually, generalization is applied after several intermediate steps have transformed the open formula in various ways. Here is the exact statement of the rule:

RULE OF GENERALIZATION: Suppose x is a theorem in which u, a variable, occurs free. Then
Vu
:x is a theorem.

(
Restriction
: No generalization is allowed in a fantasy on any variable which appeared free in the fantasy's premise.)

The need for restrictions on these two rules will shortly be demonstrated explicitly.

Incidentally, this generalization is the same generalization as was mentioned in Chapter II, in Euclid's proof about the infinitude of primes. Already we can see how the symbol-manipulating rules are starting to approximate the kind of reasoning which a mathematician uses.

The Existential Quantifier

These past two rules told how to take off universal quantifiers and put them back on; the next two rules tell how to handle existential quantifiers.

RULE OF INTERCHANGE: Suppose
u
is a variable. Then the strings
V
u:- and
-3u
: are interchangeable anywhere inside any theorem.

For example, let us apply this rule to Axiom 1:

Va:-Sa=O

axiom 1

~
ℑ
a:Sa=O

interchange

By the way, you might notice that both these strings are perfectly natural renditions, in
TNT
, of the sentence "Zero is not the successor of any natural number". Therefore it is good that they can be turned into each other with ease.

The next rule is, if anything, even more intuitive. It corresponds to the very simple kind of inference we make when we go from "2 is prime" to "There exists a prime". The name of this rule is self-explanatory:

RULE OF EXISTENCE: Suppose a term (which may contain variables as long as they are free) appears once, or multiply, in a theorem. Then any (or several, or all) of the appearances of the term may be replaced by a variable which otherwise does not occur in the theorem, and the corresponding existential quantifier must be placed in front.

Let us apply the rule to --as usual--Axiom 1:

Va:-Sa=O

axiom 1

ℑ
b:Va:-Sa=b
existence

You might now try to shunt symbols, according to rules so far giver produce the theorem

~Vb:
ℑ
a:Sa=b.

Rules of Equality and Successorship

We have given rules for manipulating quantifiers, but so far none for symbols `=' and 'S'.

We rectify that situation now. In what follows, r, s, t all stand for arbitrary terms.

RULES OF EQUALITY:

SYMMETRY: If r = s is a theorem, then so is s = r.

TRANSITIVITY: If r = s and s = t are theorems, then so is r = t.

RULFS OF SUCCESSORSHIP:

ADD S: If r = t is a theorem, then
Sr
=
St
is a theorem.

DROP S: If
Sr
=
St
is a theorem, then r = t is a theorem.

Now we are equipped with rules that can give us a fantastic variet theorems. For example, the following derivations yield theorems which pretty fundamental: (1)

Va: Vb:(a+Sb)=S(a+b)

axiom 3

(2)

Vb:(SO+Sb)=S(SO+b)

specification (SO for a)

(3)

(SO+SO)=S(SO+O)

specification (0 for b)

(4)

Va:(a+O)=a

axiom 2

(5)

(SO+O)=SO

specification (SO for a)

(6)

S(SO+O)=SSO

add S

(7)

(SO+SO)=SSO

transitivity (lines 3,6)

* * * * *

(1)

Va: Vb:(a-Sb)=((a-b)+a)

axiom 5

(2)

Vb:(SO•Sb)=((SO•b)+SO)

specification (SO for a)

(3)

(SO.SO)=((SO.O)+SO)

specification (0 for b)

(4)

Va: Vb:(a+Sb)=S(a+b)

axiom 3

(5)

Vb:((SO.O)+Sb)=S((5O O)+b)

specification ((SO-0) for a)

(6)

((SO .0)+SO)=S((SO.0)+0)

specification (0 for b)

(7)

Va:(a+O)=a

axiom 2

(8)

((SO.O)+0)=(SO.O)

specification ((S0.0) for a)

(9)

Va:(a.0)=0

axiom 4

(10)

(S0-0)=0

specification (SO for a)

(11)

((SO.O)+O)=O

transitivity (lines 8,10)

(12)

S((SO.0)+0)=SO

add S

(13)

((SO -0)+SO)=SO

transitivity (lines 6,12)

(14)

(SO.SO)=SO

transitivity (lines 3,13)

Illegal Shortcuts

Now here is an interesting question: "How can we make a derivation for the string
0=0
?"

It seems that the obvious route to go would be first to derive the string
Va:a=a
, and then to use specification. So, what about the following "derivation" of
Va:a=a
... What is wrong with it? Can you fix it up?

(1)

Va:(a+0)=a

axiom 2

(2)

Va:a=(a+0)

symmetry

(3)

Va:a=a

transitivity (lines 2,1)

I gave this mini-exercise to point out one simple fact: that one should not jump too fast in manipulating symbols (such as `=') which are familiar. One must follow the rules, and not one's knowledge of the passive meanings of the symbols. Of course, this latter type of knowledge is invaluable in guiding the route of a derivation.

Why Specification and Generalization Are Restricted

Now let us see why there are restrictions necessary on both specification and generalization. Here are two derivations. In each of them, one of the restrictions is violated. Look at the disastrous results they produce:

(1)

[

push

(2)

a=0

premise

(3)

Va:a=0

generalization (
Wrong
!)

(4)

Sa=O

specification

(5)

]

pop

(6)

⊃
Sa=O>

fantasy rule

(7)

Va:⊃
Sa=O>

generalization

(8)

⊃
SO=0>

specification

(9)

0=0

previous theorem

(10)

S0=0

detachment (lines 9,8)

This is the first disaster. The other one is via faulty specification.

(1)

Va:a=a

previous theorem

(2)

Sa=Sa

specification

(3)

ℑ
b:b=Sa

existence

(4)

Va:
ℑ
b:b=Sa

generalization

(5)

ℑ
b:b=Sb

specification (
Wrong
!)

So now you can see why those restrictions are needed.

Here is a simple puzzle: translate (if you have not already done so) Peano's fourth postulate into
TNT
-notation, and then derive that string as a theorem.

Something Is Missing

Now if you experiment around for a while with the rules and axioms of
TNT
so far presented, you will find that you can produce the following
pyramidal family
of theorems (a set of strings all cast from an identical mold, differing from one another only in that the numerals
0, SO, SSO
, and s have been stuffed in):

(0+0)=0

(O+SO)=S0

(O+SSO)=SSO

(O+SSSO)=SSSO

(O+SSSSO)=SSSSO

etc.

As a matter of fact, each of the theorems in this family can be derived the one directly above it, in only a couple of lines. Thus it is a so "cascade" of theorems, each one triggering the next. (These theorem very reminiscent of the pq-theorems, where the middle and right-] groups of hyphens grew simultaneously.)