Timeline for In what ways is ZF (without Choice) "somewhat constructive"
Current License: CC BY-SA 3.0
Post Revisions
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 22, 2021 at 3:39 | comment | added | Ingo Blechschmidt | In addition to @RodrigoFreire's nice answer, there is a double negation translation from ZF to IZF, but not from ZFC to IZF. (IZF is basically ZF without LEM. Considering IZF+Choice isn't very useful, as IZF+Choice proves LEM and hence ZFC.) That is, usage of the law of excluded middle can always be mechanically eliminated from any ZF-proof (at the expense of introducing lots of double negations in the formulation of the statement proven). For ZFC this is not the case. In this sense ZF is much closer to being constructive than ZFC. | |
| Apr 14, 2018 at 12:56 | vote | accept | Gro-Tsen | ||
| Apr 14, 2018 at 11:05 | comment | added | Ingo Blechschmidt | Secondly, it's true that some flavors of constructive mathematics accept some forms choice. The full axiom of choice is never adopted in set-theoretic constructive schools, since it entails the law of excluded middle by Diaconescu's theorem. But there are interesting models of intuitionistic logic where countable choice and even dependent choice hold, for instance the effective topos. The situation is different with type-theory based schools of constructivity, where a naive rendition of full choice is trivially provable. There you need "truncation" to formulate nontrivial versions. | |
| Apr 14, 2018 at 10:48 | comment | added | Ingo Blechschmidt | Very interesting question! I believe that Rodrigo's answer settles the main question. Let me just turn to two the asides. A further advantage of constructive proofs is their wider applicability. For instance, any intuitionistic theorem entails a "parameter-dependent version". For instance, the intermediate value theorem in its usual formulation can't be proven intuitionistically, which seems weird on first sight. But if it could, then it would entail that zeros of continuous families of continuous functions can be picked continuously, which is patently false. | |
| Apr 13, 2018 at 13:51 | answer | added | Rodrigo Freire | timeline score: 16 | |
| Apr 13, 2018 at 11:53 | comment | added | Rodrigo Freire | Levy has proved a weak form of the existential property for $ZF$ and $\Pi_2$ sentences in this paper sciencedirect.com/science/article/pii/0020025569900115 | |
| Apr 13, 2018 at 10:44 | comment | added | Asaf Karagila♦ | In the finite power set, you can talk about Dedekind-finite, and then the power set of a Dedekind-finite set might not be Dedekind-finite if you're only assuming ZF. | |
| Apr 13, 2018 at 9:38 | history | asked | Gro-Tsen | CC BY-SA 3.0 |