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

Question

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?

Answer 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.

Answer 2

Intuitionistic logic, a.k.a. constructive logic, differs from classic logic in that it focuses on 'provability' of a statement rather than 'truth'.

In classical logic, all propositions are considered to be either true or false; one xor the other.   However in constructive logic, a proposition is only ever considered definitely true or false if it can be justified to be so (either by direct evidence or logical proof); otherwise its truth is indefinite.   Thus the middle is not excluded.

Answer 3

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.