aboutlogic #09 | Andrej Bauer – 5 Stages of Accepting Intuitionistic Math & Proofs by Contradiction

00:00:00: You know, people call me a constructivist and I say no.

00:00:02: No, not the constructivists.

00:00:03: you want to constructivism go look at Torsten that's a constructive.

00:00:06: is so because i think im more somehow more apolitical about this?

00:00:13: I sort of really like oh yeah okay you wanna do something in ZFC plus measurable cardinal interesting let see what it is!

00:00:20: I'm fine with this as well.

00:00:23: Im happy with cheating when its needed So no-no

00:00:27: See what I mean.

00:00:34: Yeah, welcome to About Logic.

00:00:37: I'm very happy with Andre Bauer from the University of Ljubljana who already know Hongtan.

00:00:46: and yeah let me just start.

00:00:49: you wrote a really cool paper about five stages.

00:00:56: how classical mathematics.

00:01:00: I think it was modeled on AA, Alcoholics Anonymous.

00:01:05: or is this correct?

00:01:07: No no so first of all hello.

00:01:11: thank you for having me here!

00:01:12: It's a pleasure.

00:01:13: i much enjoyed all the previous episodes.

00:01:16: So uh...I'm glad that ah..i can contribute to this one.

00:01:21: The paper five stages of accepting constructive mathematics grew out of several years, small observations about what people think about constructed mathematics.

00:01:33: But then really it grew out.

00:01:35: a talk I gave at IAS during the special year on Univalent Foundations... ...I give a talk in The Math Seminar with the same title and then i was approached by one of the editors to write it up as a paper and so I did that eventually.

00:02:00: So, It has nothing to do with Alcoholics Anonymous but The Five Stages Of course.

00:02:04: are these five stages accepting traumatic events in ones life right?

00:02:09: Denial Anger Yes, bargaining oppression and acceptance.

00:02:14: This is a psychological One of the psychological models how people deal with traumatic events in one's life, and I say at the beginning that this is suitable because learning constructive mathematics is a traumatic event.

00:02:34: Yeah actually which stage do you think most working mathematicians are?

00:02:39: Denial

00:02:40: obviously!

00:02:42: Yes so

00:02:44: denial is the stage where your just misinformed.

00:02:47: And if we believe false things about constructive mathematics

00:02:51: So maybe we can start helping there, the community.

00:02:55: What are like a few of these things?

00:02:58: people misinterpret or may be even step back.

00:03:01: what's... Like difference between classical and constructive math?

00:03:06: Well okay so first one is what is Constructive Mathematics?

00:03:09: And People say well Constructive mathematics is mathematics without excluded middle!

00:03:14: Then this Is The First Division Point where you Say Okay So you mean denial of excluded middle, and that's most definitely not what I mean.

00:03:26: A lot is going on can be compared to a similar situation say in algebra where you generalize the structure.

00:03:33: so imagine you have something like suppose study commutative groups.

00:03:39: And then...so groups with one operation an inverse-and-a operation is commutatives.

00:03:45: xy equals yx.

00:03:46: And then one day somebody comes by and says, oh I study non-commutative groups.

00:03:51: Then they say what is that?

00:03:52: It's just like groups but without the commutativity axiom right.

00:03:59: so... That doesn't mean that person thinks x times y is not equal to Y times X. They'll just say okay some groups are commutative Some groups are not commutitive.

00:04:08: i study all of them.

00:04:10: And so, constructive mathematics is also like that.

00:04:13: It's a generalization of classical mathematics.

00:04:15: it's not in opposition to classical mathematics... ...it's more general because it has fewer laws right?

00:04:23: So there are of course branches of constructive mathematics that sort-of make further commitments and become what we call anti-classical.. ..and thats'like studying specific group which most definitely isn't abelian of the square, something like that.

00:04:39: Yeah it's not commutative but in general Constructive Mathematics just says don't use this law.

00:04:48: and so when you say they don't us this law then suddenly your universe of possibilities is much wider.

00:04:55: therefore we would have to get used to this wider Universe Of Possibilities.

00:04:59: because were talking about foundations of mathematics its going feel a very profound change.

00:05:06: One feels a profound change if you start changing laws of reasoning versus just changing some axioms about some algebraic structure.

00:05:19: You say, oh yeah now it's just the different structure.

00:05:22: To my mind there isn't lot difference It is just the difference in scale.

00:05:25: So that' s first thing.

00:05:27: What is constructive math?

00:05:29: I think most basic one line definition Don t use excluded middle all time.

00:05:34: And here comes an important caveat, only use those instances of excluded middle that you can all prove by some other means.

00:05:41: So I think everybody should prove by induction that any two natural numbers are either equal or not equal and therefore That would be An example Of Any instance of exclude Middle at one can use right?

00:05:54: so that's how i Think it starts.

00:05:57: the second thing i Would mention is to give One more is what does it mean to prove something by contradiction?

00:06:05: Because there are really two kinds of proofs that mathematicians call proved-by-contradiction.

00:06:13: It's a habit in the informal mathematics, to call a proved-By-Contradiction any argument which reaches a contradiction... Any argument where you finish by saying and now this is impossible.

00:06:27: therefore we're done.

00:06:28: but if you look at is actually being proved, there are two cases.

00:06:33: One it's what usually called proof by contradiction which is not P implies P and the other one is P implies false Which is just not p. So now I think on Wikipedia.

00:06:48: i managed to change... There is proof by contradiction, where you approve P by assuming its negation and showing that leads to a contradiction.

00:07:00: That's the standard proof-by-contradiction.

00:07:03: The other one is just how you prove not p. So we've just proved not p by assuming p in reaching a contradiction And I would call it a refutation.

00:07:11: so if thats approved by refutation It may be better name for this.

00:07:15: Now whats very sad Is that a lot of mathematicians because they use same words to describe these two phenomena, therefore think that there are some statements in mathematics which are classical but not constructive.

00:07:29: So for instance the square root of two is irrational.

00:07:33: The usual proof is constructive because it's a proof by contradiction.

00:07:39: It just proves NOT something.

00:07:43: and you know There does not exist a rational number such as when squared equals two.

00:07:49: So that would be the first stage roughly, plus some other details about choice.

00:08:06: I

00:08:20: learned this while i tried to explain on various occasions what Constructive Math was and it kind of, you know It becomes amazing when you realize that You started explaining things at the wrong level because we first have To clear up This really basic misunderstanding Where?

00:08:38: its a logical error That people normally would not commit if Its were about A domain Of knowledge they're used too For instance.

00:08:46: These these same mathematicians are of course totally capable of logical reasoning, but Are quite...are far more secure in it.

00:08:55: like if they're geometers then They know exactly how to produce correct logical arguments and geometry.

00:09:03: But then If you go to an unfamiliar territory Then It's easy To get confused.

00:09:07: And In this case the unfamiliar Territory as absurd As it might seem is logic.

00:09:12: So what's interesting Is that Mathematicians can function really well without actually knowing much about logic.

00:09:18: I can drive a car, i have no idea how it works but i can drive the car and its bit like that.

00:09:23: they develop these internal intuitions.

00:09:25: But when it gets to formal logic then confusion may arise.

00:09:30: And um...i think is largely also just matter of education.

00:09:35: Yeah so im not sure its just formal logic isn't it?

00:09:38: Just being a little precise about your reasoning.

00:09:42: I mean, not necessarily being fully formal but...

00:09:45: Yeah that's a good point!

00:09:47: It is also about being able to reflect on your own thoughts.

00:09:53: like when you carry out an argument say square root two is irrational.

00:10:00: You carried it out and know what happened in the paper written in usual style.

00:10:05: And then i ask you did you use choice?

00:10:07: Then people get scared.

00:10:10: So they, it's hard to tell what kind of reasoning that actually was because that is not typically what you are trained in.

00:10:20: Again if your an analyst or algebraist and a geometer You're not going focus on What the logical form my proof?

00:10:29: It doesn't come into training but interestingly It can be important for algebra and it can be an important geometry to observe these kinds of phenomena.

00:10:42: Because everything is so interwoven, right?

00:10:46: I think that's a interesting observation.

00:10:49: like in linear algebra we have one moment where we point at choice when show you can extend any base or something like this And then never think about again.

00:11:03: I mean that's a famous example, right?

00:11:05: Where everybody is explicitly told about all Zorn's lemma.

00:11:09: All choice!

00:11:10: Right.

00:11:11: so thats the point where you're explicitly told it.

00:11:13: but there are these micro uses of choice which often unnecessary... ...where would have something silly like for every vector x let us choose real number r sub X blah-blah-blabla There was choice.

00:11:28: You made a choice because he said R sub X and even maybe without using the word to choose.

00:11:33: Oh, by the way it goes the other way right?

00:11:35: A lot of people think that if you have a set A And You know That It Contains an Element Then To Get An Element Of A Means That You Use The Axiom Of Choice

00:11:47: But That Is False.

00:11:49: If You Have A Set I Tell You Hey!

00:11:54: Its Inhabited Has Got An Element.

00:11:57: Let X Be Such An Element.

00:11:59: that's not a choice.

00:12:00: That is called existential quantified elimination, right?

00:12:03: And logicians of course would know these things.

00:12:06: but because I think it just really literally education like maybe you were told when he was an undergrad.

00:12:13: there are this rules of logic But you never see them used live.

00:12:19: nowadays Things are changing a little bit Because so many people See formal proofs in proof assistance.

00:12:25: So i think thats improving the situation.

00:12:28: Yes its true.

00:12:30: Can we maybe step a bit back and make sure that everybody knows what extra of choice is?

00:12:35: So, I mean...I think there's the usual story right.

00:12:38: if you have infinitely many drawers.

00:12:40: And each of them contains a pair of socks can use select sock from every drawer alright

00:12:47: Right.

00:12:48: so first of all it really doesn't have to be infinitely many It's arbitrarily many.

00:12:54: This important because without excluded middle even the instances of the axiom of choice which are not infinite become quite interesting and relevant.

00:13:06: And notice how I said, Not Infinite?

00:13:09: I did NOT say finite because that's different!

00:13:13: Yes right?

00:13:14: So things

00:13:14: happen.

00:13:15: okay so but yes for me The Axiom Of Choice um...the way i usually try to explain it.

00:13:25: If you're already classically trained, You are not going to see how it could possibly fail.

00:13:30: So this is the bargaining stage where you say Okay!

00:13:35: The bargaining stage Is I'm gonna tell a model Where that choice fails.

00:13:41: so at least imagine How it would fail.

00:13:44: We all know That choice is true because It's obvious.

00:13:48: But allow me like To Tell how it could fail with a little fantasy story, and that's one way to start to explain something people have hard time imagining.

00:14:01: It is quite similar as you can see in non-euclidean geometry where straight lines are actually circles.

00:14:19: Wait, wait.

00:14:22: Just imagine like entertain me humor me for a minute.

00:14:25: Let me show you it's cool.

00:14:26: I just say okay Okay?

00:14:28: I allow your straight lines to be circles.

00:14:30: So with choice You can do the same.

00:14:33: The only thing you say is i want all functions To Be Continuous.

00:14:38: Just Imagine every function has to be continuous.

00:14:40: Then Choice will immediately fail.

00:14:42: Because For instance we cannot choose For Every Real Number An integer that Is Larger Than It.

00:14:48: We Cannot Do That Anymore because you cannot do that continuously.

00:14:53: Because the only continuous maps from real numbers to discrete space of integers are constant functions.

00:15:00: So,

00:15:01: thats how we can imagine why choice would fail.

00:15:04: Now this is naive.

00:15:06: The picture is naive.

00:15:07: You cant just randomly go and say all functions are continuous.

00:15:10: It's more complicated than that But it´s doable.

00:15:13: There are models of constructive mathematics based on idea.

00:15:18: That expands your set up so that all functions are continuous and then choice will simply fail.

00:15:25: because you can't not.

00:15:26: Because, You know I as a classical mathematician don't know how to make choice.

00:15:31: It's because inside the model.

00:15:33: All choices have to be continuous but there are some.

00:15:37: There're some possibilities where you can do that continuously.

00:15:42: So you would use models two.

00:15:44: explain this Isn't it?

00:15:47: I mean isn't they unlike itself more naive conception where you could say, I mean that if your proof something exists... You're not exposing the actual choice.

00:16:03: Keep it hidden.

00:16:04: and it's sort of like a promise which will break in this moment when yourself are allowed to look into it.

00:16:10: but i guess there is more type theory explanation

00:16:13: kind-of thing?

00:16:19: who understands what abstraction of data types is.

00:16:25: A classically trained mathematician does not know these concepts, they don't know what that means.

00:16:31: They no abstraction in different forms but not the one you're alluding to.

00:16:37: That helps explain What it mean to hide a witness Because so-to speak In ordinary mathematics everything's visible All the time.

00:16:46: Yeah, which is not a feature actually.

00:16:49: It's a bug I think.

00:16:51: Well you know

00:16:52: It can be

00:16:54: okay it's the choice its design and

00:17:00: Can A maybe good?

00:17:02: Maybe i'm just going back to denial.

00:17:04: i'm raised classically And this story of generalization Is in some sense clearly true.

00:17:09: um i mean it's more general.

00:17:11: You can but it's totally easy To have like an.

00:17:16: if then picture Just put the missing thing back and you get exactly the same think-back again.

00:17:23: And I mean, we already mentioned there are some positive results so to speak.

00:17:28: that look very weird if your grown up classically.

00:17:32: So it's maybe one example where can help getting over this weirdly looking.

00:17:39: things like the difference between not infinite and finite could be something a classical satirist would find a little weird to hear that there are finite sets with infinite subsets.

00:17:52: Something like this, is their trick to get over?

00:17:55: Yes so the first thing I will say.

00:17:58: you already committed your error as classical mathematician.

00:18:09: There is a difference between infinite set and not-infinite set, which you immediately optimize to infinite versus finite.

00:18:18: So constructive mathematics... Let me be careful!

00:18:23: Okay so there are models of constructive mathematics where weird things happen regarding finite in infinite sets.

00:18:32: but constructive mathematics in general because it's a generalization can never prove anything that is inconsistent with classical mathematics.

00:18:44: If you take Bishop's book on constructive mathematics, every single thing in there is classically valid.

00:18:52: so I think it's important to distinguish these two things and we could go back the groups right?

00:18:57: There will be.

00:18:58: if your only use of commutative group You'll find non-commutative groups really weird at first.

00:19:05: but general theory cannot possibly prove anything that you will be surprised by, because whatever you can prove using the basic axioms of for a group.

00:19:15: You can also prove using The Basic Axioms plus Commutativity-you just didn't use commutativity.

00:19:20: So it's exactly the same.

00:19:22: so what happens is that?

00:19:23: You can't prove certain things.

00:19:26: For instance I cannot prove That a finite subset over finite set sorry i cannot prove the statement every subset Of A Finite Set Is finite.

00:19:35: That is not provable constructively.

00:19:38: You should NOT jump to the conclusion that, therefore... The opposite holds!

00:19:43: Right?

00:19:47: So I think THAT takes some getting used too Which surprises me a little because at some level mathematicians know perfectly well this case.

00:19:58: For instance they would never say Because we can't prove this theorem.

00:20:03: Therefore it's opposites.

00:20:04: true They will NEVER say that.

00:20:06: But this is exactly the kind of problem that you see.

00:20:10: Oh, You can't prove that subsets or finite sets are finite!

00:20:15: This is just so strange.

00:20:16: how could it be?

00:20:17: Where's your infinite subset over a finite set?

00:20:19: No no I just couldn't prove.

00:20:21: in some models It will fail.

00:20:26: and also by the way... ...you cannot find an infinite subset of finite sets.

00:20:29: That was false to presume.

00:20:33: we have that.

00:20:37: But my favorite example is actually excluded middle itself, because people think okay you cannot prove excluded middle.

00:20:43: Hence we should be able to prove the negation of the excluded middle.

00:20:47: but obviously it can not be that the excluded Middle is false right?

00:20:55: Right!

00:20:55: The negations of excluded middle are refutable constructively and I'm going to...I mean i am gonna be very boring.

00:21:06: the kind of thing with groups.

00:21:08: You can go keep going back to groups, just keep thinking about what happens when you have groups with and without commutativity right?

00:21:15: So... With commutativity.. Of course!

00:21:18: ...you can prove that every group is commutative.

00:21:20: Now I take away the commutativity axiom.

00:21:23: Can you prove all groups are commutitive?

00:21:25: No Because we don't have a commutitivty axioms And there's some groups not commutatives.

00:21:32: You can prove that all groups are non-commutative.

00:21:35: No, of course not!

00:21:38: It's just where the negation is right?

00:21:45: We should probably try to move away from these basics.

00:21:48: this is just a denial state

00:21:51: Yes but I would like to go back to us and relate those two principles we have mentioned.

00:21:58: so you talked about exclusive middle and choice.

00:22:01: So, can you explain why choice excluded implies excluded middle?

00:22:07: That's a rather famous theorem by Diakonescu.

00:22:10: And what to do is apply choice... ...to family of sets that has finitely many elements.

00:22:20: so it's choice applied as family of inhabited set with finite family.

00:22:27: The trouble in order make the choice you kind of have to know whether it's one or two members of the family.

00:22:34: The two members are defined in such a way that if one possibility holds, then... It's gonna really be the same set twice and if there is another possibility its going to be different sets.

00:22:45: And If You Could Make A Choice, you could implicitly make this difference.

00:22:49: Things Are Set Up In A Nice Way.

00:22:52: Maybe This Is Not The Right Moment To Try To Explain The Proof But The Interesting Thing Here Is That Its Choice applied to a very small family of sets.

00:23:03: It's, it is a family of set which has an element A and B but you cannot decide whether A or B are equal.

00:23:18: Thank You very much!

00:23:19: But on the other hand in another direction.

00:23:21: so if middle doesn't imply choice can say something about this.

00:23:29: That's, I think every set theorist knows about the difference between ZF and ZFC.

00:23:36: Right?

00:23:37: ZF is classical set theory with choice And we understand very well that there's a difference between... Classical

00:23:43: logic doesn't imply the choice.

00:23:47: Let me just repeat We had it in another episode but interestingly those are equiconsistent even for the classical mathematician.

00:23:55: so There was like nothing problem coming in from choice,

00:24:01: but I mean if yeah also it is known that broadly speaking constructive and classical mathematics are equi-consistent.

00:24:11: for some reasonable notion of equiconsistence.

00:24:13: We have to be a little bit careful how we say it.

00:24:15: But certainly not the case.

00:24:17: one's problematic while other ones aren't either both problematic or they're both unproblematic

00:24:27: to the later stages, so how do you get away from denial or maybe even way from bargaining?

00:24:34: Well I think... So first i would say that one needs to have sufficient motivation.

00:24:42: To this kind of thing because it's a heavy investment mental investment intellectual investment to try to learn.

00:24:49: It is almost like learning new branch of mathematics and people don't normally once they are sufficiently far up their career and they have specialized, invested so many years in studying something very deeply studying a topic now that is starting to do something else.

00:25:07: So first I think you need sufficient motivation And of course it helps if your young.

00:25:14: But after how to do this?

00:25:19: I've seen two ways.

00:25:22: One is really true models, so that helped me.

00:25:25: I learned my constructive maths by studying realizability models and then later on also Sheaf models And i'm a lot shakier.

00:25:37: My intuition works not-so well for sheaf models.

00:25:40: It works much better for realizablity models but... ...I find sheep models even just as respectable & important.

00:25:47: So one is through models and you might be studying these models because they're interested in some particular model that you care about.

00:25:54: Because it's your kind of math, I don't know... Some schemes or something?

00:25:58: And then there are some topos, growth-and-dictopos.

00:26:01: It's internal language which is intuitionistic.

00:26:04: Then somebody shows us how to do strange things with the internal language so we can keep translating everything like, oh what does this say in the model?

00:26:14: What is they saying to model?

00:26:16: and that's how you can develop your intuition.

00:26:19: So I think it's more of maybe i should say This It's about developing The correct kind of intuition.

00:26:24: so mathematicians most definitely Develop a strong intuition About their subjects They study.

00:26:30: And uh...it's-It's about Developing A new Kind Of Intuition About What-What Logical Statements Are About That.

00:26:37: one way..The other Way that I have seen Is just people, this is more computer science-y.

00:26:44: People just sort of plunge into some proof assistant and start doing things event because the proof assistant is intuitionistic.

00:26:51: say you're in Agda Torsten's favorite proof assistant.

00:26:57: And then... You are in Agdha trying to prove excluded middle.

00:27:01: Then they stare at it saying there was nothing I could do here.

00:27:04: This kind of small logical error that you commit Is oh i can't prove this Right?

00:27:11: So, well actually it's not a logical ever.

00:27:15: You're trying to convince yourself that you can't prove excluded middle.

00:27:18: right but you've been trained to believe that Exclued Middle is true.

00:27:22: so you find very hard To have mental picture of how its'nt true.

00:27:26: and then Agda Can help because you cant do in Agda.

00:27:30: And it super obvious that you cant Do It In Agda Because you go try to do it.

00:27:35: just get stuck.

00:27:36: There's nothing I could do here.

00:27:38: there.

00:27:38: no way i'm gonna Prove this.

00:27:40: And so you start playing this little game with Agda, where you can do things.

00:27:44: You cannot do things every once in a while.

00:27:46: Torsten shows us some totally unexpected thing that you can't do which you thought wasn't possible.

00:27:53: That's cool right and then eventually you develop an intuition.

00:27:57: I have seen this happen also.

00:27:59: Actually one line actually i'm teaching also Lean.

00:28:05: This is for big class of students.

00:28:08: And what do I always say?

00:28:11: I start with introducing logic, which is actually institutionistic.

00:28:14: I just call it logic and then move on to give them classical principles.

00:28:21: To make the difference clear we've seen so far as the logic of evidence in the sense of truth tables In my counter example if you know that i don't have dogs or cats Obviously, you don't have evidence that I do not have dogs.

00:28:45: And if there is no evidence then it's cats.

00:28:48: There is a difference between the true interpretation of these statements and the evidentian interpretation.

00:28:54: That's my line!

00:28:58: I think Thorsten is touching on an important way to explain constructive math which is this idea of evidence, something else, for instance there will be models where evidence means is an infinite sequence of integers.

00:29:37: The Clinivacelitopos.

00:29:39: so they'll have different kinds.

00:29:43: but this evidence always obeys certain general laws that are used to precisely correspond to inference rules.

00:29:53: To give evidence of A and B you need a pair of evidences And the evidence of an implication is a method that takes evidences A and converts it to evidences B. But now we have these undefined terms, Evidence, Method... but It doesn't matter!

00:30:12: Those are primitive notions just like Set is a primitive notion in SetDuty and PointLine is a PrimitiveNotion In Geometry.

00:30:19: Here at this level Evidence and Method might be Primitive Notions.

00:30:23: We know what their basic behavior is supposed To Be and then anything that has that kind of behavior will be happy with.

00:30:32: So I think, it's also a very good way.

00:30:35: you touched upon this idea the difference between truth and evidence.

00:30:39: And That is also a really good way to explain things because It tells us not just when we stare at something like A or B classical mathematics about some particular statement like A or B that one would say, oh it's true and the other one will say false.

00:31:02: It is not that they disagree.

00:31:04: They cannot disagree because constructive mathematics are a generalization of Classical Mathematics-they'll never disagree.

00:31:11: What is different?

00:31:12: Is how you read and understand The meaning Of word OR.

00:31:16: That may be most important thing to realize.

00:31:20: Or means something else now what it usually means in classical mathematics.

00:31:26: Its meaning has been changed purposely, right?

00:31:30: So that's also one way to understand it and the students will see this very clearly.

00:31:40: if they stare at a definition of OR They'll say... If you look at the definition of or It is the constructive one.

00:31:51: Actually if we go back, I had this discussion here recently and because you talked about models.

00:31:58: So Here's the question.

00:32:00: We know that certain choice principles can be justified constructively.

00:32:04: so one of them is countable choice.

00:32:07: It's a translation off all those statements Which explains countable chose.

00:32:13: whenever we prove something with countable choose?

00:32:15: You can translate it into proof avoiding and into a constructive pool, right?

00:32:20: It's the set to eat interpretation.

00:32:23: But then people tell me yeah but they are models.

00:32:26: actually these are chief models where countable choice doesn't hold.

00:32:30: so I'm saying yes why does it matter?

00:32:33: as long as i have a constructor explanation that should be fine using or not accepted?

00:32:43: because there

00:32:47: Oh, you know Thorsten is Thorsten.

00:32:49: You're my favorite constructivist Because when you explain constructive mathematics nobody has the aura of that.

00:32:55: it's quite so bright When you explain it.

00:32:58: So I think this is a very good example.

00:33:01: Why would you care about the models?

00:33:03: That you don't care about right?

00:33:05: Is that your question?

00:33:07: Yeah

00:33:08: Okay but isn't that...I mean thats just like That exactly what classical mathematicians are gonna tell YOU when you try to explain constructed math, they're gonna say why would we care about this?

00:33:19: You know...you are living some strange model.

00:33:21: who cares.

00:33:22: So this is the bargaining kick right This-this is..This Is The Bargaining Stage where he tried put the crazy people inside a Model!

00:33:30: He said I don't Care About Them.

00:33:32: They can be in that Sheath Model Where Choice Fails.

00:33:35: i Don't Care about it.

00:33:36: But what I think the next stage after That is no excuse me but It's unavoidable.

00:33:42: Right there so many theorems in Mathematics.

00:33:44: Let's Say There are lots of theorems in logic, which say there will always be unintended models.

00:33:53: Whatever you try to do... You had your favorite model and tried to describe it but failed!

00:34:00: The lesson there is that the universe or the multiverse, it's telling us something.

00:34:23: It's telling as we are all here.

00:34:25: why do you think one of them special?

00:34:28: I don't think they're right.

00:34:29: You have to get up and sort-of come into terms with a fact That will always be these unexpected models And at least for me personally thats extremely beautiful So rich, there's so much of everything will never run out of this amazing exploration.

00:34:46: If you care to look for it... ...you might find something very interesting.

00:34:50: Now in a more limited context like if your computer science is in nature then You may be able to deny the importance of chief models But as we know well that you cannot really do That right?

00:35:06: It just different kinds shoes?

00:35:08: Yeah,

00:35:10: maybe.

00:35:12: I mean okay.

00:35:12: so in one sense anything which i can prove... Okay you can proof something with choice but you cannot prove it without choice because that's really non-constructive.

00:35:23: But if you proved something was countable choice then you can translate and have a constructive proof Which doesn't use countable choices.

00:35:33: So on the very pragmatic point of view Something like countable is less harmful than general choice, right?

00:35:42: It's very harmful from the point of models but that depends a bit what I'm doing.

00:35:48: I

00:35:49: am a little confused because i thought... Ah yes okay so have you ever done deeper into asking why is it that the countable choice works in statuettes ?

00:36:01: Yes of

00:36:05: the natural numbers.

00:36:09: So, if you make a choice over a trivial set then... ...you can always extract the choice function.

00:36:21: It's a bit cheating but it is a cheating which you can justify by having this translation.

00:36:27: Yes!

00:36:30: Category theoretically would say the national numbers are a projective in them.

00:36:35: Exactly set it model right?

00:36:37: So, In this sense your sweat I took to my mind you're just doing a model theory.

00:36:41: Right You were saying oh there's a model and which choice happens to hold?

00:36:45: i like that model or am happy?

00:36:47: Yeah but so good model is still constructive.

00:36:53: When we looked at heart We knew that constructive explanation of the univalence principle, right?

00:37:00: And this was found by exposing a particular model as a cubicle model.

00:37:04: Right and hence we had constructive understanding Of Univalence.

00:37:11: now if you ask me is there a constructive understanding of countable choice I say yeah because We have this Constructive Model which can use it as translation Which translates everything into into something which is acceptable even if you.

00:37:30: firstly, I don't like a countable choice.

00:37:32: But have you asked yourself whether or not there's any constructive explanation of how the choice can fail?

00:37:37: Because the chief model that shows us how choices can be failed are also constructive!

00:37:43: You're right.

00:37:44: but in this case...I mean i prove some things Like.

00:37:49: I want to prove that the kushi reels are same as hot reels And I use countable choice and that's cool, so it means the cushy deals are maybe not as problematic.

00:38:03: As people think...

00:38:05: No no what I'm arguing about is fact you like a certain thing because there has to be constructive explanation.

00:38:15: but there have been further reason why i liked this idea.

00:38:19: otherwise you would also like the constructive explanation of how choice fails.

00:38:24: Right, and in this case is because I have a proof there.

00:38:28: And would like to use countable choice right?

00:38:31: I want you'd like to do front of the choice to prove that Cushy reels are pushy complete nice and All I need here is countable shows.

00:38:39: and now you say oh but it's not constructive.

00:38:42: by I see okay But look II can give if translation office argument using the fact said they have such constructive model.

00:38:52: Sure.

00:38:52: What I would say is that there's here something where we see how a model can be used in a very nice way.

00:39:02: to explain what essentially about computation, because i think what were discussing was How are you going implement real numbers?

00:39:09: And let us implement the real number as sequences of rational approximations, Cauchy sequences and then ok but how do know this?

00:39:19: okay Don't you have a problem with countable choice?

00:39:22: And what I think your argument is showing, no.

00:39:24: I'm not going to have a problems with the countable choices because i know exactly that my computation's gonna work out nicely.

00:39:31: So in this sense yes, I completely agree.

00:39:38: I think we haven't made it all five stages so eventually We need to re-advide anyway.

00:39:44: But maybe let me just ask Marioopolis there any other Topic you would like to speak about a project.

00:39:51: You're working on because your paper I mean well being very influential It's also little old and it still Has some impact, but is there anything?

00:40:00: You would like To speak about in the last five minutes?

00:40:03: um i don't know if you guys think its better.

00:40:05: If you have any more questions you ask me for five minutes.

00:40:09: Yes Can I still sorry.

00:40:10: another question Because i always liked too i mean we i think We agree On constructive mathematics which is a bit like being vegetarian, I feel always.

00:40:22: But it turns out that i'm actually vegan because... ...I don't accept the type of propositions as small just called predicate reasoning and maybe you can convince me why impredicativity is okay?

00:40:42: That's very nice question!

00:40:44: So my first reaction was So maybe just for the viewers, what we're discussing here is whether... We are essentially discussing the question of whether there exists a complete lattice.

00:41:00: Is there non-trivial lattice that has all Suprema?

00:41:04: Because that's Supreema indexed by anything at all!

00:41:10: If soon as you have one such non-Trivial Lattice then the type of propositions form such a lattice because it's going to appear inside the larger one, the non-trivial one.

00:41:21: And so this is the same question.

00:41:23: So the question is can we ever hope to calculate arbitrary Suprema of anything other than in the trivial cases?

00:41:30: and so We know from a foundational point of view that This can potentially give you a lot additional power In what you can create and generate.

00:41:39: What kinds of objects exist?

00:41:41: I mean for starters complete lattices start to exist But also it has other implications.

00:41:49: So my first reaction is that It's a bit like constructive mathematics for lazy people, because it's so much easier sometimes to work with impregnative propositions.

00:42:07: Write down your predicates, take arbitrary...

00:42:09: It's easier to work with choice as well.

00:42:12: Yeah!

00:42:13: Of course I completely realized that i'm on slippery slope here because then it is even easier just assume false but thats the easiest thing

00:42:22: in the

00:42:23: world.

00:42:24: So you have to be careful.

00:42:27: There are a wide range of relevant models called toposys which are sufficiently rich and sufficiently important that maybe we should know how unpredictability works.

00:42:41: In realizability, you see that unpredictability kind of is in a way completely orthogonal to computation.

00:42:47: It doesn't influence computation so it's harmless.

00:42:53: So there are reasons why you can say that unpredictativity isn't going to hurt any concrete computation That might be tempted.

00:43:01: What will do?

00:43:02: It will reassure you, for instance maybe that certain computations are terminating and without it.

00:43:08: Maybe You would have a problem knowing they'll be terminating something like this But its not ever going to show up in concrete results.

00:43:17: Its never the case That within predicativity you're gonna calculate some number is two And without it your gonna calculate three.

00:43:25: Thats not gonna happen.

00:43:28: Now again, because predicativity is a generalization of unpredictability.

00:43:32: So it can never disagree one way or the other.

00:43:36: so I don't know.

00:43:37: um i have uh...I think its ideal if you can.

00:43:42: It's ideal that we prove everything also predictatively If possible.

00:43:46: but some topics We dont'know really well how to do them predictively and so I would say thats You Know A challenge!

00:43:54: Its a challenger How To Do Those Topics.

00:43:58: Yes, I think it's very complicated.

00:44:01: I mean, Pierre-Martin Leuph once said that he thought the only way to justify impredicativity is classical reasoning.

00:44:14: Why is pop small?

00:44:15: or if pop was equal to bull?

00:44:17: It must be small... Right!

00:44:20: It could have been small but not equal to a bull

00:44:22: right?!

00:44:23: No no boy.. But the question is, it's just a philosophical way to justify that impredicativity.

00:44:35: The argument I mean in predictivity is consistent as you said... ...the argument would go via consistency of classical logic right?

00:44:44: Because classical logic is consistent since impredictability is consistent!

00:44:48: Now

00:44:49: again

00:44:50: how are we going to get- You don't necessarily This depends on the technical details, but you might well have excluded middle without impredicativity.

00:45:01: That's true.

00:45:02: what I meant is actually this version where we say prop equals bool.

00:45:07: Right right okay so that's just a very crude way.

00:45:10: But sorry even if you say prop equal bool Okay If You Say Prop Equals Bool and Excluded Middle Yes Then Showed It Your Home Yeah Yeah, well.

00:45:25: Okay sure yes I mean that's kind of probably not a very nice way to try To Try to justify these things?

00:45:34: I think for me if it tried to justify impredicativity i would probably look For.

00:45:39: I Would first try to Look at models and say Well It's naturally arising in many contexts so its worth studying.

00:45:45: yeah

00:45:46: Sure I'm not saying someone was Studying everything just saying that not clear how it's intuitively justified.

00:45:57: Right, right?

00:45:58: I think there may be one of the differences between your... How you understand.

00:46:04: like people call me a constructivist and then say no-no i'm NOT a constructiivist.

00:46:10: You want to constructivists.

00:46:11: go look at Thorsten That's a constructitvist.

00:46:14: So because I think So somehow more apolitical about this.

00:46:20: I sort of really like, oh yeah okay you want to do something in ZFC plus measurable cardinal.

00:46:26: interesting let's see what it is?

00:46:27: You know... Yeah

00:46:28: i'm fine with that as well!

00:46:31: I am happy with cheating when its needed.

00:46:33: so no-no..

00:46:35: See what I

00:46:35: mean?!

00:46:39: But it's interesting how many discussions here point to pluralistic themes rather recent movement, if we think how into a cynistic and classical mathematics used to hate each other in the beginning stages.

00:46:55: And really try to get rid

00:47:05: of animosity between two particular people.

00:47:10: That originated from something that essentially wasn't mathematics and so on, let's not get into it.

00:47:15: I would just like to make maybe sort of a kind of final thought here because we probably have to finish soon.

00:47:20: You said pluralism.

00:47:21: what i think is quite important Is not just pluralism.

00:47:25: Pluralism will mean Let's respect the fact everybody does their own kinds of Mathematics.

00:47:35: I think what you need is... You also needs to study the overall, again sort of lift yourself one level up and understand the connections.

00:47:43: And maybe call this relativism because in relativity they calculate What Is The Relationship Between Different Observers?

00:47:51: And i think Also here it would be extremely important To Understand These Connections!

00:47:57: People do study that.

00:47:57: Of course It's an obvious thing.

00:48:00: But as a matter of philosophy or propaganda you know, yes pluralism is good.

00:48:06: You get a richer multiverse of mathematics but somebody should also study the multiverse itself not just pick up place to live and have little garden there.

00:48:16: never look on other side.

00:48:17: that's

00:48:18: true great.

00:48:20: so last thing we should thank again for your time.

00:48:25: next steps comment and maybe we can find some discussions.

00:48:36: And at some point, I really hope there will be a paper saying hey this podcast brought me to the theme.

00:48:41: that's why i found a philosophical justification for X or work on this theory.

00:48:48: but thats mainly for future.

00:48:50: so again thank you

00:48:52: bye-bye.