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?

  • $\begingroup$ 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.) $\endgroup$
    – Hanul Jeon
    Jul 6, 2014 at 3:47
  • 5
    $\begingroup$ $(\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.) $\endgroup$
    – MJD
    Jul 6, 2014 at 3:58
  • 1
    $\begingroup$ (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.) $\endgroup$
    – MJD
    Jul 6, 2014 at 4:22
  • $\begingroup$ @tetori : I was thinking of Hilbert style deduction system for first order logic. The logical axioms are the boolean tautologies. $\endgroup$
    – user114806
    Jul 6, 2014 at 4:27
  • 3
    $\begingroup$ 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. $\endgroup$
    – MJD
    Jul 6, 2014 at 4:30

3 Answers 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.

  • 1
    $\begingroup$ That's not an answer. It's a link to an answer. $\endgroup$ Nov 9, 2021 at 8:36
  • $\begingroup$ @JoséCarlosSantos I think the author knew that it should be a comment, rather than a full-on answer, but lacked the >50 reputation required to comment. (Not that it's an excuse: they could and should expand it into a proper answer) $\endgroup$
    – Z. A. K.
    Nov 9, 2021 at 9:00
  • 1
    $\begingroup$ Ok, I have edited my answer, and I actually did not know it should be a comment, because what follows from my original answer looks apparent to me. $\endgroup$
    – ark
    Nov 9, 2021 at 13:14

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.

  • 1
    $\begingroup$ If {T ∪ ¬p}⊢(¬q∧q) then {T ∪ ¬p} ⊢p and you can just proceed as in my post. $\endgroup$
    – user114806
    Jul 6, 2014 at 4:25
  • $\begingroup$ @user114806: I don't get the "then" part in your comment. $\endgroup$
    – Taladris
    Jul 6, 2014 at 4:41
  • 1
    $\begingroup$ Even in intuitionistic logic, $\lnot q\land q$ proves $p$. $\endgroup$
    – MJD
    Jul 6, 2014 at 4:51
  • $\begingroup$ 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? $\endgroup$
    – user114806
    Jul 6, 2014 at 6:44
  • 4
    $\begingroup$ @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$. $\endgroup$
    – MJD
    Jul 6, 2014 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$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .