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

Formula

a=a

We now replace all

free variables by

the numeral for 2:

sso=sso

Godei number

262,111,262

1

123,123,666,111,123,123,666

* * * * *

-3a:3a':a" =(SSa ·SSa')

We now replace all

free variables by

the numeral for 4:

223,333,262,636,333,262,163,636,

262,163,163,111,362,123,123,262,

236,123 '12l62 ,163 ,323

-3a:3a':SSSSO=(SSa· SSa') 223,333,262,636,333,262,163,636,

123,123,123,123,666,111,362,123,

123,262,236,123,123,262,163,323

An isomorphic arithmetical process is going on in the right-hand
column, in which one huge number is turned into an even huger number.
The function which makes the new number from the old one would not be
too difficult to describe arithmetically, in terms of additions, multiplica-
tions, powers of 10 and so on-but we need not do so. The main point is
this: that the relation among (1) the original Godel number, (2) the
number whose numeral is inserted, and (3) the resulting Godel number, is
a primitive recursive relation. That is to say, a BlooP test could be written
which, when fed as input any three natural numbers, says YES if they they
are related in this way, and NO if they aren't. You may test yourself on your
ability to perform such a test-and at the same time convince yourself that
there are no hidden open-ended loops to the process-by checking the
following two sets of three numbers:

(1) 362,262,112,262,163,323,111,123,123,123,123,666;

2;

362,123,123,666,112,123, 123,666,323,111,123,123,123,123,666.

(2) 223,362,262,236,262,323,111,262,163;

1 ;

223,362,123,666,236,123,666,323,111,262,163.

As usual, one of the examples checks, the other does not. Now this relation-

ship between three numbers will be called the substitution relationship.

Because it is primitive recursive, it is represented by some formula of TNT

having three free variables. Let us abbreviate that TNT -formula by the

following notation:

SUB{ a,a' ,a"}

(^444) On Formally Undecidable Propositions