Template:For Template:Short description Template:Infobox mathematical statement Template:Transformation rules
In propositional logic, disjunction elimination<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref><ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref> (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 <math>P</math> implies a statement <math>Q</math> and a statement <math>R</math> also implies <math>Q</math>, then if either <math>P</math> or <math>R</math> is true, then <math>Q</math> 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.
An example in English:
- 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:
- <math>\frac{P \to Q, R \to Q, P \lor R}{\therefore Q}</math>
where the rule is that whenever instances of "<math>P \to Q</math>", and "<math>R \to Q</math>" and "<math>P \lor R</math>" appear on lines of a proof, "<math>Q</math>" can be placed on a subsequent line.
Formal notationEdit
The disjunction elimination rule may be written in sequent notation:
- <math>(P \to Q), (R \to Q), (P \lor R) \vdash Q</math>
where <math>\vdash</math> is a metalogical symbol meaning that <math>Q</math> is a syntactic consequence of <math>P \to Q</math>, and <math>R \to Q</math> and <math>P \lor R</math> in some logical system;
and expressed as a truth-functional tautology or theorem of propositional logic:
- <math>(((P \to Q) \land (R \to Q)) \land (P \lor R)) \to Q</math>
where <math>P</math>, <math>Q</math>, and <math>R</math> are propositions expressed in some formal system.