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

"Yields Nontheoremhood When Arithmoquined"

Let us pause for breath for a moment, and review what has been done. The

best way I know to give some perspective is to set out explicitly how it

compares with the version of the Epimenides paradox due to Quine. Here

IS a map:

falsehood ¢Co:}

quotation of a phrase ¢:=?

preceding a predicate ¢Co:}

by a subject

preceding a predicate ¢:=?

by a quoted phrase

preceding a predicate ¢:=?

by itself, in quotes

("quining")

yields falsehood when quined ¢:=?

(a predicate without a subject)

"yields falsehood when quined" ¢:=?

(the above predicate, quoted)

"yields falsehood when quined" ¢:o:}

yields falsehood when quined

(complete sentence formed by

quining the above predicate)

nontheoremhood

Code! number of a string

substituting a numeral (or

definite term) into an open formula

substituting the Codel number

of a string into an open formula

substituting the Codel number

of an open formula into the

formula itself ("arithmoquining")

the "uncle" of C

(an open formula of TNT)

the number u (the Codel number

of the above open formula)

G itself

(sentence of TNT formed by

substituting u into the uncle,

i.e., arithmoquining the uncle)

G6del's Second Theorem

Since G's interpretation is true, the interpretation of its negation -G is

false. And we know that no false statements are derivable in TNT. Th us

neither G nor its negation -G can be a theorem of TNT. We have found a "hole"

in our system-an undecidable proposition. This has a number of ramifica-

tions. Here is one curious fact which follows from G's undecidability:

although neither G nor -G is a theorem, the formula <Gv-G> is a

theorem, since the rules of the Propositional Calculus ensure that all

well-formed formulas of the form <Pv-P> are theorems.

This is one simple example where an assertion inside the system and an

assertion about the system seem at odds with each other. It makes one

wonder if the system really reflects itself accurately. Does the "reflected

metamathematics" which exists inside TNT correspond well to the

metamathematics which we do? This was one of the questions which in-

trigued Godel when he wrote his paper. In particular, he was interested in

whether it was possible, in the "reflected metamathematics", to prove

TNT's consistency. Recall that this was a great philosophical dilemma of

On Formally Undecidable Propositions 449