Timeline for What can be preserved in mathematics if all constructions are carried out in ZF?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 27, 2022 at 9:24 | comment | added | Andrej Bauer | @SamSanders: Bishop-style constructive analysis does indeed rely on countable choice (Dependent choice). Choice-free analysis uses Dedekind reals, and is less well-developed, although there is some amount of it. For instance, the HoTT books develops the basics without choice, and there are others. It's easier to do general topology without countable choice. Choice-free algebra has been studied quite a bit and it has its own set of challenges. | |
| Sep 27, 2022 at 7:18 | comment | added | Sam Sanders | One should add that the various attempts to develop (Bishop style) constructive math without (countable) AC have largely dwindled. One can of course do certain theorems/parts of constructive math without any AC, but in the end it seems a lost cause (correct me if I am wrong). | |
| Sep 22, 2022 at 1:44 | history | edited | François G. Dorais | CC BY-SA 4.0 |
fix typos
|
| Sep 21, 2022 at 20:43 | comment | added | Andrej Bauer | @TimothyChow: that's probably hard to figure out, as classic proofs are unlikely paying attenition to where and whether there are essential uses of AC and LEM. But already showing the basic categorical structure of Kan simplicial sets is tricky without LEM – this was a stumbling block for a long while in HoTT, and was resolved by passage to cubical sets. | |
| Sep 21, 2022 at 17:14 | comment | added | Timothy Chow | Just for my own education, I take it that Blakers-Massey for simplicial sets (not just the "synthetic" form of Blakers-Massey) can also be proved without AC or LEM? | |
| Sep 21, 2022 at 15:20 | comment | added | Andrej Bauer | Thanks for your remark, I edited the paragraph to address your question more directly. It's not easy to give a precise technical answer, though, because you're asking about "all math". | |
| Sep 21, 2022 at 15:20 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 1 character in body
|
| Sep 21, 2022 at 14:54 | comment | added | Sergei Akbarov | Andrej, you misunderstand me all the way. I did not say that the orthodox foundations are better than others. I was trying to understand what happens if we remove AC from ZFC, this is not the same. | |
| Sep 21, 2022 at 14:40 | history | answered | Andrej Bauer | CC BY-SA 4.0 |