#14 aboutlogic | Dana Scott – Lambda Calculus, Forcing & the Foundations of Math

00:00:05: Hello everybody to our little podcast today.

00:00:07: We have a very special guest and we are very thankful that you take the time um, To join our podcast.

00:00:13: Dana Scott And he is famous for many things touring award winner revolutionized Computability theory set to URI so one of the most productive logicians Of his time end also He said I'm quoting from a lecture You gave in Berkeley.

00:00:33: Excuse me for that.

00:00:34: Accidentally, you became an important historian because all the very important people like Church and Gürtel or Fevermann Soloway made a lot of effort preserving some in our workings on history with this logic community which brought us so many things.

00:00:56: So thank-you very much for joining.

00:01:00: And having said hand over to Thorsten for the first question vlog so-to speak.

00:01:08: Yeah, thank you very much Dana for seeing us good to see again.

00:01:13: and yeah I wanted to start with something about the anti blunder calculus.

00:01:18: um i think uh i just saw a note which was written before you started developing this domain theory where basically we're saying that there is maybe isn't maybe not a good sort of denotational semantics for the anti-Blamda calculus.

00:01:35: But then you did find one, and maybe you can say little bit more about this?

00:01:43: Well... One thing that I want to refer people too as sorry For the centennial celebration Of Christopher Strachey!

00:01:54: I wrote up very carefully how i met him various developments that took place there.

00:02:03: And apparently sometime earlier, Roger Penrose at Austria had told him for his general work on defining programming languages he ought to use the lambda calculus.

00:02:23: and so when I first met That's partly the way he was describing things.

00:02:33: But at that time I felt there wasn't any mathematical model for the lambda culture, connected up with ordinary mathematical types and ideas.

00:02:48: so when i came to visit him in austria we should go back to the work of Cleaney and look at functional theory or functionals.

00:03:06: Cleaney in the meantime had wanted to do descriptor set theory, he got on to infinitary functions but... In earlier works I mean good thing that Cleaney did was introduce our under church partial recursive functions and formalizing recursion.

00:03:28: carry there, but then also Claney spent a lot of time thinking of recursive functionals.

00:03:36: And so what I told to Reggie was that let's look at the very specific way in which Claney defines higher types or funtials.

00:03:50: So an article I wrote up It was a version of it, later published as I indicate in the notes that i'm sharing with you.

00:04:04: And then after thinking about functionals what occurred to me is if you can do higher and higher types maybe and then the infinite type turned out to be the model for the lambda calculus.

00:04:29: because what you do when you have continuous mappings on these infinite types, they're all determined by what happens at finite types.

00:04:39: And so uh... You don't have to go- When you get into an infinite type.. ...you don't need to go higher because continuous functionals are already determined in the lower types.

00:04:51: anyway You recluded all the lower types, so everything is already there.

00:04:56: So you only need one infinite

00:04:59: type.".

00:05:00: Maybe this was connected with something that I discovered as a graduate student?

00:05:06: Uh...I studied under Alfred Tarski very much in Berkeley in the early nineteen fifties and of course i was very pleased to learn Euclidean geometry.

00:05:23: And one of the things there was that Tarski felt, in giving first-order theories about geometry it were sufficient just to use as your primitives betweenness is points on a line One being between a pair or other points Between us.

00:05:44: so that defines lines and then important thing define circles and other things, you use equidistance.

00:05:55: So that's a four-placed relation—that the distance between the first two points is the same as the distance from the other two points.

00:06:07: And those primitives are meaningful and sufficient as foundation for First Order Geometry in any dimension!

00:06:19: The question I ask Then, when I was a graduate student is well what happens in infinite dimensions?

00:06:30: In infinite dimensions you just use ordinary theory of vector spaces where the distance on them and so primitives are meaningful.

00:06:45: And all those standard vector spaces.

00:06:49: And what it turned out was that, again there's only one infinite-dimensional first order theory.

00:06:58: All the higher dimensions are the same.

00:07:03: from a point of view to First Order logic and as matter fact you can say a definite way to the theory of the infinite dimension, there's only one infinite dimensional elementary first order geometry.

00:07:30: So maybe that business...the idea is things iron out and then become stable at an infinite dimension was something in the back.

00:07:49: models for the lambda calculus and using clay needs recursive functionals.

00:07:56: But continuity was already important, does it go back to Brauer or who influenced?

00:08:05: Yes because we want you think about computable things based on ordinary ideas from going back to primitive recursive functions.

00:08:16: So of course, you just do things a little bit at the time.

00:08:19: In other words everything goes back to finite configurations.

00:08:26: and that's what basis or definition of continuity You could think of continuity functionals being A finite amount information about a function value It already completely determined by a finite amount of information about the arguments you want to get into the functional.

00:08:48: So that was there from beginning, and of course I was totally influenced by work on Kleeney and other people are about Kleeneys theory or functionals.

00:09:03: Yes so thats the untied lambda calculus.

00:09:07: but if we move towards a tight lambda calculus Again, I have got a quote.

00:09:15: I don't know if that's correct but you would note once how the type lambda calculus should've been discovered.

00:09:22: so it was obviously discovered by developed by church and others.

00:09:28: But... I think your emphasis is very natural.

00:09:34: notion from category theory.

00:09:35: Yeah yeah

00:09:37: well back to became clear later.

00:09:42: It took a while, I mean starting with algebraic topology and the emphasis that people put on using categories to give general formulations.

00:09:53: And then it sort of came back to foundational things like thinking about basic theory or functionals.

00:10:03: so they've been led to Cartesian closed category as a simple idea.

00:10:10: And so, of course then we have developments like Martin-Lurf type theory and so forth that are very influential still today in thinking about foundations for constructive mathematics.

00:10:27: And of course refer people to the works of your colleague Martin Escardo.

00:10:36: constructive mathematics are nicely formulated in terms of our type theory like that.

00:10:46: And so, yes... That's a good connection to keep in mind!

00:10:52: How do you use the rule of category theory?

00:10:54: I mean, you see already, category theory was first came with algebraic topology but then it moved into logic being a foundation.

00:11:07: So, how do you view the whole of category theory?

00:11:11: Why wasn't it so successful.

00:11:14: Well see...the thing is that theory like Zermolo Franco said theory allows arbitrary collections and arbitrary functions and so forth from things like that.

00:11:30: but mathematical applications are better systematized in terms of specialized functions.

00:11:39: And so it was that understanding, in order to see the coherence of different kinds of objects.

00:11:52: Set theory and axiom of choice or things like that is too arbitrary.

00:11:58: It's better to sort-of think basic properties Closured under basic properties.

00:12:06: And that's what is formalized as everyone knows these days in terms of category theory.

00:12:15: Yes, and nowadays higher categories become very fashionable?

00:12:21: Yes well there are lots good literature available.

00:12:25: yes

00:12:28: I mean i think maybe you would agree that the z-theory is very much about concrete encodings.

00:12:36: like to have more abstract properties of mathematical objects and then categorically see what seems to be the way.

00:12:43: Of course, on the other hand I just heard here in Berkeley lectures at the latest Towsky lecture that there's enormous amount of work in set theory about higher cardinal numbers for...I mean especially influenced by worker wooden But many authors there, of course says very elaborate development of relationships between higher cardinalities.

00:13:16: Something that was I mean the kind of complication was unthinkable thirty years ago but has really been developed...I do however keep asking those people What applications do you expect of the higher card knowledge?

00:13:37: And they hope that an important application will be and better understanding or descriptive set theory Going back to what our claney was Promoting in his time there though.

00:13:54: There's incredible development in said theory, but I'm still wanting to know What are more concrete applications?

00:14:05: And so I keep irritating people by asking that question.

00:14:10: It's always good to irritate people.

00:14:12: Yeah, if we stick shortly to satiury If i may and for the audience in nowadays every satirist leads to learn the forcing technique.

00:14:22: We normally learned it via Boolean algebras and all this was Developed in California, right?

00:14:28: So satire is a forcing became the standard technique for satyrs there.

00:14:35: But I wanted to ask you a slightly different thing that i sometimes read, That already Gürtel had nearly something like a forcing argument Something with permutation models in mind but then decided not to work more In that direction because he feared... ...that this will make satyuri To study of models of satyury rather than set to be proper, so-to speak.

00:15:02: Of course Girdel had many ideas that he never exposed and ever wrote up.

00:15:09: Another strange thing is Kreisel who was very close to Girdle.

00:15:14: I mean one of the reasons a Girdal or Kreisel were very close That Kreisel has studied Hilbert Bernhard's book Very much.

00:15:25: when it came to Princeton then There was lots to discuss with Gertl, but just as it was.

00:15:32: With Gertle in Einstein German language made a very much easier for Gertel to discuss things.

00:15:42: Chrysler and Gertles spent hundreds of hours on the telephone talking over things And of course they also liked the telephone very much because you can't Give out any germs if you're speaking over the telephone.

00:16:01: Oh,

00:16:02: yeah was always worried about his His health.

00:16:07: but anyway Chrysler actually had some ideas that could have led to forcing.

00:16:15: But it took Paul Cohen To Actually Come up with It and one of Cohen's motivations I've Always Felt Was That logicians like Pfeffermann and people that he knew in Kreisel or who visited Stanford many times where Cohen was, Cohen was PhD in Chicago but then came to Stanford all those people.

00:16:49: And Cohen really felt the logicians didn't get into correct mathematical ideas.

00:17:00: For example, Cohen completely redid for himself Tarski's decision method for geometry and all these people talking about analysis... Cohen was going to show them from the point of view a real mathematician that he could do much better in understanding understanding the consistency proofs and things like that.

00:17:32: And so I have a feeling that Cohen never read anybody else's paper, he just proved everything for himself but he needed it was of course very brilliant.

00:17:46: But then what happened?

00:17:48: after he showed the forcing techniques and Stanford, Salovey who had been a student in Chicago as well.

00:18:00: And

00:18:01: I

00:18:02: had her position at Berkeley came over to Stanford to visit Chrysler and Vefrin and myself and do better understand Cohen's work.

00:18:16: So one day he was talking to us and Salove point it out I can reinterpret here this kind of co-enforcing thing by doing a, uh... ...kind of many valued logic.

00:18:36: We can easily interpret his things as modeling set theory in a Boolean-valued logic.

00:18:46: So it just happened that over the holidays and at the end of year when I was at home thinking about it, and thought to myself wait if Solovey can go from Cohen then reinterpret his definitions as a Boolean-valued logic why couldn't we turn him around?

00:19:10: Go backwards.

00:19:12: Start with Boolean algebras first And think of what axioms in set theory you'd like to achieve But in order to have properties of the set theory, you have to make up an appropriate Boolean Algebra for it.

00:19:33: And of course I had studied under Tarski and his many collaborators a lot of work on Boolean algebras like the Boolean algebra in topological spaces, all that came from earlier work with Under Tarski and his collaborators.

00:19:55: And so I tried to apply those ideas on.

00:20:02: another fortunate thing in my development was...I had studied points at topology under JL Kelly wonderful expository and became a close friend in later life.

00:20:20: And so the influence from Tarski school, things like Kelly made me try to understand what kind of topological spaces you would need in order get the right properties of a Boolean algebra regular open sets and Boolean Dad.

00:20:48: Of course, after I quickly wrote that up over the Christmas holidays there, Salome said of course!

00:20:59: i already knew that...I thought about it as well.

00:21:03: so when we had the UCLA set theory meeting in summer, Salove and I presented Boolean Values models together on a joint paper.

00:21:17: I have to try to explain myself for one of my many failures.

00:21:25: After the Boolean, after UCLA's Scythe theory conference... ...I was on sabbatical in Amsterdam for a year and Salovey was traveling Publishing our joint paper on Boolean-Valentine models.

00:21:52: But in the meantime, The whole thing had caught on so well that people all over the world were proving new theorems Over and over again.

00:22:06: And Salovey kept saying now Our paper has to include this and it hasn't included bad and has includes All of these things are happening.

00:22:13: you have to put those.

00:22:15: I was incapable of carrying out the expansion, and so that's why I never finished a paper.

00:22:31: Luckily John Bell took it up Not being able to do the publication.

00:22:52: I'm also ashamed myself for never having published a book and look at my colleagues who write wonderful books, but I Never was able to bring Myself to organize things here.

00:23:07: But i have give some very good lectures.

00:23:10: so that's why recommending you be sure To include with this discussion here, the materials for their lectures that I gave you there because...I can point people to things they should look into even if i have this whole thing up as a book.

00:23:32: For the audience and you can click on the links in the comment section of this video And there we can download some PDFs.

00:23:40: so it's accessible there.

00:23:42: Very glad to hear if people can give corrections or expansions of the things there, I tried to indicate some of the history and development that was connected with these thing.

00:23:57: So it would be nice If...I could get some criticism back for that so we can improve the overview.

00:24:10: Yes i think is quite clear that you're very creative and very productive.

00:24:16: And I guess maybe if you had a bit of sit down, concentrate on the book... Maybe we would have lost more than gained.

00:24:25: so i think there's nothing to be ashamed or feel.

00:24:27: Well also with uh decade then i had an outreach.

00:24:35: There were excellent students there.

00:24:38: One year was advising one semester.

00:24:41: i was advising Nineteen graduate students at one time, so I spent an awful lot of time with the student.

00:24:51: So maybe my contribution has been that helped a lot people on their research

00:25:00: No question.

00:25:02: Second can you already mentioned type theory and then that's obviously something i'm very interested in.

00:25:09: So I think if we go back in the past, you already also discovered some ideas about dependent types before Pierre-Martin Lov developed his type theory.

00:25:22: Got any comments on this?

00:25:26: You looked at type systems and polymorphisms... ...and there were examples where he used some notion resembling dependent types formulated it.

00:25:39: I mean they were like these theorem, obviously system T and also System F but... Well

00:25:48: of course its a simple sort outgrowth just higher order logic.

00:25:53: so Of course one thought first order logic second order logic And so forth going up to higher types there.

00:26:06: The thing that's different though is, but usually well you think of higher order logic.

00:26:14: You also... If your doing second-order logic every formula determines a collection.

00:26:27: I mean the comprehension axiom.

00:26:29: That's correct.

00:26:30: Comprehension?

00:26:30: I thought you meant comprehension and was going to say it.

00:26:32: Comparation

00:26:33: axioms are very strong.

00:26:35: in course makes a very, very thick type theory.

00:26:41: And so what was interesting is there are so many thinner-type theories and particularly make better connection with constructive logic.

00:26:51: whereas those think in terms of higher order logic where the comprehension action you're not thinking constructively because they're thinking arbitrarily I mean anything that you could express logically determines the collection of things, it's satisfied.

00:27:14: So comprehension axiom is very strong.

00:27:19: I mean what i'm thinking about.

00:27:23: if we model higher logic to quantify over propositions but If You want To turn more mundane predicate logic into into types.

00:27:34: You get these dependent types where you do depend, for example on a number and so on.

00:27:42: which is I think the core of Pierre-Martin Röf's theory?

00:27:46: Yes yes!

00:27:47: And that's what...I think that Eskado and Tom Deogne people are showing very clearly in their work too.

00:27:58: That's key way thinking things.

00:28:01: Yeah

00:28:03: So maybe you may be.

00:28:04: let me ask do your fear well for another question.

00:28:07: or Do you think it's better to have a break now?

00:28:11: Well, I think one more question and I will say goodbye

00:28:19: Which is close to my heart.

00:28:21: Um, I Think uh i mean If interested in constructive methods this Is something many mathematicians are not sort of very aware off that there is something like interstitiality and constructive reasoning.

00:28:37: What's your view on this?

00:28:39: I mean, it's my feeling many mathematicians are not really... they're not aware of other views or more constructive view of mathematics and tend to ignore these.

00:28:52: Is this what you experience in the context?

00:28:55: ?

00:28:55: Well

00:28:55: i knew Eric Bishop very well.

00:28:57: he came from Chicago where at first first job and I met him there, his sister was a brilliant mathematician too.

00:29:13: But what happened with Arab Bishop?

00:29:15: after doing very amazing things in functional analysis?

00:29:21: He woke up one day and said all these ultrafilters have no numerical meaning numerical meaning.

00:29:35: And so he wanted to do analysis in a way that had numerical meaning and without going into it would be his proofs are classically correct, this proof is intuitionistically without adopting any kind of special logical ontology, the way that Broward wanted to do intuitionists there.

00:30:19: And then Bishop and his collaborators have carried it out very extensively.

00:30:29: but I think what the category theory is doing is, and I feel that's beautifully explained in many papers by Asgardo.

00:30:45: There's a more general view of that kind of constructivism and predicative-dependent type theory.

00:30:56: so i think point of view that Bishop wanted to get at so he could say with, during the tools we use there really is a numerical meaning to the proofs and analysis it gives.

00:31:22: So I think that predicative dependent type theory has best modern version.

00:31:31: I've constructed mathematics.

00:31:35: Yes, but

00:31:37: i think you know all about it.

00:31:39: so...

00:31:41: But its good to hear from you!

00:31:45: I take your agree with me.

00:31:47: Yeah absolutely yeah

00:31:50: great we can only say thankyou once more.

00:31:52: there's so much more We would love to ask about fixed points without so many things.

00:32:00: Well, we can meet again sometime.

00:32:04: Why don't you and get things from other people too?

00:32:10: why don't think of some questions to ask And then correspondence?

00:32:15: We Can Think Of The Questions So Then We Can Have A Discussion Again Later.

00:32:25: Yeah, hope to see you soon again.

00:32:29: Thank

00:32:30: you!

00:32:30: Thanks again!

00:32:31: Bye bye.