# Disjunction elimination

Type Rule of inference Propositional calculus If a statement ${\displaystyle P}$ implies a statement ${\displaystyle Q}$ and a statement ${\displaystyle R}$ also implies ${\displaystyle Q}$, then if either ${\displaystyle P}$ or ${\displaystyle R}$ is true, then ${\displaystyle Q}$ has to be true. ${\displaystyle {\frac {P\to Q,R\to Q,P\lor R}{\therefore Q}}}$

In propositional logic, disjunction elimination[1][2] (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 ${\displaystyle P}$ implies a statement ${\displaystyle Q}$ and a statement ${\displaystyle R}$ also implies ${\displaystyle Q}$, then if either ${\displaystyle P}$ or ${\displaystyle R}$ is true, then ${\displaystyle 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.

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:

${\displaystyle {\frac {P\to Q,R\to Q,P\lor R}{\therefore Q}}}$

where the rule is that whenever instances of "${\displaystyle P\to Q}$", and "${\displaystyle R\to Q}$" and "${\displaystyle P\lor R}$" appear on lines of a proof, "${\displaystyle Q}$" can be placed on a subsequent line.

## Formal notation

The disjunction elimination rule may be written in sequent notation:

${\displaystyle (P\to Q),(R\to Q),(P\lor R)\vdash Q}$

where ${\displaystyle \vdash }$ is a metalogical symbol meaning that ${\displaystyle Q}$ is a syntactic consequence of ${\displaystyle P\to Q}$, and ${\displaystyle R\to Q}$ and ${\displaystyle P\lor R}$ in some logical system;

and expressed as a truth-functional tautology or theorem of propositional logic:

${\displaystyle (((P\to Q)\land (R\to Q))\land (P\lor R))\to Q}$

where ${\displaystyle P}$, ${\displaystyle Q}$, and ${\displaystyle R}$ are propositions expressed in some formal system.

## Proof [1]

This rule can be derived from constructive dilemma.

Step Proposition Derivation
1 ${\displaystyle P\to Q}$ Given
2 ${\displaystyle R\to Q}$ Given
3 ${\displaystyle P\lor R}$ Given
4 ${\displaystyle (P\to Q)\land (R\to Q)}$ Conjunction introduction (1,2)
5 ${\displaystyle Q\lor Q}$ Constructive dilemma (4,3)
6 ${\displaystyle Q}$ Idempotent law (5)

1. ^ "Archived copy". Archived from the original on 2015-04-18. Retrieved 2015-04-09.{{cite web}}: CS1 maint: archived copy as title (link)