Proof by Contradiction is an important proof skill that: in order to proof $\Phi$, and $\neg \Phi$ as a new given, and attempt to deduce an evidently false statement($\bot$).

In a schema:

  • Given: $\dots$
  • To be proved: $\Phi$
  • Proof:
    • Suppose $\neg \Phi$
    • To be proved: $\bot$
    • Proof: $\dots$
  • Thus $\Phi$.

Example

A simple case:

  • Theorem:

From $\neg Q \implies \neg P$ it follows that $P \implies Q$.

  • The proof:

    • Given: $\neg Q \implies \neg P$.
    • To be proved: $P \implies Q$.
    • Concise proof:
      • Assume that $P$.
      • If $\neg Q$, then it follows that $\neg P$ (by $\neg Q \implies \neg P$).
      • Contradiction.
      • Thus $Q$.
    • Thus $P \implies Q$.

Another more complex one:

  • Theorem:

From $(p \implies Q) \implies P$ it follows that $P$. (From the book The Haskell Road to Logic, Math and Programming, exercise 3.9)

  • The proof is as follows:

    • Given: $(p \implies Q) \implies P$.
    • To be proved: $P$.
    • Proof:
      • Assume $\neg P$.
      • If $P \implies Q$, then from the given, we get $P$, contradict with our assumption.
      • So $\neg (P \implies Q)$.
    • Thus $P$.

$\neg$ introduction rule

$\neg$ introduction rule: if $\neg \Phi$ is to be proved, assume $\Phi$ as a new given, and attempt to prove something that is evidently false.

Proof by Contradiction looks very similar to the $\neg$ introduction rule. Indeed, in ordinary mathematical contexts, it’s usually better to move negation inside instead of applying $\neg$ introduction.

Proof by Contradiction sometimes looks so inviting. However, many times it must be considered poisoned. Proof by Contradiction should be considered as the last way out.