## Naming Things 0: Once upon a time, there was a guy named Sam. 1: Ooh I love story time. 0: Sam had an unusual family tree. As a child, during that earliest stage of life when we're looking around the world for the first time and learning what things are called, Sam learned the following: 1. Your Name: Sam 2. Your Father: Alonzo Church 3. Your Brother: Alonzo Church 4. Your Grandfather: Alonzo Church 1: That's a lot of Alonzo Church. 0: For real. And Sam wasn't Alonzo Church. He was the only one who wasn't. 1: Must be rough to get excluded from being Alonzo Church when everyone you know gets to be that. 0: Exactly. So when it came time for Sam to have a son, he pulled a fast one on his brother -- the first born -- and added an item of his own to own the family's family tree. So now, thanks to Sam, the family tree looked like this. 1. Your Name: Sam 2. Your Father: Alonzo Church 3. Your Brother: Alonzo Church 4. Your Grandfather: Alonzo Church 5. Your Son: Alonzo Church 1: Damn Sam. That's cold. 0: "Take that, Alonzo Church," I imagine him saying to his brother Alonzo Church, when he named his son Alonzo Church. 1: Did he actually say that? 0: No idea. But eventually Sam's son would have a son of his own. And he called--- 1: I wonder what he's gonna call it. 0: Drumroll. 1. Your Name: Sam 2. Your Father: Alonzo Church 3. Your Brother: Alonzo Church 4. Your Grandfather: Alonzo Church 5. Your Son: Alonzo Church 6. Your Grandson: Alonzo Church 1: Why are we talking about this? 0: Because trinities are known to be full of mysteries. And Alonzo Church is the first member of our trinity. 1: All five Alonzo Churches are members of the trinity? 0: No. Just one. 1: Which one? 0: Sam's son. The one who wasn't supposed to be Alonzo Church. 1: I'm glad it was that one. He seemed like the underdog. 0: Alonzo Church would go on to do a lot of things, but he's most well known for one thing. 1: What one thing? 0: For inventing the first programming language. 1: Woah seriously? 0: Before computers. Before the field even had an agreed upon definition of "computation." 1: What did it run on? 0: Paper. 1: Woah. 0: It was a strange programming language with only one type. 1: Only one type? 0: Only one type. In terms of built-in types, the language has no numbers. 1: No numbers?! 0: No booleans. 1: No booleans?!?! 0: No `if` or `for` or `while`. 1: This language sounds insane. 0: There's only one built-in type. 1: Is it Alonzo Church? 0: Nope. But Alonzo Church had a lot of experience with systems where everything is one type. 1: Like his family? 0: Yep. So when he grew up and went into the foundations of mathematics, and even more deep into the foundations of logic itself, he came up with a system where everything is functions. 1: Numbers are functions?! 0: Numbers are functions. 1: Booleans are functions?!?! 0: Booleans are functions. 1: Such an Alonzo Church thing to do. 0: It's not as crazy as it sounds. It's actually an incredibly powerful idea. He just didn't realize that at the time. 1: HE didn't realize that? 0: Nope. No one did. 1: Can I have some more details? 0: Of course. Let's go take a tour. ## The Collected Works of Alonzo Church ![[church-01.png]] 1: Woah you weren't just making that up? 0: Of course not. I would never lie to you. ![[church-03.png|400]] 1: Hey there's another one! 0: Told ya. They're all over the place. ![[church-02.png]] 1: Damn look at that handsome guy. 0: For real. Could have gone into Hollywood. 1: Why didn't he? 0: Well he's a foundational person. So naturally, he went into foundations. ![[church-04.png]] 0: Did his dissertation on the Axiom of choice. 1: What's that? 0: Well remember, by this time, it's been about 50 years since Cantor, and almost 30 years since 1900 when Hilbert announced his list of problems. So there's been a reasonable amount of work on the foundations of mathematics since then. 1: Why aren't we including those people in "The foundational people"? 0: Good point. Some of them probably deserve to be included too. But every story has to start somewhere, and for a bible on the history of computing, Church is a pretty good place to start. 1: What was going on in the 30 years before this? 0: Well there had been some work on axiomatic set theory. Mostly on a system called ZFC, or Zermelo Fraenkel (with the Axiom of) Choice. That system is still considered the "official" foundations of mathematics by mathematicians today, but it's never really been _used_ as foundations in any real sense. 1: What do you mean "used as foundations." 0: I mean nobody uses it. 1: What?! 0: Or almost nobody. They usually just talk about it or assert that ZFC proves such-and-such. It's extremely rare to see mathematicians actually working _within_ ZFC as a formal system. 1: That doesn't seem so bad. I mean we programmers don't really write in machine code, like ever. But it's sort of the "foundations" of any language that compiles to it, in a sense. 0: No no, I mean even books about ZFC don't work within ZFC. 1: WHAT?! 0: Here I'll show you. ## Standard "Foundations" > _These axioms are the official doctrine - Remarkably, this is not just the official doctrine for set theory, it turns out that this is the official doctrine for mathematics! - Very few people seem to have a problem with that which I find quite remarkable._ > -NJ Wildberger ![[zfc-hirst-01.jpg]] 1: "These hell torments"? 0: Yeah that's axiomatic set theory. 1: What's this book about? 0: Axiomatic set theory. 1: What?! 0: That's the point. No one within mathematics really "likes" ZFC. Even set theorists who chose axiomatic set theory as their favorite area to focus on. Now to be fair, that book isn't entirely about ZFC. But a third of it is devoted to set theory and "standard foundations," and the guy who wrote this part is a super competent logician. Intensely smart guy named Jeff Hirst. Not intending to single out the author. This is just sort of how ZFC is viewed. That "paradise" is pretty clearly the "paradise Cantor created" that David Hilbert's always quoted talking about. That's informal set theory, the kind that uses standard mathematical reasoning and eventually leads to paradoxes. And "these Hell torments" are axiomatic set theory. 1: And this is a book _about axiomatic set theory?_ 0: Yep. At least this part is. This book is extremely good at choosing quotes for section headings. A lot of the quotes in this section are about hell. Or L, which is a thing Gödel invented in the course of studying, well, axiomatic set theory. ![[zfc-hirst-07.jpg]] 1: Damn, seems like mathematicians really don't like axiomatic set theory. 0: Yeah, there are a bunch of dog whistles throughout this part about how mathematics probably needs some new foundations. Can't disagree. ![[zfc-hirst-10.jpg]] 1: Why not just come up with new axioms? 0: People have. This guy Harvey Friedman in the image below kicked off a revolution that completely changed our understanding of what mathematics is. Turns out most of mathematics is equivalent to one of five sentences. But mostly nobody noticed. At least not many mathematicians. ![[zfc-hirst-13.jpg]] 1: Most of mathematics is WHAT?! 0: Equivalent to one of five sentences. 1: HOLY F--- 0: Yeah I know. 1: What sentences? 0: Not now. We'll get there eventually. We're still at Church. 1: Wait though, how did most mathematicians not notice that most of their field is one of five sentences? 0: Mathematicians mostly don't pay a lot of attention to foundations. 1: Jesus. 0: And because of that, ZFC sort of ended up as an impotent figurehead type of ruler. 1: Impotent figure what? 0: Like a king with no power. Everyone points to ZFC and says "That's the foundations," but no one likes it, no one uses it, and it's basically just been sitting there for a century plus with a big crown on that says "I'm the foundations of mathematics and mathematics is the foundation of everything." That's been changing recently though. 1: How so? 0: We'll get there eventually. For now, just notice that the following is pretty typical of how mathematicians "use" ZFC, even in books that are supposed to be "about" axiomatic set theory. ![[zfc-hirst-04.jpg]] 0: Feels like normal math right? 1: I guess? Not really sure. 0: That's the point. It's mostly words. They're not actually working inside the formal system. They're just sort of writing pseudo-code and English that talks about what the proof would be like if we actually did it. 1: Isn't that what we're doing? 0: Exactly! Here's another example. ![[zfc-hirst-02.jpg]] 1: "We could"? 0: Yep. That's the standard mathematical approach to ZFC. They don't use it. They call it "foundations," but they basically always keep it at arms length. Even the logicians and set theorists. There are a few solid exceptions though. ![[zfc-hirst-03.jpg]] 0: Mendelson and Kleene do the formal stuff. 1: Who are they? 0: Mendelson is the book we saw earlier in /opt/art. 1: No way! The bit with the "hell code"? 0: Exactly. That's Mendelson's _Introduction to Mathematical Logic_. It's a pretty approachable introduction to the actually formal side of foundations. 1: The second book sounds fun! 0: Kleene? 1: Yeah! I mean if that "hell code" book was the easy one, I can't imagine what the one for "readers with a frighteningly technical bent" is like. Makes me want to read it. Who's Kleene? 0: Church's best student. 1: No way! 0: Which brings us back to Church. ![[zfc-hirst-06.jpg]] 0: We'll meet Kleene pretty soon. ![[zfc-hirst-14.jpg]] 0: And yeah, the "frighteningly technical" book is also called Kleene's Blue Bible. ![[zfc-hirst-15.jpg]] 1: What's so frightening about it? 0: It's code. 1: What's so frightening about code? 0: I mean, the book is from 1952, based on work from the 1930s and 1940s. So there's no "computer code" in there in the usual sense. 1: So how's it code? 0: Because Kleene doesn't skip steps or hand-wave or say "it can be shown." He works inside the formal system. He adds a ton of documentation -- English explanations of what's happening -- but the way he behaves as the author of that book is exactly how you'd behave if you were a programmer. 1: I am a programme--- 0: I know. But that's an extremely unusual way to behave in a math book, when you're the author. I mean he behaves as if everything he claims actually has to be implemented. He doesn't write as if he's trying to convince a human mind where you can just handwave or say "obviously" or "exercise for the reader." He writes as if he's trying to convince a machine, and then documenting heavily so humans can read the code too. Kleene was pretty clearly the first programmer. 1: Wait, I thought the first programmer was Church and Gödel and Turing? 0: Exactly. They're the first. And⁰ Kleene is the glue. Like this. $3 = \{ 0, 1, 2 \}$ 1: Do you try to be confusing on purpose? 0: What's confusing about that? 1: Everything? 0: Ok so, in Cantor's set theory, the number N is defined to be the set of all the natural numbers less than it. So 3 is the set containing 0, 1, and 2. 1: That's weird. But ok. 0: And Kleene is the curly braces and commas. The bits that hold it all together and make the set be one thing. He's the glue. 1: That feels like a stretch. 0: It's not. The best way to explain Kleene is to get back to Church. So Church's PhD dissertation was about ZFC. Standard set theory. Specifically the C. The Axiom of Choice is a sort of "constructor" for sentences that look like $\exists x P(x)$ that doesn't require you to provide an example of an $x$ that makes it true. 1: I know what a constructor is. What's the $\exists$ thing? 0: That means "There exists." Think of the Axiom of Choice as a function that you can call in standard mathematics. That function returns a sentence that says "Something exists." And you're allowed to take that sentence that says "Something exists" and use that sentence in your proofs. It's controversial because you can call that function without passing in an example of an actual Something that makes the sentence true. 1: I'm like 50% following. Rephrase? 0: It lets you prove that something exists without requiring you to give any examples. 1: WHAT?! 0: Yep. That's the C in ZFC. It's part of standard foundations. The machine code of mathematics. So Church writes his PhD dissertation being like "Maybe we can delete this code guys, it's kinda sketchy." ![[church-38.png]] 1: Ok I'm not following the mathematics but that definitely sounds sketchy. 0: So fast forward, Church goes to work on foundations. Real foundations. The kind where you actually have to construct or compute something to show it exists. Stuff that feels a lot more like programming. 1: Show me. 0: Ok so here's one of his early papers. If you read it, he's clearly bothered by "free variables" for some reason. But the sense in which he's using the term "free variables" means something a bit more like "information that we didn't include in the formal system." The bits we have to add in English after the symbols. ![[church-20.png]] 1: "Without the addition of verbal explanations." Love it! 0: That's what he's working on. Getting all the vagueness and natural language out of mathematics, at least in principle. 1: Y'know it's weird. I sort of assumed mathematicians solved that problem like... thousands of years ago. 0: Nope! Mathematics has always been a mixture of formal and informal. Church wants to see if it's possible to fully specify all the missing bits. If you read the part below closely, what he's calling "free variables" are really more like _type variables._ Notice how he starts with the sentence $a(b+c) = ab + ac$ and says the $a$, $b$, and $c$ are "free variables." Then he shows what it would mean to fix that sentence. ![[church-21.png]] 1: What's the bit with the $R(a)$s and the $\supset_{abc}$ ? 0: I think the notation is based on some old stuff Peano did. But it's not complicated. 1: Looks complicated. 0: Read it. 1: "Where $R(x)$ has the meaning '$x$ is a real number' and"... oh nevermind I feel dumb. 0: So what's Church saying here? 1: He's just saying we should add types to the variables so we know what kind of thing they are. 0: Exactly. And that tendency carried through from the 1930s to modern functional programming and why their languages tend to be strongly typed. 1: Seriously? 0: Yep. Functional programming languages are all descended from Church's first language. 1: The language where every type is Alonzo Church? 0: Functions, but yeah exactly. 1: Nice! Is that language in this paper? 0: Sort of... 1: What do you mean "sort of"? _(Narrator: 1 flips ahead through the paper)_ ![[church-collage-1.jpg]] 1: Holy F--- 0: Yeah. 1: Why does it hurt my eyes? 0: Because you skipped ahead. 1: This is traumatizing. I changed my mind. I don't think I'm cut out for this "frighteningly technical" stuff after all. 0: Don't worry, a lot of that turned out to be inconsistent. 1: What? 0: Here look. About halfway through the stuff you just flipped through, Church shows up and goes "Ok guys, so, this is awkward. Um, that first formal system from a little while back was inconsistent." ![[church-27.png]] 1: Inconsistent how? 0: Like totally broken. You can prove anything. 1: Hahahahahaha all that hell math for nothing? 0: Not for nothing! Church ends up fixing the bug by adding "types." Which after all was sort of the thing he was on about in the introduction to the first paper. 1: How do you do all that hell math and then realize the whole system is broken? 0: One of his students found the bug. But then he and the student go on to do some pretty amazing stuff together. 1: Who's the student? 0: Kleene. 1: Same guy? 0: Same guy. ![[church-37.png|400]] 1: This is even more "frighteningly technical" than the hell math from earlier. 0: Definitely. Kleene's way easier to read than this, in my opinion. 1: What's the point of all this? I mean if we're gonna be reading and writing this level of hell math there'd better be a good reason. 0: Ok well remember how the Axiom of Choice lets you prove something exists without actually, like, computing it or constructing it? 1: Yeah that seemed like cheating. 0: Ok so the point of the hell math above was that Church had gotten interested in how to define "computability." Back then they called it "effectively calculable" or "an effective procedure." But it just meant "Anything you can actually DO without cheating like how the Axiom of Choice cheats." ![[church-06.png]] 1: When are we gonna get to the programming? 0: Right now. 1: Really? 0: Really. Read this next part carefully. ![[church-15.png]] 1: Didn't he start by saying "We need to get rid of free variables" in the other paper? 0: Yeah. 1: But he just introduced free variables into his system. 0: Good catch. He'll get rid of them soon. That's what the lambda is for. 1: It would help if there was more motivation. 0: Yeah, reading Church is sort of a joy and a pain in the ass at the same time. But this funny $\{F\}(X)$ notation is just a reverse-abbreviation for $F(X)$. 1: What are the curly braces for? 0: In case you want to put the implementation of the function in there instead of just its name. 1: Implementation how? 0: That's what the lambda thing is doing. Same lambda as in modern programming languages. 1: OH, no way. ![[church-16.png]] 1: Ok I sort of get this now. So this is just lambdas? Like "lambda" lambdas? 0: Yep. 1: No numbers? No booleans? 0: Not by default. We have to implement those from lambdas. 1: How do you implement numbers using lambdas? 0: Weird idea right? Here's one implementation. They're called Church numerals. ![[church-18.png]] 1: What's going on here? 0: The number 1 is a function that takes two variables. Then it calls the first variable passing the second. 1: Excuse me? 0: The number 2 is the same idea, but it calls the first variable twice. 1: I'm so confused. 0: Here I'll show you. In python it would look like this: ![[church-numerals-in-python-1.png]] 0: Make sense yet? 1: No. 0: Wait, I should correct that. There aren't really any two argument functions in Church's system. It should be more like this. ![[church-numerals-in-python-2.png]] 1: That's worse. 0: Oh and zero would be this. ![[church-numerals-in-python-3.png]] 1: This is insane. 0: Would it make more sense if I wrote it like this? ![[church-numerals-in-python-4.png]] 1: What are `verb` and `noun`? 0: Think of it like a crank. 1: That doesn't help. 0: I mean "three" is the idea "turn the crank three times." 1: The only crank I see around here is you. 0: Ok what's "three" to you? 1: What's three? 0: Yes, explain the concept to me. 1: Three is, well, thr--- 0: You can't say "three" in the definition. 1: Ok, three is any time there are this many of something: $\circ \circ \circ$ 0: Does it matter what sort of things they are? 1: No. It's three if there's that many of anything. 0: Ok, what if you want to encode "three" in a language that only has verbs. 1: What do you mean? 0: Like Church's lambda calculus. Everything is functions. How do you encode three? 1: Put three functions next to each other? 0: How do you put them "next to" each other? We don't have lists or tuples yet. 1: Oh right. 0: Or strings, so string concatenation won't work either. 1: So what do we do? 0: Well, what do we have? 1: Functions? 0: Right. 1: What can we do with functions? 0: Let's go see what Church says. ![[church-19.png]] 1: What does this say? 0: It just says "We can plug stuff into functions and vice versa." 1: What's vice versa? Unplug stuff out of functions? 0: Exactly. 1: I'm not sure what I meant by that. What did you mean? 0: What's the opposite of turning `λx: x²` into `3²`? 1: Turning `3²` into `λ3: 3²` for any value of `3`? 0: Exactly. 1: I'm not sure what I meant by that. What did you mean? 0: I mean the 3 becomes a variable there. 1: I don't see Church doing that anywhere in this picture. 0: But that's the idea. He's just saying you can plug stuff into functions, and you can unplug things out of expressions to make functions. Nothing that any programmer hasn't done a thousand times. This isn't a deep thought. It just turns out to be deep as a non-thought. 1: Do you _have_ to talk like this?  0: Like what? 1: What do you mean it turns out to be deep as a "non-thought"? 0: Well Church himself didn't actually think this was enough to capture ALL of computation!  1: He didn't? 0: Hell no! You'd have to be insane to think that this was ALL of computation the first time you see it. I mean Church _came up_ with this idea and even HE didn't think that.  1: How do you know? 0: From Steve. 1: Who's Steve? ## The First Programmer > John Crossley: What did you do Steve? When you first started learning logic. You didn't have books did you? > > Steve Kleene: We didn't have books. > > Gerald Sacks: You had _Principia Mathematica._ > > _(Everyone laughs)_ > > Steve Kleene: Well, I never read _Principia_. Of course I thumbed it a little bit... Rosser I guess started his logic that way... But I learned logic by learning Church's system which was subsequently proved inconsistent. > > _(Everyone laughs)_ > > Steve Kleene: And y'know, it all consists of abstract lambda definability. And uh, and it was only after I got my degree that I really began to read much of the litchrachoar. 1: What's "litchrachoar"? 0: Sorry, that's "literature." 1: Did he spell it like that? 0: No, this is an old audio recording. 1: So you spelled it like that? 0: I wanted to capture his accent. 1: Well don't. 0: Ok. Just imagine it. He's got a charming sort of unpretentious midwest thing going on. > Steve Kleene: It was only after I got my degree that I really began to read much of the literature. Uh let me see. Hilbert Bernays, didn't the first volume of that appear in 1934?... Hilbert Bernays was around... I never read Lewis and Langford. 1: This is Church's student? 0: Yep. 1: The one who that book called "frighteningly technical"? 0: That's him. 1: Doesn't seem too frightening so far. 0: How so? 1: Well he never read that one book, or that other one. Said he didn't read much of the literature during school. And you said he's got an unpretentious vibe. Can't be that frightening. 0: And he learned logic from a system that ended up being inconsistent. 1: So? 0: Well I imagine that sort of thing hammers it into a person that most of what we say about logic is wrong. 1: Not following. 0: The principle of explosion and all that. In standard logic, we always say a single contradiction makes the whole system useless. But it wasn't useless. 1: Wasn't useless how? 0: Well, Steve learned logic from it. 1: What system was that again? 0: Church's first attempt at the lambda calculus. Turned out to be inconsistent. And that means this Kleene guy, easily one of the best logicians of the 20th century, learned logic from an inconsistent system. So it can't have been entirely useless. 1: How did Church figure out his system was inconsistent? 0: From Kleene. 1: Damn. 0: And a friend. That guy from earlier called Rosser who actually read Principia Mathematica. 1: What's Principia Mathematica again? 0: That's Bertrand Russell's book. 1: The paradox guy? 0: Yeah. It's not super readable. > Steve Kleene: And \[I read\] a lot of papers... _(Pauses.)_ For instance by Gödel. The first thing we knew of Gödel's paper was one time the mathematics colloquium speaker was gonna be von Neumann. And of course von Neumann had lots of things of his own to talk about but instead of that we got him there and found out he was telling us about Gödel's 1931 results. > > Someone: This was at Princeton? > > Steve Kleene: This was at Princeton and it was in the Fall of 1931. And whether he had the paper itself or not I don't know... > > C. C. Chang: Was this the first you'd heard of Gödel? > > Steve Kleene: When we went into this meeting was the first that any of us heard of Gödel. Church was teaching a logic course, Rosser and I were among the students, it was the first that any of us had heard of Gödel. I don't know whether Church was aware of Gödel's 1928 paper on completeness, he never gave it in class, because I... I never had the classical form of the propositional or predicate calculi in my coursework, I learned them for myself afterwards. > > Steve Kleene: So as soon as we heard the lecture, the paper was available. We hadn't noticed it, y'know, we didn't go looking at every journal that came into the library to search it through for papers that would interest us, maybe we should've but we didn't, so of course we went and we read the paper right off. > > Steve Kleene: Church was convinced that there were sufficient differences in the way logic was formulated in his system that it would escape the theorem that you couldn't prove its completeness in the system itself. _(Pauses)_ And of course he was right. > > _(Everyone laughs)_ 1: Why did everyone laugh there? 0: Church was right, but for the wrong reasons. He thought his system would be "good enough" to avoid Gödel's theorem and be complete anyway. Turns out early lambda calculus was complete, it could prove its own consistency, because it was inconsistent and could prove anything. 1: Logic is trippy. --- TODO: Clean this up. TODO: 6:50. Church didn't think it would be possible to implement predecessor in lambda calculus. Kleene realizing how to implement predecessor at the dentist. TODO: 7:15. > Steve Kleene: So there was no idea at the beginning that this was going to be all effectively calculable functions. TODO: 7:30. > Steve Kleene: I kept taking it as a challenge and everything I tried I could work. > Steve Kleene: It was an unexpected fallout that this could represent all effectively calculable functions. > Steve Kleene: The basic work was done between January 1932 and the next 5 or 6 months. > Steve Kleene: Everything I tried, every kind of function I tried to define, every kind of effective operation that I tried to parallel by lambda definability, I probably knocked off within the first 5 months. > Steve Kleene: For us the first concept of lambda definability was after the fact, after having formulated the notion of lambda definable functions as simply the ones for which you could find formulas in this symbolism. And discovering that everything you thought of that you wanted to prove lambda definable you could!... But it was Church, I have to give the credit to Church, I can't take it myself, he said "Y'know, don't you think maybe we've really got ALL the effectively calculable functions?" 0: He's being generous. 1: To Church? 0: Extremely generous. 1: What do you mean? I thought Church was one of the giants of this whole field. 0: He was. But even Church knew how incredible Kleene was. And Kleene gets ways less credit for all this than he deserves. Dude was clearly the first programmer. I mean sure, Church wrote the first language, Gödel wrote the first compiler, and Turing made what was arguably the first hardware design, but by that same standard, Kleene made: - Wrote the first standard library. - Found the first critical vulnerability (λ calculus inconsistency). - First to have contact with all three of the above and to demonstrate their equivalence. - First to clean up and popularize the ideas in his (frighteningly technical) _Introduction to Metamathematics_. 1: What do you mean "first standard library"? 0: Well we saw up above how lambda calculus doesn't even come with built-in booleans or integers. And Church didn't even think lambda calculus was powerful enough to express the function $f(x) = x-1$ where x is a positive integer. Kleene's the one who "implemented" all the types and functions that built things from that totally useless level all the way to what eventually became "all computable functions." So Kleene's definitely being humble. 1: Sounds like it. It's crazy I've never heard of this guy before. 0: For real. And from Church's perspective, imagine this grad student of yours who's never even taken a logic class before comes to work with you, learns your system, and then he just keeps knocking off one problem after another until the two of them ended up going from thinking $f(x) = x-1$ is too hard, all the way until Church himself got convinced that _all possible computations_ were representable inside this system. 1: How did Church get convinced? 0: Kleene won't admit this, but it was his "programming" that convinced Church. I mean sure Church designed the lambda calculus, but Kleene figured out how to use it like a frighteningly technical nerd. 1: How do you know? 0: Just read Church's papers. He makes it extremely clear. I swear he cites Kleene in one paper like a hundred times. Check it out. ## Kleene Kleene Kleene 0: Ok this is from Church's 1935 paper "An Unsolvable Problem of Elementary Number Theory." This came out about 7 months before Turing's famous paper that showed the same thing. 1: No way! ![[church-says-kleene-kleene-kleene-00.png]] 0: Turing's paper broke new ground in different ways, but Church got there first. 1: Never heard that before. 0: And if we read this paper, it's pretty clear that "Church" getting there first is like 80-90% Kleene. 1: Kleene's not even a co-author though. 0: Not sure why. Church generally seemed like a generous dude. But just drag your eyes lazily over the pictures below this. This is all from the same paper. ![[church-says-kleene-kleene-kleene-01.png]] ![[church-says-kleene-kleene-kleene-02.png]] ![[church-says-kleene-kleene-kleene-03.png]] ![[church-says-kleene-kleene-kleene-04.png]] ![[church-says-kleene-kleene-kleene-05.png]] ![[church-says-kleene-kleene-kleene-06.png]] ![[church-says-kleene-kleene-kleene-08.png]] ![[church-says-kleene-kleene-kleene-09.png]] ![[church-says-kleene-kleene-kleene-10.png]] ![[church-says-kleene-kleene-kleene-11.png]] ![[church-says-kleene-kleene-kleene-12.png]] ![[church-says-kleene-kleene-kleene-13.png]] 1: Damn that's a lot of Kleene. 0: Church is like "Our integers are different. ![[church-says-kleene-kleene-kleene-14.png]] 0: But this proof is Kleene. ![[church-says-kleene-kleene-kleene-15.png]] ![[church-says-kleene-kleene-kleene-16.png]] 1: Why is he citing him so much? 0: Kleene implemented everything. 1: Definite first programmer vibes. ![[church-says-kleene-kleene-kleene-19.png]] ![[church-says-kleene-kleene-kleene-20.png]] 1: This is an impressive git blame. 0: Seriously. Church is acting more like a faithful `git blame` implementation than a normal human writing an academic paper. 1: The more I learn about these logic folks the more I like them. 0: How so? 1: I dunno. They're nerds. It feels familiar. ![[church-says-kleene-kleene-kleene-21.png]] 1: Church is like "I'm still here guys, I'm gonna say Kleene some more." ![[church-says-kleene-kleene-kleene-22.png]] 1: Good lord man. ![[church-says-kleene-kleene-kleene-23.png]] 1: It keeps going. ![[church-says-kleene-kleene-kleene-24.png]] 1: This is getting ridiculous. ![[church-says-kleene-kleene-kleene-26.png]] 1: I don't even know what he's talking about but this makes me want to read Kleene. 0: We will. That's why I'm showing you this. 1: Why? 0: So you don't get sad when we get to the frighteningly technical book. 1: Uh oh. Is it bad? 0: Nah it's easy. You'll enjoy it. ![[church-says-kleene-kleene-kleene-27.png]] ![[church-says-kleene-kleene-kleene-28.png]] 1: I've got to say, I thought you exaggerating but that was intense. 0: That's from _one_ paper. 1: Damn, Church. 0: Ok but I was unfair to Church earlier. When Kleene said "I have to give the credit to Church, I can't take it myself," he wasn't talking about all the programming, he was talking about Church's thesis. 1: What's Church's thesis. 0: "That's everything." 1: What's everything? 0: Church's thesis is "Hey Kleene, I think maybe we got everything?" 1: _What's everything?_ 0: All the computable functions. Or effectively calculable as they called them back then. 1: That's Church's thesis. "We're done." 0: That's it. 1: Why "thesis" and not "theorem"? 0: Because it's saying "I think this informal concept equals this formal concept." Can't exactly prove that in the usual mathematical sense. It's pre-mathematics. The hypothesis is that lambda definability captures what we intuitively mean by "computable." Way more powerful than just a theorem. 1: What on earth made him thing "We got ALL computation"? 0: Kleene. 1: Kleene? 0: I mean Kleene's programming. Church was convinced before Kleene was. Then Kleene tried to disprove Church, failed, and got converted. > Someone: Was Church's thesis just an offhand remark? > > Steve Kleene: Well he spent some months sweating over it. And saying "Don't you think it's so?" And I was a skeptic! When he came out and asserted the thesis I said "He can't be right." So I went home and I thought I would diagonalize myself out. Out of the class of the lambda definable functions and get another effectively calculable function that wasn't lambda definable. Well just in one night I realized you couldn't do that, and from that point on I was a convert. > > Steve Kleene: Then Gödel arrived on the scene and--- 0: Ooh perfect. [[2/4|Gödel]] time. Follow me. 1: What abou---