Editing Disjunction elimination

{{for|the other rule of inference referred to as disjunction elimination|disjunctive syllogism}}
{{Short description|Rule of inference of propositional logic}}
{{Infobox mathematical statement
| name = Disjunction elimination
| type = [[Rule of inference]]
| field = [[Propositional calculus]]
| statement = 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.
| symbolic statement = <math>\frac{P \to Q, R \to Q, P \lor R}{\therefore Q}</math>
}}
{{Transformation rules}}

In [[propositional logic]], '''disjunction elimination'''<ref>{{cite web|url=https://proofwiki.org/wiki/Rule_of_Or-Elimination |title=Rule of Or-Elimination - ProofWiki |access-date=2015-04-09 |url-status=dead |archive-url=https://web.archive.org/web/20150418093657/https://proofwiki.org/wiki/Rule_of_Or-Elimination |archive-date=2015-04-18 }}</ref><ref>{{cite web| url = http://www.cs.gsu.edu/~cscskp/Automata/proofs/node6.html| url-status = dead| archive-url = https://web.archive.org/web/20020307080240/http://www.cs.gsu.edu/~cscskp/Automata/proofs/node6.html| archive-date = 2002-03-07| title = Proof by cases}}</ref> (sometimes named '''proof by cases''', '''case analysis''', or '''or elimination''') is the [[Validity (logic)|valid]] [[argument form]] and [[rule of inference]] that allows one to eliminate a [[logical disjunction|disjunctive statement]] from a [[formal proof|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 language|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 notation ==
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 [[metalogic]]al symbol meaning that <math>Q</math> is a [[logical consequence|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 (logic)|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]].

==See also==
* [[Disjunction]]
* [[Argument in the alternative]]
* [[Disjunct normal form]]
* [[Proof by exhaustion]]

==References==
{{Reflist}}

{{DEFAULTSORT:Disjunction Elimination}}
[[Category:Rules of inference]]
[[Category:Theorems in propositional logic]]