# Proof by Contradiction

## Contents

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

## 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 \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**.

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

## Sources

- 2008: David Joyner:
*Adventures in Group Theory*(2nd ed.) ... (previous) ... (next): Chapter $1.1$: You have a logical mind if...