Why can't you prove the law of the excluded middle in intuitionistic logic (for layman)? I am learning about the difference between booleans and classical logics in Coq, and why logical propositions are sort of a superset of booleans:

Why are logical connectives and booleans separate in Coq?

The answer there explains the main reason for this distinction is because of the law of excluded middle, and how in intuitionistic logic, you can't prove this:

Definition excluded_middle :=
  forall P : Prop, P \/ ~ P.


I have seen this stated in many different books and articles, but seem to have missed an explanation on why you can't prove it.

In a way that a person with some programming/math experience can understand (not an expert in math), what is the reason why you can't prove this in intuitionistic logic?
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.
The law of excluded middle can be proved in the following way:

$$
\cfrac{\cfrac{\cfrac{(\lnot\phi)^{(1)}}{(\phi\lor(\lnot\phi))}(\lor I) \qquad \lnot(\phi\lor(\lnot\phi))^{(3)}}{(1)\cfrac{\bot}{\phi}(RAA)}(\lnot E) \qquad \cfrac{\cfrac{\phi^{(2)}}{(\phi\lor(\lnot\phi))}(\lor I) \qquad \lnot(\phi\lor(\lnot\phi))^{(3)}}{(2)\cfrac{\bot}{(\lnot\phi)}(\lnot I)}(\lnot E)}{(3)\cfrac{\bot}{(\phi\lor(\lnot\phi))}(RAA)}(\lnot E)
$$

which is a derivation of $\vdash(\phi\lor(\lnot\phi))$ using the natural deduction rules $\lor I$, $\lnot E$ (equivalent to $\rightarrow E$, since $(\lnot\phi)$ treated as $(\phi\rightarrow\bot)$), $\lnot I$ and $RAA$. Of these only the latter (reductio ad absurdum) is not part of intuitionistic logic and hence LEM cannot be proved in it.

Furthermore, $RAA$ is equivalent to double negation (in particular, deriving $\phi$ from $\bot$ in $(1)$ is actually a derivation of $(\lnot(\lnot\phi))$, the same holds for $(2)$), so if either was included in intuitionistic logic, the proof would hold.

References:


Chiswell and Hodges - Mathematical Logic p.28-29
Van Dalen - Logic and Structure p.156