Philippe Séguin / Steve Awodey / Geoffrey Hellman / Philip Ehrlich / FW Lawvere Philosophical Insights into Logic and Mathematics Intl. Symposium, Univ. de Nancy 2 2002
← All recordings

Recorded at Philosophical Insights into Logic and Mathematics Intl. Symposium, Univ. de Nancy 2 (2002), featuring Philippe Séguin, Steve Awodey, Geoffrey Hellman, Philip Ehrlich, FW Lawvere. From the Michael Wright Collection, held by the Archive Trust for Research in Mathematical Sciences & Philosophy.

Identifier
mw0001823-cc-a_p
Format
Audio recording
Collection
Michael Wright Collection
Repository
Archive Trust for Research in Mathematical Sciences & Philosophy
Rights
Made available for personal scholarly use. Rights in recordings are generally held by the speakers or their estates. If you believe this recording infringes your rights, please contact [email protected].
Transcript
Read the automatically generated transcript

This transcript was generated by speech-recognition software from an archival recording and has not been hand-corrected. It will contain recognition errors — particularly for proper names and technical terminology — so please verify against the audio before quoting. Timestamps play the recording from that moment.

0:00 And that description is one indeed. You don't get any non-stator model by our construction. So it's exactly parallel. The problem with non-stator models is it affects them both. It cuts across the distinction between credit activity and non-credit activity. And that's a point that some of our critics weren't sensible to, I think. They were asking for the impossible, and since we couldn't deliver the impossible, they said, well, you failed. And I said, look, there's more to be done than the impossible. I mean, less to be done than the impossible, but you know what I mean. There's more to do than to try to do the impossible. You can do something like this. That's still an improvement in the situation. Well, I'm starting to be able to explain what the relationship of the question is. The audience is coming straight out. Yeah, well, I mean, let's say... It's a little, I mean, I have to, you know, it's a little delicate. You have to write it down. It takes a while. You have to prove some numbers, so I don't want to try to... I guess what's a little bit puzzling is, I don't understand how you're going to get a collection of all the natural numbers, starting from individual finite card numbers. I guess you're taking finite card numbers, something like that, and then... We have a pairing function. We have a pairing function, and so, and because there's, one of the axes is that there's more elements under pairing. So there's an individual, you know, you can do this, you have some individuals. So you can iterate the carrying function, then you guarantee you get enough things. You're going to have all these things. And so now then you start building up a structure that satisfies, essentially satisfies the axioms. Using the finite set machinery, but at each stage only making predicative moves, that is, you never have an impredicative instance of comprehension.

2:30 You have to introduce an order. You have to prove the relevant things about it. You can represent all recursive functions in relation. Then there must be some way to cut down the domain to be only the things that's got to be in the function. How does that work? The essential idea is to say that all of these are sections of everything we use in the functions of the world. It's a very, I mean, it's a very natural construction. The idea is that you're looking at predecessors, right? It's one way to characterize the natural member structure, to say that all the predecessors of any thing in the structure form a finite set. Now, in the usual setting, that's not good enough because finite isn't pinned down, right? Well, here it's not pinned down anything except by me saying I recognize a finite set variable when I see it, and I'm assuming that notion. So that's the basic idea is to be able to say all predecessors are variables. Well, look, you just look at it from the standpoint of the binary tree, right? What you'll do is you'll have the case, it will be the case that there, every single thing has at most a finite number of levels, right? You know, when you divide everything, because what you have is all the finite levels, and then you have the rest of them, okay, so in the case of no, for example, right, you have the dyadic rationals on the finite levels, and then you have the non-diadic rationals on the negative levels, plus all the erratic, right? So every single element there has more than a finite number of tens of them, and you do get... Well, sure, but then, I mean, there are lots of models of these structures that we'll have to talk about. The question is not whether we can find models of it with that standard. No, I know, I know. But now the question is to what extent does this logical script pick out those, succeed in picking out those and exclude non-standard. Right, and then what we do is improve the catalyst theory. Any other structure would satisfy... All of these conditions will be isomorphic, and the isomorphism is constructed predicatively. But the specification of the conditions is not recursive, it's not axiomatic in the system, right? There's some additional external specification of the conditions, namely the finite conditions.

5:00 Well, you have to take that as understood, just as you do when you rule out hidden lines. You say, well, I understand this point of fire. I understand what all means when I say all subsets of a set. That's an effect that you're doing from the outside if you want to put it that way. Well, Bill, that's a pretty big assumption, right? That's much bigger, much bigger, and to use your gesture, much, much bigger, right, than saying I understand what finite means. You know I agree with that, but I think you have both assumptions. All you guys understand what finite means. You wouldn't be doing that in there. There are lots of different notions of finite. That's right. It has to be relative. I'm not so sure I do. They're absolutely generic. Tarski's is nice because you have a separate infinite, you have a separate finite, and you don't find one is not the other. That's a very cute one. Well, all right, so there's more to be said. Obviously there's a discussion here, an intelligent discussion. You have to look at how this works and see, and then make the right comparisons to other things that you think work or don't work before you have your answer. I think what you said is actually very interesting, but I guess my inclination is that... Assuming that finite is well understood and not problematic, I think that's a bigger assumption than you seem to suggest. But nonetheless, I think what you said is actually very easy. But I think that's actually assuming a lot. No, it's a substantial assumption. Look, so what this is, it's a formal fragment of weak second-order logic, you can put it that way, So you have some structure or domain in the visual so you can do something. But it's well known that weak second order logic in the semantic sense is not formalized. But perhaps that's the reason, because that's what you can do with it. Where is this paper published now? JPL. No, 1995. I'll take a look at it. Yeah. You know, I mean, there are those who say, unless you can write down a categorical set of axioms for a notion, you can't quite understand it, that the categoricity is a precondition of understanding. In which case, then we're really doomed. Because in order to get a categorical set of axioms...

7:30 You'll have to put an induction principle in on finite sets, and then the whole thing will be no better than just assuming that... I don't understand what the problem is there. Oh yeah, it'll be no better than assuming the induction. But I don't see that... I don't see that it's better. You haven't convinced me yet that it's better than the next one. Well, given the conditional constraint on the notion of finite, it has to come from outside. You're trading that for predicativity. I would give it a choice between two. I'd rather have it in predicativity. Oh, I'm not pre-judging that choice. This was a question whether the predicative of this had any better way to start than the old way of starting, which was just to grab the natural numbers, the infinite natural numbers, and take them for granted as a classical, because remember, they reason with classical logic. So, I always thought that was a very unsatisfactory starting point. For anything from a philosophical point of view, if you want to do predicate analysis and say, well, that's fine, but, you know, when your first step is a paradigm of impredicativity, we can say, so this question is what this does from within the predicate of this theory of view, that's one question. Then there's a bigger question you're asking, well, you know. Relative to a notion of finiteness, what is gained by having a force of gravity. That's right, that's right. In a certain sense, that's right. I mean, one way of looking at it is that, you know, how much teeth, assuming that that finitude is well understood. What's the cash value of that, in a certain sense? Another way of saying it is you're localizing the question of creditability down to the question of finance, which is a self-interested notion to some extent.

10:00 The notion of finance. Certainly in many construals thereof, right. I don't know how you're going to get an external notion of finance that ensures a certain It's just not in your theory. You've taken impredicativity and pushed it out of your theory into this notion of finance. I wouldn't say how impredicativity would help, though. You have impredicativity in whatever your models are. You can pick out your distinguished interpretation of finance. But that seems like a very bad move, because the only way to do that is to buy into... All subsets of the infinite set. I myself have no problem with that. I don't have any problem with it either. I know, I know. But it seems to me, if one's going to have problems, one should have more problems there than there is in the ocean and fire. I suggest they both walk into it. You don't think finance is an intuitive notion? I just ended that sentence. We quote from Alice in Wonderland. We quote from Alice in Wonderland. I think it's such a... The king put on his spectacles. Oh no, the rabbit, the white rabbit put on his spectacles. Where should I begin, Mr. Registry? Begin at the beginning, and when you come to the end, then start. I'll put it this way, okay? I'll grant you if you want us to continue the notion, but what I think would be a mistake to confuse from that, that you unfolded it in a new way. I think it's such a vague notion that it can be unpacked in so many ways. That's the problem. I disagree. I think there are lots of ways to make it precise. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. I never said you couldn't. Interpretation is the standard thing you're saying. If the finite means finite, then it's going to be some sort of activity involved technically. You haven't got it in the theory, but it can be a proof of the categorical.

12:30 Well, this raises the question of how do we learn a language? I mean, one conclusion of your line of thought might be that we really don't and never could understand finite in its standard sense. It seems to make this discussion impossible. I think, by the way, we threw away most of these intuitions and replaced them with more and more placements to turn that into a very nice report. And that's exactly why we got rid of these intuitions, because they were very vague. They were used in all kinds of different ways. You look at the history of the finance. The way people used finance, they used it in a wide variety of ways. They talked about us being finance deans, right? They talked about... We're not talking about finite x where x is uncertain. We're talking about finite 7. But even... But there, but it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, it was, And then, you know, without saying, this is not that, right? And then, these are really the back-end assumptions. It turns out that it picks out exactly what we wanted to pick out, vis-a-vis the classical theory. But these are formal replacements. These are not going to—these are what the intuitions of the law are. The fact is, I don't think that people—if you read—and I haven't read this—if you go back and you read and see what people are saying about these things, I mean, that's what that really amounted to. It was kind of embarrassing. It was mumbo-jumbo. They didn't know what to say about it. Yes, some of what they said made more sense out of the formal definitions than other things. Yes, yes. The core notion was the notion of being delimited. Yeah. Something. Yeah, sorry. That. Yeah, limited. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah. Yeah.

15:00 Yeah. You're not going to get any more out of him than what he did actually, right? Yeah, I think what, well, we're putting something in there. You say it depends on... No, I'm saying it. I think those work. I think these will guard gears for him in the advances. But it took getting rid of a vague idea with a formal replacement. That's what I'm saying. Well, I would say articulate it a little bit. In a particular way. I mean, in a particular way. If you have to have a construction institution sort of motive, how could you ever get started? You have to have a notion of finiteness, you know, through your categorization. Well, that's definitely the case, but you're saying the only place we could get our notion of finiteness is through an impredicative construction? That has been historically the case, that that's the only construction you have of finiteness, or impredicative construction. You're saying you have a different one, but it relies on an antecedent notion of finiteness. And I'm saying, where did it come from? We know how to do it incredibly well, and I know it's, you know, we can't, you're not going to propose a vicious circle, but, you know, it's a similar predicate. No, I'm going to say something like, I'm going to appeal to our experience with language and with counting, you know, with counting or enumerating. You know, with syntactic structures, I mean, that's enough. Then why not just say, well, I have an assistant symbol, and a stroke is one, and I have a stroke that's one, and I feel through our use of consecutive strokes, and I say those are now the finite numbers. I think that's a repractical construction of the finite numbers. You wouldn't be happy with that, right? No, a predicate, a predicate. And you wouldn't be happy with that if you could say, oh, that's... Thank you for watching. But you're talking about the whole infinite structure of finite coordinates. And it's at that point where you say, I'm not satisfied with what you say, and just go on like that. I want a more rigorous description of that. And that's what I'm trying to say. What does the constructivist say? The constructivist appeals there to a rule.

17:30 However far we've gotten, we can go no more. They don't claim that you need a categorical axiom system. Well, this is what we thought was interesting, that although we don't use an induction principle for finite set, We do derive mathematical inductances for the members of the class. Do you derive it formally in the theory? No, no, in the theory. In the theory and not in the external mathematical climate, then? You don't, well, I mean, a proof is a proof. You know, when you're thinking about real numbers, you prove it in a system, right? And now... How do you know that's about real? How do you know the value of this person is real? Well, you proved it was real. I mean, I don't know what you mean by induction then. You're talking about in the formal system of the language, right? And you can prove it through every formula that you can build out of the language, is that the idea? Oh, what's the form of induction? The form of induction, yeah, the induction principle is proved, actually can be proved for a class, for classes. But equivalently, it would be of an instance of a predicative formula. That is a formula where only individual and finite set variables are set back.

20:00 So we don't prove that now. General induction seems to be fast, impredicative, fast quantified, and that's an interesting question of whether what you would need to extend it, and you have some remarks on that also, but how to just indirect justification is better for the experience, and if you're doing math, it has to be a conservative thing. When you do that, it doesn't take too long to test, but mathematics is not that interesting. So when you take the finance as a primitive, it's got something to do with the properties of the materials. So what are the properties of the materials? In the theory of very, very weak axioms that are evidently true on the interpretation, but those axioms don't force a theory. Forced interpretations, like things like the empty set is finite, and if you've got a finite set, and you take a union of a single thing, the result is finite, and that the intersection of any glass with a finite set is finite, and intersection is now using a sort of divider. Yeah, well, I mean, that's defined in the formula. You have a formula, right, about the function of class, and then, you know, that's it. So, you know, the axioms are, you know, when you axiomatize, you're supposed to be rebuilding the axioms, and that's exactly what we're doing. It's a different term, it's a different term, it's just that we're rebuilding the axioms. Except for there's a different term. And so, you're right, if you will. If you put something into it, you're not going to get it. The problem is what you just put into that. It's everything except for induction. You're getting piano without induction. That's right, that's right. And then without any induction, it won't exist. But just a weak separation, you still can do a lot of mathematical induction. That's surprising. Befferman was surprised. I was surprised. And now Parson thinks that there's something fishy about separation. What, Jackson separation?

22:30 Yeah. What about it? Oh, he thinks you mean the action in the U.S. system. No, in this system. Predicative separation. Somehow there's a hidden predicative there. Maybe there's more to be said about this. We thought carefully about it and tried to respond to it, but that's in the second paper. You can read through that and see where we went. It went astray. Yeah, no. And you say it's in JPL 95 and the second one is... The second one is in the volume for Charles Parsons. That's for Cher and Thiessen. You don't have any PDFs do you? No, I don't have any PDFs. Unless someone has a scanner or something, can you just scan most of these in? I think you can. It's probably on JSTOR, isn't it? Isn't the JPL on JSTOR? Oh, maybe so, yeah. Well, then you can get it as a PDF and print it out. My problem is I have to get somebody to do that for me, because without access to JSOIL, because I'm not actually a member of any academic institution, I may have loads of people to do it for me. Have you seen one? Believe me, you wouldn't want to take out a private subscription to JSOIL. Yeah, it's very good. Which one did you like the most? That is just fantastic. There's a popular one. Is that the one? Yeah. Just around behind the church where we had, where the restaurant was, we had dinner. What about the Musée du Boulogne? I'll make that open. Actually, no, the, the, the, the, the, the, the, the, the, the, the, the, the, the,

25:00 Greenwood. Are you going to go to that? Yeah. Although it might be worth it. Right? I'm going to go back to that. I'm going to go back to that. I might just poke my head in. I have to meet with Sarah, but then before the dinner, maybe an hour before the dinner at that tavern that's right by the restaurant. Oh, where we went last time? No, there's one right around the corner from this one. Can you just run it for us because I didn't get to the morning session. It's the one that we were at the first night. Oh, the very first night. And then right around the corner there was a little tavern. That's where we were. No, but I meant the one that's right in the same building as the restaurant. And was it open? No, it was closed. Oh, I see. I see. I see. You mean that restaurant, the first... The restaurant was on the first floor. The one on the corner. Yeah. And in that building there was a little table. It was closed. It was closed. I may go further. I may also... The restaurant, I mean. Subtitles by the Amara.org community We had a delicious appetizer and a huge bowl of that whole day soup and they gave us garlic bread and all sorts of stuff like that and we had drinks. And quickly, between all of these, I really, I really fall in love with mathematics. And in today's class, you... Is it just one more question, then? Or are there two more? Yeah, that one, I was going to go to. I think I'm drenched now. Yeah, what is the question? It wasn't just something that you asked me. I would say there wasn't a chance for me. Well, before dinner at the tavern, right in the same building as the restaurant, if it's closed, then the other one where we were before, down the street.

27:30 If you had some, I'm not going to speak with any of you today, I was just wondering if you had... How much have you attained that, particularly when I was watching that, I couldn't hear anything because there was so much on the ground that I wasn't able to hear anything. I could just hear what you were saying there. I was talking about with the reversal of the gauge that goes over. Did you get any of that? No, I was trying to get him to work out some measure theory stuff. These things are all related to his ideas about measure theory. Yeah, I know you were talking about that as well. That's what I'm trying to focus on. Well, I was thinking, how much of you... Thank you for your attention. Just to write a memoir, just basically to show you could use an aid memoir before it gets published, I'd be very happy indeed to offer it to you as a straight commission, you know, if you're interested. Before it gets told, my problem is one, I couldn't, you know, I haven't, I haven't been able to get you to catch this scenery when he's talking anyway. And secondly, I'm basically, I've missed anybody from the physical background. You've got to be focused on one strand and try to catch that strand. Otherwise, you won't get any of it. And right now, I'm focusing on the measure form. I'm focusing on the measure form. I'm trying to get that strand. So that's what I'm working on with the student. He's writing a dissertation. So once we get something, I'll send it along to you.

30:00 Thank you for your time, and I look forward to seeing you again next time. And that's exactly what I'm intending to do. But just a couple of webinars last night, especially this stuff, and then there were about five or ten minutes, and all I can remember, because I made it from a lobby over here, was that this reverse communication... The homologous structure works in zero dimensional spaces, and that takes care of the logic of how I stop and watch it, and it's got this extraordinary structure, which is to do with quantum times, which unfortunately, I could only hear it by one minute, so it's got to be super nice, and even if I'd been able to do it all, I would only have been able to follow it up with what I heard, but it sounded very, very exciting. I remember it came out of a question you had asked. If you have a square that's a push-out and a pull-back, then you'll probably amolage it to that and get another square, but just get a push-out and a pull-back, which is the condition that we formulated before, and that's the same formal property that a measure has, a real value measure has. Right, because there was also a whole load of conditions that gave you equivariant maps. I remember, it was the same thing. Yeah, that's right. It was the same thing. I have a question you might be aware of. And about... Oh yeah, that was something else. Yeah, that was... I was talking about the non-standard models of... Oh, that was a separate issue. Yeah, that was when you were discussing how much a classical I don't think I'm going to bother to go to this last meeting.

32:30 I've got them all in here, I've got them all in here. Sorry, thanks for reminding me. Yeah, sure. Sorry, sorry, almost forgot. Thanks a lot. I've got them all in here. Who were we supposed to see to pay for the the books? Because I took some yesterday and left a note for the people. Thank you for your attention. 6.30 at the Banche du Pouvoir in Père-Jean-Louis Pub. We have a discussion on terminologies. I tried to get in one chapter to talk about instead of philosophical insights into mathematics, how it works. There was a theorem that I wanted to explain to people, so I had to dress it up as philosophy somehow, so I didn't think about abstraction.

35:00 Subtitles by the Amara.org community In terms of your mind, I was slightly irritated that we had nothing at all about Poincaré. Nothing about Poincaré. All the history of mathematics, by the way. Well, we can make notes tonight, I guess. Nothing about the greatest mathematician of all time? Maybe his son. Yeah. Postal dinner, or something. Ex-conservative to Poincaré, the scientist. Not Poincaré. Not Poincaré. Rescuing Poincaré from his structuralist environment. His destructive, structuralist environment. I think there's not just a philosophical game here, there's a very important clash of topologies. Namely, what we call combinatorial. You look at g-sets, you look at directed graphs, you look at labeled graphs, you look at all kinds of these useful combinatorials, where they all form totals and appreciates, even pre-sheets, because they're finite in the sense that every object is Zetikin finite. There are no, it's an equational condition, actually. You take the space of endo-maps, the part of the space of, well, the invertible endo-maps, alpha beta equals one, if and only if beta alpha equals one. This is a property of the monoid of endo-maps. Yeah, so we take the monoid of endo-maps for an arbitrary, and you appreciate there's something in one of these purposes. We're just working in some topos. You notice that every object has a property, but that internally defined monoid has that property.

37:30 Alphabets are the only retracts of the answers. Yeah, the only self-retracts. In other words, if the object is a retract of itself, now, you may say, well, actually, what does that mean? You may say that Dedekind's principle is stronger than that, but my point is this. I mean, because you're asking for every object in the totals, suppose you have an endo- Oh, I understand it now. Suppose you have an endo-math. You have an endo which is monic. It's also that. I'm going to prove that using my accent. If it's monic, it may not have a retraction, but passed to the power set, automatically when you go to the power set, things pick up retractions. So if you say every object is at a confinement, that means the power set is too, and therefore it sends back down, you've got this retraction there, and it sends back down the original. The attitude I usually have about data can find that it's a very difficult condition because it's just on endoabs and so how are you going to relate that? Well, this is who every object has a property. Then the lots follows. And it's true of all these topos. So now I want to hear that. Why do these topos all have that property? G-sets for any group G? No, no, no, no. Finite G-sets for a finite group. Finite directed graphs. Finite posets. In fact, there's a theorem, you see, that among groggy copioles, the only finite ones are precinct copioles. I'm sorry, I'm saying... Subtopos itself, of course, is never finite in the sense I just said. No, you mean finite in the sense of some sort of... It could be. It could be she's or something. In other words, there are no rodentic topologies in the finite world. Basically because to preserve finite means implies preserving all means, and so everything has an end point. So all subtoposes are essential, for sure. But then you see that actually, even though you may have had a good deep topology, it turns out that it's again, it's again appreciated category actually. There's another side to it.

40:00 Now I don't know if this can be, my conjecture is that that can be proved axiomatically on the basis of my axiom. If you take any, if you take an internal... If you do an internal sheet code version, then you'll again have that property. And it will in fact be an internal efficiency code version. A whole bunch of strong properties. It should be true. But the hope is that when they're true, the finite things are the intuitive things. There should be a consequence, but there's one answer to both, I think. But I haven't understood the condition of it. The condition is supposed to be on a certain sub-category. No, I don't care. Okay, now, can you clarify what it means on 5.9? No good. No good? No good. No good. No good. No good. No good. So, there's a link about the order of definitions here. See, I don't know where we're starting. We're starting with an elementary topos that has that property? When you say topos, it always means rudimentary topos, and you're confusing what you're talking about. No, no, it always means rudimentary topos. All right, all right. So we're going to start with an elementary topos that has that property. And I just want to appreciate you over that. That should be one. And it should be actually the internal pre-sheaths, and it should be a theorem, so that the topology restricts to another mirror. You've got to wait up for me sometime, and then I catch up, and then I understand what you're saying. This has a link up with Roten's theory, because we can define the notion of a finite Goodman approach. It doesn't mean it's actually finite, but it's an intrinsic property that implies that it pre-sheaths on a finite theorem. There's a theorem in F.G.A.P. about this. Yeah? So it links up. But of course, if I'm just starting with an elementary theory, that's just getting back to the thing, basically. This elementary theory, this is the kind of thing. All I'm saying is that it should be generalized to include all the equipment and common material,

42:30 but those are things that are mathematically interesting. One would like to see what can be done about them. So if you start with that kind of a topos... Those assumptions... For example, there should be a theorem that if it's Boolean, then it's generated by invertible elements. I just mentioned the group case should be equivalent to the Boolean case. The idea is that certainly if you had the right internal theorem, as long as it would be true, and the conjecture is that all you need is this one universal, that it can come out as simple as an equational axiom, the subset of the monoid is equal to that. So I was just thinking, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, during the, Yeah, there is a vast amount of information. I know. Thank you. No, but the condition makes sense. You say, I mean, you could say, if you want to do it, then you'd have to check to see if it really propagated up. But here's another property, you see, in view of the existing theory of finiteness of topology, if I say that every opportunity is not yet to please, but you need something more mathematically useful than Chepensky or Kropotkin's finance, you might think, okay, the finite... The definition of Kuratovsky's finite doesn't depend on having a family of numbers out there.

45:00 If you have one, then you can prove various things. It's simply that by, once again, Dedekind's intersection, you can define the power of the finite units.