## Called by No Name ### Or: Church Kleene ### Or: The Unnamed Number ### Or: The Unnumbered Name ### Or: The 💯th member of the 11nity ### Or: The increasingly poorly named trinity ![[kleene-1.jpg]] > 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. 0: Crazy huh? 1: How so? 0: I mean, this is one of the best logicians of the century. 1: And he just said 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. _(Narrator: 0 clears 0's throat.)_ ## Call His Name ### Or: Kleene Kleene Kleene ### Or: The First Programmer ### Or: The First Standard Library ### Or: The First Critical Vulnerability ### Or: The First RTFM ### Or: Kleeneliness is next to Gödeliness 0: Ok so, 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. 0: So Kleene was sort of the 10x developer and Church was--- 1: The old wise sage type? 0: Exactly. But not because he was old. He was only 6 years older than Kleene. But he had spent some time in the (standard) Foundations of Mathematics, and nothing will radicalize you like standard foundations. 1: I don't think I even know what "standard foundations" is. 0: Ok, to appreciate the rest of where we're heading, we should probably do at least a drive by. 1: A drive by of what? 0: The other Church's Thesis. 1: The other Church's Thesis? 0: Yep, follow me. goto: [[3 - Old Laws No One Uses]]