How is the law of excluded middle necessary for proofs by contradiction?

Question

It is claimed that the law of excluded middle : $A \lor \neg A$, is a necessary principle for proving statements by contradiction (i.e. non constructively).

However, in first order logic, at least, proofs by contradiction may go as follows : If $\{T\ \cup \ \neg p\}\vdash p$, then by the deduction theorem, $T \vdash (\neg p \rightarrow p) $, and then by the logical axiom $(\neg p \rightarrow p) \rightarrow p$ and modus ponens, $T \vdash ~p$.

So it seems $A \lor \neg A$ is never used in the above. In what sense is it then needed for non constructive proofs?

Answer 1

A proof by contradiction is not $\{T\ \cup \ \neg p\}\vdash p$. It is $\{T\ \cup \ \neg p\}\vdash \neg q$, where $q$ is a proposition such that $T \vdash q$.

For example, a proof by contradiction may terminates by $0=1$ or $0>1$ or anything else "obviously" (for the point of view of the theory $T$) false. This is why proof by contradiction is also called "proof ad absurdum".

So, in a proof by contradiction, you start with $\{T\ \cup \ \neg p\}\vdash p$ and somehow obtain $\{T\ \cup \ \neg p\}\vdash \neg q$ for some $q$ with $T \vdash q$. So, it means that $\{T\ \cup \ \neg p\}\vdash (\neg q \wedge q)$. This is now where the Law of Excluded Middle is invoked.

Answer 2

I think that part of the problem is in the terminology used: thus, I'll prefer to avoid to speak of "proof by contradiction".

Consider the standard natural deduction rules for propositional logic ; see Dirk van Dalen, Logic and Structure (5th ed - 2013), page 30.

The rules for $\bot$ are :

($\bot$) $$\frac {\bot} \varphi$$

and :

(RAA) $$\frac {\frac {[\lnot \varphi]} \bot } \varphi$$

See also page 157 for intuitionistic logic :

We adopt all the rules of natural deduction for the connectives ∨,∧,→,⊥, ∃,∀ with the exception of the rule RAA.

The law of Excluded Middle and RAA are equivalent is classical logic; see also this post for some details.

A "standard" meta-theorem is [see page 41] :

Lemma

(a) if $\Gamma \cup \{ \lnot \varphi \}$ is inconsistent, then $\Gamma \vdash \varphi$,

(b) if $\Gamma \cup \{ \varphi \}$ is inconsistent, then $\Gamma \vdash \lnot \varphi$.

The proof is done applying (RAA), for (a), and ($\rightarrow$-I), for (b).

---

Added

In an Hilbert-style proof system, usually EM ($\lnot A \lor A$) is not an axiom. We can see the proof system of Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997), based on three axioms :

(A1) $\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{B})$

(A2) $(\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{D})) \rightarrow ((\mathcal{B} \rightarrow \mathcal{C}) \rightarrow (\mathcal{B} \rightarrow \mathcal{D}))$

(A3) $(\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$

and modus ponens as only rule of inference.

We note that (A3) is (RAA) in "Hilbert-form".

Within this system we may prove Ex Falso Quodlibet [see Mendelsom, Lemma 1.11(c), page 39] :

$\lnot \mathcal B \rightarrow (\mathcal B \rightarrow \mathcal C)$

(1) $\quad \lnot \mathcal B$ --- assumed

(2) $\quad \mathcal B$ --- assumed

(3) $\quad \vdash \mathcal B \rightarrow ( \lnot \mathcal C \rightarrow \mathcal B )$ --- (A1)

(4) $\quad \vdash \mathcal{\lnot B} \rightarrow ( \mathcal{\lnot C} \rightarrow \mathcal{\lnot B})$ --- (A1)

(5) $\quad \mathcal{\lnot C} \rightarrow \mathcal B$ --- from (2) and (3) by modus ponens

(6) $\quad \mathcal{\lnot C} \rightarrow \mathcal{\lnot B}$ --- from (1) and (4) by modus ponens

(7) $\quad \vdash (\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$ --- (A3)

(8) $\quad \mathcal{C}$ --- from (5), (6) and (7) by modus ponens twice

(9) $\quad \lnot \mathcal B \rightarrow (\mathcal B \rightarrow \mathcal C)$ --- from (1), (2) and (8) by Deduction Th twice.

As you can see, (RAA) is crucial in the above proof.

Using again (A3), it is easy to prove Double Negation [see Lemma 1.11.a, page 39] :

$\vdash \lnot \lnot \mathcal B \rightarrow \mathcal B$.

In Mendelson's system, $\lor$ is not primitive; it is defined through :

$P \lor Q =_{def} \lnot P \rightarrow Q$.

Thus, Lemma 1.11(a) is simply EM :

$\vdash \lnot \mathcal B \lor \mathcal B$.

Answer 3

Note that the "logical axiom" $(\lnot p \to p) \to p$ actually applies Peirce's law underneath (just subtituting $\bot$ in $Q$ and $p$ in $P$), and we can prove the equivalence of law of excluded middle and Perice's law (see this page). Therefore, you can say you don't need law of excluded middle to complete your proof, but you are introducing Perice's law now.

Hence, constructive logic (used by Coq) not just excludes law of excluded middle by default, but also Peirce's law and some other things that you may deem as axioms in classical logic. You can take a look at the last exercise of this chapter in Logic Foundations and try to solve it out.