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

the '611' codon comes in. Its purpose is to separate the Godel numbers of
successive lines in a TNT-derivation. In that sense, '611' serves as a punctu-
ation mark. In the MIU-system, the initial '3' of all lines is sufficient-no
extra punctuation is needed.)

(I) m = 626,262,636,223,123,262,111,666,611 ,223,123,666, 111,666

n = 123,666,111,666

(2) m = 626,262,636,223, 123,262,111.666,611 ,223,333,262,636,123,262,111,666

n = 223,333,262,636,123,262,111,666

It is quite simple to tell which one is which, simply by translating back to the
old notation, and making some routine examinations to see

(1) whether the alleged derivation coded for by m is actually a

legitimate derivation;

(2) if so, whether the last line of the derivation coincides with the

string which n codes for.

Step 2 is trivial; and step 1 is also utterly straightforward, in this sense:
there are no open-ended searches involved, no hidden endless loops.
Think of the examples above involving the MIU-system, and now just
mentally substitute the rules of TNT for the MIU-system's rules, and the
axioms of TNT for the MIU-system's one axiom. The algorithm in both
cases is the same. Let me make that algorithm explicit:

Go down the lines in the derivation one by one.

Mark those which are axioms.

For each line which is not an axiom, check whether it follows by

any of the rules of inference from earlier lines in the alleged

derivation.

If all nonaxioms follow by rules of inference from earlier lines,

then you have a legitimate derivation; otherwise it is a phony

derivation.

At each stage, there is a clear set of tasks to perform, and the number of

them is quite easily determinable in advance.

Proof-Pair-ness Is Primitive Recursive

The reason I am stressing the boundedness of these loops is, as you may

have sensed, that I am about to as~ert

FUNDAMENTAL FACT 1: The property of being a proof-pair is a

primitive recursive number-theoretical property, and can there-

fore be tested for by a BlooP program.

There is a notable contrast to be made here with that other closely

related number-theoretical property: that of being a theorem-number. To

(^440) On Formally Undecidable Propositions