## Callmy Name ### Or: Kleene Kleene Kleene ### Or: IM is what IM is ### Or: Kleeneliness is next to Gödeliness 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. [[1 - Gödel Numbers|1 - Gödel Numbers]] time. Follow me. 1: What abou---