3 ms·

It's really hard to see the history of the sciences especially in the last couple of centuries as anything but a resounding success of modern mathematics. Whate

It's really hard to see the history of the sciences especially in the last couple of centuries as anything but a resounding success of modern mathematics. Whatever qualms some people may have about classical mathematics, nobody has shown it to entail a contradiction, nor has any practical result obtained in physics, engineering or anywhere else been shown to be erroneous for mathematical reasons (modelling errors, of course, happen all the time, no matter what mathematics you use). All the issues such as Banach-Tarski disappear once you apply mathematics to real-world things. Meanwhile, classical mathematics remains insanely practical. People like you, who call Cantor's work "hot garbage", are giving constructive mathematics, which by itself can be a very useful additional way of doing maths, a bad name. Cantor's diagonal argument, for example, doesn't just disappear in a constructive framework.

andrewla 2y ago
I would argue that all the success of mathematics in modern times has been the result of constructive branches of mathematics. Where has anything useful been achieved from a non-constructive premise? Physicists and engineers are notoriously imprecise with their use of mathematics -- "all functions are integrable" and "all matrices are invertible", etc., and that's where all the real-world uses of mathematics have yielded results. I would love to hear examples where non-constructive techniques have yielded anything of interest. There have been places, for sure, where mathematicians working in those spaces have emerged with real and interesting work (Turing and von Neumann come to mind) but their work ultimately fits well within the bounds of intuitionism.
- Tainnor 2y ago
  The point "most of actually useful mathematics can be recast into a constructive framework" is a much more reasonable one than your previous one, that Cantor's work was "hot garbage" (even though of course diagonalisation is constructively valid). That said, few working mathematicians are working in a constructive framework, so almost everywhere modern mathematics is successfully used in practice (e.g probability theory), it is based on classical methods, no matter whether it could be theoretically proved constructively or not. Classical proofs are often shorter and more elegant.
  - andrewla 2y ago
    Few working mathematicians, yes, but a growing number. Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. Yes, it's true that many classical proofs are shorter and more elegant than constructive proofs. My impression (my intuition?) is that working mathematicians generally have a strong intuition as to whether a non-constructive proof can lead to a constructive argument as opposed to being a purely abstract axiom-of-choice trick of formalism. That is, you get the feeling of whether it's a question of "can be constructed, but I don't know how just yet" vs. "absolutely almost by definition cannot be constructed" and the proofs are weighted accordingly. There's a huge amount of discussion as to when the law of the excluded middle can be applied constructively which is very interesting as well; with discussions about narrowing what a "proof by contradiction" vs "proof by negation" means in particular that are really trying to explore how many classical proofs are intrinsically constructive, to hopefully narrow the gap in proof elegance over time. Probability theory remains an area where classical methods still hold pretty firm sway, despite the fact that Kolmogorov himself was pretty strongly in favor of intuitionism. It remains one of the bastions of measure theory, which remains the most pervasive intrusion of non-constructive mathematics into practical mathematics.
    - Tainnor 2y ago
      > Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. I think one big reason Lean is much more popular among mathematicians than Coq ever was is that Lean is pretty unabashedly classical (that, and mathlib). That said, for people who care about program verification, Coq might be the better choice. I'm not anti-constructivism where it makes sense.

andrewla 2y ago

I would argue that all the success of mathematics in modern times has been the result of constructive branches of mathematics. Where has anything useful been achieved from a non-constructive premise? Physicists and engineers are notoriously imprecise with their use of mathematics -- "all functions are integrable" and "all matrices are invertible", etc., and that's where all the real-world uses of mathematics have yielded results. I would love to hear examples where non-constructive techniques have yielded anything of interest. There have been places, for sure, where mathematicians working in those spaces have emerged with real and interesting work (Turing and von Neumann come to mind) but their work ultimately fits well within the bounds of intuitionism.

Tainnor 2y ago
The point "most of actually useful mathematics can be recast into a constructive framework" is a much more reasonable one than your previous one, that Cantor's work was "hot garbage" (even though of course diagonalisation is constructively valid). That said, few working mathematicians are working in a constructive framework, so almost everywhere modern mathematics is successfully used in practice (e.g probability theory), it is based on classical methods, no matter whether it could be theoretically proved constructively or not. Classical proofs are often shorter and more elegant.
- andrewla 2y ago
  Few working mathematicians, yes, but a growing number. Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. Yes, it's true that many classical proofs are shorter and more elegant than constructive proofs. My impression (my intuition?) is that working mathematicians generally have a strong intuition as to whether a non-constructive proof can lead to a constructive argument as opposed to being a purely abstract axiom-of-choice trick of formalism. That is, you get the feeling of whether it's a question of "can be constructed, but I don't know how just yet" vs. "absolutely almost by definition cannot be constructed" and the proofs are weighted accordingly. There's a huge amount of discussion as to when the law of the excluded middle can be applied constructively which is very interesting as well; with discussions about narrowing what a "proof by contradiction" vs "proof by negation" means in particular that are really trying to explore how many classical proofs are intrinsically constructive, to hopefully narrow the gap in proof elegance over time. Probability theory remains an area where classical methods still hold pretty firm sway, despite the fact that Kolmogorov himself was pretty strongly in favor of intuitionism. It remains one of the bastions of measure theory, which remains the most pervasive intrusion of non-constructive mathematics into practical mathematics.
  - Tainnor 2y ago
    > Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. I think one big reason Lean is much more popular among mathematicians than Coq ever was is that Lean is pretty unabashedly classical (that, and mathlib). That said, for people who care about program verification, Coq might be the better choice. I'm not anti-constructivism where it makes sense.