Addition
This video presents the same text shown beside it, spoken and on screen. It adds nothing the text does not say.
State
From p, derive p ∨ q — for any q whatsoever.
Show
1. A. 2. A ∨ Z (1, Add).
Watch for
It feels like cheating. It isn't: a disjunction with one true disjunct is true, whatever rides along. Its main use is building the exact disjunction a later rule needs.
Builds on
Unlocks
- Nothing yet depends on this.