Timeline for Collection of proper classes with in CZF
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Dec 11, 2021 at 0:13 | history | bounty ended | ToucanIan | ||
| S Dec 11, 2021 at 0:13 | history | notice removed | ToucanIan | ||
| Dec 8, 2021 at 6:40 | history | edited | ToucanIan | CC BY-SA 4.0 |
deleted 2 characters in body
|
| Dec 8, 2021 at 6:40 | vote | accept | ToucanIan | ||
| Dec 7, 2021 at 16:49 | answer | added | aws | timeline score: 4 | |
| S Dec 4, 2021 at 23:29 | history | bounty started | ToucanIan | ||
| S Dec 4, 2021 at 23:29 | history | notice added | ToucanIan | Draw attention | |
| Dec 1, 2021 at 2:57 | comment | added | ToucanIan | Thank you for the correction. | |
| Nov 30, 2021 at 9:45 | comment | added | Emil Jeřábek | I don’t know why “not necessarily” was removed: it was correct. CZF does not prove that no non-degenerate complete lattice is a set; it is only consistent with CZF that this holds. But on the other hand, classical ZF is also consistent with CZF, and then a plethora of complete lattices that are sets exists. I corrected it using another formulation if you don’t like “not necessarily” for some reason. | |
| Nov 30, 2021 at 9:41 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
added 15 characters in body
|
| Nov 29, 2021 at 21:41 | history | edited | ToucanIan | CC BY-SA 4.0 |
Increased clarity
|
| Nov 28, 2021 at 17:37 | history | edited | ToucanIan | CC BY-SA 4.0 |
Further corrections in light of comments
|
| Nov 28, 2021 at 12:55 | comment | added | Robert Furber | @ToucanIan A singleton is always a complete lattice, and a complete lattice is called trivial iff it is a singleton, i.e. its top and bottom elements are the same ($0=1$). Curi's argument works by showing from GUP that if a complete lattice $L$ is a set, there exists an element $a$ such that $a = \bigvee \emptyset$ and $a = \bigvee L$, so $0 = a = 1$. Therefore every complete lattice that is a set is a singleton, under GUP. | |
| Nov 27, 2021 at 23:42 | history | edited | ToucanIan | CC BY-SA 4.0 |
Correction in light of comments
|
| Nov 27, 2021 at 21:14 | comment | added | ToucanIan | I’m not sure I understand the proof. What does it mean for L to be degenerate and why does L being degenerate imply that L isn’t a set in CZF* + GUP? | |
| Nov 27, 2021 at 3:22 | history | edited | LSpice | CC BY-SA 4.0 |
Typo
|
| Nov 26, 2021 at 23:46 | comment | added | Andrej Bauer | This is just a side comment: you do know thaat no complete lattice which is a set can be exhibited in CZF? See the Main Lemma in these slides by Giovanni Curi. | |
| Nov 26, 2021 at 20:57 | history | asked | ToucanIan | CC BY-SA 4.0 |