## Link https://www.youtube.com/watch?v=pxru2Oz7zHg ## Clips ### We didnt have books start = 0:00 end = 0:30 ### I never read Principia Mathematica start = 0:25 end = 0:40 ### I learned logic from learning Church's system which was subsequently proved inconsistent start = 0:35 end = 0:55 ### Kleene realizing how to implement predecessor at the dentist start = 6:55 end = 7:10 ### Church originally didn't think it would even be possible to implement the predecessor function x-1 in lambda calculus. start = 6:50 end = 7:20 ### So there was no idea at the beginning that this was going to be all effectively calculable functions. start = 7:15 end = 7:30 ### I kept taking it as a challenge and everything I tried I could work. start = 7:30 end = 7:45 ### It was an unexpected fallout that this could represent all effectively calculable functions. start = 7:38 end = 7:55 ### The basic work was done between January 1932 and the next 5 or 6 months. start = 7:55 end = 8:15 ### 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 fist 5 months. start = 8:15 end = 9:00 ### 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. start = 8:15 end = 9:10 ### 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! start = 9:04 end = 9:45 ### 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?" Then Gödel arrived on the scene 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. And then we had done all this work before we heard of Turing. Turing's paper is also 1936. But a little later in 1936. But my impression is that Turing did it independently of knowing anything about what we were doing. start = 9:25 end = 10:35 ### Was Church's thesis just an offhand remark? 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. start = 10:30 end = 11:30 ### 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. start = 11:35 end = 12:30 ### You don't happen to have a copy of Introduction to Metamathematics do you? start = 12:30 end = 16:38 ### Well as I say, I don't know how firmly convinced Gödel was that his General Recursive Functions represented all effectively calculable functions. start = 16:38 end = 17:38