aboutlogic #16 | Schröder & Fisseni – The Language of Mathematics: Frames, Narratives & AI

00:00:00: Have you got an example like this, which comes from mathematics?

00:00:03: Do we stop hitting Dennis with telescopes maybe.

00:00:12: Welcome to our next episode of About Logic!

00:00:15: And I'm super happy that we have two guests and these two guests are doing lovely stuff namely Bernard Fesenni and Bernhard Schröder from the University of Duisburg-Essen... ...and both work for quite a while on the language of Mathematics.

00:00:31: This topic has many intersections with other themes that we already had in our podcast, like theory-improving software foundations of mathematics.

00:00:40: So thank you very much for joining.

00:00:42: Yeah it's a pleasure to be here!

00:00:43: Thank you for the invitation.

00:00:46: and let me start with a very naive question.

00:00:49: would I

00:01:01: think we have been working on how to apply the concept of frames, which is a very broad concept or a concept with many facets to the language of mathematics for some time now.

00:01:16: Before that in my master's thesis i tried to develop an annotation language for mathematical language ,which has And yeah, I think that is not a minute but maybe a start of what?

00:01:36: Yeah.

00:01:37: We will talk more about frames in another minute so let me hand over to Bernhard Schröder first.

00:01:45: Yes i can just add we are working with within the framework of thrames when we look at the language of mathematics.

00:01:58: So, although... The project in which this research is embedded it's the Naposh Project Which started in two thousand three I think and It started from looking at the language of mathematics together with some logicians from the University of Bonn, and we talked about some peculiarities in the language for mathematics.

00:02:29: From a linguistic viewpoint I had an impression that we could explain these peculiarities very well within the semantics with the dynamic approaches to semantics like dynamic predicate logic and this course representation theory.

00:02:53: And that was a start of the project, then in the first phase we developed controlled natural language which mathematical proofs could be written at least very basic proofs at first, and then later we moved to other topics which looked more pragmatic structure of proofs.

00:03:25: This leaded the occupation with frames.

00:03:31: Can I ask this a very general question?

00:03:34: Why are you interested in the language of mathematics?

00:03:36: ?

00:03:38: to give two answers.

00:03:41: One from a linguistic viewpoint and one, I think of formal mathematics... ...I'm not an expert in the last field but maybe i could say more about the linguistic viewpoints.

00:03:54: From the linguistic point proof texts are texts and text is very special kind.

00:04:00: Texts which we know what they should mean And therefore, from a semantic viewpoint we can learn very much from this text type how certain semantic structures are communicated.

00:04:27: Maybe so... We could add that the formal approaches to language and linguistics sometimes make purposes oppositions which especially true of what mathematical texts want to convey, namely that they have a very clear and accurate semantics which is not so much true maybe in spoken language or everyday use but as you will probably agree it's true for many mathematical discourses.

00:05:02: So it's an area which is so easier in a way than other.

00:05:08: I mean, if there are lots of everyday knowledge involved and maybe more difficult to say what actually the meaning should be right?

00:05:22: It's easier...it's more unambiguous that this important feature

00:05:30: It's maybe closer in some assumptions to the formal approaches sometimes come from a mathematical background and therefore it is not so surprising that they fit more into mathematical discourse than everyday language.

00:05:48: Nevertheless we find all pragmatic phenomena, which are known by other sorts of texts also through proof texts.

00:06:00: Can you give some examples of phenomena we are looking at?

00:06:06: For example, ambiguity is also present in mathematical texts.

00:06:16: Implications... So non-logical implications from assumptions.

00:06:26: what's relevant can be seen in mathematical text too.

00:06:32: And all strategies of resolving ambiguities and texts, also the way things are told worlds are kept small... All these strategies can be also seen in a mathematical text

00:06:51: which is I just thought this problem of ambiguity.

00:06:56: Or actually, this is intentional ambiguity because often we don't want to complicate our expressions.

00:07:05: So the overload... I mean same terms have lots of different meaning that are poorly seen or... This also something which plays a role in formal mathematics and computer formalization.

00:07:25: There seem to be, I mean as you say the formal languages are an idealization of informal languages.

00:07:34: So that is interesting tension here right?

00:07:38: Have we looked at how formal mathematics deals or tools deal with these issues?

00:07:47: Yes, in the thought they avoided.

00:07:50: So they avoid ambiguities and they avoid many pragmatic phenomena?

00:07:56: Actually they don't.

00:07:57: They don't avoid ambiguity.

00:08:00: Ambiguity is actually essential to have a concise expression And there's lots of work on how to dissolve ambiguity In formal mathematical texts.

00:08:16: The formal mathematics is actually closer to the informal text than you think.

00:08:24: Or as any of us suggested, maybe I shouldn't imply...

00:08:28: What kinds of ambiguities are you thinking?

00:08:31: So ambiguities would be something that cannot be absolutely resolved in context.

00:08:43: Yes so they can be resolved.

00:08:47: But the process, I mean for example type coercions.

00:08:55: I have an object of a certain type but need another type.

00:08:59: and now whenever you see an integer and you need a real number then automatically curses.

00:09:08: But this is actually ambiguous, it could be another way.

00:09:12: I mean there's mismatch that has to be resolved And they are lots of assumptions in even formal mathematics which make possible to write things without too many sort complicated annotations.

00:09:28: So for example if i talk about numbers and x plus one equals y. And now we know that X is quantified over, for example natural numbers.

00:09:40: but this isn't ambiguity because pluses also overloaded.

00:09:43: so there has to be a resolution mechanism as often more than one way to resolve these ambiguities or in the formal text right?

00:09:56: Yes I agree about it.

00:09:58: you rely on that.

00:10:01: there is an algorithm which resolves the ambiguity in a uniform way,

00:10:08: right?

00:10:08: So I mean this is arguable whether it's a uniform.

00:10:12: That's exactly the question then.

00:10:14: so and i'm just saying to research area in formal method I mean implementations of proof tools.

00:10:23: There's also work in trying exactly.

00:10:27: It just reminded me, I mean that this issue of ambiguity overloading polysame expressions which you identified is an issue in informal mathematics.

00:10:41: Actually it's also an issue and formal mathematics.

00:10:44: Yes.

00:10:44: but i would say the typical examples of ambiguity with natural language are those Easily resolvable.

00:10:54: I mean you can get a good idea about what is probably intended, but if ever for the one of the typical sentences is Dennis hit the mathematician with a telescope.

00:11:09: and Now we don't know whether the mathematician has a Dennis telescope or Dennis as a telescope.

00:11:16: And they're hitting worst.

00:11:17: and the telescope is an instrument off-hitting on.

00:11:21: And so And I think in a mathematical language which you or informal language that is compiled, there must be one meaning out of the interpretation.

00:11:35: That's normally ensured by compilers also... The sentence will not be acceptable.

00:11:42: but in natural languages we very often just proceed with probabilities.

00:11:49: Dennis is a kind person.

00:11:51: He won't hit someone with the telescope,

00:11:53: but he...

00:11:55: So it's probable that the other person has a telescope and this helps to identify the person who was hit.

00:12:04: Yes I think we

00:12:07: are already in the second half of the reply Right?

00:12:11: This is what the formal mathematician can learn from linguistic work To some degree because techniques of making things unabinguous might be better informed from how natural mathematical texts are passed, right?

00:12:29: So in some sense we jumped a little bit ahead but I didn't want to interrupt us and you had another question there.

00:12:36: Yeah this example is certainly a pausing problem expression into a tree and informal mathematics that's often done by assigning binding strengths to operators.

00:12:58: But you're suggesting in natural language this is just done by plausibility, right?

00:13:04: To what degree there's an issue of associativity and which can be resolved, I mean the two different pastries.

00:13:17: Which are not clearly explained.

00:13:20: what this meant?

00:13:22: And you say to choose between these two different different pastories.

00:13:27: You just look in the semantics.

00:13:32: based on the semantics... ...you chose a more plausible interpretation right?

00:13:40: An answer of a formal linguist, maybe psycholinguists would say something different about whether you in certain context.

00:13:49: You just expect for instance if you have seen Dennis before with the telescope?

00:14:04: very similar sentences, which had a very determinate meaning.

00:14:08: With was always used to designate the instrument and you would probably expect that with encodes the instruments in this sentence And then it will change your expectation.

00:14:21: We can discuss whether these are pragmatic or semantic issues.

00:14:25: only

00:14:28: Have we got an example like this?

00:14:29: Which comes from mathematics.

00:14:32: Do we stop hitting Dennis with telescopes, maybe?

00:14:37: So one type of ambiguity which is quite everywhere in mathematical texts are scope ambiguities.

00:14:45: Like how far does the scope of a certain assumption go?

00:14:51: or another type of ambiguous is a syntactic ambiguity.

00:14:55: you have sentences like for any A and B such that some C and D is valid, something's true.

00:15:07: And this such-that attribute can be applied to A AND B or just to B. These are quite typical cases of ambiguity which everywhere in mathematical texts.

00:15:24: To get back to my point, so these ambiguities first of all also exist in formal mathematics but they are then often resolved.

00:15:39: In a way which is also applied to programming languages right?

00:15:44: So different operators have certain binding strengths and as the result we disambigualize.

00:15:52: But you were saying that in mathematics it's more down on a sort level based on the meaning, what is a more plausible interpretation?

00:16:02: That's that difference between formal and informal mathematics I suppose.

00:16:09: In both cases let say missing.

00:16:14: bracketing strategies in natural language are of course you can try to introduce or control the interpretation of such expressions, but if you want to do it very universally.

00:16:34: The costs are quite high as you can see in controlled natural languages

00:16:41: because we don't really use brackets.

00:16:43: initial language right?

00:16:45: Right and formal mathematics You can just use brackets But breakers I'm not very popular cause they make it more difficult to read.

00:16:56: And

00:16:57: you can use something like brackets, maybe if you say quotation.

00:17:02: Yeah starting quotation ending and then You know that Something is a quotation and has to be interpreted in A different context.

00:17:12: I find actually when he have been do spoken mathematics Like If we give the lecture?

00:17:17: You Can Use the pause and how much time look The timing To Express Exactly this as a scope the scope issues.

00:17:28: But obviously, the techniques in written mathematics are obviously different and you're saying it's one way is to just go.

00:17:40: what was a more plausible interpretation?

00:17:42: Are

00:17:44: there

00:17:44: other ways to resolve these ambiguity?

00:17:47: I

00:17:51: tried to indicate that plausibility can mean different things if For instance, if you have German compounds or so.

00:18:03: You can trigger different interpretations by providing a different context and I think that in mathematics as well.

00:18:10: but it also works with English.

00:18:13: If we talk about the chicken steak and cow's steak then childrens' steak will start to laugh.

00:18:22: talk about things that are for people before, give it a context where.

00:18:27: It's clear that this is normally if you read on the menu will not laugh too much right?

00:18:34: You may be aware of ambiguity because like playing with language but most people just don't care.

00:18:41: and similarly if you have established A always refers to certain kind or variable probably take the last expectation and not what is gen maybe for someone who's not in this field, uh most prominent use out of context.

00:19:04: So there are some sort of context dependency off those process right?

00:19:09: Yes but of course contexts can mean very different things.

00:19:13: Contexts can be a syntactic context.

00:19:16: Contacts something must be consistent in the very narrow context, or context can mean a very holistic text.

00:19:33: Context can explain everything because it's a very ambiguous and weak concept.

00:19:43: Maybe let us talk about one particular thing that might be context which you worked on namely frames, the background knowledge that helps us to enrich what's actually written in there.

00:19:57: Would you be willing to give us a rough idea about that?

00:20:00: Especially since it is also artificial intelligence as so many things but another kind of AI I guess.

00:20:11: It's an old-fashioned kind of

00:20:13: A.I.,

00:20:13: nobody wants anything at the moment.

00:20:18: probably

00:20:20: It will come back, there'll be another winter of the newer methods and then

00:20:25: I don't know.

00:20:26: There is maybe also a link to modern AI in this sense that we assume that frames are learned.

00:20:34: so you learn certain about certain situations and develop expectations about them And... Of course We may hope machines also learn something like frames.

00:20:48: The idea would be that the, for instance if we know about a podcast We know there are some hosts and Some guests or maybe just one of them.

00:21:02: And Maybe if you know it's a podcast About logic?

00:21:17: Already and then we talked in the beginning whether that podcast could be with video or could just be audio as In earlier times, and That would be different kinds of podcasts And you could cross classify this With video logic podcasts and video non-logic Podcasts.

00:21:40: And so on.

00:21:41: You know how to do that?

00:21:43: We think Talking about mathematics works in a similar way with expectations of what is done at certain moment, for instance.

00:21:59: It's interesting because actually the new AI on which these large language models are based... ...is doing something like this.

00:22:11: but frames aren't pre-programmed.

00:22:14: they actually learned, so that is cover certain structures in texts and also in the current context.

00:22:23: And learn then exactly something which is frames.

00:22:29: but these frames are not prescribed or put-in.

00:22:41: It may be interesting to look at the relation between this frame concept from old AI and context-dependent learning, which was implemented in modern AI.

00:22:57: This is a large language model.

00:23:07: All I know about the frames in the newer AI models is that they are, in some sense quite flat.

00:23:17: And the frames which we talk about in the context of mathematical texts are quite rich structures... ...which also come from a fact that they're designed manually and not just learn from text.

00:23:40: I think there are aspects of such frames, which at least... At the moment hardly can be learned from texts because they're not very explicit in the text themselves what machines learn.

00:23:59: So maybe if we assume that there is a... We stay with the podcast example, you have guests in logic podcasts.

00:24:08: You could model the podcast having a subject and people having an area of research And then say normally podcasts or scientific podcasts have areas where research matches of the podcast in some sense.

00:24:32: And that would be a kind of deep modeling because you wouldn't say... The first thing to think about for people is they have an area or research also, maybe it's somewhere in their professional competence and then in a specific kind only makes any sense for people who are working in academia?

00:24:52: Maybe so on!

00:24:54: Then for podcasts Similarly, layer structure of what makes them up.

00:25:02: And I think that is not explicit in texts normally?

00:25:07: Yeah it's not implicit on one text but there are lots of texts and you can discover...I mean like the humans can discover this.

00:25:17: so it seems to be..so nobody understands exactly what these LLMs doing.

00:25:24: So thats fundamental difference to what you're doing, but they discover surprisingly deep structures when it starts playing around with them.

00:25:37: And so how would this frame project for mathematical text look like?

00:25:42: And again maybe anticipating a question of Thorsten and why would somebody do that?

00:25:48: What's the usage?

00:25:55: If we are dealing with mathematical text and try to understand how these texts are structured, the frame approach helps us fill gaps in the text.

00:26:08: It also helps us get things into a structure which can be interpreted.

00:26:17: For example... We have looked at induction proofs.

00:26:25: In these proofs, some steps which you would expect in a normal induction proof are just not mentioned.

00:26:32: They do not appear and they're left to the reader.

00:26:37: To make sense of this whole proof and reconstruct its logical structure we have to reconstruct these missing statements And we think that frames could be a good tool to do.

00:26:55: Yeah, why not?

00:26:57: I was just because you asked how the project looks.

00:27:01: so what it looks like has maybe some?

00:27:04: if You want a general picture linguists try to work with basis of texts.

00:27:09: i think bettered Has already be supposed this in What he said.

00:27:14: So The project could start and That's what We are planning at the moment too by collecting texts and pre-processing them in a way that we can discover frames, look for what parts of frames are realized or not realized.

00:27:34: And then build up knowledge about how frames were used in mathematical text.

00:27:42: Lingwitz called it corpus but people call lots things corpora at the moment.

00:27:47: so maybe you have already heard this term.

00:27:50: If you don't have anything to say more about frames, I would open maybe a third and final bunch of topics.

00:27:57: And that's one of the narratology perspectives on mathematical texts.

00:28:05: So there used be a philosophical tradition saying math is just writing stories And so writing proof text was just writing a story.

00:28:16: never do say that and others still like the idea.

00:28:20: What kind of associations is this bringing to you as linguists, as marathologists?

00:28:28: Yes we can look at the structure of mathematical texts from a viewpoint or story.

00:28:36: also frame approach may contribute because what has been told something which helps to identify the frame and then fill gaps that are not given by a frame.

00:28:59: That's an important part of this story, I think one could look at from this viewpoint to mathematical proofs.

00:29:09: another view point would be what is?

00:29:14: Is it what is told in a mathematical proof and when two proof texts are instances of the same proof?

00:29:27: We have also thought about this, maybe Bernhard could say more.

00:29:35: Maybe it's not clear why that is related to narratology... The same question can arise when you talk about, for instance a film and book or two versions of the story... ...or novel or whatever play.

00:29:57: And try to find out whether they are the same in some sense?

00:30:06: Then I think that first thing he will say is obviously they're the same but not and then you can start to discuss what kinds of identities are or similarities relevant.

00:30:22: And similarly, probably you cannot do that without mathematical texts.

00:30:28: so does it make if two proofs omit different details?

00:30:36: Can they still be the same proof?

00:30:40: I'm not sure... as with narrative literature, that you can give a definitive answer on that question.

00:30:52: But you can develop maybe interesting ways of looking at the question by that and we have tried to work out in what sense this can be similar two models employed.

00:31:13: And I think a further aspect of this storytelling approach is to look at how the discourse entities in mathematical texts are managed.

00:31:28: So, mathematical texts talking about huge discourse universes with non-finite set and so on but they have do it that they address a manageable set of discourse, let's say discourse reference.

00:31:49: So distinguisher bill objects which are referred to most.

00:31:56: for example if you talk about all numbers and in this moment you just talked about one object would you look at?

00:32:07: And what do you treat your text And the objects which are introduced in mathematical texts, they're highly related to each other.

00:32:18: They are grouped into complexes and that helps keep the set of discourse referenced.

00:32:28: so things which I refer too quite small in mathematical text much smaller than most types of texts.

00:32:38: So this is these dynamical approaches you mentioned in the very beginning.

00:32:43: life could model something like that and whatever we talk

00:32:48: about.

00:32:48: Yes,

00:32:49: actually I was just wondering what one thing so often i find about proofs.

00:32:55: they are difficult to tell.

00:33:00: You have to do them yourself basically And and often proof texts others sort of give enough hints for the reader, depending on the level of the reader to be able... ...to do the proof themselves.

00:33:19: Because you cannot actually... I think it has to be the proof or that's maybe not a preferred way to deal with this.

00:33:29: and also so there may have been frames where we can leave out lots things in the proof because all they want is enough hint.

00:33:38: You see, our proofs is by induction similar to the theorem such and such.

00:33:44: So instead because as I say it's very difficult to read poof or would say virtually impossible what you need do is execute a poof using some sort of hints which we get from text.

00:34:02: Does this play a role in your work?

00:34:08: Yes, I think if you are able to do the proof.

00:34:11: then you have a frame.

00:34:12: how too.

00:34:13: How?

00:34:13: You can't do it and you need The necessary hints To yeah to

00:34:19: fill

00:34:19: in the gaps.

00:34:20: Yeah, I Think that's yeah.

00:34:23: And i think another technique is of course analogy as you mentioned That someone says this Is quite analogous.

00:34:31: two that prove so that you can follow the same path to do the proof.

00:34:40: It's also, I think one of the points where formalizing becomes most difficult because... Most formalisms i know often just use a kind of comment in this place is similar to that proof and then you still have to model all the details yourself And humans seem to be able make sense of these comments in a much more broad way, to trigger the right frames.

00:35:11: Maybe you know better formalisms Thorsten but... No no

00:35:15: I don't know about formalism at all!

00:35:16: But I'm using chapshippity and it's quite good to do this kind of thing.

00:35:21: so astonishingly.

00:35:23: Or any LLM?

00:35:24: sorry i should mention number also.

00:35:30: Yeah, and maybe one another association about these story approaches that there is a lot of framing now in an slightly different sense of the word frame.

00:35:42: Of proof.

00:35:44: like even if they objective level... If we want to speak like that effects are clear.

00:35:49: sometimes you can motivate a lot by switching your perspective on the area You could see something as something The Wittgensteinian in me would like to say so you can craft how the audience Can understand what's given a little different text and sometimes this is quite?

00:36:10: The revolution in mathematics, right if we read Laudatios for the Fields Medal We often see something Like Person X was the first to frame area Z In terms of Area Y even If it's not changing effects.

00:36:26: Right It's just different way of writing things down, so to speak.

00:36:30: That's a highly productive motor of innovation and math.

00:36:34: would you

00:36:35: think about that?

00:36:36: Is perspective used proper like the neuratologist would use or which is not used perspective?

00:36:46: It's difficult to find the parallels right maybe... You can talk about cases for epistemic relationships or so, if something that is told from the perspective of a child and you have to kind of unpack this.

00:37:10: To understand for instance why there's just horrible event in the child doesn't even understand it might be this transfer off perspectives that are necessary for interpreting texts.

00:37:27: For the rest, it may be more similar to different kinds of media or different kind of texts dealing with a same event or the same story.

00:37:39: I'm not sure this would be called The Perspective in Erotology?

00:37:46: Within our frameworks makes sense To call it A Perspectve but i think that's Not what you Would Think Of Probably.

00:37:54: Yeah, I think what you call perspective has very much to do with the shift of frames.

00:38:01: You see some object as an instance of certain frame and then look at the same object As an incident off another frame And get new relations new techniques argumentative techniques and so on with a new frame.

00:38:22: So if it's closer too some theories of metaphor also.

00:38:29: What is traditionally called perspective?

00:38:32: Okay, I see we are around our regular time limit for these episodes but i still would invite you.

00:38:40: has anybody's still a pressing issue or want to talk about the new project wants advertise something?

00:38:48: then this will be an opportunity.

00:38:51: thinking about a point that Thorsten made, you have to do

00:38:56: proofs.

00:38:57: And I think it is an interesting point when we speak of this narratological modeling where you talk about worlds in which something changes and doing the proof also applies some changes.

00:39:16: while normally mathematical texts are special The world does not change in these proofs, but you describe as most people claim eternal truths.

00:39:31: So sorry this is a new point... No

00:39:35: no it's right on the heart of repeating discussion within about logic so their different perspectives or mouth would...

00:39:46: I don't know how quite just related to me.

00:39:49: Mathematics is all about, as you say telling stories and it's not about the real world because its constructions we do in our head.

00:40:03: And this forces me or suggests to me that I adopt a more constructive foundation where the notion of truth is rather difficult because as the notion of truth, it's difficult in a story.

00:40:22: Because certain things are not saved.

00:40:23: I mean for example that where there Captain Ahab had a blue shirt and Moby Dick It's non-mentioned.

00:40:31: So anyway this idea that mathematics has really particular kind storytelling Is important to foundations of constructive mathematics.

00:40:43: And indeed, if you look at how constructive mathematics is mathematically modeled namely by Kripke structures and Bette models exactly these are the structure of stories.

00:40:56: I mean this explains what's for example implication in a story that P implies Q later find out as P holds and Q holds even in the moment to establish this relation, but I don't know whether that relates with what you're doing.

00:41:19: And maybe in some sense mathematical texts do not tell about the fact of what they actually can or in a hypothetical sense could have done?

00:41:31: Because there are parts of these proofs where you could and never did it!

00:41:37: Yes, but also these are constructions in your head.

00:41:41: I mean they don't exist in the real world unless you're a hardcore Platonist.

00:41:49: there really things we have invented.

00:41:52: We've invented mathematics and not discovered it.

00:41:56: so that's the punchline.

00:42:00: But i think this even works on classical math into quite some degree.

00:42:04: at least the language looks like that, right?

00:42:08: There's this work on the Tetric phrase.

00:42:11: it is.

00:42:12: Bernard I'm not sure.

00:42:13: Zai are in a group so let this be...

00:42:17: Recorded Static Phrase yeah!

00:42:19: So it's an illucosinary act.

00:42:23: you say something into existing and even if maybe Platonist wouldn't say, okay you really built a triangle and now it's there.

00:42:34: And wasn't that before?

00:42:37: Our proof could very well say do the circle around point A and one round C and they intersect in points B and D as our speaking about math is often more constructive, more temporal or story like than the logical reconstruction where we just go to the deductive whole and get every statement following from the axiom in an instant.

00:43:05: So I think this is a productive endeavor even for classical math, especially in math education because their understanding without doing it's something students wish for.

00:43:17: but unfortunately that doesn't happen right?

00:43:21: Yeah!

00:43:22: And interestingly this constructives U is built into the Euclidean approach to proofs.

00:43:30: The construction phase in this proves the way he constructs some objects and then derives some claims from it.

00:43:42: And interestingly, this phallic phrase is often verbalized in Euclidean proof by an imperative of a third person.

00:43:59: There is an order to whoever, let something be.

00:44:08: So it's maybe interesting for

00:44:10: what you said

00:44:11: or if you combine this.

00:44:14: so on the one hand there storytelling and a story telling can be done by reading book but actually poofs are more like acting I mean, where you act a play and instead of just deleting it.

00:44:29: Right?

00:44:30: So that's what was this idea off that we have to do a proof.

00:44:35: UU acted.

00:44:36: And also relates too maybe with your last mentioned about the Greek text.

00:44:43: Yeah!

00:44:43: Maybe there are some similarities to cooking receipts or something like that in some sense.

00:44:52: But you can, is it the complexity that makes it possible to read cooking recipes but not proofs?

00:45:01: I mean at least i would claim.

00:45:03: You can read a cooking recipe and get an idea of what happens... ...you probably don't know what it tastes like in detail.. ..but you'll get an ideal for your have-to

00:45:18: do!

00:45:18: I think it's related to this background knowledge, right?

00:45:23: Seasoned mathematicians who stay with the cooking recipes would have some estimates what could happen even without doing the proof.

00:45:34: Like if my well-known professor says just use something like that and i don't know the details but it will work out somehow.

00:45:45: I think this is very usual in math.

00:46:00: do the recipe and actually interpret it maybe in a creative way.

00:46:23: I have slightly different version, which is also true for proofs.

00:46:26: you know if once you implement... Once you play your proof It may end up to be something slightly different from what we've seen before.

00:46:36: Yeah i think difference two plays Is that there's normally just one actor.

00:46:42: So so would he Right?

00:46:46: You manage everything in a proof.

00:46:49: Normally it's not that the triangle does something or the compass,

00:46:58: I mean there is this idea of using sort of dialogues to model quantifier nesting right.

00:47:05: so if you try to understand how for example an application These are often, and this is also a formal way to understand the logical system by actually having dialogues instead of just one person acting.

00:47:24: So that's actually...

00:47:27: But then it would be two people talking about what was done or It wouldn't be the mathematical objects that do something.

00:47:39: The

00:47:41: point

00:47:41: I was trying to make, but in a play it's actors doing something and the fact of acting would be... And the actors are more like the object on this story which will be themathematical objects right?

00:47:56: Yeah okay i think.

00:47:58: maybe this analogy is a bit tricky here.

00:48:03: I think the cooking recipe works a bit better, or maybe playing with puppets.

00:48:12: But we should not forget that there are of course important differences between recipes and proofs because Recipe is Directive Speech Act.

00:48:24: so you have... imperatives and so on.

00:48:28: But my mathematical proofs also seems to tell about facts, huh?

00:48:35: So it's an assertive speech act.

00:48:36: in most parts of it only the assumptions are usually communicated with directives speech acts.

00:48:47: Okay that another interesting story.

00:48:53: use yet another word.

00:48:55: But let me ask Thorsten and Bernhard, do you have something which he wanted to bring up or to deepen?

00:49:02: that's mentioned in our discussion?

00:49:04: I'm fine

00:49:07: too.

00:49:08: Then i guess it is time thank-you!

00:49:24: and any other papers that we mentioned, I try to add them there.

00:49:30: And then i can say thank you very much for being here.

00:49:33: it was an interesting talk!

00:49:34: Thank you

00:49:35: yeah.

00:49:35: thank you for inviting us cool.

00:49:38: Then great let me tell the audience as always don't forget to subscribe comment discuss.

00:49:47: We hope have in comments section more or less productive exchange and see you in two weeks.

00:49:55: Bye

00:49:57: bye!