Why can't you prove the law of the excluded middle in intuitionistic logic (for layman)?

Solution 1:

If you could prove the law of the excluded middle, then it would be true in all systems satisfying intuitionistic axioms. So we just need to find some model of intuitionistic logic for which the law of the excluded middle fails.

Let $X$ be a topological space. A proposition will consist of an open set, where $X$ is "true", and $\emptyset$ is "false". Union will be "or", intersection will be "and".

We define $U\implies V$ to be the interior of $U^c \cup V$, and $\neg U = (U\implies \emptyset)$ is just the interior of $U^c$.

The system I just described obeys the axioms of intuitionistic logic. But the law of the excluded middle says that $U\cup \neg U = X$, which fails for any open set whose complement is not open. So this is false for $X=\mathbb{R}$, for example, or even for the two-point Sierpinski space.

In fact, intuitionistic logic can generally be interpreted in this geometric kind of way, though topological spaces are not general enough and we need things called elementary topoi to model intuitionistic logic.

Solution 2:

Not knowing how much mathematics experience you've had, it can be difficult to explain the difference in viewpoint.

Intuitionism, and constructive logic in general, are very much inspired by the fact that we as mathematicians do not know the answers to all mathematical questions. Classical logic is based on the idea that all mathematical statements are either true or false, even if we do not know the truth value. Constructive logic does not focus so much on whether statements are "really" true or false, in that sense - it focuses on whether we know a statement is true, or know it is false. Other answers have described this as a focus on proof rather than truth.

So, before someone working in constructive mathematics can assert a statement, she needs to have a concrete justification for the truth of the statement. Arguments such as proof by contradiction are not permitted. The connective "or", in particular, has a different meaning. To assert a statement of the form "$A$ or $B$", a constructive mathematicians much know which one of the two options holds.

One kind of example of how excluded middle fails in this framework was called a "weak counterexample" by Brouwer. Here is one (I don't know if it is due to Brouwer). Consider the number $\pi$. As a fact, even in classical mathematics we do not currently know whether there are infinitely many occurrences of the digit $5$ in the decimal expansion of $\pi$. Let $A$ be the statement "there are infinitely many occurrences of $5$ in the decimal expansion of $\pi$". Then someone working in constructive mathematics cannot assert "$A$ or not $A$", because she does not know which of the two options holds. Of course "$A$ or not $A$" is an instance of the law of the excluded middle, and is valid in classical mathematics.

The key point is that the first difference between constructive and classical logic deals with what it takes to assert a particular sentence. Mathematical terms such as "or", "there exists", and "not" take on a different meaning under the higher burden of evidence that is required to assert statements in constructive mathematics.