That's a beautiful story. I've been fascinated by Gödel since I read Gödel, Escher, Bach by Douglas Hofstadter back in the 1980s. I'm not a mathematician, so I can't plumb the depths of his work, but I gain a little more insight by reading articles like this one.
I remember reading the proof of his incompleteness theorem (or the portion of it that I had time to between classes). It's surprisingly approachable. AFAIR, he came up with a way to encode proofs as symbol sequences. Proofs that actually exist have finite representations. He then proved the theorem with that somehow. (Granted, I read it over a decade ago...)
You're thinking of Gödel numbering which is an elegant technique used extensively throughout that proof. He uses it to map logical symbols, statements and entire proofs to natural numbers and then proceeds to prove things about those statements and proofs by referring to them via their Gödel numbers.
