Disjunction elimination

For the other rule of inference referred to as disjunction elimination, see disjunctive syllogism.

Disjunction elimination

Type	Rule of inference
Field	Propositional calculus
Statement	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.
Symbolic statement	$\begin{array}{cc}1.& P\to Q\\ 2.& R\to Q\\ 3.& P\vee R\\ \therefore & Q\end{array}$

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:

1. If I'm inside, I have my wallet on me.

2. If I'm outside, I have my wallet on me.

3. 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:

$\begin{array}{cc}1.& P\to Q\\ 2.& R\to Q\\ 3.& P\vee R\\ \therefore & Q\end{array}$

where the rule is that whenever instances of "$P\to Q$", and "$R\to Q$" and "$P\vee 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\vee R)⊢Q$

where $⊢$ is a metalogical symbol meaning that $Q$ is a syntactic consequence of $P\to Q$, and $R\to Q$ and $P\vee R$ in some logical system;

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

$(((P\to Q)\wedge (R\to Q))\wedge (P\vee R))\to Q$

where $P$, $Q$, and $R$ are propositions expressed in some formal system.

See also

• Disjunction
• Argument in the alternative
• Disjunct normal form
• Proof by exhaustion