Proof by Contradiction

Proof Rule

Proof by Contradiction is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.

This includes classical propositional logic and predicate logic, and in particular natural deduction.

Proof Rule

If, by making an assumption $\phi$, we can infer a contradiction as a consequence, then we may infer $\neg \phi$.

The conclusion $\neg \phi$ does not depend upon the assumption $\phi$.

Sequent Form

$\paren {p \vdash \bot} \vdash \neg p$

Explanation

Proof by Contradiction can be expressed in natural language as follows:

If we know that by making an assumption $\phi$ we can deduce a contradiction, then it must be the case that $\phi$ cannot be true.

Thus it provides a means of introducing a negation into a sequent.

Also known as

Proof by contradiction is also known as not-introduction, and can be seen abbreviated as $\neg \II$ or $\neg_i$.

However, there are technical reasons why this form of abbreviation are suboptimal on this website, and PBC (if abbreviation is needed at all) is to be preferred.

It is also known as proof of negation, that is, proof that some (positive!) assumption is not true.

Some sources do not explicitly distinguish between proof by contradiction and reductio ad absurdum, which starts with a negative assumption ($\neg \phi$).

Both can be referred to as indirect proof, but reductio ad absurdum is rejected by the intuitionistic school.

Variants

The following forms can be used as variants of this theorem:

Variant 1

$\paren {p \vdash \paren {q \land \neg q} } \vdash \neg p$

Variant 2

Formulation 1

$p \implies q, p \implies \neg q \vdash \neg p$

Formulation 2

$\vdash \paren {\paren {p \implies q} \land \paren {p \implies \neg q} } \implies \neg p$

Variant 3

Formulation 1

$p \implies \neg p \vdash \neg p$

Formulation 2

$\vdash \paren {p \implies \neg p} \implies \neg p$

Also see

• Definition:Logical Not
• Definition:Contradiction
• Reductio ad Absurdum
• Law of Excluded Middle

Sources

• 1998: David Nelson: The Penguin Dictionary of Mathematics (2nd ed.) ... (previous) ... (next): proof by contradiction
• 2008: David Joyner: Adventures in Group Theory (2nd ed.) ... (previous) ... (next): Chapter $1$: Elementary, my dear Watson: $\S 1.1$: You have a logical mind if...
• 2008: David Nelson: The Penguin Dictionary of Mathematics (4th ed.) ... (previous) ... (next): proof by contradiction
• 2014: Christopher Clapham and James Nicholson: The Concise Oxford Dictionary of Mathematics (5th ed.) ... (previous) ... (next): proof by contradiction