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

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?

-
Which logical system you used for? I think you should provide the logical system which you use. (That is, you should provide the logical axioms and rule of inferences of which you use.) – Hanul Jeon Jul 6 '14 at 3:47
$(\lnot p\to p)\to p$, which you claim is an axiom, is not intuitionistically valid. (The similar-seeming statement $(p\to\lnot p)\to \lnot p$ is valid.) – MJD Jul 6 '14 at 3:58
(This does not address your question exactly, but I wrote a short article about misunderstandings of proof by contradiction in intuitionistic logic, which may be of some help.) – MJD Jul 6 '14 at 4:22
@tetori : I was thinking of Hilbert style deduction system for first order logic. The logical axioms are the boolean tautologies. – user114806 Jul 6 '14 at 4:27
If you're taking the boolean tautologies as axioms, then you've already included the law of the excluded middle in many equivalent forms, and you are not doing constructive logic. – MJD Jul 6 '14 at 4:30

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.

-
If {T ∪ ¬p}⊢(¬q∧q) then {T ∪ ¬p} ⊢p and you can just proceed as in my post. – user114806 Jul 6 '14 at 4:25
@user114806: I don't get the "then" part in your comment. – Taladris Jul 6 '14 at 4:41
Even in intuitionistic logic, $\lnot q\land q$ proves $p$. – MJD Jul 6 '14 at 4:51
MJD : How? In intuitionistic logic q^¬q means "there is a proof of q, and there is a proof that q leads to absurdity". How does that prove (an arbitrary) p? – user114806 Jul 6 '14 at 6:44
@user114806 From $q$ deduce $q\lor p$. From $\lnot q$ and $q\lor p$, deduce $p$. Alternatively, $\lnot q$ is an abbreviation for $q\to\bot$, so from $q$ and $q\to bot$, deduce $\bot$, and from $\bot$, deduce $p$. – MJD Jul 6 '14 at 17:12

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$$

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

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

-