2.14 Proof by Contradiction

Proof by contradiction is a classical proof pattern. To prove a proposition P, assume ¬ P, derive False, and conclude P.

In Lean, this is usually written with by_contra.

Problem

You want to prove:

P

but the easiest route is to show that assuming ¬ P creates a contradiction.

Solution

Use by_contra.

open Classical

theorem by_contra_basic
    (P : Prop)
    (h : ¬ P -> False) :
    P := by
  by_contra hnp
  exact h hnp

After:

by_contra hnp

Lean changes the proof state from:

⊢ P

to:

hnp : ¬ P
⊢ False

You then prove contradiction.

Discussion

Constructively, proving ¬ P -> False gives ¬ ¬ P. It does not generally give P. The step from ¬ ¬ P to P is classical.

This is why the proof begins with:

open Classical

The tactic by_contra uses classical reasoning unless the target already has a decidable structure that supports the argument.

Direct Double Negation Form

Proof by contradiction is the same as double negation elimination.

open Classical

theorem by_contra_as_double_negation
    (P : Prop) :
    ¬ ¬ P -> P := by
  intro hnnp
  by_contra hnp
  exact hnnp hnp

Here:

hnnp : ¬ ¬ P
hnp  : ¬ P
⊢ False

The expression hnnp hnp produces False.

Example with Equality

A common use is proving an equality by ruling out its negation.

open Classical

theorem equality_by_contradiction
    (a b : Nat)
    (h : ¬ a ≠ b) :
    a = b := by
  by_contra hne
  exact h hne

Since:

a ≠ b

means:

¬ (a = b)

the hypothesis h : ¬ a ≠ b says that inequality is impossible. Assuming hne : a ≠ b gives contradiction.

Example with Disjunction

Classically, if P is not false, then P holds.

open Classical

theorem not_not_left
    (P Q : Prop)
    (h : ¬ ¬ P) :
    P ∨ Q := by
  left
  by_contra hnp
  exact h hnp

The proof chooses the left side. The remaining goal is P. It then proves P by contradiction using h : ¬ ¬ P.

Example with Existentials

A useful classical pattern is deriving existence from the impossibility of universal negation.

open Classical

theorem exists_by_contradiction
    (α : Type)
    (P : α -> Prop)
    (h : ¬ ∀ x : α, ¬ P x) :
    ∃ x : α, P x := by
  by_contra hne
  apply h
  intro x
  intro hpx
  apply hne
  use x

The proof assumes:

hne : ¬ ∃ x : α, P x

Then it proves:

∀ x : α, ¬ P x

For an arbitrary x, assume hpx : P x. Then use x proves ∃ x, P x, contradicting hne.

by_contra Names the Negated Goal

The hypothesis introduced by by_contra has the negation of the original goal.

open Classical

theorem by_contra_goal_shape
    (P Q : Prop)
    (h : ¬ (P ∧ Q)) :
    ¬ P ∨ ¬ Q := by
  by_contra hnot
  apply h
  constructor
  · by_contra hp
    apply hnot
    left
    exact hp
  · by_contra hq
    apply hnot
    right
    exact hq

This example shows why proof by contradiction can become hard to read when nested. Each by_contra introduces the negation of the current goal, which may itself be complex.

For many beginner proofs, prefer direct proofs by introducing assumptions and applying hypotheses. Use contradiction when the direct construction is awkward.

by_cases vs by_contra

by_cases splits a proposition into two cases.

open Classical

theorem by_cases_example
    (P Q : Prop)
    (hpq : P -> Q)
    (hnpq : ¬ Q) :
    ¬ P := by
  intro hp
  exact hnpq (hpq hp)

A classical version could split on P:

open Classical

theorem by_cases_example_classical
    (P Q : Prop)
    (hpq : P -> Q)
    (hnq : ¬ Q) :
    ¬ P := by
  by_cases hp : P
  · intro _
    exact hnq (hpq hp)
  · exact hp

The direct constructive proof is shorter. This illustrates an important rule: do not use classical case splits when implication and negation already give a direct proof.

exfalso Inside Proof by Contradiction

by_contra changes the goal to False. In the reverse situation, exfalso changes any goal to False.

open Classical

theorem by_contra_with_exfalso
    (P Q : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q := by
  exfalso
  exact hnp hp

Here proof by contradiction is unnecessary because False is already available. Use exfalso when you can directly derive contradiction from existing hypotheses.

Term Form

The classical theorem behind by_contra can be used directly.

open Classical

theorem by_contra_term
    (P : Prop)
    (h : ¬ P -> False) :
    P :=
  Classical.byContradiction h

The argument to Classical.byContradiction is a function from ¬ P to False.

Avoiding Unnecessary Classical Reasoning

This theorem is constructive:

theorem constructive_not_intro
    (P Q : Prop)
    (h : P -> Q)
    (hnq : ¬ Q) :
    ¬ P := by
  intro hp
  exact hnq (h hp)

A proof by contradiction version would be longer and introduce an unnecessary classical dependency.

Use by_contra mainly when the target itself must be obtained from a double-negated form, or when a classical excluded-middle argument is natural.

Common Patterns

To prove P by contradiction:

open Classical

by_contra hnp

Then prove:

⊢ False

To prove from double negation:

by_contra hnp
exact hnnp hnp

To prove an equality from not-inequality:

by_contra hne
exact h hne

To avoid contradiction when proving negation:

intro hp

then prove False directly.

Common Pitfalls

Do not use by_contra to prove a negation unless you really need a classical argument. To prove ¬ P, the direct constructive move is intro hp.

Do not forget open Classical when proving a nonconstructive theorem.

Do not let nested by_contra blocks obscure the proof state. Inspect the goal after each use.

Do not use proof by contradiction when exfalso is enough. If contradiction is already derivable from existing hypotheses, prove False directly.

Takeaway

Proof by contradiction proves P by assuming ¬ P and deriving False. In Lean, by_contra h names the assumed negation and changes the goal to False. This is a classical pattern, useful for double negation elimination, excluded-middle arguments, and proofs where a direct witness or construction is unavailable.