4 ms·
The C part of ZFC is a challenge for constructive theories
by JonChesterfield 2y ago
The C part of ZFC is a challenge for constructive theories
- sylware 2y agoI recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics. So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
- JonChesterfield 2y agoThe 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.