4 ms·
The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world
by JonChesterfield 2y ago
The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC.
I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.