# Disjunction elimination

Type Rule of inference Propositional calculus 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. ${\frac {P\to Q,R\to Q,P\lor R}{\therefore Q}}$ 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.

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:

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

## Formal notation

The disjunction elimination rule may be written in sequent notation:

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

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

$(((P\to Q)\land (R\to Q))\land (P\lor R))\to Q$ where $P$ , $Q$ , and $R$ are propositions expressed in some formal system.

## Proof 

This rule can be derived from constructive dilemma.

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