In a proof by contradiction, a negation is obtained by proving that its opposite formula creates a contradiction. The method of proof by contradiction is used for both the negation introduction (¬I) and negation elimination rules of inference, and explains that if "P" results in some contradiction, then ¬P must be true.
Proof by contradiction may be formally presented as follows:
(α → ⊥) ¬α
In this example, the symbol ⊥ is used to indicate a contradiction. Alternatively, we may formulate this by showing an actual contradiction of two formulas:
(α → (β ∧ ¬β)) ¬α
These examples show the negation introduction (¬I) version of the proof by contradiction, which introduces a negation. The negation elimination (¬E) version is the inverse:
(¬α ⊥) α
When beginning with a negation, we have the choice of choosing to conclude either α (by ¬E) or ¬¬α by (¬I), since α and ¬¬α are equivalent, according to the double negation rule.