aboutlogic #23 | Rebuilding Mathematics from the Ground Up | Giovanni Sambin

00:00:00: I was not satisfied by the standard foundation.

00:00:04: What does it have to do with reality?

00:00:07: And this, i just could not swallow in...I tried to talk With a friend.

00:00:14: he said Giovanni don't worry It's Just A Game!

00:00:18: I Could Not Understand That!

00:00:20: To me..It is not.

00:00:21: Again You Must Explain Every Reason Why you Should Believe Something.

00:00:32: Hello Everybody This is the latest installment of About Logic.

00:00:40: And I'm very pleased to have an old friend, colleague, Giovanni Zambin here and he will introduce himself a bit more i hope?

00:01:04: But I wanted to start first with maybe your most recent work and you recently published a book, Positive Topology.

00:01:13: Could you give our audience like rough estimate about the idea of what's topology classically?

00:01:19: And What are the differences in this approach?

00:01:23: so there many things to say.

00:01:25: First off all i want thank for inviting me here.

00:01:30: It is an excellent occasion.

00:01:33: promote my work and my book, which is standing there.

00:01:40: It's not something... So putting together something you said and something Thurston said.

00:01:48: We know each other since many years And this research The research included in the book goes back to many, many years ago.

00:01:59: I'm ashamed to say it goes back at least two-forty years ago into the seventies even fifties but there is always recent so It came out only last year.

00:02:13: So its very difficult.

00:02:15: we will...I'll try make a summary To understand what this situation in general.

00:02:25: but it's difficult to see in detail all details.

00:02:32: It is like telling the story of evolution, when you consider long stretches of time... ...it is difficult to explain changes just by seeing a final result.

00:02:48: So this book is the final result!

00:02:50: But to understand that you have many motivations going very much before.

00:03:00: So, about point-free topology is one of the consequences of big motivation.

00:03:08: My very... The very motivation for studying mathematics so that's really almost sixty years ago was to understand how come you must believe in something even if did not expect.

00:03:32: Like I was shocked by Euclid's proofs of his elements, the textbook in my high school is more or less exactly the Euclidean elements translated into Italian.

00:03:51: But anyway, I got the feeling of the idea of proof.

00:03:56: So in a sense i wanted to understand how come proves convinced me?

00:04:03: And then when my first year I discovered that logic existed and also that philosophy of mathematics existed... ...I remember reading a book in sixty-eight.

00:04:16: so that's long ago!

00:04:19: Since then.

00:04:21: Then I went to Berkeley for one year.

00:04:24: I was not satisfied by the standard foundation, CZF axiomatic set theory because of many reasons.

00:04:35: they will come out later perhaps but the principal one.

00:04:42: just putting it very plainly what does that have do with reality?

00:04:49: and this I just could not swallow in any way.

00:04:54: I tried to talk with a friend, who i am still in contact probably coming from place close where Thorsten was born because he came from Hamburg.

00:05:11: He said Giovanni don't worry it's just again.

00:05:15: but I could not understand that.

00:05:19: To me, it's not a game!

00:05:21: You must explain every reason why you should believe something... It is not just the game and i refused to believe in ZFC then came back and luckily bit by bit i discovered the constructive approach when i discovered per Martin Leuph And so bit by bit I became more competent.

00:06:17: sometimes discussions about this with my wife, who has a degree in philosophy.

00:06:23: So I know that it's my limit!

00:06:27: Anyway...I read the lot and history of The Last from Dead Kind Encounter onwards In particular And around the nineties I published a paper in Italian, unfortunately because it was too difficult for me to explain what i reached.

00:06:54: Namely What they call dynamic approach which means In few words Assuming nothing Which is from above.

00:07:07: Everything must be From ground natural, sorry?

00:07:14: From bottom up.

00:07:16: From bottom-up yes!

00:07:17: Human, natural real nothing given that we must believe why.

00:07:25: nobody knows why but you must believe this.

00:07:29: I just by my experience personal i mean...I cannot digest it.

00:07:36: so I discovered that the only way to explain mathematics without needing to submit some supernatural assumption was to see it is grounded on... sorry, on the ground.

00:07:56: Bottom means just what we are as human beings, so biology which includes it's not just material.

00:08:06: It includes communication spirit ideas a lot of things but still biology.

00:08:13: and

00:08:15: when I realized this i was very glad...I believe it is uh um..i was forty three which means in my opinion the peak of your maturity.

00:08:31: And then from that point on, I tried to see how to do mathematics according to such view.

00:08:40: Before that there was formal topology.

00:08:44: After that it beat by bit.

00:08:47: It took many years and became what i now call positive topology.

00:08:52: The main difference is... Formal topology putting type theory into action, so to say.

00:09:04: Proving that you can do mathematics totally based on Martin Lef's type theory.

00:09:11: in particular formal topology is a generalization of four examples given by Perl-Martin Lef and his PhD thesis.

00:09:21: nineteen seventy where at topological space.

00:09:28: I will tell a little bit later what topological space is.

00:09:32: Topological Space is constructed completely constructively, completely recursively computationally while in my opinion there are must be also ideal elements.

00:09:48: so a topological spaces usually made of points and open subsets tell how much two points are closed or separated.

00:10:16: So the way of permartin lift was to start from open subsets And define them recursively in some way, instead of starting from points which is the common way.

00:10:37: Can we just do a little example?

00:10:38: I mean like the reals and intervals are open... There

00:10:46: are two very useful examples.

00:10:51: one is real numbers.

00:10:54: So real numbers are points of the topological space and in particular basic opens, in a standard way is to assume intervals with rational endpoints.

00:11:09: Yes

00:11:10: so you immediately see the difference.

00:11:13: Rational numbers are denumerable.

00:11:16: You can generate them inductively by looking at them as fractions, so you generate all possible fractions and You can see this is an inductive generation Modulo a certain equivalence.

00:11:32: real numbers cannot be generated Inductively.

00:11:37: So if we wish to keep that's the essence of what I added If We Wish To Keep Both Ideal Elements As Points And The Computational aspect given by numbers, by inactive

00:11:55: generation

00:11:56: and so on we have to keep both things.

00:11:59: Both opens are given primitively AND points.

00:12:04: but if you give Opens as Primitive then Points are defined And they're defined very similar the way Dedekind did with real Numbers As what we now call Dedekin Cuts.

00:12:20: You start from rational numbers, see that every rational number divides the line into two separated but to disjoint.

00:12:34: But whose union is the whole thing of rational numbers?

00:12:40: and then you say I take one of these without knowing the separation point, as a new idea for real numbers.

00:12:52: It's very similar to every topological space you want to describe corresponding to dead skin cuts determined by something.

00:13:15: then you abstract and Then You define the ideal points over This more abstract situation.

00:13:26: another useful example is a tree if in my opinion trees go upwards not downwards as for Broward.

00:13:37: so If you have a tree going upward, like that and every node can be reached in a finitary way which means the set of all possible nodes is a set.

00:13:54: In this sense it can be inductively generated.

00:13:58: if you pass through the idealization You go on without stopping at the finite point At the finite level.

00:14:08: then you have the idea of arbitrary path, not finite but goes on forever so to say.

00:14:18: And that is an ideal notion because uh...you have to simplify the notion of a finite list with arbitrary length which means you never stop.

00:14:36: And that's an ideal notion.

00:14:40: In my new approach, as in the book you obtain all possible paths of a positive topology over the final nodes.

00:14:55: So this solves huge problems mathematicians had with Broward's.

00:15:05: Now, what replaces choice sequence is a path.

00:15:12: So instead of saying the creative subject chooses an option every day or so and with free creation of their creative subjects I say... ...I use geometric notion.

00:15:30: just look at tree and imagine you go up.

00:15:35: It's a geometric intuition.

00:15:37: Imagine you go up without knowing the branching and Assuming, you never stop.

00:15:45: that's very intuitive geometric notion which is exactly Described by the notion of ideal point.

00:15:55: By the way We We'll touch the discussion about Axiom of Unique Choice and so here you see already, we come later.

00:16:13: The reason for point-free topology is that in a new approach... ...we want to take care both of the computational aspects and the ideal aspect.

00:16:28: And the point-free approach is a way to deal with spaces having both computational and ideal elements.

00:16:41: The computationals are on what used to be base of topological space, which now is an open first approach that explains Pointless topology.

00:17:00: By the way, it's not pointless at all!

00:17:03: Yeah and this is a joke if you would say pointless topology You know because... There

00:17:09: was paper called like that right?

00:17:10: What's the point of...?

00:17:12: In the paper as in Is It Yours.

00:17:14: what's The Point Of Point-Free Topology?

00:17:17: No no there was a paper by Peter Johnston The Point of Pointless Topology.

00:17:24: Yeah

00:17:27: Pointless.

00:17:27: I'm not sure it was him that started the name, but anyway he used.

00:17:33: So from a constructive point of view... It's very natural to start with the open sets which are concretely definable and then the points actually something as you said which comes later Which is ideal elements.

00:17:52: What do you think added?

00:17:53: is to have this positivity that you like an interval which contains points, right?

00:18:02: You may have a interval with no points.

00:18:05: Maybe it's empty intervals or one side negative so that not positive.

00:18:10: So in the positive topology there are these positives.

00:18:15: There IS a point and its important to say there is a point It doesn't mean pointed, right?

00:18:24: So it's non-empty.

00:18:27: I mean to have

00:18:30: the... The informal topology.

00:18:31: you had one we call them infinity relation saying that a basic interval for instance in case of rational and real numbers is covered by a subset Like,

00:18:52: very

00:18:53: easy examples like an interval and you cut it in many intervals which covered that.

00:19:02: That is what I added to understand the deep logical structure underlying this definition of cover for all exist.

00:19:24: Then when I saw that, I realized we were missing the exist-for-all property to be expressed.

00:19:33: That's why the positivity relation came emerged In the formal topology.

00:19:41: one had a predicate pause which was unary predicate basic opens, which were exactly expressing what you said.

00:19:56: Namely this basic open contains a point or not in point three terms.

00:20:03: Now people asked me why do I add that?

00:20:08: and the answer is That Not only i took it away as A lot of People suggested but i strengthened.

00:20:15: It became a relation a binary Relation between an observable and a subset, arbitrary subsets of observables or basic opens.

00:20:28: And the intuition is there's point such that no exist for all... There are points in isolated neighbourhoods such that all the neighbourhoods at this point are in the subset you specify which is a very topological way to say not only that the starting basic open or observable is inhibited but also where it is because you see all its neighborhoods must be in this big subset.

00:21:10: It's not totally intuitive, projected geometry, when you pass from points and lines.

00:21:20: And then take the duals... ...and take all lines in a kind of point.

00:21:26: Things like that!

00:21:27: The positivity

00:21:29: relation is in a sense dual to the cover relations?

00:21:32: Yes

00:21:32: absolutely totally dual.

00:21:35: You can show very rigorous sense In which senses it's dual When we have points given, so to say in some cases.

00:21:46: Then you can see in detail how cover and positivity are defined In a very logical way And then the definition is totally dual To each other than when You start in a point-free Way?

00:22:02: you keep this cover and Positivity relation and define them abstractly, axiomatically so to say.

00:22:11: You call positive topology and structure satisfies some properties of these two that you discover easily when points aren't given.

00:22:25: And then you reverse things.

00:22:27: It's like with Dedekin.

00:22:29: he starts from rational numbers assuming there are the points on this geometric line sections in a point-free way and then define points.

00:22:40: And similarly, now you define the point free notion assuming that there are points... Then when you understand how to define them You keep taking them as primitive definition and defining ideal points.

00:22:59: By the way In this way you can obtain many more points.

00:23:05: In a way, what you do is this idea of synthetic mathematics.

00:23:11: So first off all... You had an analytic investigation of examples of topology, poetry-topology and positivity And then you abstract the general idea and turn it into a synthetic definition.

00:23:33: It is incredible how effective this method is.

00:23:40: You start from a case in which points are given as the set, like rationals and then by these methods you obtain all definitions basic topology positive topology morphisms and ideal point And it works perfectly.

00:24:00: It's also a good way, I think to explain the general idea as you do by starting with examples.

00:24:08: And then there are some sort of generic example that you can use to anchor your intuition about what is going on right?

00:24:17: Well yes!

00:24:19: The four examples analysed by Per were Euclidean space many dimensions, real numbers bare space the tree which one?

00:24:39: there are four examples very natural examples and in a sense the axiomatic approach or you call it synthetic approach to point free topology is just generalization of those four examples to any possible example.

00:25:04: And nobody did exactly a comparison between pairs approach and the approach for multi-pology, it would be nice historically do that but I'm sure they checked off course axiomatic approach with the notion of nowadays, or positive topology.

00:25:34: Okay maybe we can move on a little bit because you already mentioned Peer Martin-Löw and maybe should mention that you wrote book about Tide theory which was based on lectures by PeerMartin Löw right?

00:25:49: Exactly

00:25:50: yes!

00:25:52: That is way to know me.

00:25:57: Yeah, I don't know.

00:25:59: I mean suddenly read this book and was quite impressed and fascinated.

00:26:08: so you are certainly very close to Pierre-Martin Leuven but recently used you and Millie Mayetti, maybe some other people.

00:26:22: You went on and developed a sort of refinement of modern type theory right?

00:26:28: Yes

00:26:30: so after publishing... After sending the manuscript off The Little Book Intuitionistic Type Theory, the lecture notes that you mentioned I went to Sweden and to work with Per.

00:26:51: And the very first day we sat down on around a table, I told him...I remember very well!

00:27:00: I tell him, Per, i'm very glad to work you.

00:27:05: it's an honor something like that.

00:27:07: Thank You very much but please..i would not like to work all type theory itself because you will always be better than I am.

00:27:20: I have nothing to add, but i would like to see that you can do mathematics using it because type theory was convincing apart from an issue we'll touch immediately did not see at the time any supernatural assumptions, but one had to check that you... One had to prove that you can do mathematics with it.

00:27:57: And Per did not do that properly.

00:28:02: It was clear from his thesis That I already mentioned ...it was clear that You Can Do Mathematics But not in a standard way, it was very computational.

00:28:17: Intentional?

00:28:20: Probably yes

00:28:21: but actually the book is still about extensional type theory right yeah and that's what refined later in this sort of intentional type theories.

00:28:35: or what's?

00:28:38: What is equality, what's the equality type and types theory?

00:28:42: And in...in The Old Approach itself reflects exactly whatever magic equality Is there.

00:28:50: So In a sense it´s not well grounded I would say in your sense because It imports a meta-theoretic notion into the calculus and ...it has this nice advantage that it behaves very natural in the sense of that function and extensionality, if two functions agree on each point then they are equal.

00:29:11: So this is very well behaved but it's not grounded I would use your word.

00:29:22: so an intentional type theory was a refinement but and maybe that's your point, it is very hard to do mathematics in it.

00:29:34: You got the point exactly!

00:29:36: So historically so-to say... It was a lucky coincidence that Per spoke about the extensional version of Type Theory when he came to Padua And He went back to the intentional one later One year later also When I first absorbed type theory, it was the extensional version and that Was fine for me because i was interested in doing mathematics.

00:30:11: And to do mathematics you need The extension of theory otherwise what?

00:30:15: You reach is something totally different from the mathematics done by mathematicians In practice.

00:30:24: so

00:30:26: Sorry, even constructive mathematicians.

00:30:28: I mean... We shouldn't be surprised that we do things different than the average mathematician.

00:30:38: but even doing things constructively is further handicapped by working in intentional type theory?

00:30:49: Totally agree!

00:30:49: Good point!

00:30:56: To make it very short, now in the approach we developed there are two levels.

00:31:04: The intentional one at the bottom and the extensional one above.

00:31:10: to do mathematics you need the extension of one...to work with proof-assistance consistency metamathematical properties You need intentional ones And how they linked?

00:31:24: This is an idea I had in ninety-five.

00:31:28: They are linked to the following way, what they call a forget restore principle.

00:31:33: from the intensive level you forget some information To the extension one.

00:31:41: we can see in detail What it Is.

00:31:45: but You Can't Forget Something and Work at The Higher Level.

00:31:50: only if so to say you Are able to Restore It when necessary, which is a way to say that you do not lose... A way of saying don't go too high.

00:32:03: You keep contact with the ground and start from it in such strong ways so as

00:32:09: one can go back

00:32:11: when wished.

00:32:13: So this I would say was the main idea for what we call the minimalist foundation.

00:32:23: Ninety-five, it was written explicitly anyway.

00:32:29: It was somehow there in what I defined as a subset In the very first version of formal topology book paper.

00:32:39: A subset is a property While in type theory you with a property You can define the sigma type.

00:32:50: Here you take the property itself so you forget about the element telling that a certain element satisfies... Sorry, you forget about the proof.

00:33:04: That a certain elements satisfies a certain property?

00:33:08: That is information you forgot and You can show it can be restored.

00:33:16: So, doing mathematics in the minimalist foundation is this way.

00:33:21: You do not... It's a standard extension approach where two functions are equal if they give same values on the same inputs but at the same time you don't lose contact with intentional or computational aspects.

00:33:44: It's a bit complex,

00:33:46: but it works.

00:33:48: Maybe you can contrast this with another development which was led to what we could call now homotopytax theory?

00:33:57: But actually that started much earlier I think.

00:33:59: or...I mean i was looking at how he can have extanginality in intanginal type theories.

00:34:07: so these how to combine these apparent contradictions and make synthesis right.

00:34:14: And we learned how to do this.

00:34:17: Romeo wrote a paper in ninety-nine, then much later the idea of homotopy type theory which is more powerful came along.

00:34:29: but basic ideas are that we can have extensional structures and know how to compute with them.

00:34:39: so really avoid this intentional layer in a way.

00:34:44: We really talk about the homotopy type theory is actually much more extensional than traditional mathematics, it's super-extensional anyway and but its computationally well behaved.

00:35:01: so on the meta theory.

00:35:04: all computations are always computational very And that's what you just said.

00:35:10: This question of existence is addressed in, as you know I'm just in hot by the idea of a proposition.

00:35:24: so invite... So we have types and actually i think the beauty Of this modern type theory Is That We Don't Need The Notion For Proposition As A Primitive But the notion of a proposition is emergent.

00:35:42: It's a type which has no other information apart from it being inhabited, right?

00:35:47: And then that to me is very nice explanation both informally but also formally.

00:35:54: what as a proposition?

00:35:58: and okay so what does existence?

00:36:01: you already mentioned the sigma-type.

00:36:03: So if I say there exists number with certain property then the sigma type is a k of the number and its property, but this not a proposition so it has to be turned into a proposition.

00:36:16: So we have an operator which was called propositional truncation Which basically hides the element.

00:36:25: It's like you put the elements in black sacs.

00:36:28: You can only feel that there isn't any element But you cannot see color anymore.

00:36:39: Okay, maybe you should say something.

00:36:43: Yes there are many motivations and ideas that are similar.

00:36:49: in fact I'm looking forward to some PhD student or so not me unfortunately because my energy is limited.

00:36:59: That looks...that becomes familiar with both approaches homotopy type theory and minimally foundation, finds a way not necessarily rigorous to translate from one to the other.

00:37:20: Understand there are many ideas or better many motivations are similar.

00:37:27: my tendency is You mentioned the notion of proposition that can be expressed as a truncated type.

00:37:38: My tendency is to define them as primitive, because I feel the idea of Truncate Type To Be A Formal Way To Express A More Primitive Notion.

00:37:53: and then i say well We assume the more primitive notion.

00:37:58: The more primitive notions essentially is something that you can judge

00:38:02: through.

00:38:05: By the way, this was a difference between Martin Lake.

00:38:09: You know their proposition as sets principle that Propositions are can be thought of as set And the set is that of all its proofs and so on.

00:38:23: Or evidence?

00:38:26: I usually avoid the word proof, as a proposition given by notion of evidence.

00:38:33: What do i need to see to believe this proposition?

00:38:37: Anyway...I wrote notes over forty years ago trying to be faithful with what Per Martin left said, but I could not accept as natural this identification between sets and propositions.

00:39:02: The set N would be the proposition of having a natural number.

00:39:06: it's a bit...

00:39:07: Yeah!

00:39:08: But exactly that is actually fixed by this definition.

00:39:13: every proposition It corresponds to a type, but not every type is the proposition because a type may have more information like the choice of numbers.

00:39:24: But this exactly when I said that motivations and ideas are very similar.

00:39:31: it would be nice or actually to understand, because as far I know there are no papers written about this.

00:39:44: The connection... the strict connections between homotopytaic theory and minimalist foundation?

00:39:52: i'm not saying that one is better than the other!

00:39:54: I like the minimalist foundation because but not..I have a hard time with formalisms.

00:40:01: No!!

00:40:02: But that's the point!

00:40:03: Ha ha yes but for me okay.

00:40:07: Okay, I mean when i look at minimalist foundations to me it looks a bit formal because you have these levels layers and it's a bit hard to explain.

00:40:19: whereas...I would say type theory called as type theory not hot type theory is much simpler.

00:40:29: You only need the notion of a type yeah?

00:40:32: And then via everything else, right?

00:40:37: I mean as i said.

00:40:38: I explain propositions because what is a proposition?

00:40:42: A proposition is something that can have evidence for.

00:40:45: and thats the first idea yeah but then next one... But Thats all I Have!

00:40:52: There's no more to a proposition than its evidence.

00:40:56: And That´s in my mind expressed by this truncated definition.

00:41:05: Only one comment.

00:41:08: My way of understanding what is usually called the Minimalist Foundation, by the way The Minimalists Nation Is a formal system Of some attitude Sure And like all formal systems It can be A bit boring to learn or things like that.

00:41:25: The Attitude is As I as we said before of building everything from the bottom From ground up And so proposition is primitive, set is primitive and nothing else essentially.

00:41:42: You build everything from those.

00:41:46: if you look at papers then they were not written mostly only by myself.

00:41:54: there's the influence of other author to have an idea.

00:42:02: my way of looking at the minimalist foundation, The first chapter in this book is a very detailed discussion.

00:42:15: And it's less formal than what it looks by reading the papers.

00:42:21: Fair enough!

00:42:25: So let us look... I think you mentioned earlier as an axiom for unique choice.

00:42:32: Yes.

00:42:33: We have discussed axiom of choice, actually we even made the premise about the axiome of choice.

00:42:38: so maybe it's a good idea to explain what is an axioma of unique choice in particular because at least in Hort or this version type theory its not an axium and something that you can prove.

00:42:51: And what is the axio- of choice?

00:42:53: It has to remind for every x and A they exist Y & B such as certain relation holds.

00:43:02: then there exists a function for me to be, which maps elements related elements and the example of gloves.

00:43:11: You have to find matching gloves but unique choice gives you stronger precondition.

00:43:19: it says There exists a unique y, and how can you explain?

00:43:26: the unique y is just... You could encode it in predicate logic.

00:43:29: They exist a Y and all other things which have these properties are equal to this one.

00:43:34: but that's not difficult.

00:43:36: so if we had this premise that they exist an element But its'unique then I can't have function because there isn't really any choice anymore.

00:43:46: The elements already determined by their premise.

00:43:49: And just in Hort, this truncated setting I can realize that there's a sigma type if you have an A and it is the unique thing with its property.

00:44:03: This already semantically has a proposition because at most one element of it and hence the fact that exists as a truncation of sigma doesn't matter anymore in hard-formally extracts this function.

00:44:22: And especially if you think of mathematics, has some very important consequences for the mathematical practice because it restores that identification of functional relations and functions.

00:44:36: I mean... In type theory, functions are primitive and relations are something defined as functions into prop.

00:44:45: But using a unique choice, you get this alteration of... or you can say equivalence.

00:44:53: Fun from A to B is the same as relation which for any X exists in univariate blah-blah-bluh.

00:44:59: Perfect!

00:45:01: What you said.

00:45:02: I'm very glad that gave these little introduction because it perfectly constructed for me to start and explain my position.

00:45:16: When you said axiom of unique choice, uh You have a certain antecedent And the consequence?

00:45:26: The antecedents is...you Have For all x there exists only one y All x in A There exist Only One Y In B. Then you have a function from A To b. Now, I am not able to express it.

00:45:46: To analyze this in the framework of homotopy type theory.

00:45:53: but i will do that in the framework of martin lefthype theory.

00:45:57: But you'll understand how it works when moved into homotpy type theory.

00:46:04: In type theory if u have for all x in A there exist y in B. This is expressed by a pi and then a sigma.

00:46:22: The construction of sigma means that you already inside there have an algorithm to obtain the proofs of effect that, And this is what you extract to obtain consequence.

00:46:41: This is what we call the type theoretic axiom of choice.

00:46:45: If you have no truncation, then it's easily provable as you just explained right?

00:46:52: But this is not the axiome of choice that are scared off or which we try to avoid and which has been explained.

00:47:00: actually We had a premise on Diakonesco Which shows that an axioma of choice implies if through in middle.

00:47:08: So this version of the Axiom Of Choice is harmless.

00:47:11: It doesn't apply anything, it's provable in a type theory.

00:47:15: but the axiom of choice is exactly about this difference between sigma and exist because existence as a proposition.

00:47:27: so I cannot see the element

00:47:30: that's

00:47:31: in the black sac.

00:47:32: you know there are some elements i can not touch.

00:47:39: Sigma and exists, right?

00:47:41: And for exist if I say.

00:47:43: For all A's they existed B then i'm hiding the answer and there is no way uh...for me to restore The answer too.

00:47:54: get a function because it has two.

00:47:56: have to cheat the function.

00:47:58: as you see am never looking into this black sack but the functions secretly looks into it.

00:48:07: But as soon you know that there is only one solution, then you can return the color without cheating because...

00:48:18: Okay.

00:48:18: So I cannot object-I cannot discuss in these terms.

00:48:26: what do say?

00:48:27: Because i'm not familiar sufficiently with homotopy theory and the notion of truncated type.

00:48:37: but I am sure of the following thing there is a distinction in nature so to say between as you quite correctly said, between sigma and existence.

00:48:55: if to distinguish two notions of function.

00:49:01: A function where you have the instructions and a function, when you don't have the instruction to compute value then... You have difference!

00:49:12: If I play game with Bill he uses his own strategy And i use my own strategy.

00:49:23: I know that he will make move but I don't know the instructions to obtain that move.

00:49:29: Otherwise, the game is silly.

00:49:32: while i know The Instructions That i use To obtain my Move even if perhaps i'm not in the example it's Not computable.

00:49:42: It Is just intuition lot of things.

00:49:45: But i Know how i do and i Don't know How Bill Does.

00:49:51: But still I know that Bill will come with an outcome.

00:49:56: Even if i don't know what it is,I have no information on What It Is.

00:50:01: Now the main point is do we wish to keep this distinction or not?

00:50:07: My claim is That We need To Keep This Distinction because for instance a choice sequence is like The strategy of bill... I Don't Know Anything About it.

00:50:20: I simply see the outcomes.

00:50:23: So that is why i want to block the axiom of unique choice, uh...I'm not able to tell because I don't know enough what is to be blocked in homonthropy type theory To obtain it!

00:50:41: It's not provable.

00:50:44: We can think about this together but...

00:50:46: Yes yes That a good question.

00:50:49: Yeah, I agree that type theories obviously make certain simplifying assumptions and i think they are quite useful to do sort of mathematics.

00:51:04: There's question always how far we want go right?

00:51:09: We already left the classical domain and went to be intuitionists or constructivist.

00:51:15: but then it is a bit like vegetarian versus meat eater.

00:51:19: But then you can go further and become vegan.

00:51:24: I agree, so my

00:51:29: position...I don't have the metaphor with.

00:51:37: it's a bit risky with political parties or economic systems.

00:51:43: So my attitude is not to choose one political party, but to show how it works.

00:51:52: Looking at from above in an evolutionary way of looking I look what are the mechanisms by which things are constructed and so i see that certain axiomatization has aims, and I see that they work or not work.

00:52:17: In the specific case... ...I see that that axiomatization destroys a difference that I observe in reality And the difference is in the sense of general views.

00:52:30: Is what i care off.

00:52:33: it's not truth.

00:52:34: It is information.

00:52:36: I have the information about my own strategy.

00:52:41: I have no information about Bill's strategy and if you reason in terms of truth, You lose this because either mine is true or his is through Or what?

00:52:57: But it is immediately clear If your reason in Terms of Information that they really Have not theoretical information.

00:53:07: I have this information.

00:53:09: Shorty, since you mentioned that we had another appointment very soon and i wanted to give the opportunity is there like one other topic or in you would like to mention bring up else?

00:53:22: I couldn't ask a tiny question about topology to bring it back to our first?

00:53:28: no just follow your suggestions to promote reading my book.

00:53:41: You know that's definitely.

00:53:42: we can link it in the comments?

00:53:44: As I say, in the acknowledgments... ...I will thank the readers for giving me feedback on ideas I propose.

00:53:57: so i'm ready to discuss one by one with readers.

00:54:03: Yeah!

00:54:04: That is always good ideas.

00:54:06: you can comment here and we try to reply as much as possible.

00:54:10: And let me just very shortly ask, do challenged pair about put what does type two remains for practice?

00:54:19: Could you give an example of if I'm just a topologist then i look into your book.

00:54:24: is there something...I can turn out of it like the major theorem that's slightly different.

00:54:31: Oh yes, let's say so.

00:54:34: So we must be careful first that the distinction between me and Perr in mathematics is not the same as the distinction with me-between me and a standard topologist or mathematician.

00:54:48: In his case he tend His tendency was to do mathematics over intentional type theory And in my opinion, that is not the standard mathematics.

00:55:01: So a difference which is different from the differences between me and the standard mathematician One result of my approach was one very concrete result Which I found relatively recently Not in the nineties but two thousandths is that you can prove in the most rigorous, usual mathematical way.

00:55:34: That point-wise topology Is embedded in point free topology.

00:55:41: So Point Free Topology is more general than point wise topology and this proves In rigorous terms an expectation since The time of grotendic with the toposes.

00:55:58: The embedding I speak of is a special case for the generalization from topological spaces to toposes, but it's in that direction.

00:56:10: It has very precise theorem which one can prove.

00:56:17: The category of what they call concrete space is embedded categorically category of positive topologies.

00:56:28: And concrete spaces is an axiomatization basic intuitions.

00:56:56: I'm here, as you see i have been thinking about these things since ages... Since ever so to say!

00:57:04: So..I am ready to talk whenever you wish.

00:57:09: Yeah we can definitely eat again and think that will add a few repeated guests from now on.

00:57:15: but there are also some many traditions.

00:57:19: Okay yeah But thats then for the next time.

00:57:22: so our listeners thank you for tuning in.

00:57:25: Please write your comments and we really appreciate all the support.

00:57:30: And having said that, thank you once again Giovanni for joining us.

00:57:34: Thank you Giovanni it was very good!