indirect proof
Assume "not A," reach a contradiction, and conclude A.
Indirect proof (IP) lets you write A after a subproof that begins with the assumption ¬A and ends with ⊥. It differs from ¬I, which assumes A and concludes ¬A.
Examples
To prove P ∨ ¬P, assume ¬(P ∨ ¬P), derive ⊥, and conclude P ∨ ¬P by IP.
See also