Law of Excluded Middle Controversy

Basically, the "issue" is, that with LEM you can "decide" things that a machine or (a person) could never decide on their own.

Pick two random reals $a,b$. Then obviously $a<b, a>b$ or $a=b$, right? But if $a=b$, how would you ever know that? You start comparing the digits of $a$ and $b$ and find that they are all the same, but you can never know for sure, because the sequences of digits are infinite. Hence, the program comparing two numbers would never halt, if they are the same.

That is the basic idea of constructive mathematics: If a program can't decide, then it is simply undecidable. And so, it is constructively not a theorem, that for all reals $a,b$ we have $a<b, a>b$ or $a=b$.

Another issue is, that in the same fashion for any property $\phi$, there is an $x$ with $\phi(x)$ or there is no $x$ with $\phi(x)$, according to LEM. But this makes no sense constructively: "there exists" means "I can find one", but for example: Given a continuous function $f : [a,b] \to \mathbb{R}$ with $f(a) < 0$ and $f(b)>0$, you know that, classically, there is an $\xi$ with $f(\xi) = 0$, but you cannot necessarily find that exact $\xi$, you can only approximate it. This is why this theorem fails constructively (but it works if you only claim that a zero can be approximated)

I should mention: the axiom of choice implies the non-constructive existence of various objects, so it should come as no surprise, that it implies LEM in constructive mathematics (Diaconescu's theorem).

The law of excluded middle (LEM) is the crucial ingredient in any proof by contradiction (as opposed to proof of contrapositive). The objection to LEM is most easily understood in this context.

Some proofs by contradiction establish the existence of this or that mathematical object. Constructively speaking, the problem with a proof by contradiction is that it does not provide any indication of how such a mathematical object is to be found or described specifically.

Briefly put, the constructivist claim is that existence is construction, rather than proof of impossibility of nonexistence.

The constructive mindset leads one quite far afield and leads to startling conclusions, such as the idea that the traditional extreme value theorem could be false constructively.

To understand this concept intuitively, notice that there is no way to find an approximation to such a claimed extremum. This is because the extremum is not a continuous function of the input function, as one easily convinces onself by looking at simple examples of a function with two "humps" of about the same height.