3 ms·
It'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.
by tel 4y ago
It'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!