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

CHAPTER XIV On Formally Undecidable Propositions of TNT and Related Systems l The Two Ideas of the "Oyster" THIS CHAPTER'S TITLE ...

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 whos ...

the '611' codon comes in. Its purpose is to separate the Godel numbers of successive lines in a TNT-derivation. In that sense, ' ...

assert that n is a theorem-number is to assert that some value of m exists which forms a proof-pair with n. (Incidentally, these ...

Since it is a property of two numbers, it is represented by a formula with two free variables. (Note: In this Chapter we shall a ...

How do the solutions differ from the example done above, and from each other? Here are a few more translation exercises. (4) jOS ...

Formula a=a We now replace all free variables by the numeral for 2: sso=sso Godei number 262,111,262 1 123,123,666,111,123,123,6 ...

Because this formula represents the substitution relationship, the formula shown below must be a TNT-theorem: SUB{SSSSS .... .sS ...

of the substitution operation we defined earlier. If we wanted to speak about arithmoquining inside TNT, we would use the formul ...

The head and tail of u's decimal expansion, and even a teeny bit of its midsection, can be read off directly: u = 223,333,262,63 ...

-or if you prefer, "I am not a theorem of TNT." We have gradually pulled a high-level interpretation-a sentence of meta-TNT -out ...

"Yields Nontheoremhood When Arithmoquined" Let us pause for breath for a moment, and review what has been done. The best way I k ...

the day: how to prove a system consistent. Godel found a simple way to express the statement "TNT is consistent" in a TNT formul ...

u uS's ~ -3a': <TNT-PROOF-PAIR{O/a,a'} A ARITHMOQUINE{SSS ... SSSO/a", a'}> -3a': <TNT-PROOF-PAIR{SO/a,a'} A ARITHMOQUI ...

This suggestion seems rather innocuous and perhaps even desirable, since, after all, G asserts something true about the natural ...

-but the various members of the pyramidal family successively assert: "0 is not that number" "1 is not that number" "2 is not th ...

long as those properties are given to us in theorems of TNT. In other words, everything that can be formally proven about natura ...

However, we will have to get used to the idea that -G is now the one which asserts a truth ("G has a proof"), while G asserts a ...

both instances, one is powerfully driven to ~sk, "But which one of these two rival theories is correct? Which is thl' truth?" In ...

true geometry'.', for in fact, physicists will always use a variety of different geometries, choosing in any given situation the ...