# Proof by Contradiction

## 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

- $\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

- $\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 \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

## Sources

- 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... - 2014: Christopher Clapham and James Nicholson:
*The Concise Oxford Dictionary of Mathematics*(5th ed.) ... (previous) ... (next): Entry:**proof by contradiction**