aboutlogic: premises #08 | Choice vs. Excluded Middle: A Constructive Paradox

00:00:00: The maximum of choice is sort-of a form of magic, right?

00:00:03: And the clue in middle there's another form of Magic.

00:00:05: And we also have seen that from constructive point of view one form of Magick implies other forms of Magic.

00:00:16: Hello everybody!

00:00:17: Welcome to another episode of our premises series and if you wanted stay set very relevant for awhile because last two episodes were about it.

00:00:28: this time I want talk with into a sonistic set theory, something that puzzled me for quite awhile.

00:00:39: And that is that constructive sets theories don't like choice but it feels so constructive right?

00:00:45: If you construct really everything You can also pick an element out of it But that's not the dominant view.

00:00:53: So could you illuminate me little bit there?

00:00:56: Yeah to just correct I mean i think my explanation Is based on type theory my understanding of choice.

00:01:08: You can express it, I think very nicely in type CLA.

00:01:12: so and then wanted to talk about give a bit of an intuitive explanation off the action of choice?

00:01:22: And then I want to... Yeah!

00:01:26: Talk about one of my favorite proofs.

00:01:29: It's approved by guy called Dia Kunescu.

00:01:32: I think it must be from Georgia.

00:01:36: And he showed that the axiom of choice implies excluded middle, so an exclude middle is a principle for every proposition.

00:01:45: we know P or not P and the axion of choice.

00:01:48: i will explain in detail if thats okay?

00:01:55: Dennis will ask questions.

00:02:01: Sure, I

00:02:03: will do my best to

00:02:04: not

00:02:04: understand everything and ask for.

00:02:07: Okay so here's my version of the Axiom Of Choice.

00:02:11: Uh...I think okay let say we have two types or sets A & B lets' see.

00:02:16: And if you have a relation between them And uh..so ok Let me be concrete.

00:02:22: So A is left gloves gloves and B is right gloves.

00:02:28: The relation that they match has same color.

00:02:32: So, and now I know that for every left glove there is a right glove with the matching color.

00:02:38: because when i buy the gloves.

00:02:41: I always buy them in pairs yeah so I know For Every Left Glove There Is A Right Glove With The Matching Color.

00:02:48: And The Action Of Choice In The Type Stereotypical Version Tells Me Now That It's A Function From Left Gloves To Right Gloves Which For Every left Glove Returns A Red Glove of a Matching Colour.

00:03:02: So functions are to me something which I can actually so run.

00:03:07: The problem is if i buy all my gloves and put them in a big pile, then here's the left...I pull out that left glove And now there it´s the whole pile of right gloves You have to find a matching one, those are function or fines one by magic.

00:03:28: As long as the pile of gloves is fine, that's okay because you just go through all the gloves until you find one.

00:03:33: And here it is which actually related to the fact that the finite version of the XOR of choice is constructively valid and cause this goes through.

00:03:43: but if you have infinitely many gloves Which can easily happen If its a cold winter then You never will find the matching glove if you cannot.

00:03:58: And then the axiom of trial sustain, yeah?

00:04:00: No we can always find it okay.

00:04:05: so

00:04:07: that sounds pretty similar to this.

00:04:09: set your magic version I would say

00:04:13: or even type theory.

00:04:15: You Can Reduce It To A Principle That Infinite Products Commute This Trication Which Is More Like The Way it's presented in that theory.

00:04:28: But I think for me this, if you have for all exists then they exist.

00:04:34: the function that i find intuitively so thing which is most easy to understand.

00:04:44: okay maybe just stick for one second.

00:04:47: there are whole books listing things equivalent to the axiom of choice given.

00:04:55: And I think, there is a lot of convincing and cheating in both.

00:05:01: If i think about this version the infinite product of non-empty sets as Non-Empty.

00:05:08: it sounds so obvious.

00:05:10: that should definitely be true!

00:05:12: On the other hand There's always function that picks out something.

00:05:16: That sounds more cheaty.

00:05:19: We shortly spoke with Joel Hamkins In our episode on another reformulation I think where different histories could have happened and some of these four versions are more convincing than others.

00:05:34: But the devil is in detail, right?

00:05:36: The mere notion of infinite product may be one that makes sense if you already assume choice but that's progester.

00:05:45: Yes so this version for all exists.

00:05:49: then there exist.

00:05:50: a function somehow sticks with me intuitively most easy to understand, obviously it's equivalent.

00:05:59: To these other principles and for example in type theory I already said which is a z-theoretic version if you merely know that there is an element of infinite product then you have the infinite product.

00:06:16: over some truncations There is this infinite product version and it's not hard to see that what I just said, is reducible.

00:06:32: In hot you would say the infinite products a Pi type commutes with truncation.

00:06:42: And then turns out to be equivalent not necessarily for a mathematical equivalent notion, but one which is best or at least works best for me.

00:07:01: For my intuition.

00:07:02: I don't know that different people have different intuitions and this for all exists.

00:07:07: so they exist to function.

00:07:09: it's the choice functions as well of the axiom of choice.

00:07:21: But as I just, let's look at it in action and see how we can prove excluded middle which seems to be quite different.

00:07:31: so P or not?

00:07:32: p for every proposition yeah you know either P or NOTP.

00:07:38: that doesn't seem first-of all directly related.

00:07:44: And here is Diakonesco's proof.

00:07:49: So we start with the idea of a set of booleans.

00:07:56: Okay, here by set off I mean predicate on boolean.

00:08:00: so in types we have function from bool to prop and actually in leans is called set.

00:08:09: SetOfBool() is the same as bool function for bool type of propositions.

00:08:15: So it's a set of booleans.

00:08:16: It is not necessarily decidable, I mean you may know whether the Boolean is in or not

00:08:23: and however... Otherwise we would decide everything right?

00:08:25: This will

00:08:26: be quite powerful.

00:08:27: Yeah!

00:08:28: We can have ... A decidable set of Boole as function from Bool to Boole for every Boolean tells us yes or no but here for every boolean gives your proposition.

00:08:37: Proposition if you don't know could something very difficult that we can prove.

00:08:43: The proposition is something we may be able to prove, but if you don't know whether or not it can prove its negation.

00:08:50: We have a set of booleans and we know that the boolean exists such as predicate holes such a predicate whole.

00:09:12: So the type I'm looking at is the type of inhabited sets of Booleans and it's an effect that they exist in element, first of all doesn't really give me an element if just gives you this information.

00:09:28: there is one but i don't know which one right?

00:09:30: It could be true or false we do not know.

00:09:33: so the habitat set of Boolean could also both.

00:09:38: doesn't give us any information about the witness of this inhabitance is hidden in this existential statement.

00:09:47: Okay, and now the relation is actually, that's a predicate I have holds for this Boolean.

00:10:14: So so i relate non-empty sets of booleans to a Boolean and I know that for every non empty set there exists the Boolean which satisfies it.

00:10:26: That's the premise.

00:10:35: Tangle out the details for one second, just because sometimes we might think about different notions slightly differently.

00:10:42: So a proposition wouldn't be... what would be in proposition and constructive mindset?

00:10:51: A proposition is something you may able to prove.

00:10:54: And Boolean

00:10:58: has type with two elements or set was two elements true and false.

00:11:04: Okay exactly.

00:11:05: And in classical

00:11:08: math, one would say... If you have a predicate like predicate on Booleans as the function from bool to prop then You may be able to prove that two is in it or maybe able to proofs its forces but you don't know.

00:11:23: But if we have a functional for bool-to-bool Then he just put an embodian and your look and says true of force.

00:11:29: so

00:11:31: I mean this somehow different for the classical mathematician, right?

00:11:35: Frege would have said.

00:11:37: The proposition is either zero or one.

00:11:39: maybe I don't know but it is so to speak.

00:11:43: and here's a picture slightly more complexed.

00:11:45: The Goldbach conjecture really isn't zero-it isn't one... It's whatever it is.. That's

00:11:53: a proposition!

00:11:58: Okay let's go back.

00:12:03: Inhabited sets, no this word set is very overloaded.

00:12:07: Inherited predicates of Booleans and Booleans.

00:12:13: And I know for every inhabited set of Boolean there exists a Boolean so that the predicate applies to it.

00:12:19: This obvious I mean just because its inhabited.

00:12:24: But the actual choice now gives me a function.

00:12:27: It give's me a Function from any inhabited set Of Boolean To A Boolean.

00:12:33: So all of a sudden, I can see the boolean which was previously hidden.

00:12:39: Yeah?

00:12:39: And we know that i couldn't access it.

00:12:41: but the action of choice now tells me oh yeah give me an inhabited set of Boolean and I reveal the Boolean Which really was hidden.

00:12:52: this exist statement is like in type theory hides The identity Of the culprit.

00:13:01: So it doesn't give away.

00:13:03: But now the axiom of choice is no, but I can see it here as... The axiome of choice sort of basically letting me look into this existence.

00:13:17: and okay so now Diakonesco realized that already there's enough to prove excellent middle.

00:13:28: And the trick is this.

00:13:29: Okay, let's say we have a proposition p could be gold post convection and We want to prove P or not P. so to do this?

00:13:38: We define two Inhabited sets of Booleans.

00:13:43: well that's that's the trick.

00:13:44: it some main technical device.

00:13:47: So let's see cousin u in v through you Is is always contains zero.

00:13:55: But if p holds then its obvious true.

00:13:59: So it's either zero or P, so the predicate always true for zero but its true everywhere if P holds.

00:14:13: And second predicate V is ALWAYS TRUE FOR ONE OR P HOLD.

00:14:22: We can think of this as a classic thing that if P doesn't hold The first one is just true for zero and the second one was true for one.

00:14:32: If P holds, then both of them are true to zero in VAR.

00:14:36: And that's what I did.

00:14:37: because For each of these predicates... ...for each of this habitat subsets we get a Boolean right?

00:14:49: Yeah!

00:14:52: And the Boolean is of the form that the predicate holds.

00:14:58: Now we have these two booleans, and you can compare them.

00:15:03: If the two boolians are equal then P must hold because... You see?

00:15:10: The first one only contains zero as a run-run.

00:15:16: so if they had any intersection it could be just that P holds.

00:15:24: So if he has those two Booleans Yeah, and we check.

00:15:31: We can check whether brilliance are equal.

00:15:32: because if they're equal... Because others have both two or both fours So is there equal?

00:15:40: Then you know that the P must hold because it's only possibility That the two predicates agree And then an element which is in both.

00:15:51: If their equal, then P must

00:15:57: be the reason.

00:15:58: if they are not equal, then assuming p volts it would make them equal and that's a contradiction.

00:16:07: And

00:16:09: isn't using p or non-p?

00:16:14: No no this is to prove not P. we had discussed this again to prove node P constructively.

00:16:23: you assume and you derive a contradiction, that's not proof of contradiction.

00:16:32: But we should repeat it is slight difference right?

00:16:37: We want to prove if the two booleans are not equal then assume P both sets would be zero one-zero And then there would have to be equal because equal predicates get mapped to equal booleans.

00:17:01: So, so then they would have been equal.

00:17:03: but we already say it's not equal.

00:17:08: The idea is that this is constructively perfectly valid.

00:17:19: to assume P derived contradiction as the definition of not p I see.

00:17:25: And so, okay... So what we have done is that comparing these two booleans which you get from the X-ray of choice We can decide whether P or not P holds?

00:17:38: You've derived an excluded middle!

00:17:41: It's hard to argue with a proof but it still feels somehow cheaty.

00:17:51: Do you know what i

00:17:52: mean?!

00:17:55: because of this arbitrary picking.

00:17:59: The interesting thing is that the cheat, which is an axiom of choice leads to a form of magic right?

00:18:12: And it's little middle as another form of Magic.

00:18:14: and we also have seen from constructive point-of-view one form of Magick implies and why does it do this?

00:18:23: And that's sort of, I find interesting because the example of choice just tells us now you have an existence proof.

00:18:31: Existence means that we are hiding the witness so as your not revealing the witness Because in existance proof is a proposition.

00:18:44: from a type-selected point of view there is at most one way The proposition can be true.

00:18:49: So i cannot grab the element.

00:18:52: I cannot, because if i would be able to grab the element there will more than one proof of this existence statement.

00:19:00: So and that's not what we mean by proposition while proposition means something which hasn't got... We can not differentiate the proofs.

00:19:11: they're all equal.

00:19:12: just at most one proof with a definition in type zero.

00:19:16: And as an example choice basically tells us you can cheat.

00:19:19: You say okay this witness and but I'm just cheating, i am pulling it out.

00:19:33: And once you can do that then you can prove excluded.

00:19:38: middle.

00:19:40: by the way there is an important step which if two predicates are logically equivalent than they equal.

00:19:51: So I use this for the proof of the negation, because if p holds then two predicates must be equal.

00:20:06: The subsets are equal and that uses what is called propositional extangibility.

00:20:12: it says subsets are equal.

00:20:20: If they're equal, then if we apply the choice function there must also create equal booleans okay?

00:20:31: But I have just assumed that's not equal.

00:20:34: so in the end i have derived a contradiction and thats perfectly fine constructively

00:20:40: about this assumption.

00:20:42: um could one think That the full intuitionist wouldn't like it that the choice function could give different things applied to

00:20:54: a same element?

00:20:57: Okay, I'm coming off of type theory.

00:21:00: In types theory we just define that the proposition is something which has at most one proof and then it's quite natural to say there are two propositions which are logically equivalent so nothing differentiates them than their equilibrium.

00:21:16: yeah i mean this is an extentionality principle.

00:21:20: So, yeah.

00:21:21: This is not so much the question whether you're constructive or classical but it's a question of whether want to do everything intangible?

00:21:31: Or whether accept extensional principles

00:21:35: and... Just for audience just like example the extension of people being five meters tall and seven meters tall equal namely empty But it's intentionally two different notions exactly and you can discuss of course whether This is really different or not.

00:21:53: And normally in math, It isn't because

00:21:57: both the empty set as well.

00:21:58: this respect The modern type theory Is actually very extensional?

00:22:04: That's it's actually more extensional than that theory and then just comes from.

00:22:10: we have discussed all these univalence principle which is a very, very strong extensionality principle.

00:22:16: But the cheapest version of univalence is propositional extangibility Which just says this if you have two propositions and they are logically equivalent then they're equal.

00:22:28: So why do I insist on an extensionality?

00:22:31: because extensionality Is absolutely essential for abstraction And abstraction it's a very important aspect of mathematics.

00:22:42: So I don't always need to usually assume excluded middle, but I do embrace extangibility principles because you can really nice constructive mathematics.

00:23:03: This extensionality without it becomes all very complicated and lots of Yeah, details which cannot be hidden.

00:23:16: And I think it's against the spirit of mathematics whether construct or form not construct.

00:23:23: Maybe to add a hot take too that...I was always puzzled and they shouldn't say that i have no permanent position yet That there is philosophical logic because for me if you do good philosophical logic You're doing math!

00:23:41: And nowadays, I think the key difference is exactly that.

00:23:44: That doing things mathematically wants to abstract and doing philosophical logic doesn't?

00:23:52: it's more fine with dealing with intricacies of a particular system without getting into nice meta theory where everything flows easily.

00:24:06: but if this might be empirically very wrong then there are simple sociological divisions or anything, but that's how I make sense of it.

00:24:14: Yeah...I guess i'm mainly interested in using logic to do what we call mathematics.

00:24:21: or which would you do to do exact constructions?

00:24:26: I am not personally ... I find this ...using logic to analyze language is a bit too fuzzy for my taste.

00:24:40: But let's go back to the axiom of choice.

00:24:44: So Fidiaconesco showed that the axion of choice implies excluded middle, so once you have this axon of choice... You don't actually need to say any more okay I'm in a classic ...you are classical!

00:24:56: That is no question.

00:24:58: but then natural questions about other way.

00:25:03: If we have excluded middle do you have choice?

00:25:08: And answer is NO And it's interesting, so the choice is really the brutal principle which kills everything.

00:25:18: Excluded middle actually constructively quite easily understandable or explainable and explanation based on what was called a negative translation.

00:25:31: So if as an intuitionist you should explain what classical logic you would not use this Boolean explanation.

00:25:44: You will say a classical proposition is the propositions such as the double.

00:25:50: negation implies it, so NOT NOT.

00:25:52: P implies P. is the classical proposition and its sort of clear that by having NOT NOT p implies p there's no constructive content.

00:26:02: because NOT negations doesn't have any.

00:26:10: any positive is negative.

00:26:12: Positive means existence or disjunction, but negation everything disappears and evades.

00:26:20: so if you say a classical proposition it's not.

00:26:24: not p implies P. And now we have all the connectors.

00:26:28: You use conjunction for conjunction and implication for implication.

00:26:37: But now the positive connectors have to be reinterpreted.

00:26:40: So for example, P or Q you know say I use a classical definition.

00:26:44: P or q means it.

00:26:46: cannot be that both are false.

00:26:48: Yeah?

00:26:48: So p or q mean not and not q. Or p orq means not... It means NOT.

00:26:56: both are FALSE!

00:26:57: And EXIST MEANS.

00:26:59: IT CANNOT BE THAT.

00:27:00: IT'S FALS EVERYWHERE!

00:27:02: This is just a classic definition of EXIST.

00:27:05: In this system Now, in using these classical propositions you can model the whole practical logic.

00:27:13: In particular... You have elimination principles.

00:27:22: so reasoning by cases that P or Q if P implies R and q implies r then p or q implies proven implication.

00:27:36: out of P or Q you do both cases.

00:27:39: And this is interesting, I have to check this but it works as long as R is classical.

00:27:45: so not R implies R. So we can use the classical definition of disjunction where we say that P and Q are NOT both our faults.

00:27:54: That's a bit something i need to check.

00:27:56: But for this classical definition if through the middle is provable because P or not p means It cannot be that not P and NOT NOT P are true.

00:28:09: And let's clear, it can't be that NOT P is true That the rule of contradiction.

00:28:16: So in this system The system of classical propositions you can intuitionistically show In this system we can prove excluded middle.

00:28:36: What is the classical logician?

00:28:38: It's somebody who cannot see anything positive.

00:28:42: Everything a classical logitian says from a constructive point of view, it's negative.

00:28:46: if you're classical logition says they exist in numbers such that then I have my little barbell fish and my ear And let's say oh what he was saying as it can not be That this falls everywhere.

00:28:59: Yeah.

00:29:00: So like the barbellfish translation yeah.

00:29:03: Well if a classical logicians says P or Q They don't mean pure cues, they cannot be.

00:29:07: that goes their faults.

00:29:24: So in this explanation of classical logic, excluded middle holds but you can show the axiom of choice still cannot be proven.

00:29:37: Here we have a way to explain excluded middle but not choice Whereas the other way, choice does imply including middle.

00:29:47: So an extra of choice is a stronger brutalist version on classical logic?

00:29:56: Maybe one final remark.

00:29:59: I think from my side would be that classically speaking choices rather tame because it doesn't change the consistency strength of ZF.

00:30:09: so you can build from one set you read to the other and vice versa.

00:30:15: As long as you have ZF, if you had ZFC then it's ZFZF.

00:30:20: so there is nothing to discuss about in that sense.

00:30:23: You can have or don't classically add on care but of course a different perspective with the whole axiomatic logic still having this first-order logic plus axium view.

00:30:39: Yeah, that's

00:30:42: an interesting point.

00:30:43: I mean... So i tried to make the points from a constructive point of view.

00:30:47: The axiom choice is much stronger than excluded middle.

00:30:55: But now you say yeah but for a point-of-set theory.

00:31:00: I'm starting with this set theory in classical system and have it good middle And now add action of choice as they get different sets theory equi-consistent, right?

00:31:13: I guess this proof is also classical.

00:31:16: Yeah yeah absolutely!

00:31:19: So i don't have a good understanding of why it's the case... I mean certainly what was not the case.

00:31:31: if you add or don't some other axioms like power set or infinity That certainly changes the consistency, strength of system.

00:31:45: And this is also too intuitionistic in types that you have or don't have natural numbers... ...or whether your have impredicative universe of propositions changes the strength of a system.

00:32:03: So then it's completely analog I guess to classical.

00:32:09: So I think the last thing that we can do is thank To all who listened to all Who comment?

00:32:17: We will be there.

00:32:19: and of course a special thanks, too All who became channel members And we will Record another.

00:32:26: Thank you for the alefs and by me or coffee members because it's updated so quickly at.

00:32:32: we record this like a month in advance So we don't want to leave out too many people their.

00:32:38: Or is there anything else you wanted to add and discuss?

00:32:43: Thank-you very much for listening, asking.

00:32:47: So as I said, the Okonesco proof was one of my favourite proofs... ...and i hope that I did a justice time to explain it.

00:32:55: It's kind of fascinating because if you would wake me at night and ask me this choice constructively valid.. ..I'd say yes sure!

00:33:04: Of course your construct everything are there But of course I know that it's not, and even... Anyway.

00:33:14: It implies a lot of little great.

00:33:16: thank you!

00:33:17: See y'all in the week bye-bye.