Gödel, Escher, Bach - Gödel's string
- by Brad Urani
In the book Gödel, Escher, Bach: An Eternal Golden Braid by Douglas Hofstadter, the author gives us a representation of the precursor to Gödel's string (Gödel's string's uncle) as:
~Ea,a': (I don't have the book in front of me but I think that's right). All that remains to get Gödel's string is to plug the Gödel number for this string into the free variable a''. What I don't understand is how to get the Gödel number for the functions PROOF-PAIR and ARITHMOQUINE. I understand how to write these functions in a programming language like FlooP (from the book) and could even write them myself in C# or Java, but the scheme that Hofstadter defines for Gödel numbering only applies to TNT (which is just his own syntax for natural number theory) and I don't see any way to write a procedure in TNT since it doesn't have any loops, variable assignments etc.
Am I missing the point? Perhaps Gödel's string is not something that can actually be printed, but rather a theoretical string that need not actually be defined? I thought it would be neat to write a computer program that actually prints Gödel's string, or Gödel's string encoded by Gödel numbering (yes, I realize it would have a gazillion digits) but it seems like doing so requires some kind of procedural language and a Gödel numbering system for that procedural language that isn't included in the book.
Of course once you had that, you could write a program that plugs random numbers into variable "a" and run procedure PROOF-PAIR on it to test for theoromhood of Gödel's string. If you let it run for a trillion years you might find a derivation that proves Gödel's string.
