The orL proof rule expresses that if we have a disjunction P∨Q
among our assumptions, then even if we have no way of knowing which disjunct can be assumed to be true, we still know one of them can. So we consider both cases separately and once prove the sequent under the assumption P
and once prove the sequent under the assumption Q
, instead.
See also
¬,∧,∨,→,↔