I would broadly categorize myself as a constructivist rather than a classical logician. Resolves YES if in a year, I still would primarily describe myself this way. See my discussion with @IsaacKing here. Wikipedia overview here.
I will not bet.
Feb 3, 10:59pm: Change my mind: Constructive logic is the only real mathematics. → Change my mind: Will I be a constructivist in a year?
1,000
3.00I don't feel I've changed my mind on this, but the thread has lead to some interesting discussions. Thanks everyone for participating.
I strongly recommend reading this debate between Richard Clark and Michael Hannafin on the topic. I considered myself a constructivist for a few years, but this challenged my viewpoint considerably.
https://drive.google.com/file/d/1pDJiSFjNkHupqcmyhuP1PlxE9DJIeu-X/view?usp=drivesdk
AFAICT, there are these two internally consistent ways to define things like "real", "true", "valid", and you decided that you like one of these more. I think it feels like there's something deeper going on because we (perhaps implicitly) use these to do the meta-level reasoning level about it.
If you're using logic for a specific problem, then it might be answerable as to which of these is more appropriate. But in the absence of a specific purpose, I think it just boils down to aesthetics.
@adele I think you're right that in some sense, this is a matter of aesthetics or taste. People can change their mind about things like that though, so it seemed like a fun opportunity to start a discussion about it.
@VaclavRozhon I guess to stake out a particular claim: I think that the standard undergraduate math curriculum should emphasize constructivism more than it does. For me, I went through my entire undergraduate math major without really hearing anything about constructive mathematics, despite taking several courses on mathematical logic.
Why do I think this? After learning about constructivism while doing research with formal methods in grad school, it seems to me like a constructive approach to math is practically useful. When doing work in a constructive-logic based theorem prover, you get the benefit of, for example, more easily being able to make your bounds concrete.
@BoltonBailey One impression that I get, though I haven't been able to really crystallize this, is that any math that would be useful for an engineering application, it seems like it can always be done in a constructive way. If there were an explicit example of a classical proof about an important behavior of an algorithm that couldn't be explained constructively, that would go ~65% of the way to convincing me to "change my mind", but I also think my bar for the classical explanation being better would be pretty high.
Very compelling to me is Glivenko's theorem about classical provability being equivalent to intuitionistic provability of the double-negation. I feel like this dispenses with the idea that "intuitionism can prove fewer theorems". It seems like it can prove the same same theorems, just that for some of these theorems, our state of knowledge about them can be described with more nuance as: "We know that their statements can't be false/lead to contradiction".
@BoltonBailey Thanks. Being a computer scientist, my view is somewhat different. Basically, instead of thinking "can I prove this without using contradiction?", I think in terms "Can I construct this object with a polynomial-time algorithm?" If it's an infinite question then the analog is something like "Can I construct the i-th bit of the object in poly(i) time?". I think this way of looking at stuff is philosophically quite appealing, with polynomial time being closed on obvious stuff etc. The downside is that not all questions are easily rephrased as questions about existence, but for me, it's fine as my background is combinatorics/computer science where most questions can be thought about in this way. If you want to persuade me about intuitionist logic carving a better boundary for defining "constructiveness", I will happily create an analogous market. :)