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

Two natural numbers, m and n respectively, form a TNT-

proof-pair if and only if m is the Godel number of a TNT-

derivation whose bottom line is the string with Godel number n.

The analogous notion exists with respect to the MI U-system, and it is a little

easier on the intuition to consider that case first. So, for a moment, let us

back off from TNT-proof-pairs, and look at MIU-proof-pairs. Their

definition is parallel:

Two natural numbers, m and n respectively, form a MIU-proof-

pair if and only if m is the Godel number of a MIU-system

derivation whose bottom line is the string with Godel number n.

Let us see a couple of examples involving MIU-proof-pairs. First, let

m = 3131131111301, n = 301. These values of m and n do indeed form a

MIU-proof-pair, because m is the Godel number of the MIU-derivation

Ml

Mil

Mllli

MUI

whose last line is MUl, having Godel number 301, which is n. By contrast,

let m = 31311311130, and n = 30. Why do these two values not form a

MIU-proof-pair? To see the answer, let us write out the alleged derivation

which m codes for:

Ml

Mil

Mlll

MU

There is an invalid step in this alleged derivation! It is the step from the

second to the third line: from Mil to Mill. There is no rule of inference in

the MIU-system which permits such a typographical step.

Correspondingly-and this is most crucial-there is no arithmetical rule of

inference which carries you from 311 to 3111. This is perhaps a trivial

observation, in light of our discussion in Chapter IX, yet it is at the heart of

the Godel isomorphism. What we do in any formal system has its parallel in

arithmetical manipulations.

In any case, the values m = 31311311130, n = 30 certainly do not

form a MIU-proof-pair. This in itself does not imply that 30 is not a

MIU-number. There could be another value of m which forms a MIU-

proof-pair with 30. (Actually, we know by earlier reasoning that MU is not a

MIU-theorem, and therefore no number at all can form a MIU-proof-pair

with 30.)

Now what about TNT-proof-pairs? Here are two parallel examples,

one being merely an alleged TNT-proof-pair, the other being a valid

TNT-proof-pair. Can you spot which is which? (Incidentally, here is where

On Formally Undecidable Propositions 439