Sierpiński‘s Theorem

Delve into the intricacies of Second-Order Zermelo-Fraenkel Set Theory as it explores fundamental concepts such as extensionality, empty sets, foundation, unions, and power sets. Dive deeper into cardinality, product notations, the Axiom of Choice, and more.

• Set Theory
• Zermelo-Fraenkel
• Axiom of Choice
• Foundation
• Cardinality

lithanym Follow

Uploaded on Feb 17, 2025 | 6 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. First Master Seminar Talk Sierpi ski s Theorem The generalized continuum hypothesis implies the axiom of choice Felix Rech Advisor: Dominik Kirst June 14, 2019

2. Second-Order Zermelo-Fraenkel Set Theory [Kirst and Smolka 2017] Assume a type ??? and a relation _ _ ??? ??? ????. Extensionality Sets are equal if they have the same elements. Empty Set There is an empty set. Foundation The element relation is well-founded. Union For a given set, we can build the union of all elements. Power Set Every set has a power set. The numerals form a set. Infinity Replacement The image of a set under a functional relation is a set. 2

3. Empty Set There is an empty set. Foundation The element relation is well-founded. ? ?. accessible(?) accessible(?) _ _ is well-founded if all sets are accessible. 3

4. Second-Order Zermelo-Fraenkel Set Theory [Kirst and Smolka 2017] Assume a type ??? and a relation _ _ ??? ??? ????. Extensionality Sets are equal if they have the same elements. Empty Set There is an empty set. Foundation The element relation is well-founded. Union For a given set, we can build the union of all elements. Power Set Every set has a power set. The numerals form a set. Infinity Replacement The image of a set under a functional relation is a set. 4

5. Power Set Every set has a power set. Infinity The numerals form a set. Successor ? ? ? ? Numerals 0 ? + 1 ?( ?) ? ?.? = ? 5 Replacement The image of a set under a functional relation is a set.

6. Second-Order Zermelo-Fraenkel Set Theory [Kirst and Smolka 2017] Assume a type ??? and a relation _ _ ??? ??? ????. Extensionality Sets are equal if they have the same elements. Empty Set There is an empty set. Foundation The element relation is well-founded. Union For a given set, we can build the union of all elements. Power Set Every set has a power set. The numerals form a set. Infinity Replacement The image of a set under a functional relation is a set. ??? ??? ???? 6

7. Notations Cardinality Product ? ? there is a bijection ? ? ?,? ? , ?,? ? ? there is an injection ? ? ? ? ?,? ? ?,? ? Disjoint Union Infinity ? + ? 0,? ? ? ? is infinite ? 1,? ? ? 7

8. Axiom of Choice ? ??? ? ? ???. Fix and ?.?(?) ?.? ? 8

9. Axiom of Choice ? ??? ? ? ???. Fix and ?.inhabited(?(?)) ?.? ? 9

10. Axiom of Choice ? ??? ? ? ???. Fix and ?.inhabited(?(?)) inhabited( ?.? ? ) 10

11. Consequences of the Axiom of Choice Every surjection has a right inverse. Every non-listable set ? satisfies ?. Every infinite set ? has a bijection ? ? ?. Linearity: ? ? or ? ? for all sets ? and ?. 11

12. Continuum Hypothesis ? ?( ) ? ? ?( ) 12

13. Generalized Continuum Hypothesis A infinite ? ? ?(?) ? ? ? ?(?) 13

14. Ordinals Representatives for isomorphism classes of well-orders Definition. A set ? is transitive if ? ? ? ? ? ?. We define the class ? of ordinals inductively: ? is transitive ? ?. ? ? ? ? ?2 , ? = { , ? , , , ? , } 14

15. Ordinals are Representatives Every ordinal is well-ordered by the -relation. Isomorphic ordinals are equal: ? ? ? = ?. Every well-ordered set has a unique isomorphic ordinal. 15

16. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?4(?) 2. ?is an ordinal 3. ? ? 16

17. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?4(?) 2. ?is an ordinal 3. ? ? Assume ? ?. ? ?? 17

18. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?4(?) 2. ?is an ordinal Elements are ordinals. Transitivity: 18 3.

19. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?4(?) 2. ?is an ordinal Elements are ordinals. Transitivity: Assume ? ? ? ? and ? ?. Assume ? ? ? ? and ? ? ?. ? ? 19 3.

20. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?4(?) 1. ? ?4(?) 20

21. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?2? ? ?4(?) ?,? = ? , ?,? ? ? ?2? 21

22. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?2? ? ?4(?) ?,? = ? , ?,? ? ? ?2? 22

23. Hartogs Number [1915] A big ordinal ? ? ? ? ? ?2? ? ?4(?) 1. f ? ?,? = ? , ?,? ? ? ? ? ? ? ? ? ? ? ?2? 23

24. Hartogs Number [1915] A big ordinal ? ? ? ? ? ?2? ? ?4(?) 1. f ? ?,? = ? , ?,? ? ? ? ? ? ? ? ? ? ? ?2? Injectivity: Assume ? ? = ?(?) ? ? ? ? = ? 24

25. Hartogs Number [1915] A big ordinal ? ? ? ? ? 1. ? ?4(?) 2. ?is an ordinal 3. ? ? 25

26. Sierpiskis Theorem [1947] Generalized continuum hypothesis Axiom of choice 26

27. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice 27

28. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice 28

29. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) 29

30. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ?3(?) ?4(?) ? 30

31. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ?3(?) ?3? + ? ?4(?) 31

32. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ?4? ? ?3(?) ?3? + ? ?4(?) < 32

33. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ?4? ? ?3(?) ?3? + ? ?4(?) < 33

34. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ? ?3(?) ?4? ? ?3(?) ?3? + ? ?4(?) < 34

35. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ? ?3(?) ?4? ? ?2(?) ?2? + ? ?3(?) 35

36. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ? ?3(?) ?4? ? ?3? ? ?2(?) ?2? + ? ?3(?) < 36

37. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ? ?3(?) ?4? ? ? ?2(?) ?3? ? ?2(?) ?2? + ? ?3(?) < 37

38. Sierpiskis Theorem [1947] Generalized continuum hypothesis Well-ordering theorem Axiom of choice Fix a set ? (w.l.o.g. large enough). We show ? ?. ? ?4(?) ? ?3(?) ?4? ? ? ?2(?) ?3? ? ?2? ? ? ?(?) ? ? ? ? ? ? 38

39. Sets as Types Existing Class _ _ . Coercion ???????_?? ? ??? ? ??? ? ? . ? ? stands for ? ??? ? ? ? ??? ? ? 39

40. Advantages of Sets as Types Reusable Definitions and Notations ? ? ?,? ? ? ? ? ? ? ? ? ?????????? ? (? ?) ? ????? (? ?) Tracking and Checking of Types ?1 {?,? ???}.? ? ? ? ? is even ? Valid ?1 , Not valid ?1 40

41. Problems with Sets as Types is not valid. element ? ? = ? element ? = element ? 41

42. Eliminators on Sets Inspired by recursion schemes in Coq: numeral_rec ? ???.? ? ? ? Not into arbitrary types! 42

43. Conclusion 1. Higher-order axiomatisation of set theory 2. Hartogs number as a big ordinal ( ? ?) 3. Sierpi ski s theorem: Under GCH, the Hartogs number is big enough. ( ? ?) 4. Main result formalized in Coq (XM + FE) Thank you! Next Goals Type-theoretic version of Sierpi ski s theorem Consistency of the axiom of choice by exhibiting the constructible hierarchy ? 43

44. References Dominik Kirst and Gert Smolka. Categoricity results for second-order ZF in dependent type theory. International Conference on Interactive Theorem Proving. Springer, Cham, 2017. Friedrich Hartogs. ber das Problem der Wohlordnung. Mathematische Annalen 76.4 (1915): 438-443. Wac aw Sierpi ski. L'hypoth se g n ralis e du continu et l'axiome du choix. Fundamenta Mathematicae 1.34 (1947): 1-5. 44