What’s the SD on this? Are these people viewed as being complete nuts by mainstream mathematicians? I know that constructive logic is used a lot in computer science, especially formal methods, and it’s especially useful there, but how do real mathematicians view constructivists?
How many mathematicians actually subscribe to this philosophy? How is it reconciled with the rest of mathematics?
There are many thins called constructive mathematics. Some mathematicians (including me) believe that is an interesting subfield of mathematics. My first exposure was to the book Constructive Analysis" by Errett Bishop. In it he shows some fascinating results. Since constructive is very close to computable, this has some obvious applications in computing. The most interesting thing about Bishop’s work was that it gave error estimates. For example, the very definition of continuity rquired giving delta as a computable function of epsilon. This had to be uniform on a closed interval. But armed with that “modulus of continuity” you could estimate how well you find intermediate values, for example. (The intermediate value theorem was false, but you get arbitrary close to one. It is true for polynomials, however, provided the coefficients are constructible numbers.)
Then there is a group of constructivists some place in the SW, maybe New Mexico. The name Fred Richman comes to mind. I heard a talk by him once, but I cannot recall much about it. They do constructive algebra, ring theory and the like.
I suspect that the overwhelming majority of mathematicians regard them as kooks. But then that majority doesn’t know anything about the subject. Some of the sonstructivists are doing it out of interest, without thinking it is the only way to do mathematics. Topos theorists study it as one example of mathematics. Bishop was a TRUE BELIEVER who thought it the only way one could do mathematics. Some years after hsi book was published, he committed suicide and some maintain that he despaired that the masses of mathematics would not see the light.
One thing Bishop did was take classical theorems that made no sense constructively and find their constructive content and prove that. For example, the Brouwer fixed point theorem (every continuous function of a disk into itself has a fixed point) is false; there is a constructive counter-example. But the constuctive content is that for any epsilon > 0, there is a point moved by less than epsilon. Classically such a claim would actually prove the theorem because the disk is compact. This seems paradoxial until I point out that what this is about is that the classical fixed point of even a constructible function of the disk into itself might be a point whose coordinates are not constructible.
Incidentally, topos theorists have proved that any constructively meaningful statement that has a classical proof also has a constructive proof. Unfortunately the argument is itself non-constructive and gives no recipe for going from a classical proof to a constructive proof that could, in principle, be much longer.
Well, I have gone on in greater detail than you wanted, no doubt.
Thanks, that was pretty interesting.