3 ms·

> [Intuitionism] and constructivism are a much better framework for reasoning about mathematics. Just for the sake of non-mathematicians, allow me to note here

by xyzzyz 4y ago

> [Intuitionism] and constructivism are a much better framework for reasoning about mathematics. Just for the sake of non-mathematicians, allow me to note here that despite intuitionism/constructivism being around for many decades, 99%+ of mathematics research done today is not, in fact, performed in these frameworks. These are just a curiosity that few working mathematicians actually care about. These approaches do have some certain philosophical benefits, but they have some extreme practical disadvantages that result in overwhelming majority of mathematicians rejecting the notion that these are “better frameworks”. Your comment to me reads like saying that autogyro is a better framework for powered aviation than fixed wing or helicopters: regardless of your actual arguments in its favor (which may in fact be good), the fact that 99%+ of the industry disagrees is rather telling.

librexpr 4y ago
In addition to this, I'd like to add that intuitionistic logic is consistent if and only if classical logic is. This follows from the Godel-Gentzen negative translation[0], which implies that for any contradiction in classical logic, you can get the same contradiction in intuitionistic logic more or less by adding "not not" before both sides of the contradiction. The same applies to the axiom of choice: set theory with choice is consistent if and only if set theory without choice is consistent[1]. This means that you don't get any safety by rejecting the law of excluded middle, nor by rejecting the axiom of choice. For this reason, I think intuitionistic logic is trading away a lot of power for basically no gain. [0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg... [1] https://en.wikipedia.org/wiki/Axiom_of_choice#Independence https://en.wikipedia.org/wiki/Axiom_of_choice#Independence

by xyzzyz 4y ago

librexpr 4y ago

In addition to this, I'd like to add that intuitionistic logic is consistent if and only if classical logic is. This follows from the Godel-Gentzen negative translation[0], which implies that for any contradiction in classical logic, you can get the same contradiction in intuitionistic logic more or less by adding "not not" before both sides of the contradiction. The same applies to the axiom of choice: set theory with choice is consistent if and only if set theory without choice is consistent[1]. This means that you don't get any safety by rejecting the law of excluded middle, nor by rejecting the axiom of choice. For this reason, I think intuitionistic logic is trading away a lot of power for basically no gain. [0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg... [1] https://en.wikipedia.org/wiki/Axiom_of_choice#Independence https://en.wikipedia.org/wiki/Axiom_of_choice#Independence