aboutlogic: premises #02 | Hilbert’s Hotel & Cantor’s Infinity: The Story of Set Theory
Show notes
This episode is also available as a video on our YouTube channel: https://www.youtube.com/@aboutlogic
Further Reading & Resources: Get the HoTT Book for free (no advertisement): https://homotopytypetheory.org/book/ Thorsten Altenkirch: http://www.cs.nott.ac.uk/~psztxa/ Deniz Sarikaya: https://www.denizsarikaya.de/ Creative Production: Jan-Niklas Meyer: http://www.jammos.com/
Show transcript
00:00:00: About sizes, sorry.
00:00:03: I have a little story that comes in different episodes and you want to go through it?
00:00:08: It's Hilbert Hotel!
00:00:10: You know Hilbert hotel right?
00:00:11: Yeah sure
00:00:12: yeah.
00:00:13: so this is hotel number one two three or zero one-two-three at its computer scientists involved right... And then completely full and the new guest arrives.
00:00:24: So what can we do?
00:00:28: Hello, everybody.
00:00:29: Welcome to our second episode of About Logic Premises where we tossed and I just talked a little bit about some notions that might be relevant to follow the interviews with our guests.
00:00:42: And there are some great updates now.
00:00:46: We became YouTube partners in some tier so you can now hype videos which would help us reach more people.
00:00:53: So feel invited to do and of course always like, comment and subscribe.
00:01:00: And everything else you can do!
00:01:03: So that's great news.
00:01:04: thank you for all the support.
00:01:05: we are very happy to grow so quickly... ...and reach many people interested in foundations on mathematics, logics & everything related.
00:01:15: Yes welcome from me too.
00:01:18: This time I'm form a different place.
00:01:20: We're actually both in North and Germany today but not at same space Yeah, so what should we talk about?
00:01:29: I think one topic which came up from time to time is this thing called set theory.
00:01:40: Dennis as a philosopher can you tell me bit more about the history of that theory?
00:01:47: Yes sure and now i will begin with a statement.
00:01:52: How did you get this
00:01:57: idea?
00:02:01: I mean, Hamkins actually said something more nuanced.
00:02:05: Set theory has two roles.
00:02:06: right there is the academic mathematical discipline set theory similar to topology similar to calculus.
00:02:16: You can do different things and you can do set theory And it's like a proper research field or you can do a descriptive set theory and whatever.
00:02:29: This is the one role of Set Theory, And The other One Is the foundational Role.
00:02:34: I mean i guess it all started.
00:02:37: You Can Have Different Starting Points but A lot Of People Would Say It Started With Zwischenwertsatz The Intermediate Value Theorem For Bolzano-Weierstrasse.
00:02:47: So If You Draw Line Of Real Numbers Or if You Draw All fractions, it looks similar.
00:02:54: It just looks like a line because the fractions are quite dense but only in the reals.
00:03:01: you're guaranteed that a function going from negative to positive which is continuous as zero at some point and this started with push towards formalization before then was more about intuition.
00:03:18: And one very particular ambitious goal of making things rigorous is what's called logicism.
00:03:29: So people like Frieger try to reduce all of math only through logic, and as you know this logism program somehow failed in the system of Friege had a contradiction in it.
00:03:46: This XM-V was problematic.
00:03:49: And I mean, if we skip over the details that the more or less the Russell said is the problem there.
00:03:56: so you're not.
00:03:57: you don't mention Kantor at all?
00:04:00: Yeah maybe not yet but as always they are many people involved in set theory proper and Kantor's often described as father of set theory because he made this proof that there are different sizes of infinity.
00:04:20: Yeah, exactly.
00:04:22: And it's
00:04:24: actually
00:04:27: argument here
00:04:29: and there is this.
00:04:30: I mean recently they discovered some letters from Dedekind that Dedekin helped him to formulate this version of the diagonal argument and Dedekint had a prove.
00:04:47: And this together makes that there we have transcendental numbers in quite a lot of them, uncountably many.
00:04:55: This is like the very maybe first satirical paper brought into mainstream when Kronecker accepted it?
00:05:05: About sizes story I have little.
00:05:08: story comes from different episodes and they want to go through.
00:05:13: It's Hilbert hotel, you know Hilberts Hotel right?
00:05:17: Yeah yeah sure.
00:05:19: So this is hotel number one two three or maybe zero-one to three and there are computer scientists involved like that.
00:05:27: And then it completely full!
00:05:29: Then a new guest arrives.
00:05:31: so what can we do?
00:05:35: We can do two things if start with the room zero zero when the toilet which was empty
00:05:43: That's not so
00:05:45: bad.
00:05:45: More seriously, and this is the weird thing about infinities you can tell everybody to move one space further.
00:05:54: So zero go just one two three And so on.
00:05:57: okay I have a combination.
00:05:59: yeah there also the Hilbert bus company huh?
00:06:03: In The Hilbert Bus Company has buses which are numbered Zero One Two and so on and then as a hotel is full in the fool Hilbert Buss arrives.
00:06:13: What can we do?
00:06:14: Yeah, another really puzzling thing for people in earlier generations.
00:06:19: I mean just tell everybody to move two times n if you are room N and then all the Even numbers are full.
00:06:27: but all the odds are Still empty And everybody can.
00:06:31: just when the bus can just take a odd number.
00:06:35: yeah We will be tell.
00:06:36: i mean we tell the people look at your at your seat number multiplied by two and add one And that's your own number, right?
00:06:44: Now it gets worse.
00:06:46: So the Hilbert bus companies has buses numbered zero one two three and so on.
00:06:52: yeah...and they're all full when they arrive!
00:06:55: The hotel is empty in this day.
00:06:59: what can we do?
00:07:02: We can do several things.
00:07:04: I mean..we can keep the hotel mostly empty.
00:07:10: The first bus goes to all the powers of the First Prime, and then the second bus goes out.
00:07:18: But this is a bit complicated... I mean there's a simpler recipe which is one-to-one.
00:07:26: So you take your bus number And the number of seats.
00:07:34: You interleave digit by digit.
00:07:36: Ah, sure.
00:07:37: Yeah I
00:07:40: see this works!
00:07:47: But now we come to Kanto.
00:07:52: In this Hilbert's hotel in the office they have a list of all occupation lists.
00:08:01: The occupation list says room zero is occupied, room one is occupied Room two is free and so on.
00:08:08: So there are.
00:08:09: It's really big filing cabinet here, but they run out of space in the office.
00:08:15: So there decide to distribute the occupation lists on onto the rooms yeah?
00:08:22: To put one occupation list and every room.
00:08:24: uh And then guys is the class area have done it.
00:08:29: But he is a liar right.
00:08:31: Okay you You want this list off all the occupation to put into every room
00:08:37: or... In Every Room Is One List.
00:08:41: So he takes this big filing cabinet and put one occupation list, which is the infinite of assignments.
00:08:52: Zero is empty, one has occupied and so on... He puts it in each room right?
00:08:57: Okay I see there are all possible lists in that filing
00:09:01: All possible lists.
00:09:07: One list doesn't appear.
00:09:08: That's the real number.
00:09:09: One list doesn't appear, yeah?
00:09:11: The list... We look at zero and what does a list say about room zero?
00:09:20: And if it says occupied we always do so opposite.
00:09:23: So you make in your list which is every room for this room has an opposite occupation And this list cannot be in any room because every room disagrees with the list of rooms at exactly this diagonal number.
00:09:43: This is a diagonal argument using Hilbert's hotel.
00:09:50: What I meant, there was this trifecta on the continuum power and cardinality power set of the naturals and you can see the list.
00:10:08: actually Constructively, it's not clear whether this argument works for the reals.
00:10:13: This argument works For the power set Actually for the Decidable Power Set Yeah So that is very easy but I think its not clear Whether It Works for The Real Because The Reals Are Quotiented.
00:10:33: It's not so easy to do the same argument for the real constructively.
00:10:38: That is true!
00:10:40: You see, in the end you also have a constructive or lazy computing variant of the Hilbert Hotel right?
00:10:47: You can look into these arguments and see that they are effective procedures In the sense if you don't need to finish an infinite moving order And then do something else but already put in people where all the changing room, changing process
00:11:05: just function.
00:11:06: Function which assigns to every every room whether somebody is in there or not like so functions.
00:11:15: but this that these are different sizes of infinities it's probably the main story off set theory proper right?
00:11:22: It's a The story on mathematical field That's not necessarily related at all to its foundational use, just the signs of infinities.
00:11:36: Interesting point!
00:11:39: I was going to get something else in a moment.
00:11:42: so I think Kantor made a cardinal mistake which has continued since then and that is...
00:11:54: And
00:11:59: this is that he identified sets with properties.
00:12:04: I mean, he famously said he had an intuitive definition of a set.
00:12:08: A set is given by property right?
00:12:12: So for example if you have the property like being green then your has a set all green things.
00:12:18: but what's left out?
00:12:19: there is a property of what are the U-elemental.
00:12:26: And in pure set theory, there is this easy way out that we say the element of sets themselves.
00:12:35: We build everything from sets.
00:12:38: A set as a property of sets, right?
00:12:40: That's the slogan for pure-set theory.
00:12:43: but now if you look at this asset as a probability of sets then obviously negative domain equation and there's no good way to interpret this.
00:13:00: And in my view, I mean all of my understanding but maybe it is totally incorrect ZFC then cut down the infinite comprehension principle which any property gives rise to a set Which includes also these paradoxical sets that do not contain themselves.
00:13:24: But once we... yeah, this is too much.
00:13:30: So you have to cut down and say only certain properties give rise to sets And that's most of the axiom of set.
00:13:37: theory are about this right?
00:13:40: There is a pairing axiome.
00:13:43: if you had two sets then make it a set which contains at least these two sets.
00:13:49: What else does there...?
00:13:50: The power-set axioms infinity axiom always states that some sets which you could actually construct in this unlimited comprehension, but they are actually permitted.
00:14:02: Right?
00:14:02: So most of the axioms set theory has some exceptions like tangentiality and regularity are off this form and replacement.
00:14:14: But uh The thing is why if you want like Kantor wanted to specify, explain what collections are.
00:14:25: Collections or things in your sets okay?
00:14:28: Then why do you start as properties while not just saying oh I sit down and say what collections you can form instead of referring to this rather mysterious concept off a proposition into predicate yeah... And i would say that is the idea of type theory.
00:14:49: Here we are, let's form collections.
00:14:51: That is how you can do
00:14:52: it.".
00:14:54: And then propositions can be explained constructively by saying a proposition as something that you have evidence for every proposition assigned to the type of evidences.
00:15:09: I mean this definitely an interesting diagnosis on what could happen and what are the main motivational forces?
00:15:18: I guess, i would stress slightly different aspects.
00:15:22: and if we begin from Frig's problem where you had exactly these two types.
00:15:32: You are either an element or a function more-or less your set.
00:15:37: It is like two elements!
00:15:41: We have the contradiction there.
00:15:43: so we need to solve this.
00:15:45: contradictions in their two way out On top, you say set of sets or let's stay in the set picture.
00:15:55: This is something beyond a second level set and collection of those with third-level set
00:16:03: etc.,
00:16:04: this is what Russell did.
00:16:05: By the way, the Russell theory of types is not really closely related to type theories.
00:16:13: it comes from confusion.
00:16:17: As you just said, the Russell's type theory or a theory of simple types is really a way to stratify that theory.
00:16:25: And
00:16:28: then other ways just collapse it down and see what can we do if everything has the same thing?
00:16:35: Too much!
00:16:39: I think this maybe like motivation why set theory became... What it is and I mean the other one.
00:16:47: Is this study of the infinite okay?
00:16:49: Okay, I'm in.
00:16:50: I would say actually whether you accept Russell solution which actually didn't work.
00:16:55: or I mean There are several attempts to make it worth a quirk but basically these Russell Russell's approach was too inflexible was getting too complicated.
00:17:09: You couldn't actually do good mathematics in it.
00:17:13: And then Sermelo by just stating some axioms, like basically saying yeah a comprehensive is fine but here are some cases where comprehension was actually allowed.
00:17:29: It's an alternative with an alternative.
00:17:33: But the third option which has not been considered until much later as far I know maybe it should.
00:17:40: I would say Martin Lööf by saying, okay let's forget all this stuff about propositions.
00:17:51: Let's talk about types and collections as the basic idea.
00:18:03: Yeah, but maybe one slight comment.
00:18:06: I mean as far as i understand the Cermillo axiomatization is mainly a reply to people not believing his well-ordering theorem.
00:18:14: so if you have the axiom of choice You can Well order every set and that sounds weird right because it will.
00:18:20: order looks so countable first element second element And I just counted the reals, right?
00:18:33: We put them to a well order and count.
00:18:35: then contradiction.
00:18:37: Of course... After all this discussion he needed so it's to speak clearly what his basis is.
00:18:47: He came up with these ZFC axioms minus one oversight So-to-speak for replacement.
00:18:55: That was edited Because
00:18:56: in the original The Milo series There is an axiom of infinity and actually I think Zermelo defined the natural numbers in a different way than von Neumann.
00:19:08: Yeah, he just iterated brackets with
00:19:10: curly brackets And uh Actually i think for neumann ones are not uh definable In in zermelo right?
00:19:20: Uh...I'm not hundred percent sure.
00:19:22: but
00:19:24: because you need replacement Because You Need to say Here I have one construction of natural numbers and here is something else which are actually, okay let's say isomorphic that you need to address but your relation between them blah blah.
00:19:41: And then we can apply a replacement numbers are also set.
00:19:51: So then I think you need replacement at least to do things like this,
00:20:00: but maybe one tiny thing?
00:20:04: We cut the story of Satiri as a foundation short by going right away into the infinities and it's just an insane fact that you can emulate so to speak all or a lot.
00:20:19: I mean let's not think about higher categories and things like that, but of very ordinary math.
00:20:25: You can all emulate that somehow in one shared language right?
00:20:30: And it is the language...
00:20:32: Can do with higher categories as well!
00:20:34: It's just terribly ugly.
00:20:37: Yeah yeah what i mean we are still in historical context.
00:20:40: it simply interesting That you can do all the constructions You get you built from nearly nothing or for literally, nothing and one infinite set.
00:20:52: And do have this few building operations that you'll get to find the structure.
00:20:57: That looks like natural numbers.
00:20:59: look Like the reals
00:21:00: and initial numbers you put in right?
00:21:02: I mean yeah some more exciting care.
00:21:07: But
00:21:07: actually it don't put in very little you put into quite a lot.
00:21:11: i mean For example.
00:21:13: so power set axiom.
00:21:16: It's already problematic from a constructive point of view.
00:21:20: I mean, it is
00:21:22: also problematic from the classical point-of-view because its like under defined different models disagree what the power sets actually exactly do right?
00:21:33: And we wanted to make these premises shorter.
00:21:35: so input from different aspects of set theory.
00:21:40: But maybe one thing, the biggest question in set theory or what used to be the biggest questions?
00:21:46: The Continuous Hypothesis is exactly that power set is a weird thing right?
00:21:53: it's not so easy to pin down with the power setup something really how big and whether there are some things between natural numbers or the power set of the reals should be careful for constructive contact.
00:22:12: Yeah, so the power-set often is described as that we have some power analysis right?
00:22:19: Or calculus in a sense because if you want to define the real's... If you wanted to find the real do need XA actually some form of core-set action.
00:22:32: And I mean interestingly Harvey Friedman has this point he would feed it in different contexts that most of math doesn't need all the satirical hierarchy.
00:22:44: So even now, we established that can do power set and get to bigger and big infinities.
00:22:50: calculus is like one power step above The natural numbers.
00:22:57: so its not that much.
00:22:59: maybe give or take two or three iterations you And that's something quite interesting, because I mean set theory as a discipline cares about a lot.
00:23:10: That comes above it.
00:23:11: It cares about things that are so large that you cannot reach them with power set and things like that inaccessible.
00:23:17: Yeah these are large coordinates.
00:23:18: but just go back to the reals.
00:23:23: we can understand using functions as a primitive concept which constructively if you don't identify prop in pool is much weaker than this idea that you have power sets, which in a type-certic formulation means the type of propositions are small.
00:23:43: The type of proposition is smaller if we have crop equals bool because bool is small but If You don't have crop equal to bool then there isn't really good reason why prop should be small right?
00:23:55: But We still can define the wheels Basically, I mean functions from not to rationales or whatever.
00:24:04: Which is rather harmless right?
00:24:06: So you don't even need the first level of power sets at all.
00:24:13: Power set in a predicate type theory lives as next universe.
00:24:24: so it's not... The types of all predicates over a type lifts at the universe, it's an ex-universe.
00:24:32: The universe is actually correspond to these large cardinons
00:24:36: and then I mean they are in set theory.
00:24:39: if we talk about this small end big I mean sometimes there is my two relevant notions.
00:24:46: one as the class Which lives like every level of the satiratic hierarchy?
00:24:51: And when that's one diagnosis and like versus class of all ordinals is no set, because there are ordinals on every level.
00:25:00: You cannot form this.
00:25:01: the SetOfAllSet doesn't exist because less than all levels it's a class-of-all sets.
00:25:08: and in other interesting thing I mean we should introduce now.
00:25:12: but if you assume very large cardinals can somehow measure what small or big underlevels below by an ultra filter which has very reasonable axioms.
00:25:26: If you add small things, it doesn't get big and stuff like that... It helps a lot for this analysis.
00:25:32: what is big?
00:25:33: What's large?
00:25:35: Which probably quite a lot of the spirit of set theory.
00:25:42: Great!
00:25:43: Shall we call it an episode
00:25:45: four...?
00:25:46: Yeah let's call today sort-of
00:25:49: yeah.
00:25:49: We hope these in between films are better than nothing at least hopefully even quite nice.
00:25:58: So don't forget to subscribe, to hype ,to support, buy us a coffee and now you can see what new Functions YouTube is donating our little channel because we have so many thousand hours of watch time which really appreciate!
00:26:14: See you in the week most likely with an episode with Emily Rie.
00:26:21: We will learn on category theory
00:26:25: Higher categories.
00:26:28: Bye bye!
New comment