Recipe
Prove a sentence by indirect proof
Use when: the goal is not a negation you can get with negation introduction, and no direct route from the premises reaches it
Goal: the goal sentence, written at the outer level of the proof and justified by IP
Taught in Indirect proof
-
1
Open a subproof whose assumption (AS) is the goal with one negation sign in front. If the goal is compound, bracket it first.
Example
Goal O: assume \neg O. Goal P \vee Q: assume \neg(P \vee Q), not \neg P \vee Q.
Why: IP concludes A only from a subproof that assumed exactly \neg A.
-
2
Work forward inside the subproof, using the assumption and the premises, until you have some sentence and its exact negation on two lines.
Example
With \neg O \to D and \neg D as premises: \toE on the premise and the assumption \neg O gives D, which clashes with \neg D.
- the assumption itself is half of a clash — pair it with the other half directly.
- the clash is buried inside a compound line — take the line apart first (\wedgeE, \toE, and so on).
Why: a contradiction is the only thing that can end the subproof.
-
3
Cite \negE on the two clashing lines to write \bot as the subproof's last line.
Example
\bot by \negE 4, 2, citing D and \neg D.
Why: IP's pattern requires the subproof to end on \bot itself, not on the two clashing lines.
-
4
Step back out one level and write the goal, citing IP and the subproof's range.
Example
O by IP 3–5.
Why: the subproof showed the negation of the goal can't hold alongside the premises, so the goal does.
Common mistakes
- Assuming the goal itself instead of its negation.
- Closing with \negI, which writes \neg\neg O rather than O.
- Stopping at two clashing lines without writing \bot.
- Forgetting the brackets when the goal is compound, so the assumption negates only part of it.