Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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.

share|cite|improve this answer
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$$

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] :


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

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.