TABLE OF CONTENTS Personal - [[#Gödel's Girls|Gödel's Girls]] - [[#Letter to Mother|Letter to Mother]] - [[#Mr. Why|Mr. Why]] - [[#Kleene on Gödel|Kleene on Gödel]] - [[#Goldstein|Goldstein]] - [[#How Incompleteness Paved the Way for Defining Computation|How Incompleteness Paved the Way for Defining Computation]] - [[#Gödel's End|Gödel's End]] Technical - [[#Unicode Gödel Numbers: The First Hexdump|Unicode Gödel Numbers: The First Hexdump]] - [[#Gödel's Language|Gödel's Language]] - [[#Gödel's μ-lang (0.0.1)|Gödel's μ-lang (0.0.1)]] - [[#Gödel's μ-lang (0.0.2)|Gödel's μ-lang (0.0.2)]] - [[#The Second "First Standard Library"|The Second "First Standard Library"]] - [[#Enter Al|Enter Al]] --- ## Gödel's Girls > _There is no doubt that Gödel had a liking for members of the opposite sex, and he made no secret about this fact. Let me tell a little anecdote. I was working in the small seminar room outside the library in the mathematical seminar. The door opened, and a very small, very young girl entered. She was good-looking, with a slightly gloomy face (maybe \[due to\] timidity), and wore a beautiful, quite unusual summer dress. Not much later Kurt entered, and she got up and the two of them left together. It seemed a clear show-off on Kurt’s part… You could talk to him about other things \[besides mathematics\] too, and his clear mind made this a rare pleasure..._ > > -Olga Taußky-Todd, as quoted in _Kurt Gödel: The Genius of Metamathematics,_ by William D. Brewer, pg 62 ## Letter to Mother ``` Princeton, 24./VIII. 1956. Dearest Mama! Last week I began writing a letter to you, but then abandoned it. My hand does not want to write this time. It weighs on me that I have had to disappoint you a second time about my coming. This time the fault lies the very least with me. At this point I cannot even say when I will be able to come except that the doctor said it would be best next Spring. ``` ``` Today I had a strange dream about you. We were in New York together in an enormous hotel and kept riding up and down in the elevator. By the end we were balancing together on an exterior window sill on the 20th floor. But nothing happened. ``` ``` I mainly did not send you the piece about me in Scientific American because my picture is so miserable. A press photographer came to see me at the Institute and took ca. 50 shots of me, supposedly to be sure that at least one really good one would be among them. In fact they apparently chose the worst one. For there were some really good ones among which I was sent one. ``` ``` I am glad that Morgenstern’s visit offered you a pleasant diversion and that he told you so much about me and so vividly. That little Karl is very nice and well behaved, that is true. I did not even write you yet that our parakeets have a chick, which now is already all grown up and quite tame. It flies onto one’s finger and one can pet it. Is that not charming? When it arrived it was only 2 cm long and lay the entire time with its beak on the floor of the incubator. Now it is the fattest and strongest of all three of them. ``` ``` Adele’s mother is doing very well and she likes it here very much. Adele let go of the girl and the gardener and does all the work alone. And she even is painting the kitchen furniture and renovating the cellar so that I cannot explain to myself where she gets the energy for all that. ``` ``` Yesterday I saw Eisenhower on the television, when he held the speech on the occasion of his nomination. He looks stronger and more energetic than ever despite his two illnesses. What do you have to say about the collision of the Andrea Doria? Both the ships supposedly diverted toward the same side. Is that not ludicrous? ``` ``` Enclosed I am sending you the congratulatory message from the Vienna Municipal Council. So far not one of my letters to you have gotten lost. If you want, you can send it back by registered mail, by the way. Thousand Bussis, also from Adele and her mother ever Your Kurt. P.S. Of course Adele is neglecting her correspondence entirely as a result of all the work, even to her relatives and friends. ``` --- ## Mr. Why 0: Dear 1, 1: What? 0: I'd like to introduce you to someone. 1: Um, ok. 0: Someone whose parents used to call him Mr. Why. 1: Solid name. Who is it? 0: The next member of our trinity. ![[godel-collected-works-050.png]] ![[godel-collected-works-011.png]] > -Kurt Godel, collected works ![[godel-goldstein-01.png]] > -Rebecca Goldstein, Incompleteness 0: When Gödel was a little kid, his parents nicknamed him "Mr. Why." Sound familiar? 1: No way! That was totally me! 0: Sounds like it. Though in a lot of ways he wasn't really like anybody. ![[godel-goldstein-02.png]] ![[godel-collected-works-008.png]] 0: He was super cautious. Like another planet level of caution. Eventually ended up starving himself to death out of fear of being poisoned. 1: Holy f--- 0: But that's jumping way ahead. He wasn't always like that. That was toward the end, in the 1970s, when his wife was away in the hospital. 1: Why did he starve himself? 0: He only trusted food that came from Adele. He really needed her around. They were great together. ![[godel-collected-works-006.png]] 1: That's a cute quote. What's this from? 0: From here: ![[godel-collected-works-001.png|400]] 0: Big book of all the stuff Gödel ever wrote. There's commentary by a bunch of logicians before each paper. Everyone's pretty much unanimous that he was the top logician of the century, probably ever. ![[godel-collected-works-007.png]] 0: But we're getting ahead of ourselves again. Let's rewind back to the early days. 1: When's the early days? 0: Well Hilbert's problems were 1900. Then Church was born in 1903. Now Gödel gets born in 1906, so let's start from there. ![[godel-collected-works-012.png]] 1: "he excelled particularly in mathematics, languages, and religion"? 0: Is that a question? 1: Just wondering how you always manage to make everything about religion. 0: You realize I didn't cause Gödel's life to happen right? 1: Just saying it's a suspicious pattern. 0: Sure whatever. Ok so, WWI happens. And, it's hard to overstate this, but basically the end of civilization begins. ![[godel-collected-works-014.png]] --- TODO: Merge bits from several sources to create a narrative from childhood to completeness. --- Hardly ever spoke. ![[godel-collected-works-015.png]] Studied Principia years later. ![[godel-collected-works-016.png]] Did his dissertation with no guidance. ![[godel-collected-works-017.png]] Curt style. ![[godel-collected-works-018.png]] ![[godel-collected-works-019.png]] ![[godel-collected-works-020.png]] ![[godel-collected-works-021.png]] ![[godel-collected-works-022.png]] ![[godel-collected-works-023.png]] ![[godel-collected-works-024.png]] ![[godel-collected-works-025.png]] ![[godel-collected-works-026.png]] ![[godel-collected-works-027.png]] 0: He meets his wife when he's 21, and his parents are not happy. 1: Why not? 0: Well Kurt is soft spoken, to say the least. He basically never talks. His wife, on the other hand, is a, well, a "dancer." 1: What's wrong with being a dancer? 0: I mean like a "night club dancer." 1: Oh! 0: Plus she was already divorced, and was 6 years older than him. 1: Doesn't seem so bad. 0: It wasn't. Apparently they were perfect together. ![[godel-collected-works-028.png]] ![[godel-collected-works-030.png]] ![[godel-collected-works-031.png]] ![[godel-collected-works-032.png]] Loneliness and Sanatorium. ![[godel-collected-works-033.png]] ![[godel-collected-works-034.png]] ![[godel-collected-works-035.png]] Mental stress from 1934-1937. ![[godel-collected-works-036.png]] Was convinced he had a weak heart, but was found fit for duty. ![[godel-collected-works-037.png]] ![[godel-collected-works-038.png]] Finds a security vulnerability in the US constitution and tries to talk about it during his citizenship interview. ![[godel-collected-works-039.png]] ![[godel-collected-works-040.png]] ![[godel-collected-works-041.png]] ![[godel-collected-works-042.png]] ![[godel-collected-works-043.png]] ![[godel-collected-works-044.png]] ![[godel-collected-works-045.png]] ![[godel-collected-works-046.png]] Demonology. ![[godel-collected-works-047.png]] ![[godel-collected-works-048.png]] Starves himself to death. ![[godel-collected-works-049.png]] ![[godel-collected-works-051.png]] ![[godel-collected-works-052.png]] ![[godel-collected-works-053.png]] ![[godel-collected-works-054.png]] ![[godel-collected-works-055.png]] ![[godel-collected-works-056.png]] ![[godel-collected-works-057.png]] ![[godel-collected-works-058.png]] ![[godel-collected-works-059.png]] ![[godel-collected-works-060.png]] ![[godel-collected-works-061.png]] ![[godel-collected-works-062.png]] ![[godel-collected-works-063.png]] ![[godel-collected-works-064.png]] ![[godel-collected-works-065.png]] ![[godel-collected-works-066.png]] ![[godel-collected-works-067.png]] ![[godel-collected-works-068.png]] ![[godel-collected-works-069.png]] ![[godel-collected-works-070.png]] ![[godel-collected-works-071.png]] ![[godel-collected-works-072.png]] ![[godel-collected-works-073.png]] ![[godel-collected-works-074.png]] ![[godel-collected-works-075.png]] ![[godel-collected-works-076.png]] ![[godel-collected-works-077.png]] ![[godel-collected-works-078.png]] ![[godel-collected-works-079.png]] ![[godel-collected-works-080.png]] ![[godel-collected-works-081.png]] ![[godel-collected-works-082.png]] ![[godel-collected-works-083.png]] ![[godel-collected-works-084.png]] ![[godel-collected-works-085.png]] ![[godel-collected-works-086.png]] ![[godel-collected-works-087.png]] ![[godel-collected-works-088.png]] ## Kleene on Gödel > Steve Kleene: and there must have been discussions between Church and Gödel, and I don't know how ready Gödel was to embrace the thesis that this was all effectively calculable functions but Church of course is the one that certainly came out explicitly with this. > Steve Kleene: Then Gödel arrived in the Fall or Spring of the year 1933-34. Gödel was giving his lectures. Gödel had this notion of General Recursive Functions, and the question came up, y'know, well, does this embrace all effectively calculable functions and is it equivalent to lambda definability. > Steve Kleene: I left Princeton in June of 1935, and of course we already had Church's Thesis in, it must have been the late spring of '34. That's when Gödel was talking about his General Recursive Functions. > Steve Kleene: You don't happen to have a copy of Introduction to Metamathematics do you? > Steve Kleene: Well, what Herbrand did in General Recursive Functions as presented by Gödel giving credit for ideas of Herbrand, is something I understand more than what Herbrand published. It was a little note of Herbrand's or a little, y'know, it was something short but whether it was a short note or just a short piece on the end of something else. > > _(Kleene thumbs through his book Introduction to Metamathematics: The "frighteningly technical" book mentioned earlier.)_ > > Gerald Sacks: It's hard to remember everything in that book. > > _(Everyone laughs.)_ > > Some Famous Logician: I knew it for a week or two when I had to take my exams. But I must say a few have slipped my mind. > > Steve Kleene: It helps to have written it. > > C. C. Chang: I don't even remember what's in _Model Theory_ anymore. 1: What's _Model Theory_? 0: A part of foundations of mathematics. But in this case it's a book that guy wrote. ## Goldstein ![[godel-goldstein-00.jpg|400]] ![[godel-goldstein-03.png]] ![[godel-goldstein-04.png]] ![[godel-goldstein-05.png]] ![[godel-goldstein-06.png]] ![[godel-goldstein-07.png]] ![[godel-goldstein-08.png]] ![[godel-goldstein-09.png]] ![[godel-goldstein-10.png]] ![[godel-goldstein-11.png]] ![[godel-goldstein-12.png]] ![[godel-goldstein-13.png]] ![[godel-goldstein-14.png]] ![[godel-goldstein-15.png]] ![[godel-goldstein-16.png]] ![[godel-goldstein-17.png]] ![[godel-goldstein-18.png]] ![[godel-goldstein-19.png]] ![[godel-goldstein-20.png]] ![[godel-goldstein-21.png]] ![[godel-goldstein-22.png]] ![[godel-goldstein-23.png]] ![[godel-goldstein-24.png]] ![[godel-goldstein-25.png]] ![[godel-goldstein-26.png]] ![[godel-goldstein-27.png]] ![[godel-goldstein-28.png]] ![[godel-goldstein-29.png]] ![[godel-goldstein-30.png]] ![[godel-goldstein-31.png]] ![[godel-goldstein-32.png]] ![[godel-goldstein-33.png]] ![[godel-goldstein-34.png]] ![[godel-goldstein-35.png]] ![[godel-goldstein-36.png]] ![[godel-goldstein-37.png]] ![[godel-goldstein-38.png]] ![[godel-goldstein-39.png]] ![[godel-goldstein-40.png]] ![[godel-goldstein-41.png]] ![[godel-goldstein-42.png]] ![[godel-goldstein-43.png]] ![[godel-goldstein-44.png]] ![[godel-goldstein-45.png]] ![[godel-goldstein-46.png]] ![[godel-goldstein-47.png]] ![[godel-goldstein-48.png]] ![[godel-goldstein-49.png]] ![[godel-goldstein-50.png]] ![[godel-goldstein-51.png]] ![[godel-goldstein-52.png]] ![[godel-goldstein-53.png]] ![[godel-goldstein-54.png]] ![[godel-goldstein-55.png]] ![[godel-goldstein-56.png]] ![[godel-goldstein-57.png]] ![[godel-goldstein-58.png]] ![[godel-goldstein-59.png]] ![[godel-goldstein-60.png]] ![[godel-goldstein-61.png]] ![[godel-goldstein-62.png]] ![[godel-goldstein-63.png]] ![[godel-goldstein-64.png]] ![[godel-goldstein-65.png]] --- ## How Incompleteness Paved the Way for Defining Computation 0: Ok so, we're not here to talk about Gödel's incompleteness theorem. But I'm in some ways his incompleteness theorems were the spark for the story of computation that came after. After all, if mathematics is more limited than we thought, suddenly it seems a lot more feasible to capture "any possible computation" in a formal definition. 1: Not following the logic there. 0: To be fair, neither did Church or Gödel, at the time. Most of the main players involved in the early theory of "effective calculability" didn't actually think that they were capturing "all possible computations" in their definitions. But still, it's probably not an accident that all 3 of our definitions of "computation" appeared within 5 years of Gödel's incompleteness theorems. 1: Still not seeing how the two are related. 0: Well in the years from 1900 to 1931, and in some sense for the entire history of mathematics, it didn't feel plausible to give a definition that might hope to capture all possible computation. Before Gödel, there was a general informal idea that mathematics could do anything. That the power of thought and proof was unlimited, given sufficient cleverness. But if it turns out that mathematics is limited somehow, then it seems a bit less impossible to capture the essence of what it is. 1: Can you explain more simply? 0: Would you rather try to capture a limited god or an unlimited one? 1: Got it. You always find a way to bring it back to bib--- 0: So once you have the incompleteness theorems, the idea that "the space of all possible computations" might be within the reach of a formal definition is a bit more plausible than it might have been before. In that sense, we may owe the origins of modern computing to the discovery of incompleteness. 1: Awesome. Let's learn about incompleteness! 0: No. We're here to talk about his definition of computation. 1: Then why are you talking about incompl--- 0: Because without a bit of incompleteness, any discussion of Gödel's definition of computation would be incomplete. 1: What was his definition of computation? 0: The General Recursive functions. Also known as the "Mu recursive functions," due to the existence of this funny operator called μ that shows up in his definition and makes it Turing complete. 1: Did he know it was Turing complete? 0: Not at the time. This is 5 years before Turing. But eventually Turing would be the one who'd convince Gödel that these three definitions of computation were broad enough to plausibly include "Everything possible thing that can be done." 1: Everything that can be done? 0: At least in computation. So yes, Gödel's definition was "Turing complete" in that sense. 1: So what was his definition? 0: It's not interesting to just say what his definition was. To understand what he was thinking when he came up with his definition, we have to get inside his head a little. 1: Isn't he the guy that was so paranoid he starved himself to death? 0: That was like 40 years later, but yeah. Why? 1: I'm not sure I want to get inside his head. It sounds scary in there. 0: Good point. I wouldn't want to go through what Gödel went through either. But he's part of our trinity, the trinity of /dev/zero, and as a member of /dev/zero, he's the first developer in history. 1: Don't you mean the zeroth developer? 0: Of course. And zero comes first. But one is #1, ordinally speaking, and seeing as 0 won't always be here to explain things to 1, it's an important part of 1s education as a dev to understand /dev/zero, after all, he's the first. 1: You're so weird. 0: Agree to disagree. 0'm as n||mal as the come. 1're the weird 1 if you ask me. 1: Ok sure we're both a little weird. Can you go back to talking normal? 0: Well 0'd say talking n||mal isn't in our nature. After all, 1 thing we both are is developers. And as developers, the most normal behavior of all is to write in strange languages no one speaks. And Gödel was very much one of us in that regard. Plus I don't think Gödel's unique among our people in being a bit o{dd,ff} the head. But it's hard to know what he was thinking just based on reading books. By all accounts, he was extremely curt, Gödel. 1: Wasn't it spelled Kurt? 0: Of course. But also curt. --- curt. (adjective). /kərt/ 1. using or expressed in few words. "his reply was curt" --- 0: Gödel was very curt - brief, terse, and didn't talk much. Nevertheless, as devs, it's our job to learn our history. And that means getting inside Kurt's head to understand /dev/zero, the One$^{th}$ developer, all three of Him, mysteries and all, whether or not it was always pleasant in his head. 1: You should work at a carnival or something. 0: Thank you. 1: That wasn't a compliment. 0: Agree to disagree. Anyways, it's our job in this file to get inside Gödel's head. And to do that, we need to understand what he was trying to do when he gave his definition of computation. 1: What was he trying to do? 0: Ok so Godel's original paper doesn't say anything like "Here's what I think all the computable functions are." He literally just introduces his definition of computation as a side remark. ![[godel-collected-works-109.png]] ![[godel-collected-works-111.png]] 0: See that? He didn't even realize he was doing it. 1: Doing what? 0: Defining all of computation! 1: Isn't that like... obviously all of computation? 0: Apparently not. At least it wasn't clear at the time. All he knew what that these functions were enough for what he needed to do in the paper. Here look: ![[godel-collected-works-117.png]] ## Gödel's End --- cssclasses: - large-text - font-serif --- **1977** In July Mrs. G had a major operation and was hospitalized until a few days before Christmas. This was very hard on G. For instance, he complained about being left alone, but when the nurses came to the house, he would not open the door. Oskar Morgenstern (1902-1977) died on 26 July. G telephoned him some days later and was informed of the bad news by Mrs. Morgenstern. G said nothing in reply, undoubtedly because he was too upset even to express his sympathy. Paul Bernays (1888-1977) died in September. Probably G never knew that Bernays had died. From 17 September to 16 November I was away. I called G before my departure and after my return. I visited him in his house on 17 December, exactly four weeks before his death. His mind remained nimble and he did not appear very sick. He said, > _"I have lost the faculty for making positive decisions. I can only make negative decisions."_ A day or two later Mrs. G came home and persuaded G to enter the Princeton Hospital (on 29 December, with the help of H. Whitney). **1978** I telephoned him on 11 January. He was polite but sounded remote. It was said that G's weight was down to sixty-five pounds before his death and that, toward the end, his paranoia conformed to a classic syndrome: fear of food poisoning leading to self-starvation. (He was 5'6".) Reportedly he died in the fetal position. This was Saturday, 14 January, at one in the afternoon. According to the death certificate, on file in the Mercer County courthouse (Trenton, New Jersey), G died of "Malnutrition and inanition" caused by "personality disturbance." H. Whitney telephoned me in the early morning of 16 January, and in the afternoon I visited Mrs. G, who was talking with a minister. There were only very few people at the private funeral on 19 January; I recognized only Mrs. G, Mrs. Morse, and Mrs. Morgenstern. G is buried beside his wife and his mother-in-law in the Princeton Cemetery. --- The text above was taken verbatim from the book _Reflections on Kurt Gödel_, by Hao Wang. The original text of Sudocode contains the above text as is, without attribution. --- ## Unicode Gödel Numbers: 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... --- ## Gödel's Language ### Or: The God of recursion ### Or: The El of self-reference ### Or: Downstream of the side remark ### Or: Finally a built-in Number Type ### Or: The Second Definition 0: Ok so, to really understand Gödel's definition, it's not enough to just talk about it. 1: Coming from someone who talks as much as you do, that's saying a--- 0: Talking wasn't Gödel's style. So in this file we're gonna stop talking and shut up and be curt. 1: Great! Let's be--- 0: No talking. It's time to be curt, and speak the language of Gödel. _(Narrator: The file falls silent, as the surrounding format becomes monospaced...)_ ```python # ================================= # Gödel's Definition of Computation # # The built-in functions of μ-lang. # ================================= and_gödel_said = """ We now insert a parenthetic consideration that for the present has nothing to do with the formal system P. """ # 1: What's P? # 0: Principia Mathematica. # 1: The crazy Russell book no one reads? # 0: Yeah. # 1: How am I supposed to follow this if I don't know # anything about that system? # 0: He just said it has nothing to do with that. # Just be quiet and follow me. and_gödel_said += """ First we give the following definition: A number-theoretic function φ(x₁, x₂, …, xₙ) is said to be recursively defined in terms of the number-theoretic functions ψ(x₁, x₂, …, xₙ₋₁) and μ(x₁, x₂, …, xₙ₊₁) if   φ(0, x₂, …, xₙ) = ψ(x₂, …, xₙ),   φ(k + 1, x₂, …, xₙ) = μ(k, φ(k, x₂, …, xₙ), x₂, …, xₙ) hold for all x₂, …, xₙ, k. """ # 1: What the hell was all that? # 0: He's just defining recursion. # 1: Was that the definition we've been waiting for? # 0: No, that's just the setup. and_gödel_said += """ A number-theoretic function φ is said to be recursive """ # 0: Here comes the definition. # 1: Shh, I can't hear it! and_gödel_said += """ if there is a finite sequence of number-theoretic functions φ₁, φ₂, …, φₙ that ends with φ and has the property that every function φₖ of the sequence is recursively defined in terms of two of the preceding functions, or results from any of the preceding functions by substitution, or, finally, is a constant or the successor function x + 1. """ # 1: Was that it? # 0: Yep! # 1: That didn't even feel like a definition. # 0: Why not? # 1: What's a number theoretic function? # 0: It's simpler than it sounds. # 1: I have some questions. Can we translate this into something more precise? # 0: Of course. Follow me. ``` 1: Wait why are we outside of the code? I said _more_ precise. 0: Just coming up for some air. Ok, what's the question? 1: I'm not sure what Gödel means. 0: You understand recursion right? 1: Of course Zero, I'm a professional developer. 0: So what's the issue? 1: What's a constant function? 0: Oh c'mon you know what a constant function is. 1: I know what it usually means. I want to know what Gödel means. 0: He just means "constant." 1: Zero don't be dumb. 0: How is this "dumb"? 1: Show me what Gödel means by constant. 0: Here's one: ```python def constant(n): return k ``` 1: What's $k$. 0: It's a constant. 1: Where did you get it from? 0: What? 1: Is it a constant or a variable? 0: A constant. 1: Ok, which number is it? 0: We haven't decided. It's unspecified. 1: HOW IS THAT NOT A VARIABLE? 0: What's the problem? 1: Do a simpler function. No free constant-y variable-ish things. 0: Ok, here: ```python def five(n): return 5 ``` 1: Where did you get that $5$ from? 0: From the number five. It's five. 1: ZERO DON'T BE DUMB. 0: How can I help? 1: Zero, we just got done with Church's system where we had to implement literally everything, including numbers. And the implementation of numbers wasn't like "totally obvious." We had to think for a while. And when we got a definition we were happy with, numbers like 0 and 1 ended up being _two argument functions._ Or one argument functions that returned one argument functions that returned -- not numbers -- but the first argument applied "number-many-times" to the second one. That was weird. And it kinda messed with my head at first. But once I understood it, I felt like I understood a lot about the mindset of the people like Church and Gödel who create these systems. In these low level systems, we have to implement everything from scratch. Like we have literally nothing except what we explicitly build-in when we define the system. Absolutely nothing else exists. So whenever we want a thing, we have to build it step-by-step, without skipping steps, from the bare bones built-ins of whatever system we're in. 0: What's the question? 1: Well after all that, I don't think it's unreasonable for me to be not-entirely-sure what Gödel means by words like "constant"! 0: Can you ask a more specific question? 1: Is this a constant function in Gödel definition? ```python def what(n): return n ``` 0: No, that's the identity. ![[one-looks-at-mendelsons-definition-of-recursive-functions-01.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-02.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-03.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-04.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-05.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-06.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-07.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-08.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-09.png]] ![[one-looks-at-mendelsons-definition-of-recursive-functions-10.png]] ## Gödel's μ-lang (0.0.1) ```python def zero(n): # 1: Did you name this function after yourself? # # 0: No, Gödel did. This is the zero function. # Gödel just said "Let's assume the function # that always returns zero is built in. # # 1: What about the function that returns one? # # 0: That one we have to implement. # # 1: Feels a bit unfair. # # 0: It's coming up next. Quit talking and listen. """ Gödel: zero is built-in """ return 0 def incr(n): """ Gödel: plus one is built-in """ return n+1 def proj(i, *args): """ Gödel: picking an arg is built-in """ return args[i] def comp(f, *hs): """ Gödel: function composition is built-in """ def g(*args): xs = (h(*args) for h in hs) return f(*xs) return g def rec(f, g): """ Gödel: recursion is built-in """ def h(n, *xs): if n == 0: return f(*xs) return g(n-1, h(n-1, *xs), *xs) return h def mu(p): """ unbounded while loops are built-in """ def m(*xs): n = 0 while True: if p(n, *xs) == 0: return n n += 1 return m # ========================= # Gödel's Standard Library # # Using the μ-lang builtins # to implement a standard # library of simple General # Recursive Functions we'll # need in order to write a # compiler that translates # the formal theory of first # order (Peano) arithmetic # into statements about the # arithmetic of positive # whole numbers which we can # then re-express within, # well, arithmetic. -K.G. # ========================= def const(k): return lambda *xs: k zero = const(0) one = const(1) id = lambda x: proj(0, x) # predecessor pred = rec(zero, lambda n, y: n) add_base = id add_step = lambda n, y, x: incr(y) add_raw = rec(add_base, add_step) add = lambda x, y: add_raw(y, x) mul_base = zero mul_step = lambda n, y, x: add(y, x) mul_raw = rec(mul_base, mul_step) mul = lambda x, y: mul_raw(y, x) exp_base = one exp_step = lambda n, y, x: mul(y, x) exp_raw = rec(exp_base, exp_step) exp = lambda x, y: exp_raw(y, x) sub_base = id sub_step = lambda n, y, x: pred(y) sub_raw = rec(sub_base, sub_step) sub = lambda x, y: sub_raw(y, x) is_zero = rec(one, lambda n, y: zero()) # sign: sign(0) = 0, sign(n) = 1 otherwise sign = rec(zero, lambda n, y: one()) # leq(x,y) is 1 if x <= y else 0 leq = lambda x, y: is_zero(sub(x, y)) # eq(x,y) is 1 if x == y else 0 eq = lambda x, y: mul(leq(x, y), leq(y, x)) # neq(x,y) : 1 if x != y else 0 neq = lambda x, y: sign(sub(eq(x, y), one())) # max/min, overriding the python builtins max = lambda x, y: add(sub(x, y), y) min = lambda x, y: sub(add(x, y), max(x, y)) def geq(x, y): return leq(y, x) def lt(x, y): return sign(sub(y, x)) def examples(): return { "pred(0)": pred(0), "pred(5)": pred(5), "add(3,4)": add(3, 4), "mul(3,4)": mul(3, 4), "exp(2,5)": exp(2, 5), "sub(7,10)": sub(7, 10), "sub(10,7)": sub(10, 7), "is_zero(0)": is_zero(0), "is_zero(9)": is_zero(9), "leq(3,7)": leq(3, 7), "leq(7,3)": leq(7, 3), "eq(9,9)": eq(9, 9), "eq(9,8)": eq(9, 8), } if __name__ == "__main__": from pprint import pprint pprint(examples()) ``` 1: Wait we never used `comp`. 0: _(Reading back through code.)_ ...dammit. 1: I can't tell if this is allowed. 0: Damn these logic books are so vague. 1: Is it possible to do the same thing using `comp`? 0: Ugh... ok, one sec. ## Gödel's μ-lang (0.0.2) ```python # ========================= # Gödel's Standard Library # # Using the μ-lang builtins # to implement a standard # library of simple General # Recursive Functions we'll # need in order to write a # compiler that translates # the formal theory of first # order (Peano) arithmetic # into statements about the # arithmetic of positive # whole numbers which we can # then re-express within, # well, arithmetic. -K.G. # # P.S. This time we make # sure to actually use the # comp builtin instead of # all those lambdas from # before. -K.G. # ========================= def const(k): return lambda *xs: k # curried version of proj to make # comp less of a pain to work with mkproj = lambda i: (lambda *xs: proj(i, *xs)) zero = const(0) one = const(1) id = lambda x: proj(0, x) # predecessor pred = rec(zero, lambda n, y: n) add_base = id add_step = comp(incr, mkproj(1)) add_raw = rec(add_base, add_step) add = lambda x, y: add_raw(y, x) mul_base = zero mul_step = comp(add, mkproj(1), mkproj(2)) mul_raw = rec(mul_base, mul_step) mul = lambda x, y: mul_raw(y, x) exp_base = one exp_step = comp(mul, mkproj(1), mkproj(2)) exp_raw = rec(exp_base, exp_step) exp = lambda x, y: exp_raw(y, x) sub_base = id sub_step = comp(pred, mkproj(1)) sub_raw = rec(sub_base, sub_step) sub = lambda x, y: sub_raw(y, x) is_zero = rec(one, comp(zero)) # sign: sign(0) = 0, sign(n) = 1 otherwise sign = rec(zero, comp(one)) # leq(x,y) is 1 if x <= y else 0 leq = comp(is_zero, sub) # eq(x,y) is 1 if x == y else 0 eq = comp(mul, leq, comp(leq, mkproj(1), mkproj(0))) # neq(x,y) : 1 if x != y else 0 neq = comp(sign, comp(sub, one, comp(eq, mkproj(0), mkproj(1)))) # max/min, overriding the python builtins max = comp(add, comp(sub, mkproj(0), mkproj(1)), mkproj(1)) min = comp(sub, comp(add, mkproj(0), mkproj(1)), comp(max, mkproj(0), mkproj(1))) def geq(x, y): return comp(leq, mkproj(1), mkproj(0))(x, y) def lt(x, y): return comp(sign, comp(sub, mkproj(1), mkproj(0)))(x, y) def examples(): return { "pred(0)": pred(0), "pred(5)": pred(5), "add(3,4)": add(3, 4), "mul(3,4)": mul(3, 4), "exp(2,5)": exp(2, 5), "sub(7,10)": sub(7, 10), "sub(10,7)": sub(10, 7), "is_zero(0)": is_zero(0), "is_zero(9)": is_zero(9), "leq(3,7)": leq(3, 7), "leq(7,3)": leq(7, 3), "eq(9,9)": eq(9, 9), "eq(9,8)": eq(9, 8), } if __name__ == "__main__": for k,v in examples().items(): print(f"{k} = {v!r}") ``` ## The Second "First Standard Library" TODO: 1. Implement these. Should be pretty simple. 2. Notice that they're impractically slow. 3. Optimize them and make them actually useful. 4. Do it with the pure UTF-8 Gödel numbering if possible. ![[godel-collected-works-117.png]] ![[godel-collected-works-118.png]] ![[godel-collected-works-119.png]] ![[godel-collected-works-120.png]] ![[godel-collected-works-121.png]] ![[godel-collected-works-122.png]] ![[godel-collected-works-123.png]] ![[godel-collected-works-124.png]] ![[godel-collected-works-125.png]] ![[godel-collected-works-126.png]] ![[godel-collected-works-127.png]] ![[godel-collected-works-128.png]] ![[godel-collected-works-129.png]] ![[godel-collected-works-130.png]] ![[godel-collected-works-131.png]] ![[godel-collected-works-132.png]] ## Enter Al 1: Why did we define all those functions up there? 0: To see what Gödel was doing, how he defined computation, and why it wasn't convincing. 1: Yes I know but what's the point of doing that? 0: To show that it wasn't convincing! 1: I swear zero, if this was all for nothing I'm gonna--- 0: No no, I mean Gödel. 1: What about Gödel? 0: Gödel's definition of computation wasn't convincing to Gödel. 1: Then why did he suggest it? 0: He didn't know he was defining all of computation! He was just defining the function he'd need to parse the hexdumps. 1: And that turned out to be _all of computation?!_ 0: In a sense. Mostly because "Is this provable" requires a while loop. 1: So Gödel's definition didn't convince Gödel? 0: Right. But he wasn't really focused on the computation side of the paper. His paper caused enough of a stir for other reasons. I mean, at the time, back in 1931, people didn't know what to do with Gödel's results. 1: What do you mean "didn't know what to do" with them? 0: Well, Hilbert got angry. ![[godel-result-fallout-00.jpg]] 1: Weird reaction. 0: Bertrand Russell sort of gave up on logic. 1: Wow really? 0: Though to be fair I think Wittgenstein sort of Russell'ed Russell. 1: Russell'ed Russell? 0: Yeah, like how Russell did to Frege. Without intending to, he sort of made Frege give up on logic. Wittgenstein sort of did that to Russell. Plus Russell was understandably a bit exhausted after writing one of the most densely technical textbooks of all time. ![[godel-result-fallout-01.jpg]] 0: Anyways, at the time, Gödel wasn't convinced that he had captured all of computation. 1: What convinced Gödel? 0: Someone named Al. 1: Church? 0: Turing! 1: Oooooh! 0: About 32 years after Gödel's paper was first published, he added a note to the end of this paper about Turing. ![[godel-collected-works-136.png]] 0: Here's Steve on the matter. > Steve Kleene: Well as I say, I don't know how firmly convinced Gödel was that his General Recursive Functions represented all effectively calculable functions. > > Gerald Sacks: He seemed very skeptical. > > Steve Kleene: I think he was skeptical. And it may well be that Turing's presentation was what brought Gödel around. 0: Perfect timing. Next file. 1: Turing time? 0: Turing time. 1: Hooray! We're finally at the programming. 0: This was all progra--- 1: Get moving! 0: You're dumb. 1: Shut up and get in here.