/sci/ - Science & Math

>>15241217
It's a broad term. People like Wildberger and people like the HoTT crowd could well both be called constructivists, but probably don't know of each other at all.
>>15241464
I don't think there's all too many people who advocate classical mathematics breaking constructive math - and then so it's really just an appeal to keep more track of what principles you use.
On the one hand, there is Russian constructivism on the one hand, which with modern computability theory can be said to sit within the classical theory. I think it's fair (and actually fun) to keep track of when you compute something computable (recursive) and be aware of when you leave this - this programmability. Something like this is baked into type theorists work.
Somewhat relatedly, either more conservatively or orthogonal to that, there's finitists. I think you can let them do what they enjoy and don't engage when you go beyond it.
Then there's Browerian analysis, which is finitist in a sense, but uses classical math breaking axioms. "If you can evaluate a higher order function, F(f) in N, then the fact that your were able to evaluate means you inspected only finite amount of data from f." I think this not out of bound conceptually, and just shows how classical math, where it doesn't hold, is build in a loosey goosey hopeful manner.
But nobody after WWII was really interested into such a hardcore intuitionism, so who do you even insult if you reject it.
tl;dr I don't think it's too much to ask to keep track when you leave computable functions. I think people are just afraid of seeing [math]\neg\neg[/math] in their formulas. But they say something.