3 ms·
AC fails to exist, in its normal form, in constructive or intuitionistic formulations of math. This post appeals to that sort of mathematics and thus correctly
by tel 4y ago
AC fails to exist, in its normal form, in constructive or intuitionistic formulations of math. This post appeals to that sort of mathematics and thus correctly identifies that it wouldn’t make sense there.
There are weaker forms of AC which do exist, though. And formulations of math where AC is necessary and obvious, but doesn’t really imply the same thing as classical AC. But these formulations of math are very unlike the classical one we normally enjoy.
For instance, they often disallow the construction of the Reals altogether.
- quchen 4y agoWhy 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!