Law of excluded middle

The law of excluded middle (LEM) is the statement that for any proposition $𝑃$ , $𝑃 \lor \neg 𝑃$ . This is accepted in classical logic but rejected in constructive logic, although there are also intermediate logics which accept a weaker form of LEM. Moreover, even in neutral logics one can typically show

\neg \neg (𝑃 \lor \neg 𝑃) .

Informal proof

Let $𝑃$ be a proposition. Suppose towards contradiction that $\neg (𝑃 \lor \neg 𝑃)$ . Then $\neg 𝑃$ holds, for if $𝑃$ held this would contradict $\neg (𝑃 \lor \neg 𝑃)$ . Therefore $\neg 𝑃$ and $\neg (𝑃 \lor \neg 𝑃)$ , which is absurd. Therefore $\neg \neg (𝑃 \lor \neg 𝑃)$ .

Formal statement

In propositional logic we have the axiom schema $𝑃 \lor \neg 𝑃$ .
Under propositions as some types in type theory we have $\forall (𝑃 : P r o p) \to 𝑃 ⊎ \neg 𝑃$ .

Further terminology

A proposition for which LEM holds at the individual level is called decidable. It follows from above that no proposition can be shown to be undecidable internally.
DNE is equivalent to LEM, where one direction follows from the above proof.

Criticisms

One good reason to avoid the LEM is that it tends to destroy the computational content of proofs. The following Brouwerian counterexample is taken from A constructive real projective plane.

If, on the plane $ℝ 2$ , we have a proof of the statement “Given any point $𝑃$ and any line $ℓ$ , either $𝑃$ lies on $ℓ$ , or $𝑃$ lies outside $ℓ$ ,” then we have a method that will either prove the Goldbach conjecture, or construct a counterexample.

Proof

Define $(𝑎 𝑛) 𝑛 \geq 2$ by finite routine to be

𝑎 𝑛 = {0 𝑛 i s t h e s u m o f t w o p r i m e s, 1 𝑛 o t h e r w i s e .

Then apply the statement to the point $(0, \sum \infty 𝑛 = 2 𝑎 𝑛 / 𝑛 2)$ and $ℓ$ being the $𝑥$ -axis. If $𝑃 \in ℓ$ , then we have proved the Goldbach conjecture. If $𝑃 \notin ℓ$ , we have constructed a counterexample.

#state/develop | #lang/en | #SemBr