Proof by contradiction
Assume the negation of the goal, derive False, and see why that step is classical.
In this course 10 / 10
The contrapositive lesson went in one direction: from P → Q, derive ¬Q → ¬P. That direction is constructive. Going back, from ¬Q → ¬P to P → Q, is not: nothing in the hypothesis produces a proof of Q directly.
Proof by contradiction fills the gap. To prove Q, assume ¬Q and derive False. In Lean the principle is Classical.byContradiction : (¬Q → False) → Q. apply Classical.byContradiction turns the goal Q into ¬Q → False, and intro takes the assumption. Mathlib has a by_contra tactic that does both steps at once; in core Lean you use the lemma.
Compare this with proving a negation. To prove ¬P you assume P and derive False, which is simply what ¬P means, and it is constructive. Proof by contradiction assumes the negation of the goal instead. The two look alike on paper; the difference between them is exactly the classical step.
In the exercise, after intro hp and the contradiction step you hold hp : P, hnq : ¬Q and h : ¬Q → ¬P. Then h hnq is a proof of ¬P, and applying it to hp gives False.
Worked example
example (P : Prop) (h : ¬¬P) : P := by
apply Classical.byContradiction
intro hnp
exact h hnpThe example removes a double negation: assume ¬P, and h turns that into False. Your exercise first introduces P, then argues by contradiction about Q.
To prove a statement by contradiction, assume its negation and derive False with Classical.byContradiction. Proving a negation needs no such step.
Prove the converse of the contrapositive: from h : ¬Q → ¬P, conclude P → Q.
Suggested steps
- Introduce the premise
P - Argue by contradiction
- Derive
Falsefromh
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct