Axiom:Proof by Contradiction

Context

The proof by contradiction is one of the axioms of natural deduction.

The rule

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

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

The conclusion does not depend upon the assumption $p$.

This is also known as not-introduction.

It can alternatively be rendered:

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

from the definition of contradiction.

It can be written:

$\displaystyle{\begin{array}{|c|} \hline p \\ \vdots \\ \bot \\ \hline \end{array} \over \neg p} \neg_i$

• Abbreviation: $\neg \mathcal I$
• Deduced from: The pooled assumptions of $\bot$.
• Discharged assumption: The assumption of $p$.
• Depends on: The series of lines from where the assumption of $p$ was made to where $\bot$ was deduced.

Alternative Renditions

It can alternatively be rendered as:

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

The two forms can be seen to be logically equivalent by application of the Rule of Implication, Modus Ponendo Ponens and Implication Distributes over Conjunction.

A shorter variant, directly derived from the above, is:

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

Explanation

This means: if we know that by making an assumption $p$ we can deduce a contradiction, then it must be the case that $p$ can not be true.

Thus it provides a means of introducing a logical not into a sequent.

Also see

Note the similarity between this and Reductio Ad Absurdum, otherwise known as indirect proof, which has the form $\left({\neg p \vdash \bot}\right) \vdash p$.

The latter is strictly speaking not axiomatic, as it requires the acceptance of the Law of the Excluded Middle which is not accepted by the school of intuitionist logic.

Also see Consequentia Mirabilis, otherwise known as Clavius's Law.

Sources

• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{I}: \S 3$: Exercises, Group $\text{I}: 18$
• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{I}: \S 5$: Theorem $\text{T20}$
• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 3$: Theorem $\text{T34}$
• Thomas A. Whitelaw: An Introduction to Abstract Algebra (1978)... (previous)... (next): $\S 5$
• Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2.1$