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

too. The trick will be to find a string which expresses the statement

"I Cannot Be Proven in Formal System TNT +G."

Actually, it is not much of a trick, once you have seen it done for TNT. All

the same principles are employed; only the context shifts slightly. (Figura-

tively speaking, we take a tune we know and simply sing it again, only in a

higher key.) As before, the string which we are looking for-let us call it

"G' "-is constructed by the intermediary of an "uncle". But instead of

being based on the formula which represents TNT-proof-pairs, it is based

on the similar but slightly more complicated notion of TNT +G-proof-

pairs. This notion of TNT +G-proof-pairs is only a slight extension of the

original notion of TNT -proof-pairs.

A similar extension could be envisaged for the MIU-system. We have

seen the unadulterated form of MIU-proof-pairs. Were we now to add MU

as a second axiom, we would be dealing with a new system-the MIU +MU

system. A derivation in this extended system is presented:

MU

MUU

axiom

rule 2

There is a MIU + MU-proof-pair which corresponds-namely, m = 30300,

n = 300. Of course, this pair of numbers does not form a MIU-proof-

pair-only a MIU +MU-proof-pair. The addition of an extra axiom does

not substantially complicate the arithmetical properties of proof-pairs. The

significant fact about them-that being a proof-pair is primitive

recursive-is preserved.

The Godel Method Reapplied

Now, returning to TNT+G, we will find a similar situation. TNT+G-

proof-pairs, like their predecessors. are primitive recursive, so they are

represented inside TNT +G by a formula which we abbreviate in an obvi-

ous manner:

(TNT +G)-PROOF-PAlR{a,a'}

Now we just do everything all over again. We make the counterpart of G by

beginning with an "uncle", just as before:

-3a:3a':«TNT +G)-PROOF-PAlR{a,a'}AARlTHMOQUlNE{a",a'}>

Let us say its Godel-number is u'. Now we arithmoquine this very uncle.
That will give us G':

466

-3a:3a':«TNT +G)-PROOF-PAlR{a,a'}

AARlTHMOQUlNE{SSS .... SSSO/a",a'}>

~

u'S's

Jumping out of the System