## Gödel's Numbers
### Or: Names are Numbers
### Or: The Book of Numbers
TODO: In this section, we should carry out Gödel numbering before we have any concrete definition of computation. Our goal is the same as Gödel's: we start off by attempting to define "truth" inside a formal language, and then eventually realize we have to settle for "provability."
To accomplish the above goal, we start by realizing we should start somewhere simple, so we start by trying to encode "is-term", "is-formula", and other basic syntactic notions.
To accomplish that, we need to start somewhere even more simple, by defining things like "is-left-parenthesis" and "is-variable."
Then in the next file, we see which types of functions we needed along the way, and as a side note we say "Here are the functions we'll need." Gödel wasn't aiming to provide a general notion of "all computation." This only became clear later.
After the equivalence between lambda calculus and general recursive functions was proved, it still wasn't clear that this was all of computation.
It required Turing's paper before Gödel was convinced, because Turing didn't formalize "functions," he formalized "making marks on paper."