4 ms·

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

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

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.