nLab proof by contradiction

Idea

The method called proof by contradiction is a method of formal proof using the principle of excluded middle.

This principle says that for $P$ any proposition, then it or its negation is true. (The ‘or’ here is meant internally, as a formal disjunction $P \vee \neg P$.) One also speaks of classical logic if this principle is taken to hold.

But this principle implies that in order to prove a proposition $P$ it is sufficient to show that its negation is false, hence that assuming that $P$ were not true would lead to a “contradiction”. This is proof by contradiction.

Proof by contradiction is used frequently in classical mathematics.

While this method of proof is classical, it has some peculiar consequences. Notably when $P$ is an existential statement of the form “there exists an object $X$ with the property $Y$”, then a proof of such existence by contradiction alone gives no means to actually construct an example.

Therefore one also says that proof by contradiction is “non-constructive” and that an alternative proof not invoking the principle of excluded middle (if it exists) is a “constructive” proof, see at constructive logic and constructive mathematics.

Relation to refutation by contradiction

One should take care to distinguish proof by contradiction from refutation by contradiction (also called proof of negation), which nevertheless involves the derivation of a contradiction: assuming the truth of $P$, a contradiction is found, and one concludes that $\neg P$. This remains constructively valid, since it simply uses the constructive meaning of negation, i.e. the introduction rule for the connective of negation (see Bauer 2010).

Since this distinction is sometimes hard for those who have learned classical logic to the point it becomes hard to unlearn, here is another way of putting it (also mentioned by Bauer):

• A proof by contradiction is where you argue “suppose $P$ is false; then [argue blah blah blah]…, contradiction. Therefore $P$ is true.

• A refutation by contradiction is where you argue “suppose $P$ is true; then [blah blah blah]…, contradiction. Therefore $P$ is false.

For example, the standard proofs of the irrationality of $\sqrt{2}$ are sometimes called proofs by contradiction, but they are actually refutations by contradiction (showing that “$\sqrt{2}$ is rational” is false). (The usual meaning of ‘irrational’ in constructive analysis is actually something stronger than ‘not rational’, so such refutations by contradiction are not enough as they stand to prove irrationality; however, they usually can be easily strengthened to prove irrationality in the strong sense.)

Related concepts

• formal proof

References

• Andrej Bauer, Proof of negation and proof by contradiction 2010

• Wikipedia, Proof by contradiction