Timeline for A simple form of choice
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 3, 2021 at 21:08 | vote | accept | Alec Rhea | ||
| Mar 3, 2021 at 21:04 | answer | added | Asaf Karagila♦ | timeline score: 5 | |
| Mar 3, 2021 at 21:03 | comment | added | Alec Rhea | @Wojowu I'll consider it while walking the dog, thank you for the input. | |
| Mar 3, 2021 at 21:02 | comment | added | Wojowu | It is still unclear to me how you would write SC in the language of ZF. You should think how exactly you would write it as a first-order formula rather than in English. It seems to me that over NBG both SC and GSC would be equivalent to global choice, but if you claim you want to formulate SC in ZF then I would rather see what it is before making this claim | |
| Mar 3, 2021 at 21:00 | comment | added | Alec Rhea | @Wojowu So you're saying that this axiom is equivalent to choice when formulated in the appropriate background theory? | |
| Mar 3, 2021 at 20:59 | history | edited | Alec Rhea | CC BY-SA 4.0 |
added 17 characters in body
|
| Mar 3, 2021 at 20:59 | comment | added | Alec Rhea | @Wojowu Ah, I'm working in the language of ZF only when talking about SC; when talking about GSC I'm working in the language of full MK. I'll make that explicit above. | |
| Mar 3, 2021 at 20:57 | comment | added | Wojowu | What you want then sounds to me essentially like a global choice function, a class function assigning an element to every nonempty set. Over NBG its existence is equivalent to usual formulations of global choice. I don't think you can formulate it in the language of ZF. | |
| Mar 3, 2021 at 20:54 | comment | added | Alec Rhea | @Wojowu In the same way that we do for fibrations; the definition of a fibration says that Cartesian arrows exist over each arrow in the base category, but we can't choose a specific Cartesian arrow without choice. Similarly, we can know that there is a nonempty set of functions from a singleton to $X$, but unless I'm mistaken we can't pick a specific one to work with unless we have choice. This axiom gives us a specific one to work with, and we can derive choice as a consequence. | |
| Mar 3, 2021 at 20:52 | comment | added | Wojowu | "can we choose a specific one?" is a question which to me doesn't make sense on the grounds of first-order logic. How would you formalize that? | |
| Mar 3, 2021 at 20:51 | comment | added | Alec Rhea | @Wojowu specific Cartesian arrows as opposed to simply knowing they exist; instead of just knowing that a map from a singleton to $X$ exists, we have a specific chosen map to work with. | |
| Mar 3, 2021 at 20:50 | comment | added | Alec Rhea | @Wojowu ZF proves that such a map exists, but can we choose a specific one? This axiom is asserting a choice of a specific function, viewed as a set of doubletons, whose domain is the set containing $0$ and whose codomain lies in the set we want to choose from. Unless I'm mistaken, this is reminiscent of the difference between fibrations and cloven fibrations; we know that Cartesian arrows exist in the total category, but to select a specific one we need choice. If we assume that all fibrations can be cloven, we get the axiom of choice. This axiom is meant to be similar to choosing (cont.) | |
| Mar 3, 2021 at 20:46 | comment | added | Wojowu | Your axiom SC sounds like not an axiom in the usual sense, but rather it seems like you want to extend the language to include such functions (ZF alone proves that for any nonempty $X$ there is a map from a singleton to $X$). If so, then this is reminiscent of Hilbert's epsilon or Bourbaki's tau operators: en.wikipedia.org/wiki/Epsilon_calculus | |
| Mar 3, 2021 at 20:40 | history | asked | Alec Rhea | CC BY-SA 4.0 |