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

would put us in hot water, for if theoremhood is a representable attribute,

then Godel's formula G becomes as vicious as the Epimenides paradox.

It all hinges on what G says: "G is not a theorem of TNT". Assume that

G were a theorem. Then, since theoremhood is supposedly represented,

the TNT-formula which asserts "G is a theorem" would be a theorem of

TNT. But this formula is -G, the negation of G, so that TNT is inconsis-

tent. On the other hand, assume G were not a theorem. Then once again by

the supposed representability of theoremhood, the formula which asserts

HG is not a theorem" would be a theorem of TNT. But this formula is G,

and once again we get into paradox. L'nlike the situation before, there is no

resolution of the paradox. The problem is created by the assumption that

theoremhood is represented by some formula of TNT, and therefore we

must backtrack and erase that assumption. This forces us also to conclude

that no FlooP program can tell the Godel numbers of theorems from those

of nontheorems. Finally, if we accept the AI Version of the CT-Thesis,

then we must backtrack further, and conclude that no method whatsoever

could exist by which humans could reliably tell theorems from nontheo-

rems-and this includes determinations based on beauty. Those who sub-

scribe only to the Public-Processes Version might still think the Crab's

performance is possible; but of all the versions, that one is perhaps the

hardest one to find any justification for.

Tarski's Theorem

Now let us proceed to Tarski's result. Tarski asked whether there could be

a way of expressing in TNT the concept of number-theoretical truth. That

theoremhood is expressible (though not representable) we have seen;

Tarski was interested in the analogous question regarding the notion of

truth. More specifically, he wished to determine whether there is any

TNT-formula with a single free variable a which can be translated thus:

"The formula whose Godel number is a expresses a truth."

Let us suppose, with Tarski, that there is one-which we'll abbreviate as
TRUE{a}. Now what we'll do is use the diagonalization method to produce a
sentence which asserts about itself that it is untrue. We copy the Godel
method exactly, beginning with an "uncle":

3a:<-TRUE{a}AARITHMOQUINE{a",a}>

Let us say the Godel number of the uncle is t. We arithmoquine this very
uncle, and produce the Tarski formula T:

580

3a:<-TRUE{a}AARITHMOQUINE{SSS ... SSSO/a",a}>

~

t S's

Church, Turing, Tarski, and Others