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

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?

Solution 1:

Just to clarify: the intuitionists' rejection of Excluded Middle does not mean embracing $\lnot (A \lor \lnot A)$ for all $A$! Some instances of Excluded Middle are acceptable, namely those for which we can prove either $A$ or $\lnot A$.

With this in mind, two standard examples of classical theorems that are not valid intuitionistically are

Trichotomy For each $x\in\mathbb{R}$ exactly one of the following holds: $x < 0$ or $x = 0$ or $x > 0$.

Or, a particular case: $x = 0 \lor x \neq 0$.

Intermediate Value Theorem If $f:[a, b]\to\mathbb{R}$ is continuous and $f(a) < m < f(b)$ for some $m \in\mathbb{R}$, then there exists a $c\in (a,b)$ such that $f(c) = m$.

(The proof of the Intermediate Value Theorem may not obviously rely on Excluded Middle, but it does rely on the Least Upper Bound property for $\mathbb{R}$ which is also rejected by intuitionists.)

Diagnosing what is "wrong" with them intuitionistically is a bit more subtle than pointing out where they use Excluded Middle. What is usually done is to show that these theorems imply an unacceptable instance of Excluded Middle, and must therefore be rejected.

For Trichotomy, one constructs a "weak counterexample". Let $G(n) \equiv \text{"}2n+4 \text{ is the sum of two primes"}$ for $n \in \mathbb{N}$ (including 0). We then define the following sequence:

$$ a_n = \begin{cases} 2^{-n} & \text{if }(\forall k\leq n)G(k);\\ 2^{-k} & \text{if } k \leq n \text{ is the first number such that } \lnot G(k);\end{cases}$$

The predicate $G(n)$ is decidable: for each $n$, a finite calculation will show whether $G(n)$ holds or $\lnot G(n)$. Hence $(a_n)_{n\in\mathbb{N}}$ is a well-defined sequence. Furthermore, we can prove that it is Cauchy: for each $N\in\mathbb{N}$, compute $G(N)$. If true, then $|a_n - a_m| < 2^{-N}$ for all $n,m > N$; if false, then there is a $k < N$ such that $a_n = 2^{-k}$ for all $n>k$, so $|a_n - a_m| = 0 < 2^{-N}$ for all $n,m > N$. Therefore, $(a_n)_n$ defines a bona fide real number, call it $a$.

Note that nowhere in the proof that $(a_n)_n$ is a Cauchy sequence (or even a sequence) did I use the fact that either $G(n)$ holds for all $n\in\mathbb{N}$ or it fails for some $n$. I only assumed that, for any particular $n$, $G(n)\lor\lnot G(n)$. This is intuitionistically acceptable since we could (in principle) check all prime numbers less than $n$ in order to find a pair whose sum is $n$ or prove by exhaustion that there isn't such a pair.

I claim that $a$ is a (weak) counter-example to Trichotomy's corollary: it is clear from the definition that $$a = 0 \iff (\forall n\in\mathbb{N})G(n),$$ so $$a = 0 \lor a \neq 0 \iff (\forall n\in\mathbb{N})G(n) \lor \lnot(\forall n\in\mathbb{N})G(n).$$ The Right Hand Side of the last equivalence is a "problematic" instance of Excluded Middle: it asserts (intuitionistically) that the Goldbach Conjecture is either proved or refuted. At the time of my writing this, the Goldbach Conjecture remains open, so it is not intuitionistically valid to assert: Goldbach Conjecture $\lor$ $\lnot$(Goldbach Conjecture). It follows that we cannot assert $a = 0 \lor a \neq 0$.

The Intermediate Value Theorem suffers a similar fate, although one can prove (intuitionistically)

Intuitionistic Intermediate Value Theorem. If $f:[a, b]\to\mathbb{R}$ is continuous and $f(a) < m < f(b)$ for some $m \in\mathbb{R}$, then for all $\varepsilon > 0$ there exists a $c\in (a,b)$ such that $|f(c) - m| < \varepsilon$.

Even if we cannot "rescue" all theorems proved using Excluded Middle (e.g. by finding proofs that circumvent Excluded Middle), we can often prove analogous theorems that are "close enough" and classically equivalent -- although not intuitionistically equivalent!

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

Solution 3:

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.