3 ms·
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 undecid
by JonChesterfield 3y 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.
- westurner 3y agoFrom https://news.ycombinator.com/item?id=37430759#37441973 https://news.ycombinator.com/item?id=37430759#37441973 : > Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations," Optional Axiom of Choice, Complex Wave functions: https://en.wikipedia.org/wiki/Wave_function https://en.wikipedia.org/wiki/Wave_function , Quantum logic, https://news.ycombinator.com/item?id=37367951#37379123 https://news.ycombinator.com/item?id=37367951#37379123 : > [...] 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_statistical_mechanics https://en.wikipedia.org/wiki/Quantum_statistical_mechanics ) Quantum logic > Relationship to other logics: https://en.wikipedia.org/wiki/Quantum_logic#Relationship_to_other_logics https://en.wikipedia.org/wiki/Quantum_logic#Relationship_to_...