## Gödel's Numbers ### Or: The Book of Numbers ### Or: Variables are Numbers ### Or: Parentheses are Numbers ### Or: Quantifiers are Numbers ### Or: Sentences are Numbers ### Or: Proofs are Numbers ### Or: Numbers as Data Structures ### Or: The first Hexdump 0: Ok so, legend has it that Gödel started off by trying to define "truth" inside a formal language, then eventually realized he had to settle for "provability," and ended up getting the incompleteness theorems as a side effect. Let's try to follow the same train of thought. 1: How so? 0: Well, think of PA as a programming language. 1: Off to a good start. 0: Now let's see if we can define "truth" _inside_ the system, not just outside. 1: That seems hard. Can we start somewhere simpler? 0: Good idea. Let's think like developers. 1: Ok, truth is way too hard to be a starting point. How do we break it down? 0: Well we probably need some data types. 1: Isn't there only one data type in Peano Arithmetic? 0: Totally. In one sense, the only type is "natural numbers." In another sense, there are lots of types. Read the textbooks. They talk about "variables," "terms," "atomic formulas," "well formed formulas," and then they add things like "axioms" and "rules of inference." Then a "proof" is just a sequence of well formed formulas where each formula is either an axiom, or something that follows from axioms and rules of inference, or something that follows from axioms and rules of inference and anything else we proved along the way. 1: That sounds like a lot. Can we start with the simple stuff? 0: Sure. What did you have in mind? 1: Well I'd start by trying to encode "is-term", "is-formula", and the other basic stuff. The later data types like "proof" seem way too hard as a place to start. 0: Perfect. How could we encode "This is a term" or "This is a variable"? 1: What do we have to work with? 0: Numbers. 1: Just numbers? 0: Just numbers. 1: That sounds hard. 0: Does it? _(Narrator: 1 thinks for a moment.)_ 1: Can I take a quick look at what Gödel did? 0: Sure! Here's the beginning of the section in his paper on Gödel numbering. _(Narrator: 1 briefly skims the following pages.)_ ![[godel-collected-works-106.png]] 0: So he assigns a number to every character in the lan--- 1: Hah ok I get it now. 0: Are you sure? I didn't fin--- 1: Yeah I'm sure. This is totally trivial. Can't believe I didn't see it right away. 0: See what? _(Narrator: 1 types quickly into a terminal and adjacent text file.)_ 1: Here. 0: What's this? 1: I Gödeled variables. Look. ![[one-attempts-godel-numbering-02.png]] 0: You just typed "x" into a text file. 1: Exactly. Variable Gödelation complete. 0: Are you trying to do the thing to me that I do to you? 1: What thing? 0: Can you explain in what sense you think this is "Gödel numbering." 1: It's a number. Look. ![[one-attempts-godel-numbering-01.png]] 1: The Gödel number of the variable `x` is `0x78`. 0: Ok that's actually kinda funny. I'm not sure this counts though. 1: Why wouldn't it count? 0: We need to be able to support infinitely many variables. 1: At once?! I can't do that. 0: No not at once, just like $x_{0}, \; x_{1}, \; x_{7}, \; x_{101}$, these formal language things always assume you never run out of variables. You never have infinitely many all at once in any expression or whatever. They just assume you have as many variables as you need. So you need to be able to assign a number to the variable $x_n$ for any natural number $n$. 1: Easy! _(Narrator: 1 types some more, with a look of intense focus and moderate mischief on 1s face.)_ 1: Here. ![[one-attempts-godel-numbering-03.png]] 1: Mission accomplished. 0: What number is 78 31 30 31? 1: It's that number. 0: Which number? 1: C'mon zero don't be dumb. It's hex. Just concatenate the bytes together and that's the number. 0: Ok, just humor me. Suppose I wanted a number in base ten. 1: Why base 10? 0: No reason. Just want to see if you can do it. 1: Ok, base 10 it is. I guess it's a pretty nice number. It's got a 1 and a 0 in there. 0: Only in base itself. 1: What? 0: What's 10 in base 10? 1: Is this a trick question? 0: Yes. 1: What am I supposed to do? 0: Ok forget about the "What's 10 in base 10" question. Take your "Gödel numbering" scheme if we can really call it that, and then make it output numbers in base ten, and also I want you to support more than just variables. Any string in formal number theory has to be assigned a number, and the numbers of different strings have to be different. 1: Easiest thing ever. 0: Really? 1: Of course! Don't be dumb. It's trivial. 1: Here look: ```sh godel_number_anything() { printf "$1" | hexdump -e '1/1 "%02x"' \ | python -c "import sys; print(int.from_bytes(bytes.fromhex(sys.stdin.read()), 'big'))"; } ``` 1: Now everything gets a number: ```sh user@world ~ $ godel_number_anything 0 48 user@world ~ $ godel_number_anything 1 49 user@world ~ $ godel_number_anything x0 30768 user@world ~ $ godel_number_anything x1 30769 user@world ~ $ godel_number_anything "∀xP(x)" 16323438103633623081 ``` 0: _(Smiling)_ Nice work. 1: Is that sarcastic? 0: No! I'm proud of you. 1: Um, why? 0: Everyone always talks about how profound Gödel numbering is. And it definitely was when it first came out. But still, I'm at least a little impressed that you didn't let the fancy terminology distract you from the fact that everything's numbers already. A hexdump definitely counts as Gödel numbering. Nice work. 1: Thank you! 0: But since you implemented it, you're the maintainer now. 1: What does that mean? 0: It means I'm gonna complain to you when the implementation doesn't do what I expect it to. 1: I think I can handle it. There's literally no "implementation" here, it's just Unicode and hexdump. _(Narrator: @1, you have 1 new Issue alert on your codebase.)_ 1: _(Playing along)_ What is it? 0: Hi @1, I've been using your code and I think I found a bug. Look: ```sh user@world ~ $ godel_number_anything "∀x(x+0=x)" 273861846916120310563305513 user@world ~ $ godel_number_anything "∀x(x + 0 = x)" 1176227676126894985788045758205818921 ``` 1: That's not a bug zero, spaces change the number. 0: Well I'd like to request a feature that makes the numbers insensitive to whitespace. 1: Fine. _(Narrator: 1 types a few characters into a terminal.)_ 1: Here. ```sh godel_number_anything() { printf "$1" | sed 's/[ ]*//g' | hexdump -e '1/1 "%02x"' \ | python -c "import sys; print(int.from_bytes(bytes.fromhex(sys.stdin.read()), 'big'))"; } ``` 1: Feature implemented. Look. ```sh user@world ~ $ godel_number_anything "∀x(x + 0 = x)" 273861846916120310563305513 user@world ~ $ godel_number_anything "∀x(x+0=x)" 273861846916120310563305513 ``` ![[one-attempts-godel-numbering-06.png]] 0: Wonderful! This will make the numbers much more useful for my use case. 1: Don't say business words. 0: I'm just saying, I'm grateful, these numbers are more useful now. 1: What are you doing exactly? 0: I'm trying to compile the formal language of number theory into numbers. 1: It's already numbers. Just hexdump it. 0: Sure sure, but I was hoping to be able to do lots of things with these numbers. 1: Like what? 0: Well for example, I'd like to be able to determine whether a given Gödel number represents a well-formed formula that begins with a universal quantifier. 1: Can you speak programmer? 0: I'd like to be able to tell if a given number stands for a string that starts with "∀". But in the current implementation, this property is far from obvious. For example: ```sh root@world ~ $ godel_number_anything "∀x(x+0=x)" 273861846916120310563305513 root@world ~ $ godel_number_anything "∀x∀y(x+y=y+x)" 77085256997393696201791709053188838225961 ``` 0: Would you mind implementing a function that takes a Gödel number and tells me if it starts with a "∀"? 1: No problem. Would you like general support for substring detection at any location within any Gödel number? 0: That would be fantastic! How long do you think that will take. 1: A few seconds. See we used to have that feature automatically, but then some annoying user asked me to make the numbers be base ten. 0: Pssh, users are the worst. 1: I'll get right on that change request. _(Narrator: 1 types a few keystrokes.)_ 1: Here: ```sh godel_number_anything() { printf "$1" | hexdump -e '1/1 "%02x"'; } ``` 1: Now substring detection is much easier. Look. ```sh user@world ~ $ godel_number_anything "∀" e28880 user@world ~ $ godel_number_anything "∀x" e2888078 user@world ~ $ godel_number_anything "∀xP(x)" e288807850287829 ``` ![[one-attempts-godel-numbering-07.png]] 0: Wonderful! What if the ∀ doesn't come at the beginning? 1: It'll still be `e28880`. Here look. ```sh user@world ~ $ printf ∀ | hexdump -Cv 00000000 e2 88 80 |...| user@world ~ $ printf ∃x∀y | hexdump -Cv 00000000 e2 88 83 78 e2 88 80 79 |...x...y| user@world ~ $ printf abcd∀wxyz | hexdump -Cv 00000000 61 62 63 64 e2 88 80 77 78 79 7a |abcd...wxyz| ``` 1: See? ![[one-attempts-godel-numbering-09.png]] 0: This is absolutely wonderful, 1! 1: No it isn't. It's a hexdump. 0: Still, this is a much more sophisticated system than the original implementation of Gödel numbering. 1: Are you kidding? 0: Not at all! Follow me, I'll show you... goto: [[Old - 5|/lost+found/4/5]]