To prove P ∨ Q, it suffices to prove P alone (inject left) or Q alone (inject right).
Unlike conjunction, where you must prove both sides, disjunction only requires one. You choose which side to prove. There are two introduction rules — one for each choice.
P Q ——————— ∨-Intro&sub1; ——————— ∨-Intro&sub2; P ∨ Q P ∨ Q
| Prover | Syntax |
|---|---|
| Lean 4 | exact Or.inl hp / exact Or.inr hq |
| Coq | left / right |
| Agda | inj&sub1; hp / inj&sub2; hq |
Prove P → P ∨ Q. Which rules do you combine?
Start with →-Intro to assume P. Then use ∨-Intro&sub1; to inject P into the left side of P ∨ Q.
[P]¹ ———————— ∨-Intro&sub1; P ∨ Q —————————— →-Intro¹ P → P ∨ Q
You combine →-Intro (to assume P) with ∨-Intro&sub1; (to inject left).
See also: Logic §04 — Disjunction