aboutlogic #13 | Joel David Hamkins – Set Theory, Pluralism & the Multiverse View

00:00:00: The multiverse view or pluralism is more often called, setheurotic pluralism.

00:00:04: Is the view that there isn't just one true setheurtic reality but rather a kind of plurality of different sets theoretic concepts each giving rise to their own kind of satheuretic truth?

00:00:18: It's not about this theory and our descriptions of the theory.

00:00:23: rather it's a kind to their own independent set-theoretic world, so to speak.

00:00:38: Hello!

00:00:38: Yeah welcome to Aboard Logic and we're very pleased to have Joel Hamkins here who is professor at the University of Notre Dame which is not in France but close to Chicago I understand.

00:00:53: And yeah... Very nice please to have you here.

00:00:58: You previously were at the university of Oxford.

00:01:00: This is correct, yeah?

00:01:02: That's

00:01:02: right.

00:01:02: Yes I was in Oxford and before that i was for many years In New York City.

00:01:07: at the University of New York.

00:01:11: We haven't met in person.

00:01:14: we had one discussion on Twitter.

00:01:18: maybe it was called X. let see where you can go back to this.

00:01:26: Yeah, but maybe let's start with another question and that may be one of the multiverse view because we never had a guest.

00:01:32: That was requested so often at the most.

00:01:35: you were already mentioned in more than one podcast.

00:01:38: some are not published yet they will eventually So may I ask you to explain for our audience, maybe assuming that they already know that CH is independent and they heard there's this forcing construction.

00:01:52: What does the multiverse view?

00:01:54: How much does it entail?

00:01:56: are all universes still classical?

00:01:58: And maybe also... Is it about models themselves or is it about the whole multiverse as one thing?

00:02:04: or how do we imagine that?

00:02:06: Right well thats a great question.

00:02:08: so were just going jump right into.

00:02:11: Right, so the way I think about it is.

00:02:16: one wants to get straight on what mathematics Is About.

00:02:19: So What Are We Doing When we're doing Mathematics?

00:02:21: And what does this subject matter?

00:02:23: and in set theory i Think The Situation Maybe For A Long Time It's Quite Different From In Other Parts Of Mathematics.

00:02:32: But There Was when I was a graduate student for example that kind of pervasive view in Set Theory.

00:02:41: Look, set theory is about the set theoretic universe.

00:02:44: There's this one true set-theoretic universe that we're trying to understand—the nature of the truths in that universe.

00:02:53: Maybe it's something like an attitude people have with natural numbers.

00:02:58: There is this thing, the natural numbers zero one two three and so on.

00:03:02: And it has a certain arithmetic structure in there are truth values or any arithmetic statement as definitive true value in that structure.

00:03:09: okay?

00:03:10: This would be kind of arithmetic version of The Universe view.

00:03:14: That's a kind of singular reality to arithmetic truths.

00:03:19: It was quite common years ago In Set Theory.

00:03:23: A similar situation Was holding in the set theoretic universe.

00:03:27: So every set statement, according to this universe view would have its ultimate truth value and we were trying to figure out what those true values where in the theory was.

00:03:38: And of course Zermalo-Franco's set theory is part that picture.

00:03:43: but large cardinals and so on are probably also a part.

00:03:56: Okay, the multiverse view or pluralism is more often called today.

00:04:01: Setheerotic pluralism that there isn't just one true set theoretic reality but rather a kind of plurality The way it's often described, setheoretic pluralism.

00:04:21: It is not about the theory and our descriptions of the theory.

00:04:26: rather its a kind of reality based.

00:04:28: there are different concepts have said that give rise to their own independent set theoretic world so-to speak.

00:04:36: And those worlds come through different truth values for satheuristic assertions such as the continuum hypothesis or maybe even the axiom of choice Or large cardinals statements that we know are independent.

00:04:51: I find it helpful to think about the case of geometry, thought of geometry as the study Of The One True Geometry, the geometry of physical space.

00:05:08: I think it was a very common view.

00:05:10: That's what they were doing in classical times and all the way up maybe until the nineteenth century there Was still this idea.

00:05:17: that?

00:05:17: There was only one geometry.

00:05:19: And that's What the subject was about finding the geometric truths In the one true geometry.

00:05:25: but of course then with the discovery of non-Euclidean geometry, that concept kind of splintered into several different geometries.

00:05:33: We have Euclideian geometry and hyperbolic space in spherical geometry and so on... And there's a lot of different geometories now.

00:05:40: but we think of those geometries as fully real.

00:05:44: I mean maybe tell us what it's like to inhabit hyperbolic space and they get intuitions about the nature of this kind of geometry, in what its'like-to walk around that kind of space.

00:05:57: And so on... It is not just about theory but reality or mathematical structure.

00:06:04: So it a plural realism because we have different concepts And they have different natures in these different geometries.

00:06:18: So basically, I think almost everyone is a pluralist when it comes to geometry and... ...I like that example because- Oh go ahead!

00:06:27: Sorry i just had an association if I may mention this.

00:06:31: actually If you look at general relativity It seems our actual geometry isn't Euclidean but its some money for with some rather complex structure.

00:06:43: Yes, absolutely.

00:06:44: In fact it's not even any of the other ones.

00:06:47: It's not you know is not hyperbolic space or something I mean like.

00:06:50: it's nothing Like The Pongkori Disc Model Or Anything Like That Maybe Locally Or Something.

00:06:55: But The geometry of physical space is totally weird, and it's modified by the presence of matter.

00:07:02: And so on.

00:07:02: in none of them mathematical geometrical models are anything like that.

00:07:07: I mean you have to Have the physics model basically.

00:07:10: So there's this sort of severing Of the connection between the mathematical theory and physical reality.

00:07:15: and i think most Geometers today if they're looking at these various geometries aren't confused by this anymore, they wouldn't say that oh yeah I'm studying the nature of space in physical reality.

00:07:28: They would say no i'm studying this geometry or that one and geometric transformations, my geometry is defined by this you know.

00:07:41: but by invariance under say these various kinds of transformations I mean in the Erlangen program.

00:07:46: This is a way of defining the geometry by its symmetries mathematical project, which doesn't necessarily have anything to do with physical reality as far I can tell.

00:07:59: Although of course it's very helpful for the physicists to have that knowledge when they're coming up with their more physically realistic models for physical reality.

00:08:09: So i think a bit this analogy.

00:08:12: It's happened in set theory.

00:08:14: now In the same way...I mean there was a kind of independence crisis where, you know said theorists have come to discover that basically almost everything is independent of the Zermelo-Frankle axioms.

00:08:27: I mean in this same way that The Parallel Postulate was observed to be independent of Euclid's other axiomes but it's much more robust phenomenon in set theory because we have hundreds or thousands of independence results not just this handful.

00:08:41: and so this leads very naturally.

00:08:44: There are these different concepts of set and different set-theoretic universes, And they have different set theoretic truths in them.

00:08:52: So this is a kind fundamentally different picture about what the subject Is About.

00:08:55: What Are We Doing When we're doing Set Theory?

00:08:57: Well you know...we're studying The Nature Of These Truths In These Various Universes!

00:09:02: And there's quite A lot In Common To Them.

00:09:04: I mean Maybe A Lot Of Them Have ZFC For Example proving theorems in CFC.

00:09:10: that would tell us a lot about.

00:09:12: A lot of these multiverse conceptions have said, but maybe they don't all have CFC?

00:09:18: Maybe choice is failing in some ways or we get rid of power set and so on... So there's this variety of different theories.

00:09:31: So the project is to figure out what's going on in set theory generally, keeping in mind that there are these different concepts of Set That Give Rise To These Different Truths.

00:09:41: I'm not sure if that isn't answered as a question or...

00:09:46: I think it was very interesting exposition but i wonder ...that sounds almost close to my more constructivist point things out there, but we are really constructing something which we then call sets and they're different ways.

00:10:07: We can go with this sort of evolving subject But you stick to the classical interpretation in some way.

00:10:18: I think There's an affinity because constructivists Looking at situations where there's sort of multiple interpretations of the subject matter and that's inherently pluralistic, but I think maybe

00:10:33: The

00:10:34: from my not an expert in constructive mathematics And i mean.

00:10:38: Of course am a logician and aware of certain things But I don't generally work in constructive Mathematics At all.

00:10:44: you know?

00:10:45: You Know what I Think There'S A difference In That Constructive is as far As I can Tell Are also Very Concerned with our reasoning process in those different theories, it seems like much of the explanation that's surrounding constructivism is about sort of a process of deduction rather than nature-of reality itself.

00:11:18: It's less grounded at least historically grounded in a kind of semantical account of truths, but rather in the proof-theoretic deduction process.

00:11:31: This is much less true though with topuses and so on where we do have these different constructive models... Okay

00:11:41: can

00:11:41: I?

00:11:41: Sure please yes you're an expert on this!

00:11:49: But my interpretation is that mathematical knowledge is evolving and it's more like storytelling.

00:12:00: We tell a story, there are different ways we can go And hence the question of truth seems to be rather problematic because in history certain facts may not been known.

00:12:14: I always use this example Did Captain Ahub have a blue shirt?

00:12:18: I mean, for Moby Dick.

00:12:20: If we don't know it's neither true nor false because its not mentioned in the story here.

00:12:24: So if you view mathematics mathematical discourse as storytelling then The principle of excluded middle seems to be rather problematic And we can only use what's known as Kripke models, or embed models which sort of reflect the idea of storytelling unlike tooth tables.

00:12:46: So that is my personal... view on this.

00:12:50: Right, I think that sounds right and That's sort of what i was trying to allude too because it strikes me as a kind Of very common view amongst the mathematicians working in constructive mathematics is To have some kind of story like that And its exhibiting exactly What?

00:13:05: I Was trying to talk about namely It's not grounded In an objective reality different objective realities in The way they say.

00:13:12: when you Think About geometry Different geometries You know, you could.

00:13:16: I have a picture of the Euclidean plane and i can imagine hyperbolic space in various manifestations.

00:13:22: And it's not...I don't think if is as kind of story but those are just different physical realities which has objective truths under going on in them.

00:13:39: take myself to be telling the story of what it's like, say under CFC plus a measurable cardinal or something.

00:13:45: I just think that some of this set theoretic realities have measureable Cardinals in them and maybe some of them don't.

00:13:52: And also i know...I mean..i guess its an unfortunate coincidence of this word construction because, it has the precise meaning in constructive mathematics.

00:14:03: In connection with intuitionist logic and law of excluded middle but also is used sort-of a software way I think in mathematics generally.

00:14:11: just to refer methods that we have in set theory, you know like foresing and so on or inner models are truncation models.

00:14:26: And so on ultra power models and these are all methods of constructing different Models of Set Theory from a given model?

00:14:33: So the situation is quite interesting because it's If you have one kind of set-theoretic reality, then oftentimes you can define others by reference to it.

00:14:43: Interpret the other model inside of it and realize this other model as a genuine place or genuine realm in which there would be an object... You know if the given model has objective truth values and so on than the interpreted the set theoretic tools that we've discovered, you know throughout a latter half of the twentieth century forcing and all these other model construction techniques which are quite sophisticated.

00:15:18: And those are the tools by which constructing all these different models of set theory and we can think of them as real, just like it's having different groups or different partial orders is something.

00:15:42: So what I'm trying to say You described a sort of fictionalist idea.

00:15:48: I mean this is in philosophy of mathematics.

00:15:50: This is the philosophy of fictionalism where you think of mathematics as sort of telling your story, but it isn't required for pluralism.

00:15:56: i think there's also.

00:15:57: one can just have A kind of realism based view of pluralism like we Have in geometry and And this Is what I defend.

00:16:05: Also in set theory

00:16:07: I mean, you termed the coin a full-blooded Platonism at some point.

00:16:12: So it's even more platonicistic than the classical Platonist because there is little more laissez faire we have much more structures and we take all of them serious so to speak rather then maybe saying that they are nonstandard but real universe.

00:16:34: Go ahead

00:16:36: At some point, maybe a knife question.

00:16:39: Maybe I'm completely wrong so the answer could simply be no and i would know much less about your potentialists work which might fit better to this view because it feels a little more dynamic even though of course you can always step back and say its not dynamic ,it.

00:17:03: It's not really like that.

00:17:05: Is that more fitting to this fictionalist speech, or is it?

00:17:10: Oh I see!

00:17:10: That's quite interesting.

00:17:11: yeah so i think of... So because you work with Benedikt Glover and are familiar with this modelogical forcing which is one manifestation of pluralism but its definitely the only one I mean, the sort of pluralist perspective in Sethir is that there's all kinds different models of Sethir.

00:17:30: However we might construct them and sometimes they're constructed other ways besides forcing... Let me just remark on this Platonism because you mentioned full-blooded platonism which It used to be in set theory that if you said, You're a Platonist.

00:17:53: That it implied that you also had the universe of view when I was a grad student at that's what people met.

00:17:58: When Bob Salovey talked about Platonism he always meant It means there's a singular set-theoretic reality.

00:18:06: But I think now we've changed this, and Platonism is as it should be rather about the realism of underlying conceptions rather than about the singularity of the uniqueness.

00:18:17: so i consider myself a Platonist even though uh... There are different set theoretic universes where you sever the connection with uniqueness its'about Realism which goes back to this fictionalist question yeah?

00:18:29: So our understanding in The Foundations of Mathematics you know, based in fictionalism or say formalism or something.

00:18:38: Is it about the reasoning process?

00:18:39: Are there genuinely real set theoretic realms that we're trying to study right?

00:18:46: and so Platonism is for In The Ladder case not so much in the former cases.

00:18:51: So It's Not Necessarily Connected With Singularism Or Monism Right, so full-blooded Platonism has a lot of affinity with this pluralist view.

00:19:04: I mean it's explicitly pluralists.

00:19:07: about potentialism really?

00:19:09: This is another issue... So i've done a lot work on synthetic potentialism and also arithmetic potentialism.

00:19:20: Going back to Aristotle, of course there's the distinction between potentially infinite and actually infinite.

00:19:26: But this sort of current thinking on potentialism is severing the connection with infinity.

00:19:33: really what potentialism about?

00:19:36: Is your realm, is your mathematical realm completed or not ?

00:19:41: Or are their partial universe fragments that can be extended?

00:19:46: yeah And so okay in classical view, what I call sometimes Aristotelian potentialism for arithmetic.

00:19:53: You know we have this idea that well the numbers are infinite.

00:19:56: you can have more and more only finitely many at a time.

00:19:59: but But we can do this in set theory, too.

00:20:13: There's some very natural conceptions of set-theoretic potentialism.

00:20:17: so you could look at say even if you think there is a underlying reality for the set theoretic universe that cumulative hierarchy V... You could imagine well I'm it's growing its evergrowing It's never finished but it Can be made taller always?

00:20:32: So like If maybe realms would be some v-alpha in the cumulative hierarchy, and you can access... You make it taller but you never get the whole thing.

00:20:45: So this is one form of potentialism.

00:20:47: that's called rank potentialism.

00:20:49: And if you have an idea that the rank potentialist levels are always given any two of them One of them is taller than another.

00:20:59: There's a linearity to it.

00:21:01: That leads us into certain modal principles.

00:21:03: for example If you have a concept of potentialism where the worlds are linearly ordered, then you're always going to validate S-four point three.

00:21:12: There's some modal theory.

00:21:14: that point three axiom is expressing this linearity.

00:21:17: Yeah But there's other kind more radical Conceptions.

00:21:20: for example if you look at forcing as a Potentialist conception I mean in the model logic of forcing i think it now explicitly has potentialists.

00:21:28: You Have models upset theory In The context Of all Their Forcing Extensions and This Is It's actually not true in general that this is a convergent system, it's not directed.

00:21:40: If you say take the countable models of set theory and look at the forcing extensions then this is not directed...it's not convergent.

00:21:47: so there are two extensions that can't be amalgamated but nevertheless still fulfills the modal theory.

00:21:53: S-four point two which exactly the modal theorem valid on the convergent frames So its sort of convergent semantics, so it's as though its convergent.

00:22:09: If I have a model of set theory or accountable model if that three are any model said to me and had two forcing extensions that satisfy each of them some necessary statement then there is this single extension obtained by product-forcing which satisfies the conjunction being necessarily true.

00:22:23: so i can sort of put them together.

00:22:25: That's kind of directedness or convergence phenomenon.

00:22:30: And So uh...so then It's not linear.

00:22:34: we get a different model logic, S-four point two.

00:22:36: This is what Benedict and I proved.

00:22:38: yeah so in the rank potentials in case you got s four point three but then if you just look at say arbitrary models of set theory under top extension there might be different You know, then it's a theorem of mine that you get exactly only S four being valid.

00:22:59: So you don't have any amalgamation if there is no linearity and so on And its quite remarkable actually That you'll only have s for in this case.

00:23:09: I think all those project analysis are evolving.

00:23:15: We now we've got the paper i wrote with one my students Wojciech Wojoczyn on modal model theory provide tools for analyzing, say the models of any theory like graphs or groups are fields or whatever.

00:23:32: You can take all the models at this theory and view it as a potentialist system where you take a model in the theory and it accesses understand, you know what is the modal logic of group theory?

00:23:46: or What Is The Modal Logic Of Graph Theory and so on.

00:23:49: And these are quite rich questions and extremely interesting to work out.

00:23:57: these all in extensions, right?

00:24:06: So

00:24:07: you mean for which theories do we know...

00:24:09: Yeah yeah I mean if you tell me okay this axiom system has S-IV or S-III.

00:24:17: i'm not a specialist on motorlogics but what does it tell us about the logic ?

00:24:24: I

00:24:26: see so part of Part of what Benedict and I had done when we figured out the modal logic of forcing is that, um... We introduced some... Some modal vocabulary which turned out subsequently to be extremely useful for understanding The logic of these other systems in categories And so on.

00:24:53: For example, we have a concept of button and switch A switch as statement that you can turn it on and off by going to larger worlds.

00:25:04: So, you have some potential assistance with possible world that your thinking about.

00:25:07: maybe its the models of set theory under the forcing extension relation or may be its graphs under the subgraph relations induced sub graph relationship.

00:25:17: so you could add new vertices in new edges but not new edges between old points ya know?

00:25:22: That's a potentially system.

00:25:24: or maybe it's groups under the subgroup relation, so you can take a bigger group.

00:25:29: So switch is a statement that you can turn on and off by going to a bigger universe like for example in set theory.

00:25:38: they continue hypothesis is a switch, because you can force it to be true and also false.

00:25:50: It's independent in this very robust way with respect for forcing which can turn both on or off.

00:25:57: I mean classically we didn't need to force it.

00:26:04: that showed it's true in an inner model.

00:26:06: So for independence, you don't need to force it.

00:26:08: but it happens to be true.

00:26:10: not only Cohen's method not only shows that you can force not C-H But Solovey observed You could also force C H. so you turn on and off by forcing By going into a bigger universe.

00:26:22: always you change the truth value or for example in graphs.

00:26:25: think about graphs.

00:26:36: and now it has diameter at most two, but I could also add a long chain.

00:26:43: And now it doesn't have diameter too.

00:26:45: so having diameter is the switch in model graph theory?

00:26:52: Well what i didn't understand was do you get this model theory just from first order axioms or another ingredient like how we organize our models?

00:27:04: Oh, I

00:27:05: see.

00:27:07: Right okay so the proof...I mean the modal theory is a theory not about one set theoretic universe but about that universe in the context of all

00:27:20: First order models of the axioms of set theory?

00:27:23: Yes,

00:27:23: for example.

00:27:25: The

00:27:25: accessibility relation would be forcing or maybe it's top extension and end-extension.

00:27:30: we have dozens of different extension concepts For models of Set Theory And we've worked out the model logic.

00:27:38: So the model is not just given by first order theory But you also need to add this extension logic, right?

00:27:45: Yes.

00:27:45: Yeah exactly so it's

00:27:47: the say for example take any first order theory T and look at a mod t that is class of all models of T under say the substructure relation The submodal relations.

00:27:59: So

00:28:00: every model accesses bigger models into which it embeds.

00:28:06: that's the possibility relation, accessibility relations.

00:28:09: And then you get a crypti model basically.

00:28:12: so it has a modal logic and... The question is well what is that modal logic?

00:28:17: We've been able to figure out in a bunch of cases what it is.

00:28:22: There are deeper connections now than Vojček my student thinks about.

00:28:28: in terms of categories

00:28:31: I was just going through.

00:28:33: Yeah, so basically if you have any concrete category of L structures say yeah So a concrete category graphs or groups?

00:28:42: Or whatever.

00:28:43: You like so

00:28:44: by category what do I mean?

00:28:45: You don't mean category in the sense of categories theory in

00:28:48: category theory sense

00:28:50: Yes, yes, okay.

00:28:51: A concrete category though.

00:28:52: so it's kind of a set.

00:28:55: because What i want is that the morphisms are actual functions cuz they're providing counterparts for the individuals in the worlds, right?

00:29:05: So a category is a bunch of worlds which consists of individuals and the morphisms are functions on those individuals.

00:29:12: And those functions provide counterparts basically in other models.

00:29:16: Right!

00:29:17: It reveals when you're thinking about potentialism.

00:29:21: there's this cleavage between philosophers and mathematicians because in the sort of, the philosophers who like to think about potentialism they want.

00:29:30: The possible world and then there's a bigger world but the old individuals are still there as themselves right which means in a sense the morphism that their interested is the identity.

00:29:42: you know an inclusion map But it turns out you know, if I have a bunch of graphs and i think about the subgraph relation where it has to be identically a subgraph not just embedded but actually a sub graph in the sense that the individual points are the same point then uh... mathematically that conception actually as very poor amalgamation properties.

00:30:10: If I have a graph, I can extend it this way or extend to different graphs using some of those same individuals but in an incompatible way and so i wouldn't be able put them together.

00:30:19: And so mathematicians generally prefer the embedding formulation where there's morphisms.

00:30:25: then we could have amalgamation and ask well does that diagram commute?

00:30:32: Those all have consequences on the modal theory.

00:30:34: So philosophers like think about the counterpart as identity and the mathematicians prefer to have this kind of counterpart coming from morphisms.

00:30:43: And then we have to discuss commutativity explicitly, and so on...and you get better amalgamation properties.

00:30:48: but it turns out—it's a theorem that I proved with Wojciech–that the modal logic if i have a theory T – and I like the models of t- than…if I define the modal the modal assertions are identical.

00:31:06: The modal theory is exactly the same, and one of my other students Sam Adam Day proved in fact those two potentialist systems by similar.

00:31:20: which kind explains why it's true that the modal logic is identical as a deeper explanation than Wojciech and I had.

00:31:36: Can I do a tiny, tiny remark?

00:31:38: And we already mentioned Platonism and Constructivism.

00:31:43: Let me say sometimes this has like a formalist flavor to me because you are so... You and other satirists always able reinterpret things it's never.

00:31:53: It's not so much the intended structure.

00:31:56: We have this formal system and we can look at it in different ways, just stepping back and putting in graphs there is genius and insane!

00:32:05: At that moment right?

00:32:07: Such a nice example but feels a little formalistic as well because you are able to change perspective.

00:32:20: You can still be a Platonist and do that, of course.

00:32:26: Oh I see!

00:32:28: So you're saying because i'm looking at all graphs somehow this means I must be a formalist?

00:32:37: No no...I don't say it's so nice how you really look the symbols without any intended meanings in that sense.

00:32:48: So it's not a statement about the reality of mathematic objects or anything, completely agnostic on metaphysics?

00:32:55: Or one could take pluralists instead of formalist maybe.

00:33:01: Formalism can be considered form-of-pluralism I suppose right?

00:33:07: I always thought that formalism is sort of like philosophy and nihilism.

00:33:12: you know mathematics only engage with symbols.

00:33:17: So in my view, the people I mean start maybe... Maybe i have a very naive conception of Platonism.

00:33:24: They started with platonism that mathematical objects about like are real as they're like real things.

00:33:33: or like these sets there are real and some sense Or at least it's a metaphor.

00:33:38: but then realized this is not working really well disillusioned and become formalists.

00:33:48: Everything is just a game with symbols, yeah?

00:33:51: And I would hold in there between the constructive perspective to say no it's not just again with symbols its part of our culture evolving knowledge but it isn't fixed It always moving.

00:34:06: How do you relate this maybe?

00:34:09: Right i think that makes sense.

00:34:13: Formalism is sort of consonant with pluralism in the sense that your theory is not complete, and so there's going to be statements you can't prove or refute.

00:34:23: Your theory could be extended by adding such a statement as negation and this partakes out the pluralist manner for having lots different worlds.

00:34:35: regarding realism I think many mathematicians have the idea that they find it too difficult to undertake mathematics except by taking this subject matter in a realist way.

00:34:53: When i'm reasoning about a mathematical structure of a kind, even when i'm reasoning about an inner theory then imagining objects as being real and so on is actually quite helpful for Thinking about what's going on in this structure.

00:35:12: It's giving me, you know structural things to grab onto with my mind.

00:35:18: I mean and it helps but okay ultimately its arguing in a theory.

00:35:23: so i wrote A paper recently About arithmetic potentialism the universal algorithm resolved And a lot of the arguments in that, or no I'm sorry.

00:35:35: I am thinking about different paper on the linearity phenomenon and consistency strength .And i gave some arguments.

00:35:44: uh...in that paper arguing certain things are not provable from this theory ,or that theory..and always I was defaulting to well take model of this theory and argue what's going was able to show that every model of this theory has this other thing happening.

00:36:05: And so therefore, that's a theorem of that theory right?

00:36:08: and the referee objected... The referee had more view like Thorstens maybe or kind of possibly yeah Maybe it with you I'm not sure I mean i have but said well look You're really just arguing in the theory But somehow felt extremely difficult to undertake proof That way by just thinking in the theory instead of thinking I have The Theory, i take a model Of the theory now.

00:36:35: I Have objects that can reason About what they're doing and so on?

00:36:39: I Can live In that Model And think about What it's like to Live in that Model.

00:36:43: and that's how my argument went.

00:36:45: but the referee was saying well you can You don't have To have the Model you can Just argue in the Theory which of course is totally correct except They would've never been able to come up with the proof if i Was Doing It Like that.

00:36:56: no I mean explanations are very important, right?

00:37:00: And...I don't mind the Platonist metaphor.

00:37:05: But i'm just saying that it's a nature of mathematics!

00:37:10: I miss middle there.

00:37:11: I think metaphoric use of platonism is completely useful and as you say helpful here.

00:37:20: but if I step back look what am doing Then, it's not about things in the real world.

00:37:27: It is just a metaphor which I use because... ...I can think of the real-world and I'm used to thinking about objects in the Real World.

00:37:35: so that uses this metaphor to explain or understand whatever.

00:37:38: You know?

00:37:39: That was totally right!

00:37:40: And also there are something more going on with that remark Because what is philosophy of mathematics for?

00:37:49: We have these different philosophical views like Platonism fictionalism or formalism and so on.

00:37:56: And they seem quite different until their disagreeing, but of course mathematicians might have these different views that almost never disagree about what the theorems are... I mean ...about what's proven?

00:38:08: One begins maybe to realize having a philosophy in mathematics isn't telling you the nature pointing you towards what is going to be an interesting mathematical project for you to undertake.

00:38:27: So someone with the universe view in set theory, that's their philosophy they're gonna be led to finding out these sort of sweeping fundamental principles that they would like to find true In That One True Universe.

00:38:40: and this is for example The Kind Of Thing That Wooden Is Doing With His Ultimate L Program And so on.

00:38:45: he He has the universe view and he's trying to find out what are the truths in that one

00:38:52: true

00:38:52: Universe, anyway It's a way of understanding.

00:38:54: What?

00:38:55: He is trying to do And what he's motivated to do whereas someone with up the pluralist View instead theory is going to be led to looking at well how you know if you have a lot of different universes of set theory, how are they related to each other?

00:39:09: And this leads immediately into things like set theoretic potentialism and the modal logic where somehow someone with the wrong philosophy is getting it wrong on the nature of mathematical reality, rather.

00:39:27: It's that that philosophy is going to be leading them to certain kinds of projects whereas a different philosophy might be leading then other kinds of project.

00:39:36: Someone who finds constructive mathematics compelling is inevitably gonna find themselves studying toposes intuitionistic logic, but not classical logic.

00:39:50: That's what is going to happen if you have that view whereas following classical logic then you're gonna find those examples maybe less interesting or less compelling?

00:40:02: Okay yeah and I would like to get back to our... Maybe don't remember?

00:40:09: we had an interaction on Twitter.

00:40:16: You accept pluralist view on the level of axioms foundations, but I would go further and say maybe there should be also a pluralistic view about the logic we use for reasoning.

00:40:29: Maybe that is already included?

00:40:31: And at this point it was about the difference between proof by contradiction.

00:40:40: And there is actually a paper by Andre Bauer about five steps towards accepting intuitionist mathematics.

00:40:48: He was also previously on this podcast, where he makes the point that we should distinguish these two because one of... I mean it's quite a lot confusion.

00:41:05: in mathematical power These are often identified.

00:41:10: I mean, they're not distinguished which creates lots of confusion because people think if the intuitionist rejects a principle of proof by contradiction hence there cannot prove that Skirt Of Two is original!

00:41:25: Which isn't true obviously.

00:41:30: and at time you say these two things basically indistinguishable.

00:41:38: No, well okay.

00:41:39: So I think yeah remember this discussion very well and of course i know Andrei Very Well and have interacted with him quite a lot.

00:41:46: he was the guest in my home New York years ago.

00:41:48: He came to visit.

00:41:51: so Right, my view of the matter is that in constructive logic.

00:41:54: Of course you want to distinguish between these two things because they're totally different.

00:41:59: one of them is logically valid In instructive mathematics and the other one isn't And that's very important in constructive mathematics To have a different view okay?

00:42:09: In classical mathematics however This is simply not the case.

00:42:14: an in classical logic The two methods are basically this same method plus the idea that negation is a kind of duality and double-negation isn't doing anything.

00:42:26: And so if you think of the move, double-negation elimination as essentially logically trivial which it in classical logic then the distinction between proof of negation and proof by contradiction totally evaporates.

00:42:41: I mean, classical logic mathematicians have.

00:42:47: They don't distinguish between these precisely because they don't think there is a big difference uh...between the statement and its double negation-they want to basically identify those two statements and that makes the distinction evaporate.

00:43:01: And so therefore also i think maybe the constructed mathematicians overplay their hand if they want say certain proofs which almost everyone agrees are proofs by contradiction, but aren't technically proved by contradictions in constructive logic such as the irrationality of the square root two and other things.

00:43:23: Because like this... Sorry!

00:43:25: But even a standard argument assumes something is rational and then there's a contradiction.

00:43:38: It's not like assuming the negation of a statement, proving it wrong and then implying T. Yeah I totally

00:43:47: get that!

00:43:48: It is proof of negation but it isn't proved by contradiction.

00:43:50: according to this standard view in constructive logic except for what I teach my students You're using proof by contradiction whenever you prove a statement, By supposing the opposite and getting a contradiction.

00:44:12: And that includes proof of negation.

00:44:15: So okay I'm not saying That the constructive mathematicians have to use this terminology.

00:44:21: i'm just saying This is by far The most common understanding Of what it means To do a proof by contradiction.

00:44:27: It means you want to prove a statement and so assume the opposite of it, whether that's adding a negation or removing an negation is immaterial because those are just trivially the same thing in classical logic right?

00:44:40: And therefore... You know then you get a contradiction

00:44:54: possibility of constructive thinking.

00:44:56: I mean, which sort is so hidden in a way?

00:45:00: I mean even classical mathematician may say oh we have an explicit witness of this.

00:45:06: there's actually const... they're made in the metamathematics make it distinction but not in the actual logic.

00:45:11: yeah right which i think as a weakness.

00:45:14: okay that's my view.

00:45:19: What I think is important, to be open to this pluralism.

00:45:24: To say that there are actually different ways to interpret logical connectives and it leads in the case of distinguishing these two concepts which i think is quite important for avoiding confusion.

00:45:41: So, that is recently.

00:45:42: I read a girdle biography where the author also tries to explain intuitionistic logic.

00:45:49: And then he claims exactly this example squared of two rationality of square root of two.

00:45:55: it's not provable intuitionist technology because obviously there's confusion... This confusion quite widespread and creates a confusion about these pluralistic potential ways to interpret logical connectors.

00:46:12: Yeah,

00:46:13: I mean obviously in the context of any discussion involving constructive mathematics you have to distinguish between these two things?

00:46:22: Okay what i was asking is for to acknowledge that there are different ways to interpret the connectives.

00:46:35: I wouldn't ask everybody to become entusiasmist, yeah?

00:46:38: That's okay!

00:46:41: Maybe after The Revolution but...

00:46:43: Okay?!

00:46:49: So appreciate some sort of pluralistic presentation or understanding.

00:46:56: I mean, I guess also that...I argued with André about this use of the proof by contradiction being strictly used in the intuitionistic sense.

00:47:10: But i think it's harmful to say for example many of the proves conventionally regarded as proof-by-contradiction are not actually proved.

00:47:21: young people's understanding of mathematical principles to make a big fuss and say, well that is not actually proof by contradiction when they are supposing the opposite in getting a contradiction.

00:47:34: And then deducing that thing was true?

00:47:36: I think it has quite robustly described as proof-by-contradiction.

00:47:42: you said this invites confusion.

00:47:43: but no this distinction at too early a stage in a context where there is no intuitionistic logic happening for these students.

00:47:54: It's an entirely classical logic arena, then it's confusing not to call it proof by contradiction In my view.

00:48:02: Okay I guess we disagree

00:48:05: with the disagreement.

00:48:11: So

00:48:13: maybe one... something we hinted at quite a lot is this question of philosophy and math, how they interact with each other.

00:48:23: And another thing maybe in some sense we also talked about some historicity moment ago because in the intuitionistic world where Brauer was more powerful than we all learned into his next mile or maybe hiding up whatever... that important or whatever.

00:48:42: That doesn't matter, but there's a... We can play the game of Contra factual history and just say we entwish.

00:48:49: this technology is thought to first year BA students And then this distinction would make sense too.

00:48:56: have it their

00:48:57: in this right?

00:49:00: So you drew another alternative world one where CH was settled

00:49:06: and

00:49:06: blockposts Of yours.

00:49:08: But I mean that wasn't historicity in the sense the math would have been different, right?

00:49:13: The theorems will all be same as today but we never had a multiverse view.

00:49:20: Do you think that you could elaborate on this a little bit?

00:49:22: how to imagine

00:49:25: it?

00:49:25: This paper has now appeared in the New Journal of Philosophy and Mathematics for the first few years.

00:49:32: so there is sort of mathematical philosophical thought experiment I proposed.

00:49:40: I didn't want to suppose that any mathematics was different, but rather just the order in which the theorems were proved was slightly different in history.

00:49:46: Which would cause us to have a different view about what's fundamental in mathematics.

00:49:51: and so my thought experiment was the following Let's imagine back in the time of Newton and Leibniz That they were a little bit clearer About infinitesimals.

00:50:03: Yeah So i mean Of course we all know They had found calculus on infinitesimal also that it was a little bit sloppy, and people like Bishop Barkley had sort of mocked them by pointing out these flawed foundations.

00:50:18: Nevertheless even those lousy foundations were extremely successful!

00:50:23: And they basically found all the fundamental theorems of calculus quite robustly without any epsilons or deltas in that era... So I sometimes say well this example shows, do you need firm foundations to develop enduring mathematical theories of enduring value?

00:50:49: And the answer is apparently not because in calculus that's what happened.

00:50:54: We had these very ambiguous and flawed foundations of infinitesimals in the early days and yet calculus developed in a quite satisfactory and full rich manner.

00:51:08: Okay, but let's imagine they were a little bit better at infinitesimals.

00:51:11: So what I posit is that well maybe they had some idea about sort of two number realms.

00:51:15: there was the real numbers and then this larger number system Improvement on what they had.

00:51:24: and we know that this improvement, of course It's fundamentally sound because we now understand the hyper real numbers very well in infinitesimals And transfer principle and non-centered analysis.

00:51:34: So so basically my thought experiment is to imagine They did a little bit better With infinitesimal with two number realm idea and furthermore That they have these kind of beginnings.

00:51:47: The transfer principle would be just the idea that everything that's true in the real number realm is also true In the larger number realm, which we might as well call the hyperreals.

00:52:00: So something like a proto-hyperreal, prototransfer principle Also you would know the hyper reels Would Be A Real Close Field and so on because That's True in the Real Numbers.

00:52:11: And Gradually This Idea Would Emerge of this concept, of this hyperreal structure.

00:52:17: And calculus would in my thought experiment be founded on this idea.

00:52:21: so gradually over a few hundred years the ideas about this r star structure will become richer and more sophisticated Along the lines of non-centered analysis, then we wouldn't have epsilons and deltas in limits.

00:52:38: But We would have the arguments you know with taking this standard part And so on just as we do in Robinson's theory.

00:52:45: Okay So then in the late nineteenth century Of course we had these extremely important philosophically and mathematically Important results.

00:52:54: for example Dedekind gave us a categorical account of The successor function On the natural numbers.

00:53:00: right he proved that There's only one concept of successor on the natural numbers fulfilling his three axioms, you know zero is not a successor.

00:53:11: The successor function has one to one and every set of numbers containing zero closed under successor contains all the number.

00:53:18: so induction That's a categorical theory.

00:53:21: it uniquely determines the natural members up to isomorphism.

00:53:24: And in my view, this theorem is the beginning of the philosophy of structuralism and mathematics because he's identifying a structure not by giving us kind of construction on what objects are like that Frager was trying to do but rather it said no.

00:53:40: It's this theory.

00:53:41: any two models or these theories are isomorphic to each other.

00:53:44: This is essential nature of Structuralism.

00:53:48: Huntington proved in nineteen oh three The category result.

00:53:53: It's the unique complete ordered field.

00:53:55: Any two complete order fields are isomorphic.

00:53:58: Okay, so we gradually started getting category results for all of The standard.

00:54:05: I mean all of them.

00:54:06: mathematical structures You know in the pantheon and natural numbers the rationals the integers the real numbers the complex Numbers And so on We have category results For All Of Them.

00:54:16: But In My Thought Experiment World The hyper-reals around this list are star, right?

00:54:22: It's one of the familiar mathematical structures used in the foundations and mathematics.

00:54:27: And mathematicians would demand a categorical account of it in the same way that they did for all of the other structures... ...and its possible to provide a categorically count.

00:54:40: Dan Isaacson, a philosopher at Oxford really emphasizes an important philosophical role Categoristic results provide in providing meaning In mathematics.

00:54:52: So the reason why we find it meaningful to refer To the natural numbers is because We have this category result and The same for the real Numbers, And so on complex numbers?

00:55:01: So that the Meaning and reference of those structures Is grounded in the categories.

00:55:06: so we would need such a result For the hyperreal numbers and It's possible to give it.

00:55:12: If you write down the axiom ZFC plus the continuum hypothesis, then you can prove that there is only one up to isomorphism.

00:55:20: Countably saturated real close field of size continue.

00:55:24: so this it does a unique smallest countably saturated feel.

00:55:30: But that proof requires CH.

00:55:32: I mean, that theorem was actually proved in the nineteen fifties and so on but it could have been proved earlier because its just a back-and forth argument which is similar to The Huntington Results, similar to Cantor's Proof of the uniqueness of the countable dense linear order except with countable saturation.

00:55:49: now It's a recursion That goes for omega one many steps instead of just countably many steps the back-and-forth argument, but transfinite instead of only omega.

00:56:01: And so... Okay!

00:56:04: So this theory would have provided us with a categoricity result for the hyperreals which would've been recognized immediately as an essential fact for providing meaning in this concept.

00:56:19: that was totally at the core.

00:56:23: This is how continuum hypothesis would get on the list of axioms.

00:56:26: People would recognize.

00:56:28: we need it to prove this theorem, give meaning to calculus and so... ...this is a thought experiment showing that continuum hypothesis might have come to be a fundamental axiom.

00:56:42: And what does that do with the pluralist story?

00:56:45: Is now pluralism just like coincidence in slightly different world?

00:56:50: You would never see this clear truth?

00:56:53: Right, the question is... I mean, i take the argument to show that this historical contingency in what counts as a fundamental axiom and maybe you would argue well with your thought experiment about Brower taking power or whatever.

00:57:09: This historical contingancy is what are the logical truths right?

00:57:12: Or What Is The Logical System That We Should All Be Working In?

00:57:15: Maybe Also Has Some Historical Contingency Regarding That.

00:57:21: But Let Me Relate Another Story Though About How This Was Received.

00:57:25: Namely people, this philosopher Daniel Isaacson who I just mentioned in Oxford subscribes to the universe view in set theory.

00:57:37: and of course if one argues that it's possible That something is fundamental And you take that as successful then?

00:57:47: If you think there's only one universe Then you would think that its actual.

00:57:53: So he once described me Joel, you've solved the CH problem because this is a reason to accept CH.

00:58:03: I mean not just in-the-thought experiment but actually we should accept CH because it provides categorical account of infinitesimals

00:58:12: and... I wouldn't be surprised if there's an alternative sub application or line of thinking which is not compatible with CH.

00:58:22: When my observation is that actually I find this drive for completeness quite a bit misguided, because in completeness it's beneficial.

00:58:38: Because you have got more applications for your theorems and no matter which direction to go they will still hold right?

00:58:46: And so, I think it's good to be incomplete.

00:58:51: It is good to use Viga theories and I would even go as far from a sort of intuitionistic point-of-view where you can distinguish propositions or statements which are indistinguishable classically but which are important especially if your work in connection with computer science want actually compute something then these distinctions are essentially essential.

00:59:15: anyway

00:59:16: I totally agree with that.

00:59:17: And this is basically an argument for pluralism.

00:59:21: also, there's a sort of richness in the plural context... ...that is absent from the monist contexts.

00:59:29: but actually i want to remark on something you said because you said weaker foundations and it's something..I've been trying to call attention amongst philosophers or mathematics The dispute between weak and strong foundations, I think is really core.

00:59:45: And it explains so many other disputes such as the dispute between classical and constructive logic but also between the multiverse view in the universe of you and so on.

00:59:57: Sort of mathematically when your prove a theorem that's an implication then its better if you weaken the hypothesis or strengthen.

01:00:05: conclusion.

01:00:06: thats common attitude in mathematics, and I think it's maybe the same kind of attitude which makes one want to prefer weaker foundations.

01:00:19: Well we should have a weaker foundation as long as its still sufficient.

01:00:25: You know, ZFC is too strong.

01:00:32: We don't need replacement or whatever to do the kind of classical mathematical structures and so on.

01:00:38: And I think this kind of explanation Is part Of this argument i'm trying To describe.

01:00:43: for weaker foundations we want The weakest theory which is strong enough to Do what you wanna do?

01:00:49: I mean you go even farther in your remarks by saying well actually it's This sort of rich Plurality maybe of foundations are different foundation.

01:00:59: Okay, but let me give you the case that is sometimes made for a strong foundation.

01:01:03: So one can find this case from generally the universe view.

01:01:08: set theorists are pointing out look these strong foundational theories like with large cardinals and so on have consequences for fundamental mathematical facts even in arithmetic.

01:01:25: they have arithmetic For example, large cardinals have all kinds of consequences down low for sets.

01:01:35: It was a classical problem in descriptive set theory, in the early twentieth century to figure out how complex can measurable sets be.

01:01:49: How far we push it?

01:01:50: Braille sets are measureable and you know...can we push further into analytic sets or go up higher in projective

01:01:57: hierarchy?".

01:01:58: And kind of stalled at certain point they weren't ever able prove that these more complicated necessarily measurable.

01:02:06: And now we know this is independent of CFC, but it's not independent of cfc plus large cardinals.

01:02:12: actually It's a theorem if you have enough large Cardinals then every projective set of reels Is Lebesgue measurable and has the property of bearer?

01:02:22: The perfect said property so forth.

01:02:23: So it has all these regularity properties.

01:02:26: But these are things that we want to know like.

01:02:29: That's good consequence Of those strong foundations To know that well whenever you define a set by quantifying over the reels and the integers, You know then it's gonna be automatically measurable.

01:02:43: in practice This is observed to be true.

01:02:45: Whenever we can Define a set like that It isn't fact measure but okay?

01:02:48: Not a theorem though of CFC But it is a theorem if you have the stronger axioms.

01:02:54: so there's another way I could finish up.

01:02:56: The point is that what are they?

01:03:01: It seems like this idea of weakening the hypothesis of an implication is not really necessarily appropriate for foundational matters.

01:03:08: The argument for strong foundations, we're going to be pointed towards fundamental truths that we would like to know about if we seek out strong foundations.

01:03:21: but If you are never looking at a strong foundation then your gonna totally miss these consequences which actually quite welcome.

01:03:31: Yes, so my reply would be there is another way to deal with exactly the situation you mentioned which is synthetic mathematics.

01:03:41: So like actually we do this a lot We reason in... In this case type theory but reinterpret and work into model of types theory And everything that's closed under these principles.

01:03:57: for example maybe all functions are are continuous, actually all functions are measurable.

01:04:02: All types are measurable and so on.

01:04:05: And those inside the theory.

01:04:07: we have these strong principles but We can interpret them then in a much weaker theory and understand some.

01:04:14: So this is very useful for quite complicated reasoning because often or all details you would have to carry around if you do the reasoning concretely are getting out of hand.

01:04:30: And doing this synthetic reasoning addresses both points, I mean usually justification is it eliminates the boilerplate all these complications.

01:04:40: but also you do need to change your foundations and accept new fundamental principles.

01:04:48: just interpret all your theological symbols in a different way.

01:04:55: But I don't understand how that method could ever get you to the claim, say... ...that every projective set is measurable.

01:05:03: Because all of these sets can construct a projective in theory?

01:05:09: If we look from outside… You use some rather weak closure principles and always stay within this realm!

01:05:20: Okay, but some of these statements that I'm talking about though have a large cardinal strength.

01:05:25: So it's just not possible to... If you're in a situation where you know- Sure!

01:05:30: ...someof the statements then it implies…

01:05:32: Sure Yeah yeah if the statement is consistent About the real world objects they need some strengths so we can't get this.

01:05:41: But inside the theory

01:05:43: I see, okay

01:05:45: You synthetically create them.

01:05:50: Look at the paper where there is an interpretation of measure theory inside type theory and every type can be measurable.

01:05:59: It's unproblematic because actually, The foundations are so weak that you can interpret it in these different domains.

01:06:06: So its suitable for this kind of synthetic mathematics.

01:06:11: I see That's very interesting.

01:06:13: And Thorsten do we want something to ask?

01:06:15: Otherwise i will continue.

01:06:17: This is related

01:06:18: with what i just saw introduced in a way.

01:06:23: I always wonder, so mathematicians or logicians often focus on first order logic and then maybe some axioms like ZFC as the way to do mathematics?

01:06:37: And i find that we should not just be interested in questions of consistency but also How natural can we express our concepts?

01:06:54: And since you mentioned structuralism, I find that set theory with predicate logic is very low level because you always talk about including of sets.

01:07:18: Natural numbers, you have this for Neumann encoding but then there are alternatives and okay.

01:07:26: And in a way when I talk about natural numbers i don't really want to talk about the encodings... ...I want to stay abstract layer.

01:07:34: so In this context language of predicate logic is not so suitable And we have alternatives, so when you have languages like in this case type theory where they cannot talk.

01:07:50: I mean about the element relation or anything that you prove upon natural numbers holds for all isomorphic structures automatic.

01:08:02: This is a univalence principle maybe of your field.

01:08:06: So what's your comment on these?

01:08:11: So I guess, regarding Set Theory specifically.

01:08:14: I think of set theory is really this kind of two aspects to roles that set theory plays.

01:08:21: and on the one hand set theory Is its own subject matter with it's own questions?

01:08:27: And its own tools and methods and so on.

01:08:29: It was born by considering the concept of transphonic ordinals which is a concept that came out of Cantor's work on the Cantor-Bendixon theorem where he had at heart, you know this is the result when you have closed set and remove isolated points.

01:08:47: And now we've got new closed sets in your move isolated point again and iterate these.

01:08:51: but after omega many steps You might not be done because intersection all those might still have isolated points need to go transfinite.

01:09:00: so Cantor needed To invent the idea of ordinals in order to make sense Of that process.

01:09:07: and this is, In my view The sort-of birth of set theory Is in this transfinite Idea.

01:09:13: And other people Adrian Matthias for example described Set Theory as a study of well founded recursive definitions and constructions.

01:09:21: It's inherently about these sort of Transfinite iterated processes which are very interesting fascinating robust idea.

01:09:32: And of course, part of that picture then is the cumulative universe of sets which is itself Transfinite iterative construction, but on the other hand said theory also happens to serve in this almost philosophical role as a foundation of mathematics.

01:10:02: It was found itself quite convenient for that matter and The reason for it is that mathematicians notice.

01:10:10: That essentially any mathematical structure of any kind can be Interpreted in set theory And this is making at very robust and Important, it was important in mathematics to have a foundation.

01:10:25: A single foundation I mean Not a single one but to have the foundation that into which all of other Mathematics could be interpreted as strong.

01:10:34: important because you know You want to prove?

01:10:35: The fundamental theorem of algebra But your using methods in topology and so on yeah borrowing theorems from another subject And applying it in this subject and that's incoherent unless you have a Foundation in which you can view both subjects is taking place, and set theory was able to serve in that role.

01:10:54: And I think it's very important to distinguish these two roles because like the concerns about junk theorems are really only—they're concerned with these other mathematical ideas and transplanted recursive constructions.

01:11:22: My point was about the third aspect, which is quite natural from computer science where you have programming languages that support abstraction like high-level languages or low level languages.

01:11:39: They're not modular.

01:11:43: In my view, set theory is not very modular in the sense that it doesn't support certain kinds of abstractions which I find are useful in mathematics

01:11:52: because you wouldn't want to look at some theorem in field theory translated into the language and also no one ever does that.

01:12:03: And so it is this very low level thing, but the advantage of The fact That set theory Is This Very Low Level Kind Of Structural idea you know there's only Though There'S Only One Type Everything As A Set and There's Only One Binary Relation You Know Membership Relation and everything Is Built on that.

01:12:23: what It Enabled However was a spectacular metamathematical analysis and the independence results.

01:12:32: And it's difficult to imagine such a successful implementation of those foundational ideas about independence occurring with some other much more elaborate foundational methods, so I think that is part of explanation for success in terms you know, the independence phenomenon and those matters.

01:13:01: And okay one can say well look we have hiding-valued, Boolean valued models in these other contexts but there... One could also view a lot of that work as derivative to what had already taken place so we wouldn't have discovered it directly I think without.

01:13:21: I mean,

01:13:22: first of all it would not diminish the historical role of set theory as you also say bringing forward foundations which i think is important and what we do.

01:13:32: We reduce to one set or foundation only turns out to be a sets theory yeah?

01:13:40: I mean that's theory with this predicate logic As you see its very syntactically convenient Very small But it's maybe not conceptually convenient.

01:13:52: The way things are constructed a bit strange in the way, and if you... I'm going

01:13:57: to push back on that because part of this successive set theory is You know, what is a partial order?

01:14:07: Well it's the set of objects with certain binary relation and those are very easy to implement in set theory.

01:14:14: And they're really easily implemented in my favorite

01:14:18: series as well... No question!

01:14:20: However.... To

01:14:20: say that makes this

01:14:21: complicated I don't think its accurate.

01:14:23: Okay

01:14:24: yeah i mean okay but what i refer you into?

01:14:27: if In sets theory would talk about x y natural number X plus Y equals Y plus X then i really quantify implicitly over all sets, which turn out to be element of the set of natural numbers.

01:14:41: And I find that those sets theory in my view at the beginning is about collections.

01:14:47: so if you just talk about the water collection how can we form collections and separate this from like a set?

01:14:55: it's same as propositions the contour description.

01:15:00: You end up with a theory which is much better behaved for mathematical abstraction, right?

01:15:05: Because you cannot talk about encodings.

01:15:07: Yeah!

01:15:07: You don't really want to...to talk about the elements of set-of-natural numbers in any way.

01:15:14: but uh..in...in....in the...in the type theoretic foundations, elements are part of the syntactic structure of your mathematical argument and hence into their structure.

01:15:27: We can only talk about them in a structurally invariant way, which I think is preferable if you actually want to do mathematics and that's what we actually do when we formalize mathematics then being not modular or able to be independent on encoding makes your abstraction process much harder.

01:15:53: So this is a different aspect of the foundation, right?

01:15:57: It's not about as you say these transfinite structures or other aspects but it's a third aspect which is how modular and how well abstraction supported.

01:16:13: I guess i would respond to that by saying maybe two perspectives on what sets are.

01:16:22: The kind of the picture-of-set theory that comes from say, from the category set is that points are sort of homogeneous.

01:16:31: And a said it's just collection at these point and we can move them around and expect universe to be inherently homogenous in have lots of automorphisms.

01:16:40: for that reason whereas the picture sets emerges form the cumulative conception of sets isn't like that all.

01:16:48: its completely rigid because it's part of the idea of sets that they're appearing in this hereditary accumulation process, and the role that a given set is playing is not just about its elements but also its heredity element structure.

01:17:06: That's inherently part hierarchy.

01:17:12: And you might say, well I don't want to interpret mathematics in that picture because it doesn't have the right kind of homogeneity properties that i want...I don't wanna ever look deeper into the structure or the internal structure of the elements whereas in the cumulative hierarchy picture every set has this inner Sure, there's these other foundations.

01:17:39: Now the question is do we really want a foundational system in which objects out of which other structures are built or homogeneous?

01:17:49: Or not?

01:17:50: and are their advantages to having that kind of homogeneity right?

01:17:55: actually I mean i would give it different description when you write mathematical statements so as some aspect in natural numbers.

01:18:07: Now I can apply the operation plus to it, right?

01:18:11: But if i had to x plus y and y is a Boolean then this is nonsensical statement here.

01:18:19: And so you would say like a nonsensible statement as a statement which syntactically doesn't make sense...I mean that has no meaning.

01:18:27: but I'd go further with saying a statement Which does not treat these collections or types in a coherent way is meaningless, so you build in the structure of typing.

01:18:44: In your theory and one benefit that since we cannot talk about elements because element relation is non-judgment it's something which is part of your syntax.

01:19:00: It's not a part.

01:19:01: you can reason or say if x is an element then whatever.

01:19:06: that's not something which you can express, but actually it turns out.

01:19:09: You do need to express your kind of mathematics very well without this feature yeah?

01:19:16: But it supports abstraction in a better way and so that is the bit of an orthogonal consideration.

01:19:24: I would say

01:19:25: No!

01:19:26: Of course thats totally right.

01:19:28: criticizing type theory or the other sort of alternative foundations.

01:19:33: They're quite robust for what they are attempting to do.

01:19:37: sometimes, For example people talk about this issue and use the phrase junk theorem And I think it's adjacent to concepts that you were talking about.

01:19:45: where The problem with interpreting say numbers as von Neumann ordinals.

01:19:50: Yes

01:19:50: two is subset of C

01:19:53: Is two a subset of three an element Or one equal to power set zero.

01:20:00: Okay, my view on this junk theorem is that every foundation is gonna have a chunk of its certain kind.

01:20:07: Even type theory has junk.

01:20:09: for example.

01:20:10: you know if I had type-theory okay i'm not expert in type theory but uh... But when your defining certain types maybe you define types where say ordered triples In terms of ordered pairs You know there's going to be nature in that definition, there's a couple of different ways you could do it.

01:20:27: You know?

01:20:28: You can say an ordered triple is a pair consisting of a pair and another individual or something...

01:20:39: These two times are equal.

01:20:41: Okay so when you write down the definition then you have to ...you could write on alternative definitions but this This is kind of junk and it's just also coding in exactly the same way that sets are doing coding, I think.

01:20:57: It's coding in-the type definitions.

01:21:00: And so the question is well where we're going to put the coding?

01:21:03: this coding Is inherent in Mathematical activity.

01:21:07: i have a concept maybe its expressed In type theory.

01:21:10: i define other concepts relative To it by defining new types and so on and Maybe you say Well no matter how You do what i'm gonna prove That they're homotopic.

01:21:20: Nevertheless, the definition was in a particular detailed way and I need to prove that agrees with other ways of doing it.

01:21:27: That's the coding...

01:21:31: You arrive to some degree intentionally.

01:21:35: these things are different like for example these different encodings or triples are intentionally different And if you proof somethings then take care of this intentional structure.

01:21:45: But mathematically, they're not different.

01:21:48: This is actually a consequence of this univalence principle.

01:21:52: Mathematically there are actually equal and this because I can never talk about the encoding.

01:21:59: so that's power of what's called homotopythal theory.

01:22:05: maybe you have heard.

01:22:07: Maybe that's something for the next episode.

01:22:10: I would love to continue this, and they have like twelve other questions.

01:22:14: you are collaborating with so many people there.

01:22:16: You're doing lovely stuff.

01:22:19: There are these Keppke Touring Machines.

01:22:21: They are your touring machines, Transfinite Computation.

01:22:25: So many more things to ask but we are out of time unfortunately.

01:22:28: Let me say two last thing.

01:22:31: We were a little unfair because we jumped so many topics jump into so many different research programs and maybe we were unfair to our audience because you're also great in giving the introduction to logic, foundation or philosophy of math.

01:22:46: I mean there are at least two proofs that will be linked in the comments section on this description And one is your... Maybe if you can help me if i butcher the title Your Introduction Into The Philosophy Of Math That You Wrote

01:23:00: During Oxford.

01:23:01: Yeah,

01:23:03: and this is really a great book.

01:23:04: It's also for the pure philosopher accessible.

01:23:08: And then there is another book in.

01:23:11: Am I correct that?

01:23:12: This was born out of a series of posts that you them re-merge to one book on infinities, or am I wrong with this?

01:23:20: So the

01:23:21: book is called The Book of Infinity.

01:23:22: And and i had written this book in preparation for...I mean to give my infinity class here at Notre Dame..and i serialized it on my sub-stacks so that chapters as i wrote them were appearing.

01:23:35: um uh....so i was conceiving it as a book from the start and releasing the chapters one at a time .And now i have several other books that are being released.

01:23:48: Okay, that's a great resource.

01:23:49: You should visit That one and we will also link to your blog And hopefully have you here again.

01:23:57: Thank you so much.

01:23:57: It was such pleasure talking with you.

01:23:59: obviously We had more to discuss and argue about.

01:24:05: Thankyou

01:24:05: very much for the pleasure of talking.

01:24:10: So let me say it To audience don't forget to comment.

01:24:13: subscribe.

01:24:14: We'll answer in comments at the next episode.