I recently just started the MIT openware Mathematics for computer science course. The method of proof by contradiction was introduced in one of the lectures, I did not really accept it easily as the other methods such as the proof by contraposition, proof by cases or by a direct proof. This is because what I thought about is: If I assume A and then I find a contradiction, if all my steps were valid and true then A must not be true, but why must it be false, maybe it’s something else that we just do not know about, this is related to the law of excluded middle.

So why is the law of excluded middle true?

What exactly is classical logic and intuitionist logic?

  • 7
    $\begingroup$ Excluded middle is no more true than any other axiom of maths. One must choose to either assume it is true (as an axiom of the logic we use to deduce mathematical truths), or choose to reject it. There are some mathematicians (in the minority) who are called intuitionists who do indeed make the choice not to include the law of the excluded middle. $\endgroup$ Aug 30, 2021 at 17:49
  • 4
    $\begingroup$ If you start with a true statement and apply correct arguments, then you cannot land in a contradiction, assuming you work in a consistent theory. The only remaining possibility is that the original statement is false. It makes no sense to omit this very important tool since many important results can only be derived with a proof by contradiction. Math without this principle is extremely poor. $\endgroup$
    – Peter
    Aug 30, 2021 at 18:01
  • 2
    $\begingroup$ From it's use over thousands of years, there are no known inconsistencies resulting from its application to logical propositions are unambiguously either true or false. It works. It makes sense. It is self-evident. If you want a challenge, you can try to do math without it, but most will find ordinary math challenging enough as it is. $\endgroup$ Aug 30, 2021 at 19:08
  • 1
    $\begingroup$ I hadn't been clear enough: my request for example was a separate question from asking about the motivation of intuitionists. As for being so sure, does one need to be? One can use the law of excluded middle as a reasonable assumption the same way one takes the symmetry of '=' as a built-in given in the language of first-order arithmetic. Since an intuitionist is unwilling assume LEM, is there a stronger reason beyond "I can't be sure that there's no middle position"? To be clear, the domain of discussion here is mathematics and FOL, not philosophy and less "pure" disciplines. $\endgroup$
    – ryang
    Aug 30, 2021 at 19:28
  • 2
    $\begingroup$ @RyanG Regardless of whether you agree with the philosophical arguments of intuitionists, constructive logic has a valuable place in mathematics. Constructive logics are the internal languages of many interesting kinds of categories, especially toposes. You seem to be misunderstanding constructive logic when you request "an accessible example in mathematics where if P is not true, it isn't necessarily false." As I explain in my answer, constructive logic agrees that if $P$ is not true, it is false. $\endgroup$ Aug 30, 2021 at 21:28

2 Answers 2


This is an interesting question and a common mistake that people make when discussing constructive logic (which is also known as intuitionist logic, although in some contexts the terms "constructive" and "intuitionist" have slightly different meanings).

Constructive logic is a form of logic where the claim $P \lor \neg P$ is not assumed to be true. Neither are equivalent logical rules such as $\neg \neg P \implies P$ (double negation elimination) and $(\neg P \implies \neg Q) \implies (Q \implies P)$ (proof by contrapositive). Constructive logic does not claim these three logical rules are wrong. It simply takes no position on whether these rules are valid or not.

Classical logic is constructive logic plus accepting the validity of $P \lor \neg P$. Note that this means anything you can prove with constructive logic can also be proved with classical logic.

The proof that you're outlining is basically using the statement

$$(P \implies \bot) \implies \neg P$$

This rule is known as the "proof of negation" rule.

In case you haven't seen the symbol, $\bot$ is the logical symbol for "False".

This principle is completely valid in constructive logic. In fact, in constructive logic, $\neg P$ is typically defined to be the statement $P \implies \bot$. In other words, $\neg P$ is just shorthand for $P \implies \bot$.

So if you start by assuming $P$ and proving $\bot$ (aka starting with $P$ and deriving a contradiction), then you have proved $P \implies \bot$, which is exactly the meaning of $\neg P$.

The principle that most people have trouble with is the following one: $\bot \implies P$. This principle is known as "ex falso quodlibet" or "the principle of explosion". I personally call it "false implies everything".

This principle is a valid principle in constructive logic. It is always the case that $\bot \implies P$, no matter what $P$ is.

Now if we start with $P$ and derive a contradiction, we have actually started with $P$ and proved $\bot$. This means we have proved $P \implies \bot$. We also get $\bot \implies P$ for free from the "ex falso" rule. So we have actually shown $P \iff \bot$.

In other words, if we start with $P$ and derive a contradiction, we have shown that $P$ and "false" are logically equivalent. That is, we have shown that $P$ is false.

What is not valid in constructive logic is "proof by contradiction". This is the rule stating that

$$(\neg P \implies \bot) \implies P$$

Or, in other words, $\neg \neg P \implies P$. This rule is also known as "double negation elimination".

The "law of excluded middle", which is the principle $P \lor \neg P$, is actually misnamed. In fact, even without the "law of excluded middle", we can still prove that $P$ cannot be neither true nor false. In other words, we can still prove that $P$ doesn't take a "middle value" which is both not true and not false.

Formally speaking, the statement "It cannot be the case that both $P$ is not true, and $P$ is not false" can be stated succinctly as $\neg (\neg P \land \neg \neg P)$. This is because "$P$ is not true" translates to $\neg P$, and "$P$ is not false" translates to $\neg \neg P$.

The statement $\neg (\neg P \land \neg \neg P)$ is just a special case of the Law of Noncontradiction, which states $\neg (Q \land \neg Q)$. The Law of Noncontradiction is always true in constructive logic. In fact, if we expand all the $\neg$s in $\neg (Q \land \neg Q)$ to $\implies \bot$, we get the statement $(Q \land (Q \implies \bot)) \implies \bot$, which is just a special case of modus ponens and is quite straightforward to prove.

I hope this helps! Please comment if you have any questions.

  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$
    – Pedro
    Sep 1, 2021 at 8:40

First things first: Proof by contradiction, double negation elimination ($\mathsf{DNE}$), the law of excluded middle ($\mathsf{LEM}$) and the contraposition principle ($\mathsf{CP}$) are all equivalent. This can be seen from the viewpoint of intuitionistic logic and I have once written down a few of these equivalence proofs in another answer.

Now to "what is the difference between classical and intuitionistic logic?".

To give a conveniently concise answer to this, let's have a look at the following very formal but precise way to specify the deduction rules of intuitionistic propositional logic (IPL):

enter image description here

To give a very quick explanation: Every rule states at the top of the line what you need to show in order to conclude what is below the line. Presenting rules in this way and building proofs with them is know as the system of natural deduction and if you want to know more about this, I can really recommend the write-up on the Lean prover page as a starting point.

So what is now the difference between IPL and classical propositional logic (CPL)? It's simply that CPL has one more rule compared to IPL, namely $\mathsf{DNE}$: $$ \frac{\Gamma \vdash \neg \neg \phi}{\Gamma \vdash \phi} $$ And that's it! The difference is the presence or absence of one single rule and this carries over to the respective predicate logic. This has major consequences to how much information a proof contains, as in classical logic we can give proofs that are themselves non-informative. This is not possible - by design - in intuitionistic logic. And again: all it takes is to leave out one rule.

It can be shown that rule we left out ($\mathsf{DNE}$) cannot be derived from the rules that are still present, but this requires some more work in the form of e.g. a semantics for the logic.

Overall, from the natural deduction viewpoint, this means $\mathsf{LEM}$ is a valid principle in classical logic, as it is build in from the start. Its validity can be further justified by looking at the classical semantics, showing that CPL constitutes a sound logical system. IPL can neither prove nor disprove $\mathsf{LEM}$/$\mathsf{DNE}$, it simply opts to not assume it, and as a benefit from this, intuitionistic proofs are always informative.

(Instead of $\mathsf{DNE}$ we could also have added a rule expressing $\mathsf{LEM}$, $\mathsf{CP}$ or proof by contradiction as they are equivalent by what I mentioned at the start.)

  • $\begingroup$ What do you mean by “ in classical logic we can give proofs that are themselves non-informative”, is this not the case in intuitionistic logic? $\endgroup$ Aug 30, 2021 at 20:01
  • 2
    $\begingroup$ @MohamedShereef No it's not the case for intuitionistic logic; and that is the whole reason people are interested in these kinds of logics. $\endgroup$
    – Léreau
    Aug 30, 2021 at 20:09

You must log in to answer this question.

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