It is obvious that in constructive mathematics, you cannot use the law of excluded middle. What else would be the reasons for not adopting constructive stance in mathematics?
This is a philosophical question rather than a mathematical one, although mathematical results can provide significant insight.
On its own, not being able to use excluded middle is not a justification for constructive logic any more than being able to use excluded middle is a justification for classical logic. The justification comes in the benefits that are derived from avoiding excluded middle, or are derived from using it.
Classical logic is the logic of structures - of things that "exist" in some sense, or at least have objective properties independent of whether we can verify those properties. Thus, for example, if I have a function that assigns each real number either "red" or "blue", then either every real number is assigned "red" or some real number is assigned "blue". That latter fact is not "constructively provable" - because constructive mathematics is not about what is true as much as it is about what we can verify (of course, anything we can verify to be true is true). Just because I know that "not every real number is assigned red" does not mean that I actually know a specific real number that is assigned "blue", and thus I have no way to verify that some real number is assigned "blue" even though I know, classically, that there must be one.
Thus, in a sense, classical logic is the logic of truth and constructive logics are logics of verification. By verification I mean more than just "proof"; I mean the sort of thing that is captured in the BHK interpretation. In settings where we are interested in that sort of verification - for example, in computable mathematics - a constructive logic will work well. In settings where we simply want to reason about truth, rather than about concrete verification, classical logic is better. Most mathematicians are interested in reasoning about mathematical objects, and because of this they use classical logic.
|show 3 more comments|
Historically the main reason that Hilbert and others have rejected constructive mathematics was because it mean that they have to use more restricted ways of reasoning and some felt that forbidding PEM in mathematics is to tie the hands of mathematician. Or in another colorful language due to Hilbert, it felt as being expelled from "Cantorian Paradise" of set theory (Mathematicians are very conservative people regarding mathematics).
It also seemed that by accepting constructivism one needs to throwing away a considerable amount of mathematics developed by that time. Even more troubling for them was the fact that some classical results become not just unprovable but false in their literal constructive reading! (Not very surprising after all, you can't expect much if you try to read an English sentence as if it is written in French.)
For that matter, the rejection was not as philosophical as it might seem. Hilbert himself was a finitist. He saw ideal objects as means that help one prove results, but he thought that they are not really needed. One of the goals of his proof theory program was to make sure that using "ideal" objects like abstract sets and real numbers does not lead to incorrect results about "real" objects like natural numbers.
In addition, stating or proving results in a constructive way is often not straight forward. The constructive language takes into account information when we talk about mathematical objects. How an object is represented and given becomes important. Classically equivalent concepts (e.g. $\lnot (\lnot p \land \lnot q)$ vs. $p \lor q$, Dedekind real numbers vs. Cauchy real numbers, etc.) become distinct.
I would suggest having a look at Bishop style constructive mathematics. Bishop tried to address these issues and obtain a constructive mathematics which is compatible with classical mathematics and would be more acceptable for classically minded mathematicians.
Another issue, as mentioned in the comments, was that at some point Godel proved that from the perspective of security of mathematical foundations, there is not much difference between classical and constructive. Simplified, this means that proving a result classically is the same as proving the Godel translation of the result constructively. So the main original supportive argument for constructive mathematics (i.e. it is more secure) became useless.
Constructive mathematics suffered a continuous decline among mathematicians until its relevance to computers become clear. It seems to me that eventually the relation with computational mathematics (e.g. Martin-Löf style type-theory) was a more important factor in revival of constructive mathematics that philosophical issues. (Bishop style constructivism also had a considerable effect).
One justification I've heard is something like this: one of the purposes of constructive mathematics is that it is closer to being applicable in the real world. But non-constructive methods are useful for getting to results more expediently. Once a result is proven non-constructively, its constructive content (and hence is real-world applicability) can be investigated.