¬P means P → ⊥. To prove ¬P, assume P and derive a contradiction.
In natural deduction, negation is defined as implication to absurdity. The rule ¬-Intro is therefore a special case of →-Intro: you assume P, derive the absurd proposition ⊥, and conclude ¬P. The assumption P is discharged, just as in →-Intro.
[P]¹ ⋮ ⊥ ————— ¬-Intro¹ ¬P
| Prover | Syntax |
|---|---|
| Lean 4 | intro h (since ¬P = P → False) |
| Coq | intro H |
| Agda | λ h → … |
See also: Logic §06 — Negation | Strategies §04 — Contradiction
Prove ¬(P ∧ ¬P). Assume P ∧ ¬P and extract a contradiction.
Assume P ∧ ¬P. Use ∧-Elim&sub1; to get P and ∧-Elim&sub2; to get ¬P. Then apply ¬P to P (via →-Elim, since ¬P is P → ⊥) to obtain ⊥.
[P ∧ ¬P]¹ [P ∧ ¬P]¹
————————— ∧-Elim&sub1; ————————— ∧-Elim&sub2;
P ¬P
——————————————— →-Elim
⊥
——————————— ¬-Intro¹
¬(P ∧ ¬P)