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:

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:

👁 {\displaystyle {\begin{aligned}1.\quad &P\to Q\\2.\quad &R\to Q\\3.\quad &P\lor R\\\therefore \quad &Q\end{aligned}}}

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.

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.

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