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

Because this formula represents the substitution relationship, the formula

shown below must be a TNT-theorem:

SUB{SSSSS .... .sSSSSO/a,SSO/a',SSSSSS ..... SSSSO/a"}

262,111,262 --------------S's 123,123,666,111,123,123,666 --------- S's

(This is based on the first example of the substitution relation shown in the

parallel columns earlier in this section.) And again because the SUB for-

mula represents the substitution relation, the formula shown below cer-

tainly is not a TNT-theorem:

SUB{SSSO/a,SSO/a',SO/a"}

Arithmoquining

We now have reached the crucial point where we can combine all of our

disassembled parts into one meaningful whole. We want to use the machin-

ery of the TNT-PROOF-PAlR and SUB formulas in some way to construct a

single sentence of TNT whose interpretation is: "This very string of TNT

is not a TNT -theorem." How do we do it? Even at this point, with all the

necessary machinery in front of us, the answer is not easy to find.

A curious and perhaps frivolous-seeming notion is that of substituting

a formula's own G6del number into itself. This is quite parallel to that other

curious, and perhaps frivolous-seeming, notion of "quining" in the Air on

C's String. Yet quining turned out to have a funny kind of importance, in

that it showed a new way of making a self-referential sentence. Self-

reference of the Quine variety sneaks up on you from behind the first time

you see it-but once you understand the principle, you appreciate that it is

quite simple and lovely. The arithmetical version of quining-let's call it

arithmoquining-will allow us to make a TNT-sentence which is "about

itself".

Let us see an example of arithmoquining. We need a formula with at

least one free variable. The following one will do:

a=SO

This formula's G6del number is 262,111,123,666, and we will stick this

number into the formula itself-or rather, we will stick its numeral in. Here

is the result:

SSSSS ..... SSSSSO = SO

-----------262,111,123,666 S's

This new formula asserts a silly falsity-that 262,111,123,666 equals 1. If

we had begun with the string -a=SO and then arithmoquined, we would

have come up with a true statement-as you can see for yourself.

When you arithmoquine, you are of course performing a special case

On Formally Undecidable Propositions^445