3 ms·

I mean absolutely no disrespect to anyone doing serious work in CT or in Haskell - and I'm actually very interested in Haskell as a language per se and have bee

I mean absolutely no disrespect to anyone doing serious work in CT or in Haskell - and I'm actually very interested in Haskell as a language per se and have been exploring it more in recent months - but having spent some time in Haskell communities, I have to agree. There's a lot of empty posturing by people who don't really seem to understand a lot of mathematics but still seem to have very strong convictions about certain aspects of it (constructivism is another such thing).

btilly 4y ago
I'm curious why you call out constructivism. I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof." To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system. Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.
- Tainnor 4y ago
  > I've only really seen constructivism talked about by people who actually have a strong math background. Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it. But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen some NJ Wildberger video where he shittalks the real numbers. So it's not even just constructivism per se, more this mix of unprincipled finitism + constructivism + no axiom of choice (or any mixture thereof), as opposed to anything grounded in some rigorous methodology. Basically the "I don't understand set theory or logic but I've heard that Banach Tarski is weird, so mainstream mathematics must be full of shit". You'd think people wouldn't have hot takes about mathematics, but somehow they do.
  - btilly 4y ago
    I'm glad I haven't seen that then. But conversely it does annoy me to see classical mathematicians dogmatically claim as true statements that depend on their philosophy. And that I have seen a lot of. As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.) But can we agree to both dislike people who argue that 0.999... is not 1?
  - krsrhe 4y ago
  - zozbot234 4y ago
    You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible. And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").
    - btilly 4y ago
      In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.) As for choice, try doing much functional analysis without Zorn's lemma. There are parts of math that you can do constructively. But most of it you really can't. And choice is embedded in a lot more math than you'd guess.
      - zozbot234 4y ago
        > In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." [T]he two disagree on what a function is. Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsense. In many ways, it ought to be a lot easier for someone committed to constructivist semantics to grok a classical development than the converse - because decision procedures, computations etc. are way more of an afterthought to mainstream mathematicians.

btilly 4y ago

I'm curious why you call out constructivism. I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof." To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system. Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.

Tainnor 4y ago
> I've only really seen constructivism talked about by people who actually have a strong math background. Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it. But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen some NJ Wildberger video where he shittalks the real numbers. So it's not even just constructivism per se, more this mix of unprincipled finitism + constructivism + no axiom of choice (or any mixture thereof), as opposed to anything grounded in some rigorous methodology. Basically the "I don't understand set theory or logic but I've heard that Banach Tarski is weird, so mainstream mathematics must be full of shit". You'd think people wouldn't have hot takes about mathematics, but somehow they do.
- btilly 4y ago
  I'm glad I haven't seen that then. But conversely it does annoy me to see classical mathematicians dogmatically claim as true statements that depend on their philosophy. And that I have seen a lot of. As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.) But can we agree to both dislike people who argue that 0.999... is not 1?
- krsrhe 4y ago
- zozbot234 4y ago
  You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible. And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").
  - btilly 4y ago
    In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.) As for choice, try doing much functional analysis without Zorn's lemma. There are parts of math that you can do constructively. But most of it you really can't. And choice is embedded in a lot more math than you'd guess.
    - zozbot234 4y ago
      > In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." [T]he two disagree on what a function is. Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsense. In many ways, it ought to be a lot easier for someone committed to constructivist semantics to grok a classical development than the converse - because decision procedures, computations etc. are way more of an afterthought to mainstream mathematicians.