## Church's Descendants ### Or: Church's Congregation ### Or: The Transitive Closure of Church's Students ### Or: Reminiscences of Logicians 1: What's a reverse begat list? 0: Well picking up where we left off: - That book was by Jeff Hirst. - Jeff HIrst's advisors were Harvey Friedman (who we saw up above) and Stephen Simpson (who worked on the same "Five sentences" research program as Friedman). - Harvey Friedman and Stephen Simpson both had the same advisor, Gerald Sacks. - Gerald Sacks's advisor was John Barkley Rosser. (Another one of Rosser's students was Elliott Mendelson, who was mentioned above, as the author of the book that does foundations formally but less "frighteningly technical" than Kleene.) - And John Barkley Rosser's advisor was Alonzo Church. (Who was also the advisor of Stephen Kleene.) - That's a reverse begat list. 1: Damn, that was good! 0: And here's Steve Kleene talking to Gerald Sacks about Alonzo Church and J. B. Rosser. 1: Ok nevermind this was pretty well planned after all. --- > 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)_ 1: Why did everyone laugh there? 0: Nobody reads _Principia Mathematica._ > 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)_ 1: Why did everyone laugh there? 0: Inconsistent systems are supposed to be useless in logic. But that can't be entirely true because Kleene's one of the best logicians in the past century and he learned logic from a system like that. 1: Logic is trippy. > 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. > > 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: Man, logic is trippy. > 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.)_ --- ## Kleeneliness is next to Gödeliness ### Or: Kleene Kleene Kleene ### Or: The First Programmer ### Or: The First Standard Library ### Or: The First Critical Vulnerability ### Or: The First RTFM ### Or: Frighteningly Technical ![[kleene-1.jpg]] 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: Which Church's Thesis? 0: The one we didn't talk about yet. 1: Not the PhD one? 0: Not the PhD one. 1: What's the other 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. 1: What's a lambda definable function? 0: That's the first programming language. 1: The first programming language? 0: Defined by Church. With standard library implemented by Kleene. And on the basis of which Church's Thesis (this one) was conjectured. 1: Details please! 0: Follow me. [[4 - Church's Numbers]]