In propositional logic, disjunction elimination (sometimes named proof by cases, case analysis, or or elimination), is the valid argument form and rule of inference that allows one to eliminate a disjunctive statement from a logical proof. It is the inference that if a statement P implies a statement Q and a statement R also implies Q , then if either P or R is true, then Q has to be true. The reasoning is simple: since at least one of the statements P and R is true, and since either of them would be sufficient to entail Q, Q is certainly true.
If I'm inside, I have my wallet on me.If I'm outside, I have my wallet on me.It is true that either I'm inside or I'm outside.Therefore, I have my wallet on me.
It is the rule can be stated as:
P → Q , R → Q , P ∨ R ∴ Q where the rule is that whenever instances of " P → Q ", and " R → Q " and " P ∨ R " appear on lines of a proof, " Q " can be placed on a subsequent line.
The disjunction elimination rule may be written in sequent notation:
( P → Q ) , ( R → Q ) , ( P ∨ R ) ⊢ Q where ⊢ is a metalogical symbol meaning that Q is a syntactic consequence of P → Q , and R → Q and P ∨ R in some logical system;
and expressed as a truth-functional tautology or theorem of propositional logic:
( ( ( P → Q ) ∧ ( R → Q ) ) ∧ ( P ∨ R ) ) → Q where P , Q , and R are propositions expressed in some formal system.
