aboutlogic premises #10 | Is Unique Choice Really a Choice? (Follow-up to Giovanni Sambin)

The unique choice says if we assume for all the XS to Unique element, then that conclusion is valid than there exists a choice function. And basically you could ask If there's only one possible choice? Are we making a choice at all? So hello everybody welcome to this premises and today We want to talk about an old friend of the series namely the axiom of choice.

It came up again and again. And before Torsten will take over, talk a little bit about the principle of unique choice which plays quite a role in most likely last weeks maybe three weeks ago's episode with Giovanni Sambin. I wanted to start shortly to remind you all what the Axiom Of Choice said. so starting The axiom of choice used to be in the very first axiomatization of set theory, so we still say ZFC.

But C is just stressed there not because being an extension like F extending z as an axioms system but already Termelo had a choice principle and actually he kind of really needed it because his well-ordering theorem, which is one of the many equivalent things to choice was casted into doubt. People didn't thought that's a good thing.

you can well order every set and again to remind you a well ordering like an ordering where each subset has its smallest element. think about the integers. And so he introduced this choice axiom Which just said if you have infinitely non-empty sets, you can have a choice function which picks from each of them one element.

So this mind sound trivial. it might sound very problematic. I think there are people disagree. maybe the last thing i want to stress is that they're so many things that are equivalent to choice. and we just learned in this open AI dump equivalent to choice, if that theorem holds. But they are like literally books with things that are equivalent to chose.

the infinite product of non-empty set is not empty as lack for instance another famous example. and then The other nice thing is that you can play around with choice a little bit. You can have only countable choice So you just assume it four countable sets but you can also have stronger properties. Today, Thorsten you wanted to talk about unique choice right?

Yes. Maybe first of all the reminder. in one alternative version of choice which I quite like is if you have a relation between two types let's say that's the stock type theory and for every element in A they access elements Bs. it's a relational holds Socks and left socks, no gloves. Left and right gloves and matching gloves as an example.

then there exists a function from left gloves to right gloves which always choose the matching pair As long you have finally many gloves. it's clear. how can do this? How can construct these choice? But if you have infinitely many, then... You may never find some matching graph or not. Not that we don't really a function.

choosing it and so this shows the maximum choice is related to constructivity. So If he want to have functions which can actually run Then This Is Not Compatible with the axiom of choice in general. The axiome of choice is also just what you said, In type theory we can have this equivalent formulation that a product or types if every it's inhabited then the whole product isn't habitat.

This is really. And maybe another thing to remember is choice in excluded middle. So, excluded middle that for every proposition you have P or not P it's often identified as classic logic. and previously we talked about the Diakonesco theorem which says action of choice implies excluded middle. And maybe it's interesting to ask the other question, does a clue in middle imply choice?

What do you think? Okay. Now I shouldn't say...I should not think too long because of the flow of the podcast but just assuming excluded middle shouldn't imply choice because we can have ZF with intuitionistic logic and classical logic sorry. With classical logic without Yes, and we can be more precise.

I mean... We actually justify or explain an excluded middle in intuitionistic logic. And that's maybe surprising But it was possible! That is called the negative translation. So what do you say? The classical proposition where the double negation implies the proposition. So it's a reminder, intuitionistically can prove that any proposition P implies its double negations, P implies not non-P but no non-p implies p is not provable.

intuitionistically now you can say these propositions we call negative and For example, every negated proposition is negative. because why? Because triple negation implies single negation. So that's a thing you can prove in illusionistic logic. Every negative preposition Is negative. and for me the intuitive idea is That negative propositions are one which have no information Which contain No information.

And it turns out If we just look at negative proposition, then we can justify excluded middle. because if you redefine disjunction. Disjunction in an intuitionistic logic is something positive it contains information. and if you know P or Q which one holds either P OR Q but classically P ORQ is equivalent to if cannot be that both are false.

That's classical equivalence, and we can just replace this junction P or Q by it cannot be the both of false so not p and not q And it turns out for negative proposition. this classical disjunction behaves like distinctions also properties in particular reasoning by cases for this proposition. And we also need to do this.

where you predicate logic, We say that exists some things exist an x which p of x holds is the same. it cannot be. there isn't one. and again all the principles for existential negative propositions or negativ predicates hold for this translation however is not provable in the setting, so it's still intrusionistically not provible.

So this negative translation is a way intrusionistically to explain exclusive middle and I always have little joke as say what was classical logician? Classical logician? somebody who cannot see anything positive because the classical logic is the logic which, from an enthusiastic point of view it's a logic of negative propositions.

The logic of propositions that do not contain any information? I mean maybe just this tiny remark...I'm not sure whether name was Glivenko but there are some of these translations using exactly that phenomena putting in front every atom to negations on. Yes, but the problem with Glivenko is it only works for propositional logic.

Yeah so that doesn't work for predicate logic. Okay again we knew about these choiceless classical worlds. and I think the math also... I mean classically speaking there are good motivations to drop choice as well in the non-Lebec measurable sets. A prime example with choice. You can construct a set such that its volume is not translation invariant, so you move it around and the change volume And then doesn't sound right.

But what did classical math do? They bite the bonnet. they say yeah okay these sets are fine but don't have volume. One famous example of the Banachtarski paradox for splitting a ball, moving it around re-merging them. And now you have two balls off such that the first one has the same size each of them as the same set.

and then there are these whole determinancy axioms. so you might want to talk about infinite games in order. they're always being winning strategy. You might need to drop choice because else construct weird subsets of the reals or even the natural such that these things don't always work out. So adding choice really changes them off.

and I mean, I guess the main argument for choices is sociologically in your linear algebra you do the dance and say look an order for every vector space to have a base. You need choice? And we really want it. so are happy. Yeah, it simplifies the mathematics. It ignores some distinctions and hence that makes sort of easier to swallow.

so I think its quite sensible. sometimes if we assume choice you can present like this but sometimes the distinctions which are flattened by assuming choice are actually interesting and relevant here. So hence you can be a bit, accept of the multi-verse view when say okay sometimes I reason I assume choice at some times I don't yeah.

so what do i think is just to me in a way interstitial logic. it's more minimal smaller foundation But you can choose which principles, and sometimes maybe just want to add choice. And some times not so. for example in Lean Choice is an axiom but also work without choice. I will give one example where i think actually Lean is a bit weak when we use it intrusionistically which comes to, this is a good motivation for the topic I wanted to discuss.

Namely this unit choice and it came up in our meeting with Giovanni Sambin. so let me just say what unit choice says and viewing choices best presented For all A, they access to B that the relation holds. Then we have a function from A-to-B which chooses the elements and unique choice just says if for every element in A there exists The Unique Element In B such as the Relation Holds And the Unique Elements We can Just Define.

In Predicate Logic We Say There Is An Element And All Other Elements Which Satisfies The Relations Are Equal To It. This Mouthful. But it Can Be Just X v right exists in exclamation mark, but it's just a macro. for there is unique element. all other elements which satisfies this relation or this predicate are equal to this one.

Yeah if you have two they're actually the same. yeah. so uh For example my mother everybody's mother is its unit choice and any two mothers turn out to be the same. That's an example. And a unique choice says if we assume for all the access to Unique element, then that conclusion is valid and there exists a choice function.

Basically you could ask... If it has only one possible choice are we making a choice at all? But it feels weird that this might fail, so to speak. Because you have the recipe to take that one right? Yeah but still of course its an infinite procedure doing for all infinite sets at once. So in HOT is actually provable.

First let me quickly explain how we model existence. And in hot, there are two ways to model existence actually. The one is called the sigma type. So for example if I want to say that they exist. a parallel number... ...I form the type of pairs or numbers together with proofs and their prime. For example three and the proofed at three is prime and five and so on.

This is called a sigma-type And it is not a proposition in the sense of HOT. So what's the proposition? That's an interesting point! In HOT, we don't assume propositions as primitive but we define them... We define them as types which have no information and only interesting aspect to this type that they are inhabited.

So a proposition is the type which has at most one element, so if an empty type or any type with exactly one element it's a proposition. Now as I just explained this sigma-type isn't a proposition because we can have lots of possible choices and to make what is called truncated, and truncation means basically we put the element in a black sack.

And you can feel that the sack as non-empty but we cannot identify the color of this element. so it still feels it. Existence explained like this... It's interesting that the axiom of choice with the sigma type It's provable in type theory. But the action of choice with existence, where okay existence is defined as there is a sigma-type and it's truncated so that for example they exist.

a prime number Is uh The type of pairs off of numbers together with a proof That's prime but we put it into blackjack And you cannot see which number We have chosen. that it merely exists as a terminology is. And now the point. this for unique choice, if you have any access to a unique line then this pair existence at sigma type.

because the unit choice says, I mean prime number is a bad example. but if i say all prime numbers which are less than three this...I can show that there's only one such prime number. so hence if I choose this prime number. I know I must have chosen two and uh ...and I haven't hidden any information right?

So in very formally using the principles of these typeformers, sigma types and this truncation which means black sac. We can prove the axiom of U雷 choice! So yeah... And okay I say previously when i was running in Lien it had to do with effect that unit choice is not constructively provable in lean. So what do I mean?

Okay, let me tell you the story...I'm teaching an automata theory and i am using lean and i define. an automator has a finite type of states with a decidable equality. so these are two things i need for my automata of an automata, finite automata has to be finite. But I also need to be able to identify whether two states are equal and it turns out that if in Lean i can use classical logic ,i can use axiom-of-choice but i can also stay in a constructive fragment .But the problem is in this constructive fragment which i want to use because i want run my functions on automata.

We don't have a unique choice and I can explain why. That's the way Lillian is doing propositions, so we do not have any unique choice. And now it turns out that using Unique Choice i can prove that Finiteness implies decidability of equality. The reason is because finiteness Is given by an enumeration of elements.

If you have an enumeration of elements I can compare elements by just checking whether the indices are the same. So using unique choice, i can prove that finite types have a decidable equality but in lean this is not possible. so each time when I define an automata and use new type of states as a decidable equality, even so one implies the other.

And okay I could also turn them into types instead of propositions and that would cause other problems if i do this. So I want finiteness and decidability ,I want to be propositions inconvenient not to have unique choice, even though it's a constructive principle which is valid and hard and constructively acceptable.

That so interesting! And I mean that may be again this me not being user of lean. just adding these axioms on top break the constructiveness because it means you cannot run your function anymore. I mean, I can use lean has an axiom x of choice and they can't use that there. but as soon as i used then my function contain this choice principle in a cannot run them if i do.

if we're doing same in hot in cubicle actor they have them both as proposition and one implies the other. And it's fine, I need to use unique choice at this point. so then in this point unique choices is essential. you get both You gets a unique choice, you get avoiding of duplication... ...and maintain that it's constructive.

So you can run your programs. Yeah interesting Great! Anything else we would love to share about Unique Choice? Yes, because maybe we should go back to Giovanni and Mellimaietti. They developed this minimalist foundation... ...and it's a bit like Lien in the sense of intuitionistic part of Lien where you don't have unique choice.

And I think the reason really is that Giovanni separates types and propositions. So, propositions are something primitive whereas in Hott there's a modern version of type theory, a proposition is just this special kind of a type which enables us to prove things like unique choice. Now, Giovanni has got other reasons why he that doesn't want to have any choice which are in the philosophy of constructions, the choice sequence and formal points.

In his setting it's useful to make this distinction right? Which also shows anyway there may be as many foundations. We both agree on intuitionism or constructive mathematics, we have different ways to approach it. Maybe just one comment on that... Well maybe a challenge. but sometimes you say something that people would clearly agree.

saying into a stonistic math is generalization of classical math and in some sense this Trivially true because you can add the principles and get everything, so to speak. So of course if you add them You got everything? If your don't you get something else. so it's more general. But but now you made the point that for the minimal foundation in some sense having these slight differences really change The fabric of what you're doing.

For instance choiceless set theory is fine. You can do it But the whole idea of size is different. It's not where you can have something like cardinal numbers, but if you are really honest they're slightly different because we don't have the well ordering right? We just cannot pick a line off all ordinals and everything is comparable.

And Of course A lot of things hold a lot of stuff Can be emulated. that there always these tiny differences That I it feels to me Like You Are willing To Say For The Minimal Foundations Oh This is not simply a generalization, because it really matters. But for interest-synistics logic you don't... You aren't willing to say that?

I think one shouldn't reduce logic just too game with symbols. but we should start with the explanation. Let me go back. When I introduce...I'm doing the logic course now and obviously, I do Intrusionistic construction but also classical principles. And so what's different? My explanation is that Intrisionistic logic is a logic of evidence.

Don't say proof as an evidence! I am accepting a proposition if you give me evidences for it while classical logic is based on the idea of tools and tries to capture this. Now, in my view it's that... The classical view is like that. mathematics is a bit like real world right? In real-world even if we don't know something We know it's either true or false, at least that our picture of whether reality is another question.

That's the idea for realty. Whereas mathematics are constructions which take place in our head and we can talk about them and try to share them. but the notion And we had this analogy, this Captain Ahab story. The notion of truth is a bit problematic because I mean even Joel Humkins says okay when you talk about sets then yeah... We need this multiverse.

and so in the sense what would say that to have a notion of evidence, if you tell me something and I can give evidence for it. But truth seems to be the bit of misleading concept here. And once I go this way and say okay its evidence then It seem very natural to identify proposition with type of its evidences.

I can write down, if you give me an element of this type then i accept it and that is the proposition as types translation. Now what we have said is a bit of refinement because these types behave a bit different to what were used in propositions Because they carry around their own evidence. And hence there's now this refinement is not every type but propositions are the types which have at most one element and that's a story.

And once I take this idea, which i think can conceptually explain quasi-directly a good story to explain the concepts, to start with concept and then see what we end up as. What formal systems you can design that reflects this and so on? I would probably call it a day for these premises but just to teaser maybe potential other one...I think there is still tiny problem because of approaches where people try to have both classical and into a sonistic quantors in one system.

And then things got messy, and it's not always very easy. while this should work out with evidence and truth right? I couldn't say...I don't know whether you had cereals for breakfast but or i don't that you don't have..but So I can switch between having evidence and stating a matter of fact in natural language, but an informal system.

Having both is slightly complicated. so yeah never understood this because Because i kind have i mean i can just define the classical connectives in intuitionist logic. as i said i mean pure. it's not. both are false. I have seen people talking about this, but i never really got the essence of why one needs it.

But im sure missing something here and Im not saying its my own ignorance that they didn't understand this. But thats maybe an ideal starting point. lets see whether we can invite somebody for a topic or just need to have. look ourselves then do a premises working Great. Thank you for these elaborations on Unique Choice and to y'all, thank you for listening and subscribing for supporting us by becoming channel members or at Buy Me a Coffee or commenting and sharing in social media.

it's all appreciated! And its already season three so still quite unbelievable. but let's continue as long. Yeah, yeah. Thank you for listening and see again bye-bye.

aboutlogic premises #10 | Is Unique Choice Really a Choice? (Follow-up to Giovanni Sambin)

Kapitelklicken springt direkt hin

Shownotes

Transkriptvom Podcast bereitgestellt · Zeitmarken springen hin