One counterintuitive aspect of the axiom of choice is a theorem of Diaconescu and independently Goodman and Myhill that, in some constructive set theories that don't begin with the law of the excluded middle, the axiom of choice implies the law of the excluded middle. But in other systems such as Martin-Löf type theory, the corresponding form of the axiom of choice is completely constructive and does not imply the law of the excluded middle.
|
1 | [made Community Wiki] | ||
|
|
||||
