Timeline for Do all toposes satisfy the internal Zorn's lemma?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 15, 2023 at 17:33 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 18 characters in body
|
| Apr 15, 2023 at 16:58 | comment | added | Simon Henry | That seems to be also equivalent to ZL: If an inductive poset (in either sense) has a maximal chain, then an upper bound for that chain is a maximal element. | |
| Apr 15, 2023 at 16:55 | comment | added | მამუკა ჯიბლაძე | How interesting! Can "every poset has a maximal chain" be weaker than ZL? | |
| Apr 15, 2023 at 16:46 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 20 characters in body
|
| Apr 15, 2023 at 16:36 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 472 characters in body
|
| Apr 15, 2023 at 16:28 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 472 characters in body
|
| Apr 13, 2023 at 18:26 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 69 characters in body
|
| Apr 13, 2023 at 18:11 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 703 characters in body
|
| Apr 13, 2023 at 16:55 | comment | added | მამუკა ჯიბლაძე | Hm I never paid enough attention to D4.5.14. Very interesting, thank you for pointing to it! This mixture of external and internal is extremely confusing, I must say. | |
| Apr 13, 2023 at 14:41 | comment | added | Simon Henry | Regarding ZL+ => LEM. I would say no : if Bell is correct and ZL+ holds in localic topos in which 1 is projective, then I believe the assumption that 1 is projective is weaker than Boolean for a localic topos - it has to do with being of covering dimension 0 or something like that. but I'm not 100% sure of what I'm saying here. | |
| Apr 13, 2023 at 14:34 | vote | accept | მამუკა ჯიბლაძე | ||
| Apr 13, 2023 at 14:34 | comment | added | Simon Henry | Regarding comparison between internal logic and standard set theory the most up-to-date reference is probably MIke Shulman's paper arxiv.org/abs/1808.05204 but I think for my previous comment you can replace "bounded ZF" by Zermelo set theory with no changes | |
| Apr 13, 2023 at 14:34 | comment | added | მამუკა ჯიბლაძე | Oh sorry, I confused myself: you have LEM from the beginning! | |
| Apr 13, 2023 at 14:29 | comment | added | Simon Henry | I'm not sure what to add here. Bell ZL is enough to prove AC (assuming LEM) as you need to apply ZL to the the poset of partial section of a surjective map $X \to Y$ which has supremum of chains. So that it is still in line with my previous comment. I don't know if ZL+ holds in all all localic topos - beyond that Bell says he doesn't know how to prove it. I'm not sure what you are asking about WAC, but from what I can see it is also equivalent to AC under LEM, so also fail in the above-mentioned example. | |
| Apr 13, 2023 at 14:24 | comment | added | მამუკა ჯიბლაძე | Sorry, one more thing - could you give reference for LEM => Bounded ZF? I am way behind the progress it seems, what I remember is that you cannot go beyond the Zermelo set theory... | |
| Apr 13, 2023 at 14:20 | comment | added | მამუკა ჯიბლაძე | Also, his $\mathrm{WAC}$ is about $\neg\neg$-dense version of choice, no? | |
| Apr 13, 2023 at 14:19 | comment | added | მამუკა ჯიბლაძე | Thank you! Can you also clarify the following one? In Remark (2) (on page 1271) he also discusses difference between his $\mathbf{ZL}$ (which requires chains to have suprema) and "ours" which he calls $\mathbf{ZL}^+$. He says he only can prove that the latter persists if $1$ is projective? | |
| Apr 13, 2023 at 14:12 | comment | added | Simon Henry | I looked at Bell's paper as well and to me none of the change is significant in the presence of LEM. I can confirm that LEM + ZL => AC holds: The most convincing argument is simply that the internal logic of a topos with LEM (and NNO) is "essentially equivalent" (up to the change of language...) to Bounded ZF, and this proof doesn't rely on any unbounded replacement. Note that the claim Bell makes about ZL being "Strongly persistent" only means it is valid in all localic Grothendieck topos. Where indeed it is well known that LEM valid <=> the locale is boolean <=> internal/external AC valid | |
| Apr 13, 2023 at 14:06 | comment | added | მამუკა ჯიბლაძე | Great examples, thanks! But are you sure internal Zorn => internal choice goes without problems? I looked into papers by Bell linked to in the comment above by Peter LeFanu Lumsdaine, and there several subtleties are exposed which require some modified formulations of both Zorn and choice... | |
| Apr 13, 2023 at 13:56 | history | answered | Simon Henry | CC BY-SA 4.0 |