Comment by JonChesterfield
2 years ago
Homotypy is a constructive one. It drops the assumption that any given proposition is either true or false, on the grounds that lots of propositions are undecidable and that's fine. A consequence of no law of the excluded middle (the p or ~p one) is no axiom of choice, so ZFC isn't going to be compatible with it, but ZF probably is.
Personally I'm convinced constructive maths is the right choice and will cheerfully abandon whatever wonders the axiom of choice provides to mathematics, because I'm not a mathematician and I care about computable functions.
From > [...] is it ever shown that Quantum Logic is indeed the correct and sufficient logic for propositional calculus and also for all physical systems?
( Quantum statistical mechanics: https://en.wikipedia.org/wiki/Quantum_logic#Relationship_to_...