3 ms·
Why does it fail to exist? It’s an axiom that can be added to intuitionistic axiom systems just as well as for classical ones, no? It’s orthogonal to the law of
by quchen 4y ago
Why does it fail to exist? It’s an axiom that can be added to intuitionistic axiom systems just as well as for classical ones, no? It’s orthogonal to the law of the excluded middle after all. In constructive mathematics with AC, you would just call the selected set element AC(your-set).
- tel 4y agoIt's been a while so I've forgotten the details, but I believe in some versions of constructive mathematics AC is enough to derive LEM.
- quchen 4y agoOh hey Tel, do I remember you right from #haskell on Freenode? : - D
- tel 4y agoNot on there a ton, but yes!
- throwaway81523 4y agoThat is called Diaconescu's theorem. https://en.wikipedia.org/wiki/Diaconescu%27s_theorem https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
- tel 4y agoThank you!