Rule ORE Glossary
Definition
| X ⊢ A OR B | Y, A ⊢ C | Z, B ⊢ C | ORE |
| X, Y, Z ⊢ C | |||
The first input (source) line holds a disjunction. The second and third hold any formula derived from assumptions of the two disjuncts. The output of the rule is a line holding the same formula. The assumptions on which the conclusion depends are those of the premises, minus the two discharged.
Comments
The disjunction rules ORI and ORE allow reasoning with alternatives. A OR B is what holds whichever of the alternatives (A or B) is the case. ORE is the most complicated of all the natural deduction rules, as it is the only one to require three input lines and to discharge two assumptions. The reading is clear, however: what follows from the disjunction is whatever follows from each of the alternatives separately. As annotation, cite the three source line number, with the two discharges, and "ORE".
Example
SP {p IMP r, q IMP r, p OR q ⊢ r} PL {1} {1} {p IMP r} {A} PL {2} {2} {q IMP r} {A} PL { 3 } {3} { p OR q } {A} PL {4} {4} {p} {A} PL { 1,4 } {5} { r } {1, 4 IMPE} PL {6} {6} {q} {A} PL { 2,6 } {7} { r } {2, 6 IMPE} PL { 1,2,3 } {8} { r } {3, 5 [4], 7 [6] ORE} EP|
|
|
||||||||
Hover the mouse over elements in the proof or in the rule template above, to see how the inference at line 8 matches the abstract form of the rule.