Which theorems of classical mathematics cannot be proved without using the law of excluded middle?

Question

The law of excluded middle is a logical principle that says that for any sentence $A$, the sentence $A\lor\,\neg A$ is true. This is a valid law of classical logic, but is rejected by intuitionistic logic. However, for some the proofs of mathematical theorems that use the law of excluded middle, there exists an alternative proof of the theorem that does not use the law of excluded middle. Is there any theorem of classical mathematics that cannot be proved without using the law of excluded middle?

Answer 1

Well what do you mean by "theorem of classical mathematics"? The answer is going to change depending on how you define it.

If for example you have first-order theory over a language with a predicate symbol $P$ that has no axioms at all. Then $\forall x\ ( P(x) \lor \neg P(x) )$ is a theorem, but is not provable in intuitionistic logic.

For a more crucial example, take any formal system $S$. Then "$S$ is consistent or $S$ is inconsistent." is a classically valid sentence but not provable intuitionistically. So not having classical logic makes one unable to state intuitively true facts.

Answer 2

There are quite a few other common theorems we cannot prove without some level of classical logic (but which do have constructive analogs).

Analysis

For example, the following two theorems cannot be proved in constructive logic:

The Cauchy Sequence real numbers form a complete metric space.

The Cauchy Sequence and Dedekind Cut definitions of the real numbers are equivalent.

To prove the above two facts, it suffices to assume the "very weak choice principle". This very weak choice principle states: suppose that $P$ and $Q$ are predicates on $\mathbb{N}$. If $\forall n \in \mathbb{N}, P(n) \lor Q(n)$, then there is some function $f : \mathbb{N} \to \{0, 1\}$ such that for all $n \in \mathbb{N}$, if $f(n) = 0$ then $P(n)$, and if $f(n) = 1$ then $Q(n)$. This fact is easy to prove using classical logic - define $f(n) = 0$ if $P(n)$, and $1$ otherwise. Many constructivists assume this axiom (or a stronger version such as countable choice). The three major schools of constructivism - Bishop's school, Markov's school, and Brouwer's school - all assume a version of countable choice strong enough to imply the above.

Other examples include the intermediate value theorem (see ryan221b's answer) and the mean value theorem. There is an approximate version of the mean value theorem; as far as I can tell, it appears to require the very weak choice principle mentioned above.

Finally, a kicker: without classical logic, it's impossible to prove

Not all functions $\mathbb{R} \to \mathbb{R}$ are continuous.

It's perfectly consistent with constructive logic that all such functions are continuous - in fact, any such function that can be defined constructively can be constructively proved to be continuous.

Cardinality

Another example of a theorem which cannot be proved constructively is the Schroder-Bernstein theorem, which states that if there is an injection $A \to B$ and an injection $B \to A$, one can find a bijection between $A$ and $B$. This theorem is actually equivalent to the Law of Excluded Middle!

The fact that every subset of a finite set is finite is equivalent to Excluded Middle (in fact, even saying that every subset of a 1-element set is finite is equivalent to Excluded Middle).

The fact that every set whose elements can be finitely enumerated is finite is also equivalent to Excluded Middle (in fact, it suffices to consider sets of the form $\{x_1, x_2\}$).

More starkly, without the law of excluded middle, one cannot rule out the existence of an injective function $\mathbb{N}^\mathbb{N} \to \mathbb{N}$. This really throws the whole idea of "cardinality as size" out the window.

Algebra

Plenty of results in algebra rely on the axiom of choice. Since this axiom in turn proves Excluded Middle, these results are not constructive. Examples of such theorems are that every vector space has a basis, or that every nonzero ring has a maximal ideal.

Other examples which are equivalent to excluded middle include

• $\mathbb{Z}$ is a Principle Ideal Domain
• Every subspace of a finite-dimensional $\mathbb{R}$-vector space is finite-dimensional
• Every quotient of a finite-dimensional $\mathbb{R}$-vector space is finite-dimensional

Other unprovable statements which are weaker than excluded middle but still can't be proven include

• Every $\mathbb{R}$-matrix can be put into row-reduced echelon form
• Every square $\mathbb{R}$-matrix is either invertible or not

However, much of algebra is constructive. For example, an identity holds for all groups (or all rings, or all monoids, etc.) if and only if it can be proved constructively from the group axioms.

Number Theory + Computability Theory

There are actually quite a few statements in number theory which are equi-provable under classical and constructive logic. In particular, any intuitionistically $\Pi_2$ statement is provable constructively if and only if it's provable classically. A $\Pi_2$ statement is one which can be phrased as $\forall m \exists n P(n, m)$, where all the quantifiers occurring in $P$ are bounded (meaning that they are of the form $\forall a \leq b$ or $\exists a \leq b$). This includes many open problems like the twin primes conjecture, the $3n + 1$ conjecture, the Goldbach conjecture, Landau's conjecture, Schinzel's hypothesis, Legendre's conjecture, the weak Bunyakovsky conjecture, $P \neq NP$, and more.

However, there are some statements which are not provable constructively.

For every unary primitive recursive function $f : \mathbb{N} \to \mathbb{N}$, either there is some $n$ such that $f(n) = 0$, or for all $n$, $f(n) \neq 0$.

Not all functions $f : \mathbb{N} \to \mathbb{N}$ are computable.

In fact, any function $\mathbb{N} \to \mathbb{N}$ which can be defined constructively can also be constructively proved to be computable.