Timeline for A simple form of choice
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 4, 2021 at 2:52 | comment | added | Andreas Blass | As far as I can see, your (SC) amounts to adding to the language of ZF a unary function symbol, say $C$, adding to ZF the axiom schema $\forall x\,(x\neq\varnothing\to C(x)\in x)$, and introducing the notation $f_x(0)$ for $C(x)$. Then you should also extend the separation and collection (or replacement) schemas of ZF to allow formulas containing $C$. | |
| Mar 4, 2021 at 1:31 | comment | added | Alec Rhea | @Wojowu Suspecting that my questions here in the comments are too elementary, I asked this question formally over at MSE if you'd like to continue the discussion there. | |
| Mar 4, 2021 at 0:49 | comment | added | Alec Rhea | @Wojowu I'm still slightly confused, sorry Asaf if this is blowing up your notifications. Unless I'm mistaken, we can express choice in ZF as $\forall X((X\neq\emptyset\wedge\emptyset\notin X)\implies\exists f:X\to\bigcup X\forall A\in X(f(A)\in A))$. If we instead use $\forall X(X\neq\emptyset\implies\exists f(f:\{X\}\to X))$ as you suggest above, we have that $\forall X\in\{X\}(f(X)\in X)$ as specified explicitly in the choice axiom right? Where do we lose choice? Apologies if these questions are very elementary, I feel like I'm missing something fundamental here. | |
| Mar 4, 2021 at 0:39 | comment | added | Alec Rhea | @Wojowu Ah, I see what you mean, thank you. | |
| Mar 4, 2021 at 0:38 | comment | added | Wojowu | I assumed $X$ is a set here. You can't quantify over classes in ZF (unless you use an axiom schema), but in NBG that would work. | |
| Mar 4, 2021 at 0:35 | comment | added | Alec Rhea | @Wojowu But $\{X\}$ is empty if $X$ is a proper class. $\{X\cap V_\alpha\}$ contains what it should, even if $X$ is proper. | |
| Mar 4, 2021 at 0:34 | comment | added | Wojowu | Yes, your formula doesn't really accomplish anything more explicit than just postulating existence. For the record I don't see any relevance to $\alpha$, you could also write $\forall X\text{ nonempty}\exists f(f:\{X\}\to X)$. Both your and my version are trivially provable in ZF. | |
| Mar 4, 2021 at 0:18 | comment | added | Alec Rhea | @Wojowu What is wrong with the following? $\forall X\exists\alpha(\exists f(f:\{X\cap V_\alpha\}\to X\cap V_\alpha))$, where we also specify that $X$ is nonempty and that $\alpha$ is an ordinal and $V_\alpha$ is the $\alpha$-th stage of the cumulative hierarchy. I'm sure this is wrong, but I'm trying to understand how; is this still just the existence of a function and not equipping a class with a simple choice function? | |
| Mar 3, 2021 at 23:23 | comment | added | Alec Rhea | @Wojowu Trying to make sure I understand your stipulation, you're saying that a downside to this form of choice that didn't occur to me is the necessity of an extension of the formal language or the addition of an axiom if we want to work in ZF, so there is baggage associated with this form of choice? | |
| Mar 3, 2021 at 22:01 | comment | added | Asaf Karagila♦ | @Wojowu: Yes, you have to add something. You can add an axiom instead that states that $V=\rm HOD$ (up to a set, if you must) and then use that to define a choice function. But that's as good as it gets. Add a symbol, or add an axiom. In either case, it's barely a schema. | |
| Mar 3, 2021 at 21:30 | comment | added | Wojowu | I see, so at any rate you have to expand the language (by this Skolem function). This was my main concern here (as I expressed in comments to the question). | |
| Mar 3, 2021 at 21:24 | comment | added | Asaf Karagila♦ | @Wojowu: As I said, barely. You need to add a Skolem function, essentially, and cheat and use Scott's trick. You're right that applying $f$ to all classes is a third-order action, and I should have been more careful there. | |
| Mar 3, 2021 at 21:12 | comment | added | Wojowu | How would you write the axiom SC in the language of ZF (as a schema or otherwise)? | |
| Mar 3, 2021 at 21:10 | comment | added | Alec Rhea | Very cool, thank you. | |
| Mar 3, 2021 at 21:08 | vote | accept | Alec Rhea | ||
| Mar 3, 2021 at 21:04 | history | answered | Asaf Karagila♦ | CC BY-SA 4.0 |