aboutlogic: premises #07 | Fixing Russell’s Paradox: The Birth of ZFC & Constructive Set Theory

Show notes

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: Hi everybody!

00:00:00: This is just a very short thank you to all who support us, who comment and subscribe.

00:00:05: And in particular our AboutClub members on Bibucoffee.

00:00:09: So huge thanks to someone and James as well as YouTube channel members particularly Alephs Tatwitani and Bartos.

00:00:22: Thank You!

00:00:27: Okay hello.

00:00:28: welcome to AboutLogic.

00:00:30: two premises again And we want to continue where he left off last time.

00:00:36: The last time, We talked about the early history of set theory and we ended with Russell's and Russell's paradoxes .

00:00:46: Today ,we want talk about the fixes as Dennis can maybe tell me again what other ways to fix this paradox?

00:01:01: So maybe give me like, thirty seconds to recall two things.

00:01:05: I mean one thing is we have these two players in set theory the cardinals describing how big a set is and the ordinals go looking really at The finer structure.

00:01:18: so for instance if you have a copy of the real numbers omega And add one element on top of it.

00:01:24: It's another well-ordering, and other ordinal but still the same cardinal.

00:01:28: so this is maybe the one thing to remember in.

00:01:30: The Other Thing To Remember Is Exactly This Fregen Problem or The Russell Set?

00:01:36: The set Of All Sets Not Containing Themself Which Destroyed The Logicism Program Of Frege To Bring Back The Whole Of Mathematics To Logic.

00:01:48: Indeed, there were two solutions.

00:01:50: Friege had these two systems of objects and functions or properties.

00:01:56: one was Russell himself who added new more layers.

00:02:01: so second order type third-order types.

00:02:04: fourth other types off things on level below.

00:02:09: the other is the set theory approach that everything.

00:02:16: Yeah,

00:02:17: exactly.

00:02:18: And then restricting how to build these things up from less complex things in some sense rather than having this full comprehension scheme which just gave you the set for every property as you could imagine?

00:02:33: Yes and one thing that I always find fascinating is the language of set theory.

00:02:41: i mean okay yeah so it was an idea of their mellow was, then as you say already to give some precise axioms how what we can see about sets and in particular how sets can be formed.

00:03:01: But yeah he was starting from this idea.

00:03:04: I think it was starting form the scantor idea that sets are properties but not every property gives rise.

00:03:14: I

00:03:17: mean, more pragmatically as we already touched on he gave a well-ordering theorem and it was questioned.

00:03:24: So if your proof gets questioned you need to become more precise.

00:03:31: so he came up with this list there exactly.

00:03:34: And then they are some details.

00:03:35: He forgot one axiom.

00:03:39: That's why now talk of ZFC It is not Samuelo Seturi but Samuelo Franklin Seturi But that's maybe details.

00:03:49: Yeah, but let us first talk about Zermelo and then we look at Frankl.

00:03:54: So what Zermelow did... One thing which I find always fascinating when you see the axiomatic definition of set theory is how sparse it is.

00:04:06: because you only have one relation-the element relationship–and everything as a set You don't start with any elements, like you could say.

00:04:15: Like starting those numbers or we're starting this spun some data types and then we form sets of them.

00:04:21: but no it's very sparse.

00:04:24: its just set if your right time is.

00:04:27: curly brackets.

00:04:30: I always thought analogy to the disc world less on some elephants rest on some turtles, and then the turtles rest on more turtles.

00:04:44: And the turtles all the way down right?

00:04:46: But that theory is the other way around.

00:04:49: when you take a set... You go down ,you end up with nothing!

00:04:54: You always ... you go down and it ends obviously with the empty set.

00:04:59: I mean in The Footnote there are also sets here with Uwe LeMent which has like another theory but in some sense doesn't really add as much set theory without anything else.

00:05:13: Yeah, and then also a remark I mean my very first mathematical life was the Life of a Graph Theorist.

00:05:19: so i always insist Set Theory is also the language of directed graphs.

00:05:25: if you draw small models of set theories or fragments of ZFC You often drew them graph like one you have two points And If One Is An Element Of Another You Have A Narrow Between Them.

00:05:39: So you can also say the very foundation of Martha's directed graph theory, if you really want to.

00:05:45: But are there not trees usually?

00:05:49: I mean... You don't have circles which is well

00:05:52: founded.

00:05:52: Oh yeah but you cannot do same element twice in different paths.

00:05:56: so it's directly... Yeah

00:05:57: however you like!

00:05:58: I mean..you can also have circles.

00:06:00: then you have non-well founded set theories Which we can have.

00:06:04: infinite descending sequences We can do a lot but of course ZFC will not have circles.

00:06:12: So maybe that's okay, one thing which I think good to understand is how this actually works with ZFC or ZF?

00:06:21: No, the middle Z. The three levels are Z, ZF and ZFC.

00:06:28: so the middle of Z theory already had a basic idea.

00:06:34: So there are some axioms which are always about this element relation, when it's something an element of something else.

00:06:41: And they're different kinds of.

00:06:44: the first axiom is the axiome of externality and says if two sets have exactly the same elements that equal right?

00:06:53: But for all x axis in y even only access in z then Y equals to Z has the same element.

00:07:02: But most axioms, not all but the most axios of sets theory are actually axiom which tell you how your construct... How you're allowed to construct sets.

00:07:14: So for example this axiome of pairing it says if you have two sets x and y You can make a new set Which contains X & Y. And yeah some other sets union power set and particularly important separation or limited comprehension.

00:07:33: So if you have a set and the property, then we can make new sets which are the elements of this set that satisfies its properties.

00:07:44: For example here is a set with natural numbers And there's also a property of being.

00:07:48: even You can define it as an even number.

00:07:51: This doesn't allow you to do this Russell paradox because There isn't a set of all sets, so there's no way.

00:07:58: I mean if they would add this then you'd have to paradox.

00:08:00: but in the...there is no axiom that has a set for all sets and hence it avoids those axioms.

00:08:12: Maybe one side remark these three levels are historically slightly inaccurate because Z already contained choice.

00:08:23: Yeah, exactly.

00:08:24: But we make it explicit because we often want to talk about choiceless worlds and maybe then we can do the other footnote.

00:08:32: that choice is so embedded in this very notion of cardinals... The choiceless set theory looks quite different from ZFC.

00:08:45: What's missing?

00:08:45: Then why came Franklin around and said I'm part

00:08:51: Yes, so let's look at first the definition of natural numbers in modern sets theory.

00:08:56: I mean okay this is important that all the important concepts of mathematics could be defined in set theory.

00:09:05: and So as a first example with the natural number we start with empty set And then the set containing the empty set.

00:09:12: and the set contains zero to one of all elements, or numbers smaller than it.

00:09:24: And that's one way to define natural numbers.

00:09:26: and this axiom infinity basically says there is such a set containing the natural number which was invented by von Neumann.

00:09:40: so there are sets containing all the von Neuman numbers Maybe more, I mean this axiom doesn't say that.

00:09:50: actually it's quite interesting.

00:09:51: But then with limited comprehension you can cut down and have the actual natural numbers.

00:09:57: but there are different definitions of natural numbers And actually Zemelo had another one where every natural number is a set of the natural number.

00:10:12: before You start with empty sets It's just a one element set which contains only the previous natural number.

00:10:22: And now

00:10:24: I mean, in some sense this is more natural right?

00:10:26: This would be your first suggestion because for finite numbers it's lovely to count the markets and you know where are but of course at the infinite that breaks down Because we cannot really have infinite curly brackets infinite yet, but you can do this with the von Neumann ordinals.

00:10:50: So I know already said that word where you can say take all natural numbers and unite over them.

00:10:57: You have omega then you can continue from there.

00:11:01: yeah.

00:11:02: And maybe another benefit?

00:11:03: The element symbol now is exactly less than

00:11:09: relation

00:11:10: if you call it a benefit otherwise its successor.

00:11:14: So that might be another benefit, but just to think about these things.

00:11:20: Yes so the axiom which is missing.

00:11:24: if you have one version of serial numbers can you prove then the other version?

00:11:29: It's not exactly an isomorphism, but that idea if you have a set and then you can construct another set by replacing all elements called replacement.

00:11:52: Then this also the set.

00:11:53: The

00:11:54: function image so to speak?

00:11:57: You can define these replacements between for example... If we start with von Neumann natural numbers The Zermelo ones, there's a relation.

00:12:13: and now by replacement you know this is also set.

00:12:18: I think your set reels but we already needed for the naturals right?

00:12:22: Yeah naturals okay

00:12:23: maybe i haven't said that.

00:12:25: Okay may be i misspoke... I meant natural numbers.

00:12:27: yeah There another axiom which he also mentioned the Axiom of Foundation Which was Audi in the Zermelos theory not off-the-form Of building new sets.

00:12:41: It just says that the relation going down in curly brackets is always finite as well-founded.

00:12:53: So there's no set with a cycle we discussed before,

00:13:01: right?

00:13:03: I mean it's philosophically while motivated if you have this iterative concept of sets or building up things because how should these infinitely discreeting sets have been built up, right?

00:13:14: But then the other reply would be that it's also model theoretically very nice because you get rid of a lot of non-standard models.

00:13:23: You really got this B models we talked about.

00:13:28: so but I think for the math is relatively tame i don't but I'm no expert and not well-founded set theories.

00:13:41: I think Peter Axel

00:13:42: is

00:13:43: somebody to ask, Steve Awody who was a guest also had something done about them?

00:13:47: iIm not entirely sure.

00:13:49: yeah alas we can't ask peter anymore.

00:13:51: ,but okay yes so there are actually instead of just giving up foundation you can do the opposite and add anti foundation which allows you now to construct these cyclic sets.

00:14:06: Yeah, now there are these two things I would love to talk about.

00:14:09: And one thing is large Cardinals.

00:14:11: i would like To Talk About them.

00:14:12: we don't give credit to this huge field of set theory that much or because it came up with Joel Hamkins for instance.

00:14:21: Now the other thing.

00:14:22: It Would Be constructive Set theories.

00:14:24: Because When We talked About This Building Up These Sets and That Power Set Is a Weird Thing Maybe I start With Constructive Set Theory Light Which Would be maybe V equals L. So if you build up these satiratic universe by power set, iteration of powerset for the whole length of the ordinals so to speak and we said that the power set is underdetermined in this sense it might be larger than other models.

00:14:59: but there's a smallest model constructive model of set.

00:15:08: three equals L in now, and the classic sense constructive.

00:15:13: And there it's basically you really add an all subsets that are definable because you would always need to add them.

00:15:21: You can never leave out one of those Because you're really can point to them right?

00:15:25: So we get a problem if you leave out One of then.

00:15:27: so these are therefore for sure and For the non-definable things are messy but That's maybe another topic.

00:15:37: You get what is called an inner model of your set theory, something... If you have one model of a set theory this lives within it and that for sure.

00:15:47: And we talked with Dana Scott.

00:15:50: I hope he will have him again.

00:15:52: One the big blows against V equals L as an axiom extension For set theories that you cannot really have large cardinals in them In some stronger sense.

00:16:04: But that's for another episode.

00:16:06: Yeah, and then there is proper...

00:16:07: Maybe we can talk a bit about the continuum hypothesis which you mentioned already maybe in last podcast or last premise?

00:16:19: Can you say it and also mention this constructable model I think given by Gürtel to prove that this was consistent right?

00:16:28: Exactly!

00:16:30: We already mentioned sometimes go as well.

00:16:33: Kanto believed that the power set of natural numbers is the second smallest infinite set.

00:16:39: It cannot be the smallest one because these are the natural numbers and our set is really bigger, but we don't know where it lives actually.

00:16:47: And Kanto wanted to show us that this is also a very productive program which brings up the descriptive set theory and definability again not for today.

00:17:03: And then as you mentioned, Gödel showed that there are models of ZFCs or structures that fulfill everything we want where the power set is indeed the second smallest one.

00:17:14: Namely this V equals L. But and we talked about that in the Dana Scott episode Cohen and this whole Berkeley school were thinking where the reels are very big, so we somehow systematically add reels into their real number line coin reels in that first proof and then the real numbers get bigger than on this being of a second level.

00:17:47: So it's really ZFC will never settle The continuum type with us whether the power set off the natural numbers is Of the second smallest infinite cardinality.

00:17:58: Yes also you're free to add the continuum hypothesis or the negation of the continuum.

00:18:04: And I think we had this multiverse view already by Hamkins that, uh... This is maybe different conceptions on what you mean by a set?

00:18:15: It's not… Yeah so yeah.

00:18:18: I mean classically Set Theory wanted to settle that and they want it settled in two ways both introduced by Grudel.

00:18:25: one was these inner model theory And once was this large cardinal program in.

00:18:31: somehow if you go for bigger and bigger infinities, then you might hope to get a finer model of set theory.

00:18:41: You want to understand it really?

00:18:45: Maybe some how the settles... For the large Cardinal Program until very recently I would have said that it proved not enough.

00:18:57: ever really a candidate showing CH under these assumptions.

00:19:03: And nowadays weird stuff happened for very large cardinals beyond choice, and I don't understand it at all.

00:19:09: so i need to be silent whether this might help or not.

00:19:13: You can quickly explain what the Large Cardinal is?

00:19:16: Yeah sure!

00:19:19: In some sense we already met our first Large Cardinel namely Omega.

00:19:24: So, from nothing below really constructed an infinite set.

00:19:29: You can do power sets as often you want and will never get infinite from the finite one.

00:19:35: so it's inaccessible form below.

00:19:39: It

00:19:40: is a model of set theory without infinity.

00:19:44: Exactly!

00:19:45: And now weird thing happens if we continue these power-set operation for the whole length of ordinals, you would say okay.

00:19:54: You are done now but this will be a model set theory and we know that it cannot exist in... We can not prove its existence because otherwise we would have proved the consistency of ZFC.

00:20:06: Because if there is a model look at consistent.

00:20:09: But This Cannot Happen because ZFC models arithmetic.

00:20:13: so it's prone to Girdel's incompleteness theorem saying No systems being strong enough to do a little arithmetic, so PA is sufficient for that and which consistent can prove its consistency.

00:20:29: So we will never show you build this whole universe, so-to speak, iterating the power sets... And another large cardinal would be… You could say – Do all of it!

00:20:42: The set of all these, in an inaccessible Cardinal, just add them And then of course, you can repeat from there.

00:20:51: You can do a lot of these iterative power set operations and continue to larger and larger cardinals.

00:20:59: If you really play this game a lot ,you go into what's called Malo Cardinals .

00:21:05: Then there is larger stuff after that motivated by other things – reflection principles, wooden cardinals… A lot used to be Reinhardt Cardinals, which was so large that they finally got inconsistent.

00:21:27: How do you know?

00:21:30: I mean...I already have some trouble with plain ZFC but now I mean,

00:21:39: consistency-wise you will not gain anything from them.

00:21:43: If you are worried about ZFC consistency... Yeah

00:21:47: sure let's say okay that actually we have a similar story in type theory which they're called universes.

00:21:58: and the question is how long can?

00:22:05: For type theory we can always say, oh yeah okay.

00:22:08: We can model this with set theory and we're still below power sets but then you take that theory and there is no limit.

00:22:18: so it's not clear.

00:22:21: even if you believe ZFC consistent You don't know whether your large carbons are consistent And at some point actually things become inconsistent.

00:22:34: Yeah, but one should acknowledge two things.

00:22:37: First is I mean now this is the classical story.

00:22:40: Hamkins will disagree.

00:22:42: these large cardinals formed in order so it really went up more and more which is a sociologically interesting phenomenon probably

00:22:51: maybe?

00:22:53: So it's not messy.

00:22:55: Peter Kerner wrote about that wouldn't many others.

00:22:59: And then the other thing.

00:23:00: Nothing turned out to be inconsistent, but the Reinhardt cardinals and they were constructed to be The largest thing you could came up with.

00:23:09: this wasn't natural anymore in the sense of It developed out-of-work.

00:23:14: This was really let's push it to the limit And then things only break.

00:23:18: which is do you

00:23:19: think however?

00:23:21: You add these large cardinals.

00:23:24: They're always included in each other.

00:23:26: so it's not like you can at these cardinals or these.

00:23:30: But

00:23:33: then the footnote.

00:23:34: Hamkins has some candidates for natural large cardinal axioms that don't live on On their linear order.

00:23:42: The classical story is that they do so.

00:23:46: most satirists will say They are all just extending in the universe more and more.

00:23:52: Okay,

00:23:53: yeah should we call it a day?

00:23:55: For our satiristic programs I pitched constructive set theory, but maybe we...

00:24:01: Yes.

00:24:02: I know how to say a few things about constructive.

00:24:04: Yeah, please!

00:24:05: Okay so one is you can try make that theory constructive and this has been tried in the two series iZF and CZF And basically what they do?

00:24:22: They don't use classical logic, they used antigenistic predicate And then they limit the axioms.

00:24:29: So in particular, the axion of choice is omitted or replaced by something weaker and also one of them never known which switch as a power set axiom is also omitted but it's also replaced with something weaker.

00:24:53: I am not a big fan of them, because they seem to be quite artificial.

00:24:58: It's like you take ZFC and then you fix it... And there are no clear whether that is really constructive in the sense if we can prove something exists but also have witness for it.

00:25:13: so existence property i think its unknown as it holds.

00:25:18: So one issue with set theory as far I'm concerned is this non-constructivity, which you can fix but it fixes maybe a bit artificial.

00:25:34: But the other one and maybe we have already talked about this a little bit... ...is that set theory is very intentional in the way you could always talk about elements and how sets are constructed.

00:25:49: And really in mathematics we don't care about how sets are constructed, or how collections are constructed.

00:25:58: We only care of their behavior in a way and so we want to have more exchangeable structural view.

00:26:05: And that's exactly where I think is one of the main advantages of type theory.

00:26:10: That gives us structural mathematics directly because you can... In Type Theory You cannot talk about The elements independently with the elements of a type, which is given.

00:26:25: So you can never look into it as definition of your type.

00:26:30: so there's these two things Which matter to me?

00:26:33: This is why I prefer using Type Theory.

00:26:40: If we want to be constructive then Type Theory seems to be very natural.

00:26:46: The existence property holds by definition And I mean, you can still be... You can still add extra middle or whatever principle you want.

00:26:57: But also not edit and that's nice.

00:27:03: Especially if we think about computer science.

00:27:05: so we're interested in constructions of things which actually run.

00:27:09: the other thing is maybe also related to computer science.

00:27:12: Is this?

00:27:12: That you don't want to reveal implementations here on to do things even being able to hide implementation details and replace one construction by another one, which has the same properties.

00:27:26: And this sort of externality I think is tightly connected to using type theory?

00:27:35: I mean...I should just say that one slight defense.

00:27:40: Pfeffermann may be not most non-constructive person in world but he probably this idea of distinguishing between mathematical and non-mathematical questions.

00:27:56: And they had even like some ideas off CH being a non-athematical question that you get rid of it, I learned that from Matteo de Secchiai... That you might hope that you can abstract away or make precise what's garbage theorems.

00:28:17: But we can make it

00:28:20: easy, right?

00:28:22: The non-gabbage theorems.

00:28:24: So once which you can write down on type theory

00:28:26: Yeah I mean i think there is a lot of back and forth coding...I Think You Can Get A Lot Of Garbage Coded Into Type Tury As Well but maybe that's for another day.

00:28:38: um great here We call It Day Or Maybe Let Me Use This Because this This Can Be Easily Cut Out If You Don't Want To Answer.

00:28:47: I recently heard rumors about a poster of yours in your office giving raising some doubts, but it just stands on set here.

00:28:56: Do you want to elaborate?

00:28:58: Yeah!

00:28:59: No no the opposite... What Neil was saying is that i had uploaded a cartoon about type theory and he says Are you still following this?

00:29:20: We will come back to it.

00:29:22: So another cliffhanger, lovely!

00:29:25: As always thank you all for tuning in and asking questions supporting us via memberships by via coffee or commenting via sharing while discussing with each other.

00:29:38: It starts becoming a nice community.

00:29:40: we already see people sometimes answering to each other, adding historical facts.

00:29:45: So I've now learned a lot looking into the comments

00:29:49: and it's

00:29:52: always keep some coming.

00:29:53: And then see you around.

00:29:56: maybe next week we likely have another special guest who is involved in one of these AI companies revolutionizing math getting us all either empowered or jobless, whatever you want to think about.

00:30:13: That's the best of our words isn't it?

00:30:15: Then see you around!

00:30:17: Bye bye.

New comment

Your name or nickname, will be shown publicly
At least 10 characters long
By submitting your comment you agree that the content of the field "Name or nickname" will be stored and shown publicly next to your comment. Using your real name is optional.