aboutlogic #11 | Season 1 Recap: Feedback, Highlights & Season 2 Preview

00:00:00: We are super happy for all the support we got and it's really unbelievable to have a nearly hour-long podcast on formal sciences with two unexperienced hosts, so if we extrapolate from that.

00:00:14: And in the first three months ,we grew by effect of infinity.

00:00:18: because Hello everybody and welcome to this slightly non-standard episode of About Logic because season one is over.

00:00:40: We had ten guest, ten conversation interviews whatever you want to call.

00:00:45: it was a great time And we are really happy how this was perceived.

00:00:51: How many of you joined?

00:00:52: Listened the positive comments The support from the community...we have people sharing their results on X us.

00:01:03: maybe start with something.

00:01:04: There will be another season, there will be Season Two starting in two weeks.

00:01:10: but for today we wanted to recap shortly what happened in Season One and uh...to do so let me list a few facts.

00:01:22: first the first season was supported by the Akademie der Wissenschaften in Hamburg The Academy of Sciences & Humanities in Hamburg.

00:01:29: We are super grateful.

00:01:33: As I mentioned, given the positive feedback we want to continue with season two.

00:01:37: Then without that support.

00:01:39: so for that reason We will add a small donation linked by me a coffee to cover costs below.

00:01:47: So if you have some money to spend Feel free to do that but don't feel obliged.

00:01:52: this will Continue in any case for awhile.

00:01:59: Then I should mention we have over one thousand subscribers and we are super grateful for that And everybody who hasn't subscribed yet, but listens.

00:02:07: Should feel bad because it's the subscribers Who keeps us motivated?

00:02:11: Don't?

00:02:12: you don't do not need to feel you

00:02:14: can also subscribe and don't listen.

00:02:16: That's fine.

00:02:17: Yeah

00:02:18: You can also just play the video in the background and go to sleep.

00:02:22: We're fine with all of this.

00:02:25: It is actually good to go asleep.

00:02:29: statistics that listen to about logic videos is very good if you have sleeping issues.

00:02:35: Yeah,

00:02:36: actually I'm one of these people...I mean not with About Logic because my own voice is horrible for me but i am always listening to podcasts and sometimes my wife hates before that!

00:02:46: And too loud but normally within years

00:02:51: it works.

00:02:53: yeah we had over two thousand hours watch time.

00:02:56: That's insane for us literally days and days of people watching the interviews, all in all for us it looks like a great success.

00:03:08: And before talking about season two we wanted to clarify few questions that were raised on comments so let me forward them to Thorsten because most are more on constructive side.

00:03:21: I would say If you ask Hilbert, that's the same.

00:03:32: That is actually one comment we oversimplified with Hilbert Brouwer problematics but maybe for another episode.

00:03:44: So let me first say Torsten do want to say anything I haven't mentioned so far.

00:03:49: among

00:03:51: Yeah, I mean...I think it's really cool to see this sort of audience engagement that the people are interested in commenting asking questions.

00:04:01: We try to respond them but sometimes we may miss something because maybe you're just distracted.

00:04:08: But generally they had some good and interesting discussions.

00:04:14: It is good are not just watching it, but actually engaged.

00:04:20: So I find this is really good and actually...I mean i'm enjoying doing this getting some sort of feedback especially positive feedback also critical comments remarks or suggestions like we should interview.

00:04:40: For example, somebody said we should interview Joel Humkins and he is coming up.

00:04:48: And other people like Oshe Reiber I think also was mentioned that we interviewed him.

00:04:55: so let's talk to him.

00:04:57: So thats very good.

00:05:00: There was a bit of controversial discussion That people say okay i'm pushing too much for sort of like this constructive angle.

00:05:11: And I think that's true, in some cases i was really going for it and maybe didn't give all guests enough time to expand their ideas.

00:05:26: but at the end having a bit of controversy is actually making the podcast more lively.

00:05:38: I don't think i'm going to give up on asking people about intuitionism.

00:05:44: But, obviously it's not the only issue we are interested in.

00:05:57: That is probably a good statement!

00:05:59: So you already replied one of your comments that But there were a few more formal questions.

00:06:08: So let me ask you about that.

00:06:10: in the, uh... In Andre's episode we talked about realizability models without ever mentioning what they are and so maybe could you say if your words about that?

00:06:24: Yes!

00:06:25: Realizability relates.

00:06:28: I mean You said A certain proposition is realized by a code, which it's program or code of the Turing machine.

00:06:40: And I mean this based on this BHK interpretation of logic that every logical statement can be realized and this very important in instructing programs from proofs, which is used by people like Heimutsch-Wichtenberg and Ulrich Berger on realizability.

00:07:06: Now it's subtly different to type theory.

00:07:11: so type theory is very typed as the name suggests whereas realizabilty uses usually untyped realizers sort of programs, Turing machines and so on.

00:07:27: So yeah it's related.

00:07:32: And there are also realizability models of type theories but There is a slight tension between them.

00:07:42: I would just have said existence on steroids.

00:07:45: We really mean existence whenever we say that But i think your version was more refined than the slope.

00:07:55: There are actually two ways to interpret existence in realizability.

00:07:58: You can say, there is a witness and I don't care about it.

00:08:04: as far as the realizer has concerned... ...and that's really part of the realiser!

00:08:12: And you can play with this difference

00:08:22: here.

00:08:25: in there, right?

00:08:26: Who could you say a few more...

00:08:28: Brauerheit and Kolmogorofia.

00:08:30: Yeah I think it goes the same direction It's an idea.

00:08:40: The question is maybe what's the difference between BHK and Curry Howard?

00:08:44: because they go on the Yes, I think in some ways they're close enough that you really have to go into a lot of historic details.

00:09:08: To tell them apart... In the way all these things BHK, realizability, Martin Roof are part of an evolution of ideas which influence each other.

00:09:22: and there is come in storyline here.

00:09:28: and the story line is somehow to understand logic via programs or realizers, have a constructive interpretation of logic.

00:09:42: And I think that has evolved... In my view.

00:09:45: personally i prefer type theoretic perspective where The fact that you have a realiser is not the first point.

00:09:57: You just explain things, and the fact they can be realised by a drawing machine... ...is just sort of secondary observation.

00:10:06: I mean it's everything you do in theory as constructive And its not surprising to realise your program.

00:10:17: Is it fair to say that like one half is coming from the proof theoretic side of things, so?

00:10:23: To speak and the other comes more from like lambda calculus computability theory or Would you say yeah image doesn't help for me.

00:10:34: That was always.

00:10:35: It's another comment on history.

00:10:38: I mean i wouldn't reduce this talk of the history and depending on your emphasis, right?

00:10:52: Yeah.

00:10:52: So I mean yeah.

00:10:54: that's another good comment on these concepts.

00:11:04: Maybe for now we can keep it at that.

00:11:06: And let me allow this side remark That our podcast is a weird spot because We are doing as advanced things As we talk about so to speak.

00:11:17: So it's inaccessible sometimes even for me.

00:11:20: Sometimes when you talk with Andre, I have my problems quite frankly just to follow.

00:11:29: and on the other

00:11:31: side... Some of the philosophical subtleties that i missed from the other hand because Im a DIY philosopher so im lagging lots.

00:11:46: Wittobstah and history, quotes.

00:11:51: I'm relying on Dennis to have out there.

00:11:57: With

00:11:58: Wittgenstein early in the late Wittkenstein how they are fighting each other

00:12:06: already.

00:12:07: a spoiler for season two.

00:12:10: yeah great So yeah, then the other side.

00:12:14: we want to be accessible.

00:12:15: We want to give definitions, Thorsten you are doing great job sometimes in stopping and asking for notions that I used but we will mess it up necessarily because It's impossible to do both always.

00:12:30: so please really keep Asking these questions.

00:12:34: that really helps us to see where we did things wrong with.

00:12:41: The logical order of concepts wasn't clear or something like that.

00:12:46: Yeah, I think it's quite important.

00:12:50: so what we try to achieve is people who are just interested on any level can take advantage off the conversation and yes both us should make sure you pull down our guests like ourselves, right?

00:13:13: And how's the audience.

00:13:14: But if there is something not clear then I think it's a very important and very useful If people use comments to ask additional questions and so on.

00:13:27: Actually I wonder here as an idea which I haven't discussed in advance whether we should maybe regularly do Q&A sessions with the audience or meet the audience and have a meeting where people can join.

00:13:43: And there we very continue some discussion, maybe some of the guests may be happy to join as well but that's not essential.

00:13:56: Yeah I would love it!

00:13:57: We should add an Outlook part into our overview episode today at the end what we can do.

00:14:07: I mean you also mentioned having maybe something lecture-like on type two and i think there are many other ideas, people could write down what they would wish for the future... Maybe within about logic may be adjacent?

00:14:24: We can figure out a lot of things.

00:14:27: Please use comments to suggest things!

00:14:30: Obviously.

00:14:36: But also what else we can do.

00:14:42: For example, I mean in the moment you are very philosophical and actually he also posts a podcast to audio only but this may be question about degree.

00:14:55: maybe whiteboards could be involved or not.

00:14:58: that people think of it as general questions would be good to hear or want to see.

00:15:11: Yeah, exactly there's also a community tab where you cannot make such comments independent of concrete episodes which is sometimes helpful because for all the episodes we don't always see all new comments.

00:15:24: so if we missed something it was our error.

00:15:28: error.

00:15:29: so that can happen.

00:15:30: but let me ask you another technical term mentioned in the episode of Steve Awoddy, somebody asked about relative identity.

00:15:43: I have to look it up!

00:15:45: I think relative identity and philosophy is that identity depends on the context.

00:15:51: so depending upon the context certain things are identical or maybe not identical.

00:15:57: Maybe what you know about it, I'm not an expert on this.

00:16:01: But somebody thought maybe related to HOT which also has a different view of identity where the identity is structure and in that moment there's a different perspective or identity.

00:16:22: But if somebody has a concrete suggestion about relative identity, who we should talk about and please put it on.

00:16:31: I mean i'm wondering whether it's closer to isomorphism because things are isomorph in the given context right?

00:16:39: You could do

00:16:40: things like look

00:16:43: but i mean delicate issue between

00:16:46: me.

00:16:47: It's

00:16:48: okay, maybe he has a point.

00:16:50: I'm just thinking about it because in set theory two sets are equal if they have the same elements and this is not an ocean which is state... This is the principle of... I mean this follows the axiom of externality but that follows from the idea what the set is where the set basically given by predicate And hence you can distinguish isomorphic sets.

00:17:17: So the type theory is a different language and you cannot talk about elements in isolation.

00:17:22: That's the point I always made, right?

00:17:26: In types theory... Elements that you talked to are always typed.

00:17:34: so we can't ask questions like if they're empty set an element of this type because it doesn't really make sense.

00:17:45: the identity in H.O.T is different or in type steel, in general since we cannot observe differences between isomorphic types.

00:17:58: hence univalence sort of completes a story by saying okay if you can not distinguish them then they are just equal because I mean what else?

00:18:08: This says...I would say it's maybe my misunderstanding hit me But I think it's life and its principle of indiscerne builds, right?

00:18:17: There are two things.

00:18:19: And they share all what you can say about something equal... ...and maybe this could be related to the idea relative identity.

00:18:27: that in set theory where as a context we have much more observations The identity of sets is just the equality which comes from set theory.

00:18:42: But in type theory where you have a very more disciplined and cannot express things, I mean theorems.

00:18:53: Propositions that we don't actually want to say in mathematics... And they are not expressible.

00:18:58: but hence as consequence then isomorphic sets become equal or isomorphive types becomes equal?

00:19:07: That's one of the main ideas of automotive type theory.

00:19:15: Yeah, that's... I mean there are a lot things to discuss right?

00:19:19: There is this Streicher paper where maybe you know the details better than i do but some category theory angle might make some differences visible To these notions.

00:19:35: But let's postpone it for another extra episode to talk more about Rott.

00:19:44: Unfortunately, we cannot invite Streicher anymore but there are

00:19:48: a few people who

00:19:49: will miss Etliens.

00:19:53: Unkif!

00:19:55: Let me pass over another question that was the one of relative consistency.

00:20:00: is this also relative identity?

00:20:03: Is it the same relative or what's to make?

00:20:07: I'm not sure.

00:20:08: I thought it just means you have a logical theory and another one is consistent relative to this one, right?

00:20:16: That was my understanding.

00:20:17: but maybe there's something more subtle going on.

00:20:20: No no

00:20:21: that's-that's it.

00:20:22: But i mean due to Goethe second theorem we all can get most of the time You know because absolute consistency proof doesn't work.

00:20:33: It's actually, I mean...I think that now looking back at Goetels.

00:20:40: The main theorem of Goetel is really the second one.

00:20:44: First one is a technical pre-play to the second run right?

00:20:52: You basically you explore it as first in this second run.

00:20:59: To be clear what it is!

00:21:00: The first incompleteness theory says that any theory extending a very, very weak version of arithmetic which doesn't even include induction is if it's consistent then it has sentences which can either be proven or disproven.

00:21:20: So completeness here is the question... It's a very classical idea that you can either prove or just prove any proposition right?

00:21:29: This interesting because That is something which, it's just true in classical propositional logic.

00:21:36: But this not actually truly an intuitionistic propositional logics.

00:21:40: so its rather unsurprising that there are statements which can be now proven or disproven as a sort of classical illusion may maybe possible but the second theorem slightly stronger version of arithmetic, now including an induction.

00:22:03: Because you basically use the proofs for first one in second one and if internalize it by internalizing... You can say that any consistent theory cannot prove its own consistency.

00:22:19: And thats a very natural statement.

00:22:22: I mean what do u expect?

00:22:25: I mean, what's the logical system?

00:22:27: The logical system is a reflection of our reasoning.

00:22:31: Of our intuitive ability to reason and attempt to make it precise.

00:22:39: but then... Then its quite obvious that you believe that this system is consistent.

00:22:47: But thats not something we can prove in the system.

00:22:52: That seems to me, even this out-understanding girl's proof just from a very intuitive point of view.

00:22:59: that is completely natural.

00:23:01: It would be completely weird and unimaginable.

00:23:06: if you have a theory which can prove its own consistency

00:23:10: I mean... You could argue it was easy say on the inside right?

00:23:15: But when i get your intuition like pulling yourself

00:23:23: Pulling on your hair.

00:23:27: But I mean, there's a lot of nuance here.

00:23:32: even that provable and true are different things.

00:23:36: it is not trivial so to speak.

00:23:39: Now we know what

00:23:41: truth... I'm not even sure... We had some discussion about whether

00:23:46: the truth

00:23:47: is such good notion.

00:23:50: My view on mathematics or mathematical logic in particular is that, I mean it's a storytelling of mathematics.

00:24:03: And hence its not about tools but evidence.

00:24:07: so okay thats my perspective and we had discussion again.

00:24:13: you can think like an ideal epistemic space, you can find evidence for everything that is there.

00:24:22: You could have this idea...

00:24:28: I mean as a case of the unknown they are complete theories.

00:24:33: The

00:24:35: oldest formal theory Euclid's geometry is complete.

00:24:42: so if we formulate in practical logic and every statement about in geometry is either provable or can be disproven, right?

00:24:52: So yeah you kind of have completeness.

00:24:55: Yeah and they are also in some sense complex ones because it's branching out.

00:25:01: It's not like baby arithmetic lies at the very bottom Of course piano arithmetic on top but there things next to it.

00:25:15: Lovely example.

00:25:16: Yeah, I mean the point is this is a second Incompleteness theorem.

00:25:22: The second one it's like okay It's about.

00:25:25: it's all about logic where we already assume that you can talk about itself.

00:25:29: right so and yes.

00:25:35: So something which emerges.

00:25:37: you invent logical theories And then in certain theories or uncertain I mean, what has to make clear logic is nothing so holy or fallen from the heaven.

00:25:50: It's a part of human activity that makes our reasoning more precise and it's an invention for humans not given by any superior Being.

00:26:01: I just invented by people.

00:26:04: and then we investigate our invention.

00:26:07: Right?

00:26:08: We look at this is meteor logic, we don't look at the logic.

00:26:11: We investigate all an invention And to think that our invention Is sort of so good That it can vouch for itself Seems to be absurd idea in my view.

00:26:25: At

00:26:28: this point, we should also say thank you to our post-production team who's investing a lot of time making these and I will ask him to cut out the blasphemy in post production.

00:26:44: No no just joking!

00:26:49: But let me stick shortly longer.

00:26:52: relative consistency.

00:26:55: And in set theory, this is really an industry to talk about these relative consistency results.

00:27:02: Because like there's whole large cardinal things and we will talk about this with Hamkins as basically that because if you build up your universe of sets then the power-set iteration gets too larger.

00:27:14: so maybe let us skip detail for now?

00:27:20: If you want to closure Kappa, that's already a model of everything below it.

00:27:28: You get your problem because ZFC cannot prove the existence of such an inaccessible cardinal and otherwise It would prove its own consistency right so?

00:27:39: And Everything on top off that will then be even more unprovable if you want to call it like that.

00:27:47: and Weirdly these things aren't only up in the sky they have like real world consequences and if you take like games on from end to end as real things so there's some interaction they are.

00:28:03: these are the determinacy axioms.

00:28:05: And we will talk with Hamkins about that because there is this lovely result of him, maybe not all natural large cardinal axiom are indeed linearly ordered which A lot of set theorists I guess share.

00:28:26: By the way, just to make a type theory comment about that?

00:28:31: Sure!

00:28:32: We also have... The counterpart for large cardinals in type theories are what's called universes and there is lots of... It would be nice actually maybe to relate some sets theoretic ideas on these large cardinal and probability of mathematical concepts to the type theoretic assumption of assuming that certain universe exists.

00:28:58: I know there's a branch where some large cardinal notions were related to category TREs, so these around for PENCAS principle and i will look it up and edit for the chat because its a colleague who extended something.

00:29:21: No, better.

00:29:22: But maybe I missed that colloquial meeting but i will link something you know.

00:29:29: um great is there any other notion?

00:29:32: That you think we mentioned quite often and regret that We never defined it or do You think we should go to our look back at the episode so far.

00:29:41: okay yeah let's Let's do this.

00:29:43: i can't think of anything just now.

00:29:47: Yeah, anything.

00:29:48: I mean we shouldn't say what's.

00:29:49: our favorite episode is because all of our guests are great and we love them All equally.

00:29:55: but maybe anyways Are there some highlights?

00:29:57: Some things that made you think um longer about the topic That you want to single out or Maybe some groupings where some episodes fit together in your eyes?

00:30:12: yeah so okay We started with Kevin Buzzard, which I thought was a good start in particular because Lean is becoming more and more used.

00:30:27: Then we had this meeting with Graham Priest who actually wanted to challenge him but I completely failed.

00:30:38: mostly He was very good at not engaging in my attempt to have an argument with him.

00:30:50: I mean, i had some doubts about the source of philosophical logic sort-of thing here and I hated it that he subsumed internationalistic logic under philosophical logic.

00:31:03: but okay let's not go back from my point Didn't go so well, but what was the next one?

00:31:13: Then we had Steve Awadi.

00:31:16: Yeah okay that's easy for me.

00:31:18: I mean...I thought Steve expressed some ideas very clearly better than i can do it and But I was really pleased to him.. I think he was very Confluent with my own views And obviously We need to be careful.

00:31:38: I mean, sometimes we want people to agree with us but it's also good for people whether there is some tension and Joel was certainly having published more... And he was very happy to engage into arguments.

00:31:55: Okay so up next is Colin?

00:31:58: Yes that was a bit of sociology or mathematics.

00:32:03: if i remember correctly

00:32:08: The good old fashioned philosopher of math would say so, but the modern Philosopher's mathematical practice will probably say these things aren't too easy to distinguish.

00:32:19: But I mean that was probably one Of the main takeaways off the episode right?

00:32:22: That Well when talking about philosophy Colin would Talk a lot of thing others call sociology

00:32:36: And maybe I went too far.

00:32:37: I think there was this criticism in the fact that intuitionism is really sort of ignored in mathematics, but I don't think it's something Colin had thought about or... There were a bit of mismatch when I tried to push him into his direction and maybe

00:33:00: he went way too far.

00:33:06: a lot of philosophers have mathematical practice, they would say like even if mathematicians do something totally stupid who am I to say that?

00:33:16: They know better.

00:33:18: I will keep silence about their practice and i'll just think what are actually doing point two things...

00:33:27: This sort of upsets me as you may know because If you want to study the philosophy of mathematics, so last people.

00:33:39: You should ask them mathematicians Yeah

00:33:42: But it's not about taking their statement at face value right?

00:33:46: It's like in history if you asked The living witnesses you get an historical account

00:33:53: but that's not always okay.

00:33:54: So what I think is Well would appeal to some mathematicians as to be reflective About your own practice and And my.

00:34:06: There are some who do this, but most mathematicians are completely blasé about it.

00:34:14: And also if you say something about philosophy they run away right?

00:34:18: So I mean that's just a something which i find quite... It is also again not all of them But there many of those which aren't really interested in communicating outside.

00:34:34: they are sort of neo-domain, and this I find disappointing.

00:34:42: It's disappointing because I think mathematics is absolutely interesting and fascinating!

00:34:47: And it should be presented in a way which is accessible to people who were interested but maybe not yet know everything... perspective I think.

00:35:06: Yeah, there are some horses there but in general i agree it's a discipline with over five thousand sub-disciplines right that we had the situation to be

00:35:21: able... Obviously you have something which is not just in mathematics.

00:35:28: and And again, obviously they are very great counter examples.

00:35:41: I mean

00:35:43: and there even counterexamples who claim to be not-counterexamples.

00:35:50: but let's not spell that out and reopen an old discussion.

00:35:56: Great!

00:35:57: Then Alexander talked about tier improving and legal aspects And we have got a critical comment there that this was more like across examination.

00:36:10: Yes, so I guess it's going back to my view on philosophical logic or let say epistemic logic.

00:36:19: So an epistemiic logic... Or maybe philosophical logic is attempt actually model how people reason in reality Whereas, I mean what i would call mathematical logic is an idealization.

00:36:36: It's like in a way how people should reason... ...in the precise way right?

00:36:44: And and I'm personally interested in this mathematical logic which via its idealized it not platonic but just particular ways of reasoning which tries to avoid sort of these everyday confusions and so on, because that's particularly important in mathematics.

00:37:07: But okay... And Alexander was trying to have a logic or he is one of the people doing logics to formalize this epistemic, how people actually reason.

00:37:34: This was also a very important aspect of the good old AI in the eighties.

00:37:42: they tried to make precise what is sort of reasoning by default and so on.

00:37:48: going into these lines and claim are using which I would call epistemic logic.

00:37:57: You

00:37:57: mean Alexander, right?

00:37:58: Alexander!

00:37:59: Sorry, I confused you with Alexander.

00:38:01: No worries.

00:38:07: And then...I come from the old AI.

00:38:08: it was basically a failure.

00:38:12: maybe its good to analyze why it is a failure because i think this idea that could completely model these sort of way people reason is a fallacy.

00:38:29: It creates systems which are really complicated, hard to understand and they're certainly not trustworthy.

00:38:37: because there's this illusion of precision.

00:38:42: because you do something in the formal system.

00:38:44: but the question is what does it actually mean?

00:38:46: What did he do with his formal

00:38:47: system?".

00:38:49: To me I'm on lesson from modern AI and these large language models,

00:38:56: etc.,

00:38:57: is that they actually take it on.

00:39:00: I mean don't try to perfectly model it but do the sort of statistic analysis... Do something which is actually inspired by how humans actually reason?

00:39:14: There's very context-dependent.

00:39:17: It's not pure or perfect in a way.

00:39:22: The best approximations are these sort of statistical methods, and I find it a bit surprising that something like Alexander isn't taking this on because... This is happening now.

00:39:38: That lots of lawyers get fired because they're replaced by an AI which obviously has got some problems but then Going there and doing sort of the old AI for legal text, I find is... That was my criticism.

00:40:00: This was a bit out-of-date basically.

00:40:05: Yeah let me just make this small remark.

00:40:08: I mean in neither case sure whether it's really about modeling our human brain with our fallacies or whatever.

00:40:15: I think they're like very contextual like for Alexander, they are parts of the law that a very rule-based and very formal.

00:40:26: And which is also so complex.

00:40:28: you cannot overlook them anymore.

00:40:31: So I think this example was mergerset acquisitions in U-Law or something Like That.

00:40:39: There it's quite plausible.

00:40:41: there are strict rules You can apply but its hard to check these formalities.

00:40:48: So in some sense, I think there might be a slightly different program.

00:40:53: And of course then the truth is always in the middle mixtures of architectures... ...of humans and computers.

00:41:02: but law as i think always dialectic it's always part of conversation.. ..and to really understand Law you have know where comes from what's purpose.

00:41:17: So to try, to separate out some sort of formal rules I think is not really very helpful.

00:41:28: But that was my criticism.

00:41:29: but...

00:41:32: We will not find consensus here especially since Alexander isn't there?

00:41:38: Yeah it's not fair!

00:41:43: Let us move on to episode eight with Debora.

00:41:47: Yeah, yeah that was interesting.

00:41:51: I mean so i asked the question whether she is a Platonist and she said no but haven't yet understood then exactly where she positions herself.

00:42:03: maybe you can comment on this.

00:42:05: Oh!

00:42:05: I

00:42:06: think she would say it doesn't matter in her view because she's describing satiratic practice And She could do that as a platonist or whatever.

00:42:17: But her study is about the practice of satirists.

00:42:21: And I mean, she knows a lot of satiree but... ...I don't think she sees herself as a satirist.

00:42:26: who's part of that community so to speak?

00:42:31: So in this sense it's again similar to Colin.

00:42:35: But you studied lots of sad theories or...

00:42:39: Yeah!

00:42:40: You can always have your

00:42:42: own more lessons.

00:42:42: She was forced into this.

00:42:46: I mean, i don't think you can study something without having some philosophy about it or have an idea.

00:42:53: And that was my question!

00:42:55: That's another super interesting question a meteorological one.

00:42:59: for this philosophy of mathematical practice which i'm doing because there are some people who say and i am one of them You should do a lot of math ,you should incorporate yourself in their practice and then speak about it, because you really get the details.

00:43:18: And on the other side people would say oh no-no!

00:43:21: Then you are biased... ...then your opinions should be like observing.

00:43:27: let me make this very extreme.

00:43:29: You shouldn't go to laboratories and observe the wild tribe of mathematicians.

00:43:37: No doubt they meet at that time eat cake And from this groundwork, that's as objective as you can get.

00:43:45: This is of course also not to how anthropological work looks nowadays right?

00:43:50: I'm oversimplifying but for that... You could do more things and there are great examples for that as well For people observing an outsider and making the astonishingly impactful observations.

00:44:10: So Bettina Heinz, it's maybe one book I mentioned because only in German the In-Welt and Mathematik did such a study at Max Planck Institute in Bonn.

00:44:22: It was so interesting!

00:44:27: Yeah i guess okay that is an interesting perspective obviously completely valid but pushing forward the dialogue and reflection about mathematics, different approaches to mathematics.

00:44:48: Obviously I'm not perfectly neutral in this but maybe there's a difference between us.

00:45:00: It is very important also for me to ask these sort of innocent questions.

00:45:07: Yeah, there's this guy in BBC who is always interviewing some very sort of extremist Louis Robux.

00:45:15: I don't know whether you know him.

00:45:16: he's interviewing so many extreme people i mean Nazis and settlers in Israel or whatever but his very sort... He's not challenging them challenging their views, but he gets out that they say what they think which is usually enough to see how absurd it is.

00:45:43: He has this ability just sort of get them to tell him about the very racist and whatever views by listening.

00:45:53: so his doing exactly want to do or are doing with respect to mathematicians?

00:46:01: Yeah,

00:46:03: probably.

00:46:04: So it's interesting.

00:46:05: I will have a look.

00:46:06: and but uh...I mean i'm not in the UK!

00:46:09: I should know maybe what I don't.

00:46:10: sorry No

00:46:11: no no But he is very remarkable.

00:46:18: Okay great um then there is episode nine And now you need to help me A second.

00:46:23: who was that?

00:46:24: Sorry It's quite recent

00:46:27: Was it not André Bauer?

00:46:32: Oh right, you're right there.

00:46:33: We had a change in schedule.

00:46:35: He was originally for season two and then we moved him earlier.

00:46:41: So yeah It was lovely episode.

00:46:45: Do you want to say something or...?

00:46:47: Yeah I mean André is the great guest The great sort of communicator.

00:46:56: I just, it's another of these which i really enjoyed and you could say okay because we are quite close but then we have got some subtle differences.

00:47:05: Which is hopefully interesting as well.

00:47:11: But yeah...I mean he has a very good communicator.

00:47:15: He gives late lectures And also good in the podcast.

00:47:20: Yeah

00:47:21: i've enjoyed that talk alot.

00:47:24: I think we need an episode more on Topos theory because it's coming up always, but not fully illuminated yet in this podcast.

00:47:36: Maybe people disagree and already know enough about that?

00:47:41: That was just a tangent!

00:47:42: Let me take over for Episode X our final episode because there we experimented a little bit with the format.

00:47:50: We had one moderator this time,

00:47:53: usually you have two... I thought i was barred from it for bad behavior in the first attempt to

00:47:59: uh but don't say so and i mean we will also even have an episode where Actually, that's something I would like to ask the audience whether it will be better sometimes for single episodes.

00:48:20: To have more things.

00:48:21: but i'm also a fan of this because its fun for me having it like that.

00:48:29: But in general we'll keep it to moderators there.

00:48:32: This is not full democratic issue here.

00:48:36: maybe We can add few more non-standard episode between.

00:48:42: If this thing really keeps growing like that, then we should probably definitely invest even more time into it.

00:48:50: So

00:48:50: please spread the word and subscribe.

00:48:56: give us some little money via this link, this coffee link.

00:49:02: We have to buy some coffee obviously otherwise can't survive.

00:49:05: And

00:49:08: if Niklas is giving more or less symbolic price for the work.

00:49:17: And there's software and some stuff, so it is not about thousands of euros.

00:49:22: but so far... It has a little minus to us as you can only run so long on deficit that again season two will be there!

00:49:37: Yeah, and that was also a very philosophical one.

00:49:40: I would say we We talked a little bit about notions or like epistemic injustice again A lot of relation to Colin who was also mentioned a few times there.

00:49:52: so let's i guess the rough overview About season one.

00:49:57: And um?

00:50:00: I Guess II did I will jump back.

00:50:03: it said only historical footnote but we talked about the girdle sentences.

00:50:08: Did you know that Gürtel and von Neumann talked about the second Gürl sentence?

00:50:14: Yes.

00:50:15: It's a lovely story, Raktu!

00:50:17: Do we want to tell it or should I...?

00:50:18: No no... I mean for Neumannen said to Gürttel yeah what about basically the Second Theorem where he realized that you can derive the unproved of consistency from the first one?

00:50:32: And Gürschen was like Yeah sure i have thought about this.

00:50:37: It wasn't worth publishing.

00:50:40: Nowadays, I would turn my whole career into that single observation if i could have made it back then.

00:50:47: The

00:50:47: question is whether Gürer was completely honest or maybe it was von Neumann who actually... You

00:50:57: never know but there are also these arguments and we will talk about this in one of the specials episodes of next season that we actually won't announce, Gürtel knew a lot things he didn't mention like something forcing with permutation models.

00:51:17: There's always rumour like this but I've never looked into it.

00:51:22: and now the notebooks translated by Merlin Karl because she used very weird shorthand And so it was very hard to access the notebooks on Google, but that's also for the future.

00:51:42: Shall we talk shortly about season two?

00:51:44: Yes you should try!

00:51:47: We have some recordings.

00:51:49: and then there are the two Bernhans.

00:51:58: Maybe you can summarize this a bit

00:52:02: better than me... get to computer linguists who worked on the language of mathematics.

00:52:08: So they come from The Naprosh Project that will proof checking and They looked at math as a text, you can look at many different texts And also work on some good old-fashioned frame semantics.

00:52:24: so two lovely guests Bernhard Fisseni and Bernhard Schröder.

00:52:28: There we had this tube format

00:52:32: as an

00:52:32: experiment,

00:52:33: yeah.

00:52:34: So then we had old Shriver.

00:52:37: so he is a very impressive guy.

00:52:40: I mean his coming from mathematical physics and He's doing some very abstract.

00:52:51: He uses the very abstract language Motivated actually by physics And he using homotopy type theory to talk about stuff like quantum field theory and stuff.

00:53:03: And this is quite interesting application of the language-of type theory to do some very sophisticated high level physics where you basically, if you try It's impossible.

00:53:29: So you need to sort of high-level language, and Ross is very good in his very clear explaining these things I think.

00:53:39: so maybe if you don't agree with it?

00:53:44: Yeah i think he's so high up that even if he's very clear...it's a very hard to follow for me

00:53:49: at times.

00:53:49: yeah really

00:53:52: cool stuff I mean, then we already spoil it a little bit about that.

00:54:02: Joel Hemkins agreed to talk with us which was very nice and there we might even have a part two because we haven't finished all the topics.

00:54:12: And i should mention We listened to your advice but back Then i think we weren't aware of The thing.

00:54:18: you are seeing That today Already that we Are fine With being A Little Longer in Season Two Because people wished for that, but we don't will pivot to hours and the hour of episodes.

00:54:29: I mean there are other podcasters doing that But it won't be as strict with our forty minutes Episodes in the future.

00:54:40: Yeah And then they're a few not fully confirmed episodes.

00:54:44: Let me mention long time collaborator Jose Antonio Perez Escobar's who will talk about Wittgenstein.

00:54:51: you also mentioned that And there we might even try to have a little presentation within the podcast as well, change of pace.

00:55:01: Just look how different things work out and then you will look forward to get your feedback.

00:55:08: Then two other highlights that I want to mention them

00:55:13: now?

00:55:14: We are going talk to Emily Riel who is... Quite interesting mathematician who's doing I mean, it's very well known for work on infinity categories Yeah and i think she is in my experience also very.

00:55:37: She's doing very abstract stuff but she can explain things very nicely so i enjoy this.

00:55:44: And the other person In a similar direction actually is Mike Schulmann from San Diego, who's one of the... I mean i'm working with him and he was one of some most clever people.

00:56:00: It it's very frustrating to work with somebody like this because you shouldn't let any problems lying around.

00:56:07: He will solve them in no time yeah but now he's great!

00:56:11: And also a very good presenter.

00:56:17: some project on higher observation of type theory, and he's actually as a mathematician very unusual.

00:56:25: He went down in and implemented this on the computer system.

00:56:29: so that makes it good.

00:56:31: off tension to the first presentation by Kevin Buzzard who is using his user of lean but Uses lean, okay has got some influence maybe known the design of lean and the muscle and so on.

00:56:48: And Mike really sits down implements a theory we have thought about in years thought about and implement new system which is quite unusual I would say for a mathematician.

00:57:09: The lines are blurry right?

00:57:11: I'm mislabeling you as a mathematician.

00:57:13: all Even if you say I'm a computer scientist, sorry for that.

00:57:19: For me it's simply fluent and we could call Steve a philosopher but i wouldn't hesitate to do that And he might say no-no at least now am a mathematician But for me its very fluid.

00:57:34: It is interacting even with linguistics or other fields With sociology.

00:57:40: from me This something nice about logic as field

00:57:47: Because I mean, uh...I hope i'm not giving anything away when they say that your family comes from Kurdistan and has this analogy.

00:57:58: That logic is a bit like Kurdistan you know?

00:58:02: There are some parts which in mathematics Some parts in linguistics, some parts in philosophy, some things like computer science And everywhere there are persecuted minorities.

00:58:18: Yeah, that's some truth to that.

00:58:21: unfortunately I guess... We shouldn't stay too long with metaphors but it is also something about drawing lines right?

00:58:29: If the more arbitrary you draw these lines, this disciplinary boundaries or lines on a map The more problems will cause and its very.

00:58:41: And let me stay now on the scientific side of the metaphor.

00:58:44: It's a very weird place to be as somebody being really interdisciplinary or transdisciplinary, because you always get your professorship for one chair and at other head.

00:58:55: we want this interdisciplinary stuff but I'm not sure whether there is already framework where it is solved?

00:59:03: No!

00:59:03: I mean funding agencies emphasize interdisciplinarity But if it actually comes down to the hard decisions where you give some money, then turns out that doesn't really play such a big role.

00:59:20: Yeah

00:59:22: indeed I mean as a philosopher panel maybe you would like philosophy project rather than sixty percent philosophy projects thirty percent mathematics ten percent computer science and same for other directions right?

00:59:39: I mean, that's another topic.

00:59:42: The big grants have caused a problem in the academic structure because we... We have a lot of youngsters highly qualified people and only so many permanent positions.

00:59:52: but i mean That maybe also for an other episode.

00:59:55: then it is not about logic But about university design and governance And things like that.

01:00:06: Yeah!

01:00:06: Then let us come to a slight outlook thing.

01:00:10: So you already mentioned this idea of having whiteboard sessions, interactive things.

01:00:19: I mean we said so for upcoming guests.

01:00:22: there is also a secret superstar which will see whether it works out?

01:00:36: What!

01:00:37: I want to create some excitement.

01:00:39: Let's see whether that works out, yeah?

01:00:41: Yeah it is a historic figure.

01:00:44: he told... He was fine with being talked like this.

01:00:49: Talked in his way and said you become an historic figure just by being around for too long.

01:00:56: Great!

01:00:58: With these hints i would guess somebody else which we should also invite but thats too cryptic.

01:01:05: before the audience There's somebody where you are close by at some times of the year.

01:01:15: Great, so let me just invite the audience to comment what you wish for.

01:01:20: in future there will always be a delay with implementation because we pre-recorded couple episodes and I'm sure it'll keep this too weak schedule.

01:01:32: whether you would go for a full lecture, whether this should be something for channel members if we have something like that at some point.

01:01:41: Also

01:01:41: exclusive content or...

01:01:43: Yes there's an interest in sort of tutorials and lectures on particular topics but it will also interesting to know where they'll be something which we shall add.

01:01:54: Yeah indeed!

01:01:55: Okay great then let me use that say thankyou once again.

01:01:59: too many people I don't forget.

01:02:02: So of course our subscribers, our listeners.

01:02:05: Our guests Thorsten thank you to you and Jan Niklas And the Academy of Sciences for funding their first season To the algorithm who shows us two other people to all those Who shared as actually something I was very happy about.

01:02:27: one Very friendly commentator mentioned that they shared our episodes on X. Maybe somebody will do so on Reddit, maybe not all fine and we'll do some self-advertisement or mailing lists but in any case... We are super happy for the support that you got!

01:02:51: It's really unbelievable to have a nearly hour long podcast with two unexperienced hosts.

01:03:02: this growth.

01:03:03: So if we extrapolate from that and in the first three months, we grew by a factor of infinity

01:03:29: because.