Proof by Contradiction

From ProofWiki
Jump to: navigation, search

Proof Rule

Proof by contradiction is a valid deduction sequent in propositional logic.

Proof Rule

If, by making an assumption $\phi$, we can infer a contradiction as a consequence, then we may infer $\neg \phi$.
The conclusion does not depend upon the assumption $\phi$.

Sequent Form

$\left({p \vdash \bot}\right) \vdash \neg p$


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 \mathcal I$ 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.

Some sources do not explicitly distinguish between Proof by Contradiction and Reductio ad Absurdum.

Both can be referred to as indirect proof.


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

Variant 1

$\left({p \vdash \left({q \land \neg q}\right)}\right) \vdash \neg p$

Variant 2

Formulation 1

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

Formulation 2

$\vdash \left({\left({p \implies q}\right) \land \left({p \implies \neg q}\right)}\right) \implies \neg p$

Variant 3

Formulation 1

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

Formulation 2

$\vdash \left({p \implies \neg p}\right) \implies \neg p$

Also see