Timeline for Bishop quote stating that axiom of choice is constructively valid
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 22 at 14:50 | history | edited | Christopher King |
edited tags
|
|
| Jan 25, 2017 at 16:51 | comment | added | Ingo Blechschmidt | The term "constructive mathematics" is used with related but subtly different meanings. The lingua franca of the mathematical multiverse is "intuitionistic logic" (classical logic is intuitionistic logic plus the axiom of excluded middle). Sometimes "constructive mathematics" refers to doing mathematics using only intuitionistic logic. But sometimes "constructive mathematics" refers to one of several specific schools, where some further axioms are used (for instance Markov's principle or the anti-classical axiom that any function $\mathbb{R}\to\mathbb{R}$ is continuous). | |
| Jan 24, 2017 at 23:50 | answer | added | Andrej Bauer | timeline score: 29 | |
| Jan 24, 2017 at 20:04 | comment | added | user104007 | A friend of mine gave me this link: michaelt.github.io/martin-lof/… | |
| Jan 24, 2017 at 18:45 | comment | added | Andreas Blass | The axiom of choice says that there exists a choice function for any family of inhabited sets. The hypothesis here is that, for each of the sets in question, there exists an element. When you interpret "for all ... there exists" constructively in this hypothesis, that interpretation amounts to the existence of a choice function. (I've glossed over a lot, in the hope of conveying the essential idea, so watch for Andrej's answer to clarify things.) | |
| Jan 24, 2017 at 18:38 | comment | added | Andrej Bauer | I can explain but need to feed the kids first. | |
| Jan 24, 2017 at 18:25 | review | First posts | |||
| Jan 24, 2017 at 18:27 | |||||
| Jan 24, 2017 at 18:22 | history | asked | user104007 | CC BY-SA 3.0 |