 Adopting a natural deduction system, the proof-theoretical contribution of disjunctive formulas can be defined by the following two rules, which regulate (i) how disjunctions can be drawn as conclusions (disjunction introduction rule, \(I_{\vee}\), also known as addition) and (ii) how conclusions can be drawn from disjunctions (disjunction elimination rule, \(E_{\vee}\), also known as reasoning by cases):